Package natural-divides-lcm-def: Definition of natural number least common multiple
Information
| name | natural-divides-lcm-def |
| version | 1.0 |
| description | Definition of natural number least common multiple |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-01 |
| checksum | 5286f18fcc7de1e800747c9bcae0713dd188971b |
| requires | base natural-divides-def natural-divides-gcd natural-divides-thm |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-divides-lcm-def-1.0.tgz
- Theory source file natural-divides-lcm-def.thy (included in the package tarball)
Defined Constant
- Number
- Natural
- lcm
- Natural
Theorems
⊦ ∀a. lcm 0 a = 0
⊦ ∀a b. lcm a b * gcd a b = a * b
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∨
- ¬
- cond
- ⊥
- ⊤
- Bool
- Number
- Natural
- *
- div
- divides
- gcd
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ⊥ ⇔ ∀p. p
⊦ ∀t. t ∨ ¬t
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀n. 0 * n = 0
⊦ ∀a b. divides (gcd a b) a
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀a b c. divides a b ⇒ divides a (b * c)
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀a b. gcd a b = 0 ⇔ a = 0 ∧ b = 0
⊦ ∀a b. ¬(a = 0) ⇒ (divides a b ⇔ (b div a) * a = b)