Next: Theorems about Successor Up: The Natural Numbers Previous: The Natural Numbers

## Natural Numbers: Basic Definitions

The basic definitions are held in the file lib_nat. We find it useful to define the double iterator and double induction, and the constants one to ten. This file also defines the algebraic functions addition, multiplication and exponentiation. We also define pred (predecessor) in one step from this we define truncated subtraction (minus).

``` ** Module lib_nat Imports lib_bool
\$nat : SET
\$zero : nat
\$suc : nat->nat
\$nat_elim :
{C_nat:nat->TYPE}(C_nat zero)->
({x1:nat}(C_nat x1)->C_nat (suc x1))->{z:nat}C_nat z
[[C_nat:nat->TYPE][f_zero:C_nat zero]
[f_suc:{x1:nat}(C_nat x1)->C_nat (suc x1)][x1:nat]
nat_elim C_nat f_zero f_suc zero  ==>  f_zero
|| nat_elim C_nat f_zero f_suc (suc x1)  ==>
f_suc x1 (nat_elim C_nat f_zero f_suc x1)]

nat_rec = ... : {t|TYPE}t->(nat->t->t)->nat->t
nat_iter = ... : {t|TYPE}t->(t->t)->nat->t
nat_ind = ... :
{P:nat->Prop}(P zero)->({n:nat}(P n)->P (suc n))->{n:nat}P n
nat_double_elim = ... :
{T:nat->nat->TYPE}(T zero zero)->
({n:nat}(T zero n)->T zero (suc n))->
({m:nat}({n:nat}T m n)->T (suc m) zero)->
({m:nat}({n:nat}T m n)->{n:nat}(T (suc m) n)->T (suc m) (suc n))->
{m,n:nat}T m n
nat_diagonal_iter = ... :
{C|TYPE}(nat->C)->(nat->C)->(C->C)->nat->nat->C
nat_diagonal_ind = ... :
{phi:nat->nat->Prop}({m:nat}phi zero m)->({n:nat}phi (suc n) zero)->
({n,m:nat}(phi n m)->phi (suc n) (suc m))->{n,m:nat}phi n m
nat_d_rec_for_int = ... :
{C:nat->nat->TYPE}(C zero zero)->({m,n:nat}(C m n)->C (suc m) n)->
({m,n:nat}(C m n)->C m (suc n))->{m,n:nat}C m n
is_suc = ... : nat->Prop
is_zero = ... : nat->Prop
zero_not_suc = ... : {n:nat}not (Eq zero (suc n))
suc_not_zero = ... : not (is_suc zero)
zero_or_suc = ... : {n:nat}or (Eq n zero) (is_suc n)
one = ... : nat
two = ... : nat
three = ... : nat
four = ... : nat
five = ... : nat
six = ... : nat
seven = ... : nat
eight = ... : nat
nine = ... : nat
ten = ... : nat
plus = ... : nat->nat->nat
times = ... : nat->nat->nat
exp = ... : nat->nat->nat
pred = ... : nat->nat
minus = ... : nat->nat->nat
ackerman = ... : nat->nat->nat
if_zero = ... : {t|TYPE}nat->t->t->t
zero_not_one = ... : not (Eq zero one)```

Lego
Fri May 24 19:01:27 BST 1996