Package natural-exp-log-def: Definition of natural number logarithm

Information

namenatural-exp-log-def
version1.8
descriptionDefinition of natural number logarithm
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-05
requiresbool
natural-add
natural-def
natural-exp-thm
natural-order
showData.Bool
Number.Natural

Files

Defined Constant

Theorem

k n m. k m n n < k (m + 1) log k n = m

Input Type Operators

Input Constants

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