Package natural-divides-gcd-thm: Properties of natural number greatest common divisor

Information

namenatural-divides-gcd-thm
version1.6
descriptionProperties of natural number greatest common divisor
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-05-26
checksum48338ff0f28767ba09e2903ff3001c043708f79e
requiresbase
natural-divides-def
natural-divides-gcd-def
natural-divides-thm
showData.Bool
Data.Pair
Number.Natural
Relation

Files

Theorems

a. gcd 0 a = a

a. gcd a 0 = a

a. gcd a a = a

b. fst (egcd 0 b) = b

a. gcd a 1 = 1

a. gcd 1 a = 1

a b. divides (fst (egcd a b)) a

a b. divides (fst (egcd a b)) b

a b. gcd a b = gcd b a

a b. fst (egcd a b) = gcd a b

a. egcd a 0 = (a, 1, 0)

a b. gcd a b = a divides a b

a b. gcd b a = a divides a b

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

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

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

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

a b c. divides b a divides (gcd b c) a

a b c. divides b a divides (gcd c b) a

b. egcd 1 b = (1, 1, 0)

a b c. gcd (gcd a b) c = gcd a (gcd b c)

a b. a b gcd a (b - a) = gcd a b

a b. b a gcd (a - b) b = gcd a b

a b. gcd a b = 0 a = 0 b = 0

a b s t. divides (gcd a b) (distance (s * a) (t * b))

a b. s t. distance (s * a) (t * b) = gcd a b

a b. ¬(a = 0) gcd a (b mod a) = gcd a b

a b c. divides c (gcd a b) divides c a divides c b

a b c. divides (gcd a (b * c)) (gcd a b * gcd a c)

a b c. gcd (a * b) (a * c) = a * gcd b c

a b c. gcd (b * a) (c * a) = gcd b c * a

a b. gcd a b = 1 gcd (a * a) b = 1

a b. gcd b a = 1 gcd b (a * a) = 1

a b. gcd b (a * a) = 1 gcd b a = 1

a b. gcd (a * a) b = 1 gcd a b = 1

a b c. gcd b (a * c) = 1 gcd b c = 1

a b c. gcd b (c * a) = 1 gcd b c = 1

a b c. gcd (a * b) c = 1 gcd b c = 1

a b c. gcd (b * a) c = 1 gcd b c = 1

a b c. gcd a b = 1 gcd a (b * c) = gcd a c

a b c. gcd a b = 1 gcd a (c * b) = gcd a c

a b c. gcd b a = 1 gcd (b * c) a = gcd c a

a b c. gcd b a = 1 gcd (c * b) a = gcd c a

a. ¬(a = 0) egcd a 1 = (1, 1, a - 1)

a b. ¬(a = 0) s t. t * b + gcd a b = s * a

a b. ¬(a = 0) s t. t * b + gcd b a = s * a

a b x y. x < a y < b chineseRemainder a b x y < a * b

a b s t. distance (s * a) (t * b) = 1 gcd a b = 1

a b. (c. divides c a divides c b c = 1) gcd a b = 1

a b.
    gcd a b = if a = 0 then b else if a b then gcd a (b - a) else gcd b a

a b c. gcd b c = 1 divides b a divides c a divides (b * c) a

a b c. gcd a (b * c) = 1 gcd a b = 1 gcd a c = 1

a b c. gcd (b * c) a = 1 gcd b a = 1 gcd c a = 1

a b c. gcd a b = 1 gcd a c = 1 gcd a (b * c) = 1

a b c. gcd b a = 1 gcd c a = 1 gcd (b * c) a = 1

ap b. let a ap + 1 in let (g, s, t) egcd a b in t < a

a b s t g. s * a + g = t * b divides g a divides g b gcd a b = g

a b s t g. t * b + g = s * a divides g a divides g b gcd a b = g

a b s t g.
    distance (s * a) (t * b) = g divides g a divides g b gcd a b = g

ap b. let a ap + 1 in let (g, s, t) egcd a b in s < max b 2

a b g.
    divides g a divides g b
    (c. divides c a divides c b divides c g) gcd a b = g

a b g s t. ¬(a = 0) egcd a b = (g, s, t) t * b + g = s * a

ap b. let a ap + 1 in let (g, s, t) egcd a b in t * b + g = s * a

a b g s t. ¬(a = 0) egcd a b = (g, s, t) s < max b 2 t < a

a b.
    ¬(a = 0) s t. egcd a b = (gcd a b, s, t) t * b + gcd a b = s * a

a b x y n.
    gcd a b = 1 x < a y < b chineseRemainder a b x y = n
    n mod a = x n mod b = y

ap bp xp yp.
    let aq ap + 1 in
    let bq bp + 1 in
    let g fst (egcd aq bq) in
    let a aq div g in
    let b bq div g in
    let x xp mod a in
    let y yp mod b in
    chineseRemainder a b x y < a * b

ap bp xp yp.
    let aq ap + 1 in
    let bq bp + 1 in
    let g fst (egcd aq bq) in
    let a aq div g in
    let b bq div g in
    let x xp mod a in
    let y yp mod b in
    chineseRemainder a b x y mod a = x

ap bp xp yp.
    let aq ap + 1 in
    let bq bp + 1 in
    let g fst (egcd aq bq) in
    let a aq div g in
    let b bq div g in
    let x xp mod a in
    let y yp mod b in
    chineseRemainder a b x y mod b = y

a b.
    chineseRemainder a b =
    let (g, s, t) egcd a b in
    let ab a * b in
    let sa s * a in
    let tb (a - t) * b in
    λx y. (x * tb + y * sa) mod ab

p.
    p 0 0 (a b. gcd a b = 1 p a b)
    (c a b. ¬(c = 0) p a b p (c * a) (c * b)) a b. p a b

p.
    (a. p a 0) (a b. ¬(b = 0) divides b a p a b)
    (a b c. ¬(b = 0) c = a mod b ¬(c = 0) p c (b mod c) p a b)
    a b. p a b

External Type Operators

External Constants

Assumptions

¬

¬

bit0 0 = 0

t. t t

n. n n

a. divides a 0

a. divides a a

m. wellFounded (measure m)

p. p

t. t ¬t

m. ¬(m < 0)

n. n < suc n

a. divides 1 a

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t t

n. ¬(suc n = 0)

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. n - n = 0

n. distance 0 n = n

n. distance n n = 0

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m * 1 = m

n. n div 1 = n

n. n mod 1 = 0

m. 1 * m = m

m n. m m + n

a b. divides (gcd a b) a

a b. divides (gcd a b) b

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

m. m 0 m = 0

a. divides 0 a a = 0

n. suc n - 1 = n

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

a b. fst (a, b) = a

a b. snd (a, b) = b

p x. p x p ((select) p)

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

x. a b. x = (a, b)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

a b. (a b) a b

m n. m * n = n * m

m n. m + n = n + m

m n. distance m n = distance n m

m n. max m n = max n m

a b. a = b divides a b

m n. m < n m n

m n. m + n - m = n

m n. distance (m + n) m = n

a. divides a 1 a = 1

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

() = λp q. (λf. f p q) = λf. f

n. ¬(n = 0) 0 mod n = 0

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

t1 t2. ¬t1 ¬t2 t2 t1

m n. m < n m div n = 0

m n. m < n m mod n = m

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

m n. suc m < suc n m < n

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. max m n = if m n then n else m

m n. suc m * n = m * n + n

m n. ¬(n = 0) m mod n < n

m n. ¬(n = 0) m div n m

p. (x. p x) a b. p (a, b)

p. (x. p x) a b. p (a, b)

a b c. divides a c divides a (b * c)

m n. m n d. n = m + d

a b. divides a b c. c * a = b

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

m n. n m m - n + n = m

m n. m n n m m = n

a b. divides a b divides b a a = b

f. fn. a b. fn (a, b) = f a b

m n. m < n d. n = m + suc d

m x y. measure m x y m x < m y

p. (x y. p x y) y x. p x y

m n. ¬(m = 0) m * n mod m = 0

a b. ¬(b = 0) divides a b a b

x y z. x = y y = z x = z

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. m + n = m + p n = p

p m n. m + p = n + p m = n

m n p. m + n < m + p n < p

m n p. n + m < p + m n < p

m n p. m + n m + p n p

p m n. distance (m + p) (n + p) = distance m n

m n p. m < n n < p m < p

m n p. m < n n p m < p

m n p. m n n < p m < p

m n p. m n n p m p

a b c. divides a b divides b c divides a c

m n. m suc n m = suc n m n

m n. m * n = 0 m = 0 n = 0

m n. m + n = 0 m = 0 n = 0

m n. distance (distance m n) (distance m (n + 1)) = 1

p. p 0 (n. p n p (suc n)) n. p n

a b. ¬(a = 0) (divides a b b mod a = 0)

n m. ¬(n = 0) m mod n mod n = m mod n

m n. ¬(n = 0) (m div n = 0 m < n)

m n p. m < max n p m < n m < p

m n p. m * (n + p) = m * n + m * p

m n p. m * distance n p = distance (m * n) (m * p)

m n p. (m + n) * p = m * p + n * p

p m n. distance m n * p = distance (m * p) (n * p)

a b c. divides a b divides a c divides a (b + c)

a b c. divides c a divides c b divides c (gcd a b)

a b. divides a b if a = 0 then b = 0 else b mod a = 0

a b. ¬(a = 0) (divides a b (b div a) * a = b)

m n. ¬(n = 0) (m div n) * n + m mod n = m

m n p. n m m + p - (n + p) = m - n

m n p. m * p = n * p m = n p = 0

m n p. m * n m * p m = 0 n p

m n p. m * p n * p m n p = 0

a b c. divides (a * b) (a * c) a = 0 divides b c

a b c. divides (b * a) (c * a) a = 0 divides b c

m n p. m * n < m * p ¬(m = 0) n < p

m n p. m * p < n * p m < n ¬(p = 0)

a b a' b'. (a, b) = (a', b') a = a' b = b'

m n p. n m (m - n) * p = m * p - n * p

m n p. distance m n = p m + p = n n + p = m

a b c. c b divides a b divides a c divides a (b - c)

p c x y. p (if c then x else y) (c p x) (¬c p y)

m n p. ¬(n * p = 0) m mod n * p mod n = m mod n

r. wellFounded r p. (x. (y. r y x p y) p x) x. p x

n a b. ¬(n = 0) (a mod n + b mod n) mod n = (a + b) mod n

p.
    (n. p 0 n) (m n. n < m p n m p m n)
    (m n. p m n p m (n + m)) m n. p m n

a b x y.
    chineseRemainder a b x y =
    let (g, s, t) egcd a b in (x * ((a - t) * b) + y * (s * a)) mod a * b

a b.
    egcd a b =
    if b = 0 then (a, 1, 0)
    else
      let c a mod b in
      if c = 0 then (b, 1, a div b - 1)
      else
        let (g, s, t) egcd c (b mod c) in
        let u s + (b div c) * t in
        (g, u, t + (a div b) * u)