--- /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