Package natural-divides-gcd-def: Definition of natural number greatest common divisor

Information

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

Files

Defined Constants

Theorems

a b. divides (gcd a b) a

a b. divides (gcd a b) b

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

m. wellFounded (measure m)

p. p

(¬) = λp. p

() = λp. p ((select) p)

t. (λx. t x) = t

() = λp. p = λx.

t. t t

t. t

() = λp q. p q p

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

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

a b. snd (a, b) = b

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

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

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

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

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

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

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

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

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

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

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

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