Nat.thy

Renamed a few types and vars

(*  Title: 	HOL/nat
    ID:         $Id$
    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Definition of types ind and nat.

Type nat is defined as a set Nat over type ind.
*)

Nat = WF +

types
  ind
  nat

arities
  ind,nat :: term
  nat     :: ord

consts
  Zero_Rep	:: "ind"
  Suc_Rep	:: "ind => ind"
  Nat		:: "ind set"
  Rep_Nat	:: "nat => ind"
  Abs_Nat	:: "ind => nat"
  Suc		:: "nat => nat"
  nat_case	:: "['a, nat=>'a, nat] =>'a"
  pred_nat	:: "(nat*nat) set"
  nat_rec	:: "[nat, 'a, [nat, 'a]=>'a] => 'a"
  "0"		:: "nat"		("0")

translations
  "case p of 0 => a | Suc(y) => b" == "nat_case(a, %y.b, p)"

rules
 (*the axiom of infinity in 2 parts*)
  inj_Suc_Rep  		"inj(Suc_Rep)"
  Suc_Rep_not_Zero_Rep	"~(Suc_Rep(x) = Zero_Rep)"
  Nat_def		"Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
    (*faking a type definition...*)
  Rep_Nat 		"Rep_Nat(n): Nat"
  Rep_Nat_inverse 	"Abs_Nat(Rep_Nat(n)) = n"
  Abs_Nat_inverse 	"i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
    (*defining the abstract constants*)
  Zero_def  		"0 == Abs_Nat(Zero_Rep)"
  Suc_def  		"Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
     (*nat operations and recursion*)
  nat_case_def	"nat_case(a,f,n) == @z.  (n=0 --> z=a)  \
\                                      & (!x. n=Suc(x) --> z=f(x))"
  pred_nat_def 	"pred_nat == {p. ? n. p = <n, Suc(n)>}"

  less_def "m<n == <m,n>:trancl(pred_nat)"

  le_def   "m<=(n::nat) == ~(n<m)"

  nat_rec_def	"nat_rec(n,c,d) == wfrec(pred_nat, n,   \
\                        nat_case(%g.c, %m g. d(m,g(m))))"
end