Nat.ML

--- a/Nat.ML	Tue Feb 15 10:05:17 1994 +0100
+++ b/Nat.ML	Wed Feb 16 15:13:53 1994 +0100
@@ -122,6 +122,8 @@
 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
 val n_not_Suc_n = result();
 
+val Suc_n_not_n = n_not_Suc_n RS not_sym;
+
 (*** nat_case -- the selection operator for nat ***)
 
 goalw Nat.thy [nat_case_def] "nat_case(0, a, f) = a";
@@ -216,15 +218,12 @@
 
 (** Elimination properties **)
 
-goalw Nat.thy [less_def] "n<m --> ~ m<n::nat";
-by (rtac (wf_pred_nat RS wf_trancl RS wf_anti_sym RS notI RS impI) 1);
-by (assume_tac 1);
-by (assume_tac 1);
+val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<n::nat";
+by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_anti_sym]@prems))1);
 val less_not_sym = result();
 
 (* [| n<m; m<n |] ==> R *)
-val less_anti_sym = standard (less_not_sym RS mp RS notE);
-
+val less_anti_sym = standard (less_not_sym RS notE);
 
 goalw Nat.thy [less_def] "~ n<n::nat";
 by (rtac notI 1);
@@ -234,6 +233,10 @@
 (* n<n ==> R *)
 val less_anti_refl = standard (less_not_refl RS notE);
 
+goal Nat.thy "!!m. n<m ==> m ~= n::nat";
+by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
+val less_not_refl2 = result();
+
 
 val major::prems = goalw Nat.thy [less_def]
     "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
@@ -310,8 +313,8 @@
 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
 val Suc_less_eq = result();
 
-val [major] = goal Nat.thy "Suc(n)<n ==> P";
-by (rtac (major RS Suc_lessD RS less_anti_refl) 1);
+goal Nat.thy "~(Suc(n) < n)";
+by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
 val not_Suc_n_less_n = result();
 
 (*"Less than" is a linear ordering*)
@@ -345,8 +348,9 @@
 val le0 = result();
 
 val nat_simps = [not_less0, less_not_refl, zero_less_Suc, lessI, 
-	     Suc_less_eq, less_Suc_eq, le0, 
-	     Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq, 
+	     Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
+	     Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
+             n_not_Suc_n, Suc_n_not_n,
 	     nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
 val nat_ss = sum_ss  addsimps  nat_simps;
@@ -375,12 +379,12 @@
 val not_leE = result();
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
-by(simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
+by(simp_tac nat_ss 1);
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
 val lessD = result();
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
-by(asm_full_simp_tac (HOL_ss addsimps [less_Suc_eq]) 1);
+by(asm_full_simp_tac nat_ss 1);
 by(fast_tac HOL_cs 1);
 val Suc_leD = result();