Package natural-divides-gcd: Natural number greatest common divisor

Information

namenatural-divides-gcd
version1.2
descriptionNatural number greatest common divisor
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksumeeb322e47152398e7b3e1d39f16e9cf77961939f
requiresbase
natural-divides-def
natural-divides-thm
showData.Bool
Data.Pair
Number.Natural
Relation

Files

Defined Constants

Theorems

a. gcd 0 a = a

a. gcd a 0 = a

a. gcd a a = a

a b. divides (gcd a b) a

a b. divides (gcd a 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

b. ¬(b = 0) fst (egcd 0 b) = b

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

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

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 c. divides c a divides c b divides c (gcd a b)

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

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

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

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

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

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)

External Type Operators

External Constants

Assumptions

¬

bit0 0 = 0

t. t t

a. divides a 0

a. divides a a

m. wellFounded (measure m)

p. p

t. t ¬t

a. divides 1 a

(¬) = λp. p

() = λp. p ((select) 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

n. ¬(suc n = 0)

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. distance 0 n = n

n. distance n n = 0

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. m * 1 = m

m. 1 * m = m

m n. m m + n

() = λp q. p q p

m. suc m = m + 1

a. divides 0 a a = 0

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)

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

x y. x = y y = x

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

a b. a = b divides a b

m n. m + n - m = n

a. divides a 1 a = 1

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. q. (x. p x q) q

t1 t2. ¬t1 ¬t2 t2 t1

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

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

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)

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

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

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

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

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

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

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

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

p q r. p q r p q r

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

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

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

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

r. (x. y. r x y) f. x. r x (f x)

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)

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)

p q. (x. p x q x) (x. p x) x. q x

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

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

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

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

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)

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

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

r.
    wellFounded r
    h.
      (f g x. (z. r z x f z = g z) h f x = h g x)
      f. x. f x = h f x

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