--- a/src/HOL/Divides.ML Mon Apr 20 10:37:00 1998 +0200
+++ b/src/HOL/Divides.ML Mon Apr 20 10:38:30 1998 +0200
@@ -56,7 +56,22 @@
by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
by (stac (mod_geq RS sym) 2);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
-qed "mod_eq_add";
+qed "mod_add_cancel2";
+
+goal thy "!!k. 0<n ==> (n+m) mod n = m mod n";
+by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_cancel2]) 1);
+qed "mod_add_cancel1";
+
+goal thy "!!n. 0<n ==> (m + k*n) mod n = m mod n";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_cancel1]))));
+qed "mod_mult_cancel1";
+
+goal thy "!!m. 0<n ==> (m + n*k) mod n = m mod n";
+by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_cancel1]) 1);
+qed "mod_mult_cancel2";
+
+Addsimps [mod_mult_cancel1, mod_mult_cancel2];
goal thy "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
by (res_inst_tac [("n","m")] less_induct 1);
@@ -77,7 +92,7 @@
goal thy "!!n. 0<n ==> m*n mod n = 0";
by (induct_tac "m" 1);
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
-by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
+by (dres_inst_tac [("m","m*n")] mod_add_cancel2 1);
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
qed "mod_mult_self_is_0";
Addsimps [mod_mult_self_is_0];