latte-integers.int
A formalization of the type of integers.
=
(= [n int] [m int])(eq/equal n m)
Definition: The equality on integers.
int
(int):type
Axiom: The type of integers.
int-case
(int-case [P (==> int :type)])(==>
(P zero)
(forall [x int] (and (P (succ x)) (P (pred x))))
(forall [x int] (P x)))
Theorem: Case analysis for integers.
int-induct
(int-induct [P (==> int :type)])(==>
(P zero)
(forall [x int] (==> (P x) (and (P (succ x)) (P (pred x)))))
(forall [x int] (P x)))
Axiom: The induction principle for integers (as an axiom).
one
(one)(succ zero)
Definition: The integer one.
pred
(pred)(fun/inverse succ succ-bijective)
Definition: The predecessor as the inverse of the successor.
pred-bijective
(pred-bijective)(fun/bijective pred)
Theorem: The predecessor function is bijective
pred-injective
(pred-injective)(fun/injective pred)
Theorem: The predecessor function is injective
pred-of-succ
(pred-of-succ [y int])(= (pred (succ y)) y)
Theorem: The predecessor of the successor of y is … y.
pred-surjective
(pred-surjective)(fun/surjective pred)
Theorem: The predecessor function is surjective.
succ
(succ)(==> int int)
Axiom: The successor integer.
succ-bijective
(succ-bijective)(fun/bijective succ)
Axiom: The successor function is bijective.
succ-ex
(succ-ex [y int])(exists [x int] (= (succ x) y))
Theorem: An integer y is the successor of at least another integer.
succ-injective
(succ-injective)(fun/injective succ)
Theorem: The successor function is injective.
succ-of-pred
(succ-of-pred [y int])(= (succ (pred y)) y)
Theorem: The succesor of the predecessor of y is … y.
succ-single
(succ-single [y int])(q/single (lambda [x int] (= (succ x) y)))
Theorem: An integer y is the successor of at most another integer.
succ-surjective
(succ-surjective)(fun/surjective succ)
Theorem: The successor function is surjective.
succ-unique
(succ-unique [y int])(q/unique (lambda [x int] (= (succ x) y)))
Theorem: There is a unique successor to an integer y.
zero
(zero)int
Axiom: The integer zero.