Package natural-exp-log-def: Definition of natural number logarithm
Information
| name | natural-exp-log-def |
| version | 1.13 |
| description | Definition of natural number logarithm |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-01 |
| checksum | 4b0771b751d95b14328530b53c43044a6b51aba0 |
| requires | bool natural-add natural-def natural-exp-thm natural-order |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-exp-log-def-1.13.tgz
- Theory source file natural-exp-log-def.thy (included in the package tarball)
Defined Constant
- Number
- Natural
- log
- Natural
Theorem
⊦ ∀k n m. k ↑ m ≤ n ∧ n < k ↑ (m + 1) ⇒ log k n = m
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- Bool
- Number
- Natural
- +
- <
- ≤
- ↑
- bit1
- minimal
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ⊥ ⇔ ∀p. p
⊦ ∀t. t ∨ ¬t
⊦ ∀m. ¬(m < 0)
⊦ (¬) = λp. p ⇒ ⊥
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∨ ⊤ ⇔ ⊤
⊦ ∀n. ¬(suc n = 0)
⊦ ∀t. t ⇒ ⊥ ⇔ ¬t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀m. suc m = m + 1
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. suc m ≤ n ⇔ m < n
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀n. 0 ↑ n = if n = 0 then 1 else 0
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n
⊦ ∀x m n. x ↑ m ≤ x ↑ n ⇔ if x = 0 then m = 0 ⇒ n = 0 else x = 1 ∨ m ≤ n