diff -r 000000000000 -r 7949f97df77a Nat.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nat.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,51 @@
+(*  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 0
+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	:: "[nat, 'a, nat=>'a] =>'a"
+  pred_nat	:: "(nat*nat) set"
+  nat_rec	:: "[nat, 'a, [nat, 'a]=>'a] => 'a"
+  "0"		:: "nat"		("0")
+
+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 == (%n a f. @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,   \
+\                        %l g. nat_case(l, c, %m. d(m,g(m))))"
+end