Package natural-def: Constructing the natural numbers

Information

namenatural-def
version1.20
descriptionConstructing the natural numbers
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-02-10
requiresaxiom-infinity
bool
function
showData.Bool
Function
Number.Natural

Files

Defined Type Operator

Defined Constants

Theorems

n. ¬(suc n = 0)

m n. suc m = suc n m = n

P. P 0 (n. P n P (suc n)) n. P n

Input Type Operators

Input Constants

Assumptions

¬

¬

p. p

t. t ¬t

(¬) = λp. p

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. ( t) ¬t

t. t ¬t

f. injective f ¬surjective f

() = λp q. p q p

t. (t ) (t )

p x. p x p ((select) p)

f y. (let x y in f x) = f y

t1 t2. t1 t2 t2 t1

() = λp q. (λf. f p q) = λf. f

f. surjective f y. x. y = f x

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

() = λp q. r. (p r) (q r) r

p q. (x. p q x) p x. q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x) q x. p x q

t1 t2 t3. (t1 t2) t3 t1 t2 t3

p. (x. y. p x y) y. x. p x (y x)

f. injective f x1 x2. f x1 = f x2 x1 = x2

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2