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

gcd_tupled_primitive_def

|- gcd_tupled =
   WFREC
     (@R.
        WF R /\ (!x y. ~(y <= x) ==> R (SUC x,y - x) (SUC x,SUC y)) /\
        !x y. y <= x ==> R (x - y,SUC y) (SUC x,SUC y))
     (\gcd_tupled a.
        case a of
           (0,y) -> I y
        || (SUC x,0) -> I (SUC x)
        || (SUC x,SUC y') ->
             I
               (if y' <= x then
                  gcd_tupled (x - y',SUC y')
                else
                  gcd_tupled (SUC x,y' - x)))

gcd_curried_def

|- !x x1. gcd x x1 = gcd_tupled (x,x1)

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 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

|- (gcd 0 y = y) /\ (gcd (SUC x) 0 = SUC x) /\
   (gcd (SUC x) (SUC y) =
    (if y <= x then gcd (x - y) (SUC y) else gcd (SUC x) (y - x)))

GCD_IS_GCD

|- !a b. is_gcd a b (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