Declaration of type 'nat' as a datatype (this allows usage of
exhaust_tac and induct_tac on type 'nat'). Moved some proofs
using natE from NatDef.ML to Nat.ML.

--- a/src/HOL/Nat.ML	Fri Jul 24 13:30:28 1998 +0200
+++ b/src/HOL/Nat.ML	Fri Jul 24 13:34:59 1998 +0200
@@ -4,6 +4,101 @@
     Copyright   1997 TU Muenchen
 *)
 
+(** conversion rules for nat_rec **)
+
+val [nat_rec_0, nat_rec_Suc] = nat.recs;
+
+(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
+val prems = goal thy
+    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
+by (simp_tac (simpset() addsimps prems) 1);
+qed "def_nat_rec_0";
+
+val prems = goal thy
+    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
+by (simp_tac (simpset() addsimps prems) 1);
+qed "def_nat_rec_Suc";
+
+val [nat_case_0, nat_case_Suc] = nat.cases;
+
+Goal "n ~= 0 ==> EX m. n = Suc m";
+by (exhaust_tac "n" 1);
+by (REPEAT (Blast_tac 1));
+qed "not0_implies_Suc";
+
+val prems = goal thy "m<n ==> n ~= 0";
+by (exhaust_tac "n" 1);
+by (cut_facts_tac prems 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "gr_implies_not0";
+
+Goal "(n ~= 0) = (0 < n)";
+by (exhaust_tac "n" 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed "neq0_conv";
+AddIffs [neq0_conv];
+
+(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
+bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
+
+Goal "(~(0 < n)) = (n=0)";
+by (rtac iffI 1);
+ by (etac swap 1);
+ by (ALLGOALS Asm_full_simp_tac);
+qed "not_gr0";
+Addsimps [not_gr0];
+
+Goal "m<n ==> 0 < n";
+by (dtac gr_implies_not0 1);
+by (Asm_full_simp_tac 1);
+qed "gr_implies_gr0";
+Addsimps [gr_implies_gr0];
+
+qed_goalw "Least_Suc" thy [Least_nat_def]
+ "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+ (fn _ => [
+        rtac select_equality 1,
+        fold_goals_tac [Least_nat_def],
+        safe_tac (claset() addSEs [LeastI]),
+        rename_tac "j" 1,
+        exhaust_tac "j" 1,
+        Blast_tac 1,
+        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
+        rename_tac "k n" 1,
+        exhaust_tac "k" 1,
+        Blast_tac 1,
+        hyp_subst_tac 1,
+        rewtac Least_nat_def,
+        rtac (select_equality RS arg_cong RS sym) 1,
+        Safe_tac,
+        dtac Suc_mono 1,
+        Blast_tac 1,
+        cut_facts_tac [less_linear] 1,
+        Safe_tac,
+        atac 2,
+        Blast_tac 2,
+        dtac Suc_mono 1,
+        Blast_tac 1]);
+
+qed_goal "nat_induct2" thy 
+"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
+        cut_facts_tac prems 1,
+        rtac less_induct 1,
+        exhaust_tac "n" 1,
+         hyp_subst_tac 1,
+         atac 1,
+        hyp_subst_tac 1,
+        exhaust_tac "nat" 1,
+         hyp_subst_tac 1,
+         atac 1,
+        hyp_subst_tac 1,
+        resolve_tac prems 1,
+        dtac spec 1,
+        etac mp 1,
+        rtac (lessI RS less_trans) 1,
+        rtac (lessI RS Suc_mono) 1]);
+
 Goal "min 0 n = 0";
 by (rtac min_leastL 1);
 by (trans_tac 1);

--- a/src/HOL/Nat.thy	Fri Jul 24 13:30:28 1998 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 24 13:34:59 1998 +0200
@@ -6,21 +6,15 @@
 Nat is a partial order
 *)
 
-Nat = NatDef +
+Nat = NatDef + Inductive +
 
-(*install 'automatic' induction tactic, pretending nat is a datatype
-  except for induct_tac and exhaust_tac, everything is dummy*)
+setup
+  DatatypePackage.setup
 
-MLtext {|
-|> Dtype.add_datatype_info
-("nat", {case_const = Bound 0, case_rewrites = [],
-  constructors = [], induct_tac = nat_ind_tac,
-  exhaustion = natE,
-  exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
-                        THEN_ALL_NEW (rotate_tac ~1),
-  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
-|}
-
+rep_datatype nat
+  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
+  inject   "[[Suc_Suc_eq]]"
+  induct   nat_induct
 
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
 instance nat :: linorder (nat_le_linear)