next up previous contents
Next: Iteration Principles 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 : Type(nat)
 $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
 ** Label (!nat!) nat
 ** Label (!nat elim!) nat_elim
 ** Label (!nat zero!) zero
 ** Label (!nat suc!) suc
[[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)]

   Gen (!nat is zero!) as nat_is_zero = ... : nat->Type
   Gen (!nat is suc!) as nat_is_suc = ... : nat->Type
   Gen (!nat zero injective!) as nat_zero_injective = ... :
    (Eq zero zero)->{P|Type}P->P
   Gen (!nat suc injective!) as nat_suc_injective = ... :
    {ix0,iy0|nat}(Eq (suc ix0) (suc iy0))->{P|Type}((Eq ix0 iy0)->P)->P
  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)
  suc_n_not_n = ... : {n:nat}not (Eq (suc n) n)
 ** Config Qnify nat suc_n_not_n 
  zero_or_suc = ... : {n:nat}(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
  fact = ... : nat->nat
  zero_not_one = ... : not (Eq zero one)



Conor McBride
11/13/1998