# HG changeset patch
# User wenzelm
# Date 1476638334 -7200
# Node ID 41e027ab985caace734a2097b90a313c24fe7e2e
# Parent  0cde0b4d4cb5cb80b360b9c3fd3926b437dfabcf# Parent  fb3bc899fd513c0e336fcaf4c86698e1c5b2a079
merged

diff -r fb3bc899fd51 -r 41e027ab985c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 16 18:22:19 2016 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 16 19:18:54 2016 +0200
@@ -28,12 +28,6 @@
 
 text \<open>@{const divide} and @{const modulo}\<close>
 
-lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
-  by (simp add: div_mult_mod_eq)
-
-lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
-  by (simp add: mult_div_mod_eq)
-
 lemma mod_by_0 [simp]: "a mod 0 = a"
   using div_mult_mod_eq [of a zero] by simp
 
@@ -345,6 +339,11 @@
   shows   "(a div d) div (b div d) = a div b"
   using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
 
+lemma cancel_div_mod_rules:
+  "((a div b) * b + a mod b) + c = a + c"
+  "(b * (a div b) + a mod b) + c = a + c"
+  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
 end
 
 class ring_div = comm_ring_1 + semiring_div
@@ -1042,10 +1041,10 @@
             SOME (t, u) => dest_sum t @ dest_sum u
           | NONE => [tm]));
 
-  val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
-
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
-    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
+    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
 )
 \<close>
 
@@ -1806,10 +1805,10 @@
   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   val dest_sum = Arith_Data.dest_sum;
 
-  val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
-
-  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
-    (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
+  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
+
+  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
+    (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
 )
 \<close>
 
diff -r fb3bc899fd51 -r 41e027ab985c src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 18:22:19 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 19:18:54 2016 +0200
@@ -51,13 +51,12 @@
 \<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 
 declare dvd_def[algebra]
-declare dvd_eq_mod_eq_0[symmetric, algebra]
+declare mod_eq_0_iff_dvd[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare div_by_0[algebra]
 declare mod_by_0[algebra]
 declare mult_div_mod_eq[algebra]
-declare div_mod_equality2[symmetric, algebra]
 declare div_minus_minus[algebra]
 declare mod_minus_minus[algebra]
 declare div_minus_right[algebra]
diff -r fb3bc899fd51 -r 41e027ab985c src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Oct 16 18:22:19 2016 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 16 19:18:54 2016 +0200
@@ -410,7 +410,7 @@
   end
 \<close> "Cooper's algorithm for Presburger arithmetic"
 
-declare dvd_eq_mod_eq_0 [symmetric, presburger]
+declare mod_eq_0_iff_dvd [presburger]
 declare mod_by_Suc_0 [presburger] 
 declare mod_0 [presburger]
 declare mod_by_1 [presburger]
@@ -418,13 +418,11 @@
 declare div_by_0 [presburger]
 declare mod_by_0 [presburger]
 declare mod_div_trivial [presburger]
-declare div_mod_equality2 [presburger]
-declare div_mod_equality [presburger]
 declare mult_div_mod_eq [presburger]
 declare div_mult_mod_eq [presburger]
 declare mod_mult_self1 [presburger]
 declare mod_mult_self2 [presburger]
-declare mod2_Suc_Suc[presburger]
+declare mod2_Suc_Suc [presburger]
 declare not_mod_2_eq_0_eq_1 [presburger] 
 declare nat_zero_less_power_iff [presburger]