nat.ML

 goal Nat.thy "n ~= Suc(n)";
 by (nat_ind_tac "n" 1);
 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";
 by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1);
 val nat_case_0 = result();

 by (rtac lessI 1);
 val zero_less_Suc = result();
 
 (** 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);
 by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
 val less_not_refl = result();
 
 (* 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 \
 \    |] ==> P";

 
 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
 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*)
 goal Nat.thy "m<n | m=n | n<m::nat";
 by (nat_ind_tac "m" 1);

 goalw Nat.thy [le_def] "0 <= n";
 by (rtac not_less0 1);
 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;
 
 (*Prevents simplification of f and g: much faster*)

 goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<m::nat";
 by (fast_tac HOL_cs 1);
 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();
 
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
 by (fast_tac (HOL_cs addEs [less_anti_sym]) 1);