Package natural-divides-gcd-def: Definition of natural number greatest common divisor
Information
| name | natural-divides-gcd-def |
| version | 1.0 |
| description | Definition of natural number greatest common divisor |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-04 |
| checksum | a8e2147635c7935579ed2da524c27845d57fe6b3 |
| requires | base natural-divides-def natural-divides-thm |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-divides-gcd-def-1.0.tgz
- Theory source file natural-divides-gcd-def.thy (included in the package tarball)
Defined Constant
- Number
- Natural
- gcd
- Natural
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)
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊤
- Bool
- Number
- Natural
- divides
- Natural
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ (∀) = λp. p = λx. ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀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
⊦ ∀a b.
∃g.
divides g a ∧ divides g b ∧
∀c. divides c a ∧ divides c b ⇒ divides c g