# HG changeset patch
# User berghofe
# Date 990537103 -7200
# Node ID 680ebd093cfed628ba65ec77234525fe47a608c2
# Parent  a5e0289dd56c0907ee52e1bd169905fdeeb524b3
Representing set for type nat is now defined via "inductive".

diff -r a5e0289dd56c -r 680ebd093cfe src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue May 22 15:10:06 2001 +0200
+++ b/src/HOL/NatDef.ML	Tue May 22 15:11:43 2001 +0200
@@ -4,38 +4,15 @@
     Copyright   1991  University of Cambridge
 *)
 
-Goal "mono(%X. {Zero_Rep} Un Suc_Rep`X)";
-by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
-qed "Nat_fun_mono";
-
-bind_thm ("Nat_unfold", Nat_fun_mono RS (Nat_def RS def_lfp_unfold));
-
-(* Zero is a natural number -- this also justifies the type definition*)
-Goal "Zero_Rep: Nat";
-by (stac Nat_unfold 1);
-by (rtac (singletonI RS UnI1) 1);
-qed "Zero_RepI";
-
-Goal "i: Nat ==> Suc_Rep(i) : Nat";
-by (stac Nat_unfold 1);
-by (rtac (imageI RS UnI2) 1);
-by (assume_tac 1);
-qed "Suc_RepI";
+val rew = rewrite_rule [symmetric Nat_def];
 
 (*** Induction ***)
 
-val major::prems = Goal
-    "[| i: Nat;  P(Zero_Rep);   \
-\       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
-by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_lfp_induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "Nat_induct";
-
 val prems = Goalw [Zero_def,Suc_def]
     "[| P(0);   \
 \       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
 by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
-by (rtac (Rep_Nat RS Nat_induct) 1);
+by (rtac (Rep_Nat RS rew Nat'.induct) 1);
 by (REPEAT (ares_tac prems 1
      ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1));
 qed "nat_induct";
@@ -77,7 +54,7 @@
 Goalw [Zero_def,Suc_def] "Suc(m) ~= 0";
 by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1);
 by (rtac Suc_Rep_not_Zero_Rep 1);
-by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
+by (REPEAT (resolve_tac [Rep_Nat, rew Nat'.Suc_RepI, rew Nat'.Zero_RepI] 1));
 qed "Suc_not_Zero";
 
 bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
@@ -92,7 +69,7 @@
 Goalw [Suc_def] "inj(Suc)";
 by (rtac injI 1);
 by (dtac (inj_on_Abs_Nat RS inj_onD) 1);
-by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
+by (REPEAT (resolve_tac [Rep_Nat, rew Nat'.Suc_RepI] 1));
 by (dtac (inj_Suc_Rep RS injD) 1);
 by (etac (inj_Rep_Nat RS injD) 1);
 qed "inj_Suc";
diff -r a5e0289dd56c -r 680ebd093cfe src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Tue May 22 15:10:06 2001 +0200
+++ b/src/HOL/NatDef.thy	Tue May 22 15:11:43 2001 +0200
@@ -35,8 +35,16 @@
 
 (* type definition *)
 
+consts
+  Nat' :: "ind set"
+
+inductive Nat'
+intrs
+  Zero_RepI "Zero_Rep : Nat'"
+  Suc_RepI  "i : Nat' ==> Suc_Rep i : Nat'"
+
 typedef (Nat)
-  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep`X))"   (lfp_def)
+  nat = "Nat'"   (Nat'.Zero_RepI)
 
 instance
   nat :: {ord, zero}