Theory "gcd"

Signature

Definitions

is_gcd_def

⊢ ∀a b c.
      is_gcd a b c ⇔
      divides c a ∧ divides c b ∧ ∀d. divides d a ∧ divides d b ⇒ divides d c

lcm_def

⊢ ∀m n. lcm m n = if m = 0 ∨ n = 0 then 0 else m * n DIV gcd m n

Theorems

IS_GCD_UNIQUE

⊢ ∀a b c d. is_gcd a b c ∧ is_gcd a b d ⇒ c = d

IS_GCD_REF

⊢ ∀a. is_gcd a a a

IS_GCD_SYM

⊢ ∀a b c. is_gcd a b c ⇔ is_gcd b a c

IS_GCD_0R

⊢ ∀a. is_gcd a 0 a

IS_GCD_0L

⊢ ∀a. is_gcd 0 a a

PRIME_IS_GCD

⊢ ∀p b. prime p ⇒ divides p b ∨ is_gcd p b 1

IS_GCD_MINUS_L

⊢ ∀a b c. b ≤ a ∧ is_gcd (a − b) b c ⇒ is_gcd a b c

IS_GCD_MINUS_R

⊢ ∀a b c. a ≤ b ∧ is_gcd a (b − a) c ⇒ is_gcd a b c

gcd_ind

⊢ ∀P.
      (∀y. P 0 y) ∧ (∀x. P (SUC x) 0) ∧
      (∀x y.
           (¬(y ≤ x) ⇒ P (SUC x) (y − x)) ∧ (y ≤ x ⇒ P (x − y) (SUC y)) ⇒
           P (SUC x) (SUC y)) ⇒
      ∀v v1. P v v1

gcd_def

⊢ (∀y. gcd 0 y = y) ∧ (∀x. gcd (SUC x) 0 = SUC x) ∧
  ∀y x.
      gcd (SUC x) (SUC y) = if y ≤ x then gcd (x − y) (SUC y)
      else gcd (SUC x) (y − x)

gcd_def_compute

⊢ (∀y. gcd 0 y = y) ∧ (∀x. gcd (NUMERAL (BIT1 x)) 0 = NUMERAL (BIT1 x)) ∧
  (∀x. gcd (NUMERAL (BIT2 x)) 0 = NUMERAL (BIT2 x)) ∧
  (∀y x.
       gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT1 y)) =
       if NUMERAL (BIT1 y) − 1 ≤ NUMERAL (BIT1 x) − 1 then
         gcd (NUMERAL (BIT1 x) − 1 − (NUMERAL (BIT1 y) − 1))
           (NUMERAL (BIT1 y))
       else
         gcd (NUMERAL (BIT1 x))
           (NUMERAL (BIT1 y) − 1 − (NUMERAL (BIT1 x) − 1))) ∧
  (∀y x.
       gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y)) =
       if NUMERAL (BIT1 y) − 1 ≤ NUMERAL (BIT1 x) then
         gcd (NUMERAL (BIT1 x) − (NUMERAL (BIT1 y) − 1)) (NUMERAL (BIT1 y))
       else gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y) − 1 − NUMERAL (BIT1 x))) ∧
  (∀y x.
       gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT2 y)) =
       if NUMERAL (BIT1 y) ≤ NUMERAL (BIT1 x) − 1 then
         gcd (NUMERAL (BIT1 x) − 1 − NUMERAL (BIT1 y)) (NUMERAL (BIT2 y))
       else gcd (NUMERAL (BIT1 x)) (NUMERAL (BIT1 y) − (NUMERAL (BIT1 x) − 1))) ∧
  ∀y x.
      gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT2 y)) =
      if NUMERAL (BIT1 y) ≤ NUMERAL (BIT1 x) then
        gcd (NUMERAL (BIT1 x) − NUMERAL (BIT1 y)) (NUMERAL (BIT2 y))
      else gcd (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y) − NUMERAL (BIT1 x))

GCD_IS_GCD

⊢ ∀a b. is_gcd a b (gcd a b)

GCD_IS_GREATEST_COMMON_DIVISOR

⊢ ∀a b.
      divides (gcd a b) a ∧ divides (gcd a b) b ∧
      ∀d. divides d a ∧ divides d b ⇒ divides d (gcd a b)

GCD_REF

⊢ ∀a. gcd a a = a

GCD_SYM

⊢ ∀a b. gcd a b = gcd b a

GCD_0R

⊢ ∀a. gcd a 0 = a

GCD_0L

⊢ ∀a. gcd 0 a = a

GCD_ADD_R

⊢ ∀a b. gcd a (a + b) = gcd a b

GCD_ADD_R_THM

⊢ (∀a b. gcd a (a + b) = gcd a b) ∧ ∀a b. gcd a (b + a) = gcd a b

GCD_ADD_L

⊢ ∀a b. gcd (a + b) a = gcd a b

GCD_ADD_L_THM

⊢ (∀a b. gcd (a + b) a = gcd a b) ∧ ∀a b. gcd (b + a) a = gcd a b

GCD_EQ_0

⊢ ∀n m. gcd n m = 0 ⇔ n = 0 ∧ m = 0

GCD_1

⊢ gcd 1 x = 1 ∧ gcd x 1 = 1

PRIME_GCD

⊢ ∀p b. prime p ⇒ divides p b ∨ gcd p b = 1

L_EUCLIDES

⊢ ∀a b c. gcd a b = 1 ∧ divides b (a * c) ⇒ divides b c

P_EUCLIDES

⊢ ∀p a b. prime p ∧ divides p (a * b) ⇒ divides p a ∨ divides p b

FACTOR_OUT_GCD

⊢ ∀n m. n ≠ 0 ∧ m ≠ 0 ⇒ ∃p q. n = p * gcd n m ∧ m = q * gcd n m ∧ gcd p q = 1

GCD_SUCfree_ind

⊢ ∀P.
      (∀y. P 0 y) ∧ (∀x y. P x y ⇒ P y x) ∧ (∀x. P x x) ∧
      (∀x y. 0 < x ∧ 0 < y ∧ P x y ⇒ P x (x + y)) ⇒
      ∀m n. P m n

LINEAR_GCD

⊢ ∀n m. n ≠ 0 ⇒ ∃p q. p * n = q * m + gcd m n

GCD_EFFICIENTLY

⊢ ∀a b. gcd a b = if a = 0 then b else gcd (b MOD a) a

LCM_IS_LEAST_COMMON_MULTIPLE

⊢ divides m (lcm m n) ∧ divides n (lcm m n) ∧
  ∀p. divides m p ∧ divides n p ⇒ divides (lcm m n) p

LCM_0

⊢ lcm 0 x = 0 ∧ lcm x 0 = 0

LCM_1

⊢ lcm 1 x = x ∧ lcm x 1 = x

LCM_COMM

⊢ lcm a b = lcm b a

LCM_LE

⊢ 0 < m ∧ 0 < n ⇒ m ≤ lcm m n ∧ m ≤ lcm n m

LCM_LEAST

⊢ 0 < m ∧ 0 < n ⇒ ∀p. 0 < p ∧ p < lcm m n ⇒ ¬divides m p ∨ ¬divides n p

GCD_COMMON_FACTOR

⊢ ∀m n k. gcd (k * m) (k * n) = k * gcd m n

GCD_CANCEL_MULT

⊢ ∀m n k. gcd m k = 1 ⇒ gcd m (k * n) = gcd m n

BINARY_GCD

⊢ ∀m n.
      (EVEN m ∧ EVEN n ⇒ gcd m n = 2 * gcd (m DIV 2) (n DIV 2)) ∧
      (EVEN m ∧ ODD n ⇒ gcd m n = gcd (m DIV 2) n)