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

Information

name	natural-divides-gcd-def
version	1.3
description	Definition of natural number greatest common divisor
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2015-05-25
checksum	533aef22d91ee7b4a1247e6e804f31e7bcf622f6
requires	base natural-divides-def natural-divides-thm
show	Data.Bool Data.Pair Number.Natural Relation

Files

Package tarball natural-divides-gcd-def-1.3.tgz
Theory source file natural-divides-gcd-def.thy (included in the package tarball)

Defined Constants

Number
- Natural
  - chineseRemainder
  - egcd
  - gcd

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

External Type Operators

→
bool
Data
- Pair
  - ×
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ¬
  - cond
  - ⊥
  - ⊤
- Pair
  - ,
  - snd
Number
- Natural
  - *
  - +
  - -
  - <
  - bit1
  - div
  - divides
  - mod
  - zero
Relation
- measure
- wellFounded

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

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

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