# HG changeset patch
# User paulson
# Date 952614458 -3600
# Node ID c7772d3787c3657a5a6c1384a39ebe99de52c6b3
# Parent  5bf82327aa368c8db4ad5cbdb1430a131cbfd0d4
mod_less, div_less are now default simprules

diff -r 5bf82327aa36 -r c7772d3787c3 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Thu Mar 09 16:07:01 2000 +0100
+++ b/src/HOL/Divides.ML	Thu Mar 09 16:07:38 2000 +0100
@@ -48,6 +48,7 @@
 by (rtac (mod_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "mod_less";
+Addsimps [mod_less];
 
 Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
 by (div_undefined_case_tac "n=0" 1);
@@ -61,18 +62,18 @@
 qed "le_mod_geq";
 
 Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
-by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
+by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
 qed "mod_if";
 
 Goal "m mod 1 = 0";
 by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
 qed "mod_1";
 Addsimps [mod_1];
 
 Goal "n mod n = 0";
 by (div_undefined_case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
+by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
 qed "mod_self";
 
 Goal "(m+n) mod n = m mod (n::nat)";
@@ -105,7 +106,7 @@
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
+by (asm_simp_tac (simpset() addsimps [mod_geq, 
 				      diff_less, diff_mult_distrib]) 1);
 qed "mod_mult_distrib";
 
@@ -118,7 +119,7 @@
 Goal "(m*n) mod n = 0";
 by (div_undefined_case_tac "n=0" 1);
 by (induct_tac "m" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
+by (Asm_simp_tac 1);
 by (rename_tac "k" 1);
 by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
@@ -136,6 +137,7 @@
 by (rtac (div_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "div_less";
+Addsimps [div_less];
 
 Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
 by (rtac (div_eq RS wf_less_trans) 1);
@@ -148,7 +150,7 @@
 qed "le_div_geq";
 
 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
-by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
+by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
 qed "div_if";
 
 
@@ -158,7 +160,7 @@
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps [add_assoc, div_less, div_geq,
+	      (simpset() addsimps [add_assoc, div_geq,
 				   add_diff_inverse, diff_less])));
 qed "mod_div_equality";
 
@@ -171,12 +173,12 @@
 
 Goal "m div 1 = m";
 by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
 qed "div_1";
 Addsimps [div_1];
 
 Goal "0<n ==> n div n = 1";
-by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
+by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
 qed "div_self";
 
 
@@ -205,12 +207,12 @@
 
 Goal "0 div m = 0";
 by (div_undefined_case_tac "m=0" 1);
-by (asm_simp_tac (simpset() addsimps [div_less]) 1);
+by (Asm_simp_tac 1);
 qed "div_0"; 
 
 Goal "0 mod m = 0";
 by (div_undefined_case_tac "m=0" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
+by (Asm_simp_tac 1);
 qed "mod_0"; 
 Addsimps [div_0, mod_0];
 
@@ -221,11 +223,11 @@
 by (Clarify_tac 1);
 by (case_tac "n<k" 1);
 (* 1  case n<k *)
-by (asm_simp_tac (simpset() addsimps [div_less]) 1);
+by (Asm_simp_tac 1);
 (* 2  case n >= k *)
 by (case_tac "m<k" 1);
 (* 2.1  case m<k *)
-by (asm_simp_tac (simpset() addsimps [div_less]) 1);
+by (Asm_simp_tac 1);
 (* 2.2  case m>=k *)
 by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
 qed_spec_mp "div_le_mono";
@@ -237,7 +239,7 @@
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rename_tac "k" 1);
 by (case_tac "k<n" 1);
- by (asm_simp_tac (simpset() addsimps [div_less]) 1);
+ by (Asm_simp_tac 1);
 by (subgoal_tac "~(k<m)" 1);
  by (Asm_simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
@@ -262,7 +264,7 @@
 by (res_inst_tac [("n","m")] less_induct 1);
 by (rename_tac "m" 1);
 by (case_tac "m<n" 1);
- by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
+ by (Asm_full_simp_tac 1);
 by (subgoal_tac "0<n" 1);
  by (Asm_simp_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
@@ -274,7 +276,7 @@
 (* case n=m *)
 by (subgoal_tac "m=n" 1);
  by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [div_less]) 1);
+by (Asm_simp_tac 1);
 qed_spec_mp "div_less_dividend";
 Addsimps [div_less_dividend];
 
@@ -285,12 +287,12 @@
 by (excluded_middle_tac "Suc(na)<n" 1);
 (* case Suc(na) < n *)
 by (forward_tac [lessI RS less_trans] 2);
-by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
+by (asm_simp_tac (simpset() addsimps [less_not_refl3]) 2);
 (* case n <= Suc(na) *)
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
 					   mod_geq]) 1);
 by (etac disjE 1);
- by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
+ by (Asm_simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [Suc_diff_le, diff_less, 
 				      le_mod_geq]) 1);
 qed "mod_Suc";
@@ -301,7 +303,7 @@
 (*case n le na*)
 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
 (*case na<n*)
-by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
+by (Asm_simp_tac 1);
 qed "mod_less_divisor";
 
 
@@ -334,15 +336,13 @@
 
 Goal "(m+m) mod 2 = 0";
 by (induct_tac "m" 1);
-by (simp_tac (simpset() addsimps [mod_less]) 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed "mod2_add_self_eq_0";
 Addsimps [mod2_add_self_eq_0];
 
 Goal "((m+m)+n) mod 2 = n mod 2";
 by (induct_tac "m" 1);
-by (simp_tac (simpset() addsimps [mod_less]) 1);
-by (Asm_simp_tac 1);
+by Auto_tac;
 qed "mod2_add_self";
 Addsimps [mod2_add_self];
 
@@ -366,8 +366,7 @@
 by (div_undefined_case_tac "n=0" 1);
 by (res_inst_tac [("n","m")] less_induct 1);
 by (case_tac "na<n" 1);
-by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
-				      mult_less_mono2]) 1);
+by (asm_simp_tac (simpset() addsimps [zero_less_mult_iff, mult_less_mono2]) 1);
 by (subgoal_tac "~ k*na < k*n" 1);
 by (asm_simp_tac
      (simpset() addsimps [zero_less_mult_iff, div_geq,