# HG changeset patch
# User paulson
# Date 893061510 -7200
# Node ID d55e2fee208436757fdb490e1236347c906272d5
# Parent  595f905cc34891efec082d0229246b36fbd4ea0c
New laws for mod

diff -r 595f905cc348 -r d55e2fee2084 src/HOL/Divides.ML
--- 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];