src/HOL/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);