# HG changeset patch
# User haftmann
# Date 1481984534 -3600
# Node ID 50c715579715f9b60391a51f427dcb398f0378f0
# Parent  7759f176618947850d06742edb84530e48ed280c
reoriented congruence rules in non-explosive direction

diff -r 7759f1766189 -r 50c715579715 NEWS
--- a/NEWS	Sat Dec 17 15:22:14 2016 +0100
+++ b/NEWS	Sat Dec 17 15:22:14 2016 +0100
@@ -6,6 +6,24 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Swapped orientation of congruence rules mod_add_left_eq,
+mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
+mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
+mod_diff_eq.  INCOMPATIBILITY.
+
+* Generalized some facts:
+    zminus_zmod ~> mod_minus_eq
+    zdiff_zmod_left ~> mod_diff_left_eq
+    zdiff_zmod_right ~> mod_diff_right_eq
+    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
+INCOMPATIBILITY.
+
+* Named collection mod_simps covers various congruence rules
+concerning mod, replacing former zmod_simps.
+INCOMPATIBILITY.
+
 * (Co)datatype package:
   - The 'size_gen_o_map' lemma is no longer generated for datatypes
     with type class annotations. As a result, the tactic that derives
@@ -74,7 +92,6 @@
 * Solve direct: option "solve_direct_strict_warnings" gives explicit
 warnings for lemma statements with trivial proofs.
 
-
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
 * More aggressive flushing of machine-generated input, according to
diff -r 7759f1766189 -r 50c715579715 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -3206,7 +3206,7 @@
       using of_int_eq_iff apply fastforce
       by (metis of_int_add of_int_mult of_int_of_nat_eq)
     also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
-      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
+      by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
     also have "... \<longleftrightarrow> j mod n = k mod n"
       by (metis of_nat_eq_iff zmod_int)
     finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
diff -r 7759f1766189 -r 50c715579715 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
@@ -45,8 +45,8 @@
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset =
       put_simpset HOL_basic_ss ctxt
-      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
-          mod_add_right_eq [symmetric]
+      addsimps @{thms refl mod_add_eq mod_add_left_eq
+          mod_add_right_eq
           div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
           mod_self
           div_by_0 mod_by_0 div_0 mod_0
diff -r 7759f1766189 -r 50c715579715 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Dec 17 15:22:14 2016 +0100
@@ -31,8 +31,6 @@
              @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
 val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
 
-val mod_add_eq = @{thm "mod_add_eq"} RS sym;
-
 fun prepare_for_mir q fm = 
   let
     val ps = Logic.strip_params fm
@@ -71,7 +69,7 @@
     val (t,np,nh) = prepare_for_mir q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = put_simpset HOL_basic_ss ctxt
-                        addsimps [refl, mod_add_eq, 
+                        addsimps [refl, @{thm mod_add_eq}, 
                                   @{thm mod_self},
                                   @{thm div_0}, @{thm mod_0},
                                   @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
diff -r 7759f1766189 -r 50c715579715 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -189,97 +189,6 @@
   finally show ?thesis .
 qed
 
-text \<open>Addition respects modular equivalence.\<close>
-
-lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a + b) mod c = (a mod c + b) mod c"
-proof -
-  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a mod c + b + a div c * c) mod c"
-    by (simp only: ac_simps)
-  also have "\<dots> = (a mod c + b) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis .
-qed
-
-lemma mod_add_right_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a + b) mod c = (a + b mod c) mod c"
-proof -
-  have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a + b mod c + b div c * c) mod c"
-    by (simp only: ac_simps)
-  also have "\<dots> = (a + b mod c) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis .
-qed
-
-lemma mod_add_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a + b) mod c = (a mod c + b mod c) mod c"
-by (rule trans [OF mod_add_left_eq mod_add_right_eq])
-
-lemma mod_add_cong:
-  assumes "a mod c = a' mod c"
-  assumes "b mod c = b' mod c"
-  shows "(a + b) mod c = (a' + b') mod c"
-proof -
-  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
-    unfolding assms ..
-  thus ?thesis
-    by (simp only: mod_add_eq [symmetric])
-qed
-
-text \<open>Multiplication respects modular equivalence.\<close>
-
-lemma mod_mult_left_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a * b) mod c = ((a mod c) * b) mod c"
-proof -
-  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
-    by (simp only: algebra_simps)
-  also have "\<dots> = (a mod c * b) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis .
-qed
-
-lemma mod_mult_right_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a * b) mod c = (a * (b mod c)) mod c"
-proof -
-  have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
-    by (simp only: div_mult_mod_eq)
-  also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
-    by (simp only: algebra_simps)
-  also have "\<dots> = (a * (b mod c)) mod c"
-    by (rule mod_mult_self1)
-  finally show ?thesis .
-qed
-
-lemma mod_mult_eq: \<comment> \<open>FIXME reorient\<close>
-  "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
-by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
-
-lemma mod_mult_cong:
-  assumes "a mod c = a' mod c"
-  assumes "b mod c = b' mod c"
-  shows "(a * b) mod c = (a' * b') mod c"
-proof -
-  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
-    unfolding assms ..
-  thus ?thesis
-    by (simp only: mod_mult_eq [symmetric])
-qed
-
-text \<open>Exponentiation respects modular equivalence.\<close>
-
-lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
-apply (induct n, simp_all)
-apply (rule mod_mult_right_eq [THEN trans])
-apply (simp (no_asm_simp))
-apply (rule mod_mult_eq [symmetric])
-done
-
 lemma mod_mod_cancel:
   assumes "c dvd b"
   shows "a mod b mod c = a mod c"
@@ -331,6 +240,121 @@
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
+named_theorems mod_simps
+
+text \<open>Addition respects modular equivalence.\<close>
+
+lemma mod_add_left_eq [mod_simps]:
+  "(a mod c + b) mod c = (a + b) mod c"
+proof -
+  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+    by (simp only: div_mult_mod_eq)
+  also have "\<dots> = (a mod c + b + a div c * c) mod c"
+    by (simp only: ac_simps)
+  also have "\<dots> = (a mod c + b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis
+    by (rule sym)
+qed
+
+lemma mod_add_right_eq [mod_simps]:
+  "(a + b mod c) mod c = (a + b) mod c"
+  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_add_eq:
+  "(a mod c + b mod c) mod c = (a + b) mod c"
+  by (simp add: mod_add_left_eq mod_add_right_eq)
+
+lemma mod_sum_eq [mod_simps]:
+  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
+proof (induct A rule: infinite_finite_induct)
+  case (insert i A)
+  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
+    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
+    by simp
+  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
+    by (simp add: mod_simps)
+  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
+    by (simp add: insert.hyps)
+  finally show ?case
+    by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_add_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a + b) mod c = (a' + b') mod c"
+proof -
+  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+    unfolding assms ..
+  then show ?thesis
+    by (simp add: mod_add_eq)
+qed
+
+text \<open>Multiplication respects modular equivalence.\<close>
+
+lemma mod_mult_left_eq [mod_simps]:
+  "((a mod c) * b) mod c = (a * b) mod c"
+proof -
+  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+    by (simp only: div_mult_mod_eq)
+  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+    by (simp only: algebra_simps)
+  also have "\<dots> = (a mod c * b) mod c"
+    by (rule mod_mult_self1)
+  finally show ?thesis
+    by (rule sym)
+qed
+
+lemma mod_mult_right_eq [mod_simps]:
+  "(a * (b mod c)) mod c = (a * b) mod c"
+  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
+
+lemma mod_mult_eq:
+  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
+  by (simp add: mod_mult_left_eq mod_mult_right_eq)
+
+lemma mod_prod_eq [mod_simps]:
+  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
+proof (induct A rule: infinite_finite_induct)
+  case (insert i A)
+  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
+    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
+    by simp
+  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
+    by (simp add: mod_simps)
+  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
+    by (simp add: insert.hyps)
+  finally show ?case
+    by (simp add: insert.hyps mod_simps)
+qed simp_all
+
+lemma mod_mult_cong:
+  assumes "a mod c = a' mod c"
+  assumes "b mod c = b' mod c"
+  shows "(a * b) mod c = (a' * b') mod c"
+proof -
+  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+    unfolding assms ..
+  then show ?thesis
+    by (simp add: mod_mult_eq)
+qed
+
+text \<open>Exponentiation respects modular equivalence.\<close>
+
+lemma power_mod [mod_simps]: 
+  "((a mod b) ^ n) mod b = (a ^ n) mod b"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
+    by (simp add: mod_mult_right_eq)
+  with Suc show ?case
+    by (simp add: mod_mult_left_eq mod_mult_right_eq)
+qed
+
 end
 
 class ring_div = comm_ring_1 + semiring_div
@@ -338,9 +362,28 @@
 
 subclass idom_divide ..
 
+lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
+  using div_mult_mult1 [of "- 1" a b] by simp
+
+lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
+  using mod_mult_mult1 [of "- 1" a b] by simp
+
+lemma div_minus_right: "a div (- b) = (- a) div b"
+  using div_minus_minus [of "- a" b] by simp
+
+lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
+  using mod_minus_minus [of "- a" b] by simp
+
+lemma div_minus1_right [simp]: "a div (- 1) = - a"
+  using div_minus_right [of a 1] by simp
+
+lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
+  using mod_minus_right [of a 1] by simp
+
 text \<open>Negation respects modular equivalence.\<close>
 
-lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+lemma mod_minus_eq [mod_simps]:
+  "(- (a mod b)) mod b = (- a) mod b"
 proof -
   have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
     by (simp only: div_mult_mod_eq)
@@ -348,7 +391,8 @@
     by (simp add: ac_simps)
   also have "\<dots> = (- (a mod b)) mod b"
     by (rule mod_mult_self1)
-  finally show ?thesis .
+  finally show ?thesis
+    by (rule sym)
 qed
 
 lemma mod_minus_cong:
@@ -357,51 +401,37 @@
 proof -
   have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
     unfolding assms ..
-  thus ?thesis
-    by (simp only: mod_minus_eq [symmetric])
+  then show ?thesis
+    by (simp add: mod_minus_eq)
 qed
 
 text \<open>Subtraction respects modular equivalence.\<close>
 
-lemma mod_diff_left_eq:
-  "(a - b) mod c = (a mod c - b) mod c"
-  using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
-
-lemma mod_diff_right_eq:
-  "(a - b) mod c = (a - b mod c) mod c"
-  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
+lemma mod_diff_left_eq [mod_simps]:
+  "(a mod c - b) mod c = (a - b) mod c"
+  using mod_add_cong [of a c "a mod c" "- b" "- b"]
+  by simp
+
+lemma mod_diff_right_eq [mod_simps]:
+  "(a - b mod c) mod c = (a - b) mod c"
+  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+  by simp
 
 lemma mod_diff_eq:
-  "(a - b) mod c = (a mod c - b mod c) mod c"
-  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
+  "(a mod c - b mod c) mod c = (a - b) mod c"
+  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
+  by simp
 
 lemma mod_diff_cong:
   assumes "a mod c = a' mod c"
   assumes "b mod c = b' mod c"
   shows "(a - b) mod c = (a' - b') mod c"
-  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
-
-lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
-  using div_mult_mult1 [of "- 1" a b]
-  unfolding neg_equal_0_iff_equal by simp
-
-lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)"
-  using mod_mult_mult1 [of "- 1" a b] by simp
-
-lemma div_minus_right: "a div (-b) = (-a) div b"
-  using div_minus_minus [of "-a" b] by simp
-
-lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)"
-  using mod_minus_minus [of "-a" b] by simp
-
-lemma div_minus1_right [simp]: "a div (-1) = -a"
-  using div_minus_right [of a 1] by simp
-
-lemma mod_minus1_right [simp]: "a mod (-1) = 0"
-  using mod_minus_right [of a 1] by simp
+  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
+  by simp
 
 lemma minus_mod_self2 [simp]:
   "(a - b) mod b = a mod b"
+  using mod_diff_right_eq [of a b b]
   by (simp add: mod_diff_right_eq)
 
 lemma minus_mod_self1 [simp]:
@@ -455,18 +485,21 @@
   assume "a mod 2 = 1"
   moreover assume "b mod 2 = 1"
   ultimately show "(a + b) mod 2 = 0"
-    using mod_add_eq [of a b 2] by simp
+    using mod_add_eq [of a 2 b] by simp
 next
   fix a b
   assume "(a * b) mod 2 = 0"
+  then have "(a mod 2) * (b mod 2) mod 2 = 0"
+    by (simp add: mod_mult_eq)
   then have "(a mod 2) * (b mod 2) = 0"
-    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
+    by (cases "a mod 2 = 0") simp_all
   then show "a mod 2 = 0 \<or> b mod 2 = 0"
     by (rule divisors_zero)
 next
   fix a
   assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
+  then have "a = a div 2 * 2 + 1"
+    using div_mult_mod_eq [of a 2] by simp
   then show "\<exists>b. a = b + 1" ..
 qed
 
@@ -1052,6 +1085,24 @@
     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
+lemma mod_Suc_eq [mod_simps]:
+  "Suc (m mod n) mod n = Suc m mod n"
+proof -
+  have "(m mod n + 1) mod n = (m + 1) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma mod_Suc_Suc_eq [mod_simps]:
+  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
+proof -
+  have "(m mod n + 2) mod n = (m + 2) mod n"
+    by (simp only: mod_simps)
+  then show ?thesis
+    by simp
+qed
+
 
 subsubsection \<open>Quotient\<close>
 
@@ -1860,12 +1911,12 @@
 apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
 done
 
-lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
+lemma zmod_zminus1_not_zero:
   fixes k l :: int
   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   by (simp add: mod_eq_0_iff_dvd)
 
-lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
+lemma zmod_zminus2_not_zero:
   fixes k l :: int
   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   by (simp add: mod_eq_0_iff_dvd)
@@ -2094,7 +2145,7 @@
     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
 apply (rule iffI, clarify)
  apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq)
+ apply (subst mod_add_eq [symmetric])
  apply (subst zdiv_zadd1_eq)
  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
 txt\<open>converse direction\<close>
@@ -2107,7 +2158,7 @@
     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
 apply (rule iffI, clarify)
  apply (erule_tac P="P x y" for x y in rev_mp)
- apply (subst mod_add_eq)
+ apply (subst mod_add_eq [symmetric])
  apply (subst zdiv_zadd1_eq)
  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
 txt\<open>converse direction\<close>
@@ -2427,24 +2478,6 @@
  apply simp_all
 done
 
-text \<open>by Brian Huffman\<close>
-lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
-by (rule mod_minus_eq [symmetric])
-
-lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
-by (rule mod_diff_left_eq [symmetric])
-
-lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
-by (rule mod_diff_right_eq [symmetric])
-
-lemmas zmod_simps =
-  mod_add_left_eq  [symmetric]
-  mod_add_right_eq [symmetric]
-  mod_mult_right_eq[symmetric]
-  mod_mult_left_eq [symmetric]
-  power_mod
-  zminus_zmod zdiff_zmod_left zdiff_zmod_right
-
 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
 
 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
@@ -2504,28 +2537,29 @@
 apply (rule Divides.div_less_dividend, simp_all)
 done
 
-lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
+lemma (in ring_div) mod_eq_dvd_iff:
+  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
 proof
-  assume H: "x mod n = y mod n"
-  hence "x mod n - y mod n = 0" by simp
-  hence "(x mod n - y mod n) mod n = 0" by simp
-  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
-  thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0)
+  assume ?P
+  then have "(a mod c - b mod c) mod c = 0"
+    by simp
+  then show ?Q
+    by (simp add: dvd_eq_mod_eq_0 mod_simps)
 next
-  assume H: "n dvd x - y"
-  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
-  hence "x = n*k + y" by simp
-  hence "x mod n = (n*k + y) mod n" by simp
-  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
+  assume ?Q
+  then obtain d where d: "a - b = c * d" ..
+  then have "a = c * d + b"
+    by (simp add: algebra_simps)
+  then show ?P by simp
 qed
 
-lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
+lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   shows "\<exists>q. x = y + n * q"
 proof-
   from xy have th: "int x - int y = int (x - y)" by simp
   from xyn have "int x mod int n = int y mod int n"
     by (simp add: zmod_int [symmetric])
-  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
+  hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
   hence "n dvd x - y" by (simp add: th zdvd_int)
   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
 qed
diff -r 7759f1766189 -r 50c715579715 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -72,7 +72,7 @@
 declare zmod_eq_0_iff[algebra]
 declare dvd_0_left_iff[algebra]
 declare zdvd1_eq[algebra]
-declare zmod_eq_dvd_iff[algebra]
+declare mod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
 context semiring_parity
diff -r 7759f1766189 -r 50c715579715 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -112,7 +112,8 @@
   case 3 show ?case by auto
 next
   case (4 _ a1 _ a2) thus ?case
-    by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
+    by (induction a1 a2 rule: plus_parity.induct)
+      (auto simp add: mod_add_eq [symmetric])
 qed
 
 text{* In case 4 we needed to refer to particular variables.
diff -r 7759f1766189 -r 50c715579715 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -133,7 +133,7 @@
 
 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
 apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps field_simps)
+apply (simp_all add: Rep_simps mod_simps field_simps)
 done
 
 end
@@ -147,12 +147,12 @@
 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
 apply (induct k)
 apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps)
+apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
 done
 
 lemma of_int_eq: "of_int z = Abs (z mod n)"
 apply (cases z rule: int_diff_cases)
-apply (simp add: Rep_simps of_nat_eq diff_def zmod_simps)
+apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
 done
 
 lemma Rep_numeral:
diff -r 7759f1766189 -r 50c715579715 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -626,7 +626,7 @@
       by (auto simp add: set_conv_nth)
     \<comment> "the following bound is terrible, but it simplifies the proof"
     from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
-      by (simp add: mod_add_left_eq)
+      by (simp add: mod_add_left_eq [symmetric])
     moreover
     \<comment> "why is the following so hard to prove??"
     have "\<forall>m. m < (Suc m)*(length w) + k"
diff -r 7759f1766189 -r 50c715579715 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -251,7 +251,7 @@
   done
 
 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
-  by (metis cong_int_def zmod_eq_dvd_iff)
+  by (metis cong_int_def mod_eq_dvd_iff)
 
 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   by (simp add: cong_altdef_int)
@@ -429,7 +429,7 @@
   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
 
 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
-  by (metis cong_int_def minus_minus zminus_zmod)
+  by (metis cong_int_def minus_minus mod_minus_cong)
 
 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   by (auto simp add: cong_altdef_int)
diff -r 7759f1766189 -r 50c715579715 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -369,7 +369,7 @@
     hence th: "[a^?r = 1] (mod n)"
       using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
       apply (simp add: cong_nat_def del: One_nat_def)
-      by (simp add: mod_mult_left_eq[symmetric])
+      by (metis mod_mult_left_eq nat_mult_1)
     {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
     moreover
     {assume r: "?r \<noteq> 0"
diff -r 7759f1766189 -r 50c715579715 src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -167,7 +167,7 @@
     fix a b
     assume a: "P_1 res a" "P_1 res b"
     hence "int p * int q dvd a - b"
-      using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int zmod_eq_dvd_iff[of a _ b]
+      using divides_mult[of "int p" "a - b" "int q"] pq_coprime_int mod_eq_dvd_iff [of a _ b]
       unfolding P_1_def by force
     hence "a = b" using dvd_imp_le_int[of "a - b"] a unfolding P_1_def by fastforce
   }
@@ -187,7 +187,7 @@
     assume a: "x \<in> BuC" "y \<in> BuC" "f_1 x = f_1 y"
     hence "int p * int q dvd x - y"
       using f_1_def pq_coprime_int divides_mult[of "int p" "x - y" "int q"] 
-            zmod_eq_dvd_iff[of x _ y] by auto
+            mod_eq_dvd_iff[of x _ y] by auto
     hence "x = y"
       using dvd_imp_le_int[of "x - y" "int p * int q"] a unfolding BuC_def by force
   }
diff -r 7759f1766189 -r 50c715579715 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -40,7 +40,7 @@
   apply (insert m_gt_one)
   apply (rule abelian_groupI)
   apply (unfold R_def residue_ring_def)
-  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
+  apply (auto simp add: mod_add_right_eq ac_simps)
   apply (case_tac "x = 0")
   apply force
   apply (subgoal_tac "(x + (m - x)) mod m = 0")
@@ -55,7 +55,7 @@
   apply auto
   apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   apply (erule ssubst)
-  apply (subst mod_mult_right_eq [symmetric])+
+  apply (subst mod_mult_right_eq)+
   apply (simp_all only: ac_simps)
   done
 
@@ -64,9 +64,9 @@
   apply (rule abelian_group)
   apply (rule comm_monoid)
   apply (unfold R_def residue_ring_def, auto)
-  apply (subst mod_add_eq [symmetric])
+  apply (subst mod_add_eq)
   apply (subst mult.commute)
-  apply (subst mod_mult_right_eq [symmetric])
+  apply (subst mod_mult_right_eq)
   apply (simp add: field_simps)
   done
 
@@ -116,9 +116,9 @@
   apply auto
   apply (rule the_equality)
   apply auto
-  apply (subst mod_add_right_eq [symmetric])
+  apply (subst mod_add_right_eq)
   apply auto
-  apply (subst mod_add_left_eq [symmetric])
+  apply (subst mod_add_left_eq)
   apply auto
   apply (subgoal_tac "y mod m = - x mod m")
   apply simp
@@ -143,13 +143,11 @@
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
   unfolding R_def residue_ring_def
-  apply auto
-  apply presburger
-  done
+  by (auto simp add: mod_simps)
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   unfolding R_def residue_ring_def
-  by auto (metis mod_mult_eq)
+  by (auto simp add: mod_simps)
 
 lemma zero_cong: "\<zero> = 0"
   unfolding R_def residue_ring_def by auto
diff -r 7759f1766189 -r 50c715579715 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -456,7 +456,7 @@
     unfolding round_def
     unfolding steps_to_steps'
     unfolding H1[symmetric]
-    by (simp add: uint_word_ariths(1) rdmods
+    by (simp add: uint_word_ariths(1) mod_simps
       uint_word_of_int_id)
 qed
 
diff -r 7759f1766189 -r 50c715579715 src/HOL/SPARK/Manual/Proc1.thy
--- a/src/HOL/SPARK/Manual/Proc1.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Manual/Proc1.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -5,10 +5,10 @@
 spark_open "loop_invariant/proc1"
 
 spark_vc procedure_proc1_5
-  by (simp add: ring_distribs pull_mods)
+  by (simp add: ring_distribs mod_simps)
 
 spark_vc procedure_proc1_8
-  by (simp add: ring_distribs pull_mods)
+  by (simp add: ring_distribs mod_simps)
 
 spark_end
 
diff -r 7759f1766189 -r 50c715579715 src/HOL/SPARK/Manual/Proc2.thy
--- a/src/HOL/SPARK/Manual/Proc2.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/SPARK/Manual/Proc2.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -5,7 +5,7 @@
 spark_open "loop_invariant/proc2"
 
 spark_vc procedure_proc2_7
-  by (simp add: ring_distribs pull_mods)
+  by (simp add: ring_distribs mod_simps)
 
 spark_end
 
diff -r 7759f1766189 -r 50c715579715 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 17 15:22:14 2016 +0100
@@ -824,8 +824,8 @@
 val div_mod_ss =
   simpset_of (put_simpset HOL_basic_ss @{context}
     addsimps @{thms simp_thms
-      mod_eq_0_iff_dvd mod_add_left_eq [symmetric] mod_add_right_eq [symmetric]
-      mod_add_eq [symmetric] div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
+      mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq
+      mod_add_eq div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
       mod_self mod_by_0 div_by_0
       div_0 mod_0 div_by_1 mod_by_1
       div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -308,17 +308,12 @@
 
 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
   apply (induct n arbitrary: w)
-   apply simp
-   apply (subst mod_add_left_eq)
-   apply (simp add: bin_last_def)
-   apply arith
-  apply (simp add: bin_last_def bin_rest_def Bit_def)
-  apply (clarsimp simp: mod_mult_mult1 [symmetric] 
-         mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
-  apply (rule trans [symmetric, OF _ emep1])
-  apply auto
+   apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
+   apply (smt pos_zmod_mult_2 zle2p)
+  apply (simp add: mult_mod_right)
   done
 
+
 subsection "Simplifications for (s)bintrunc"
 
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
@@ -647,28 +642,6 @@
   "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
-lemmas zmod_uminus' = zminus_zmod [where m=c] for c
-lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
-
-lemmas brdmod1s' [symmetric] =
-  mod_add_left_eq mod_add_right_eq
-  mod_diff_left_eq mod_diff_right_eq
-  mod_mult_left_eq mod_mult_right_eq
-
-lemmas brdmods' [symmetric] = 
-  zpower_zmod' [symmetric]
-  trans [OF mod_add_left_eq mod_add_right_eq] 
-  trans [OF mod_diff_left_eq mod_diff_right_eq] 
-  trans [OF mod_mult_right_eq mod_mult_left_eq] 
-  zmod_uminus' [symmetric]
-  mod_add_left_eq [where b = "1::int"]
-  mod_diff_left_eq [where b = "1::int"]
-
-lemmas bintr_arith1s =
-  brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
-lemmas bintr_ariths =
-  brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
-
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
 
 lemma bintr_ge0: "0 \<le> bintrunc n w"
diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -643,14 +643,14 @@
 lemma mod_BIT:
   "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
 proof -
-  have "bin mod 2 ^ n < 2 ^ n" by simp
-  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
-  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
-    by (rule mult_left_mono) simp
-  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
-  then show ?thesis
-    by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
-      mod_pos_pos_trivial)
+  have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
+    by (simp add: mod_mult_mult1)
+  also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
+    by (simp add: ac_simps p1mod22k')
+  also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
+    by (simp only: mod_simps)
+  finally show ?thesis
+    by (auto simp add: Bit_def)
 qed
 
 lemma AND_mod:
diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -8,6 +8,10 @@
 imports Main
 begin
 
+lemma one_mod_exp_eq_one [simp]:
+  "1 mod (2 * 2 ^ n) = (1::int)"
+  by (smt mod_pos_pos_trivial zero_less_power)
+
 lemma mod_2_neq_1_eq_eq_0:
   fixes k :: int
   shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Word.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -282,10 +282,10 @@
 subsection \<open>Arithmetic operations\<close>
 
 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
-  by (metis bintr_ariths(6))
+  by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
 
 lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
-  by (metis bintr_ariths(7))
+  by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
 
 instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
 begin
@@ -295,16 +295,16 @@
 lift_definition one_word :: "'a word" is "1" .
 
 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +"
-  by (metis bintr_ariths(2))
+  by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
 
 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -"
-  by (metis bintr_ariths(3))
+  by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
 
 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
-  by (metis bintr_ariths(5))
+  by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
 
 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
-  by (metis bintr_ariths(4))
+  by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
 
 definition
   word_div_def: "a div b = word_of_int (uint a div uint b)"
@@ -332,9 +332,6 @@
   unfolding word_succ_def word_pred_def zero_word_def one_word_def
   by simp_all
 
-lemmas arths = 
-  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
-
 lemma wi_homs: 
   shows
   wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
@@ -1340,10 +1337,11 @@
     and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
     and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
     and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
-  by (simp_all add: uint_word_arith_bintrs
-    [THEN uint_sint [symmetric, THEN trans],
-    unfolded uint_sint bintr_arith1s bintr_ariths 
-      len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
+         apply (simp_all only: word_sbin.inverse_norm [symmetric])
+         apply (simp_all add: wi_hom_syms)
+   apply transfer apply simp
+  apply transfer apply simp
+  done
 
 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
@@ -1443,7 +1441,7 @@
   with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
     by auto
   then show ?thesis
-    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
+    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
 qed
 
 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
@@ -2699,7 +2697,7 @@
 lemma nth_w2p:
   "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
   unfolding test_bit_2p [symmetric] word_of_int [symmetric]
-  by (simp add:  of_int_power)
+  by simp
 
 lemma uint_2p: 
   "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
@@ -2723,16 +2721,7 @@
   done
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
-  apply (unfold word_arith_power_alt)
-  apply (case_tac "len_of TYPE ('a)")
-   apply clarsimp
-  apply (case_tac "nat")
-   apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
-   apply (rule box_equals) 
-     apply (rule_tac [2] bintr_ariths (1))+ 
-   apply simp
-  apply simp
-  done
+  by (induct n) (simp_all add: wi_hom_syms)
 
 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
   apply (rule xtr3) 
@@ -3244,6 +3233,9 @@
 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
 
+lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
+  by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
+
 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
   unfolding word_numeral_alt by (rule and_mask_wi)
 
@@ -3342,12 +3334,12 @@
   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
-  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
+  by (auto simp add: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
 
 lemma mask_power_eq:
   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
   using word_of_int_Ex [where x=x]
-  by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
+  by (auto simp add: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
 
 
 subsubsection \<open>Revcast\<close>
@@ -4242,7 +4234,7 @@
   apply (simp add: word_size nat_mod_distrib)
   apply (rule of_nat_eq_0_iff [THEN iffD1])
   apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
-  using mod_mod_trivial zmod_eq_dvd_iff
+  using mod_mod_trivial mod_eq_dvd_iff
   apply blast
   done
 
@@ -4579,9 +4571,9 @@
   shows "(x + y) mod b = z' mod b'"
 proof -
   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
-    by (simp add: mod_add_eq[symmetric])
+    by (simp add: mod_add_eq)
   also have "\<dots> = (x' + y') mod b'"
-    by (simp add: mod_add_eq[symmetric])
+    by (simp add: mod_add_eq)
   finally show ?thesis by (simp add: 4)
 qed
 
@@ -4591,11 +4583,8 @@
       and 3: "y mod b' = y' mod b'"
       and 4: "x' - y' = z'"
   shows "(x - y) mod b = z' mod b'"
-  using assms
-  apply (subst mod_diff_left_eq)
-  apply (subst mod_diff_right_eq)
-  apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
-  done
+  using 1 2 3 4 [symmetric]
+  by (auto intro: mod_diff_cong)
 
 lemma word_induct_less: 
   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
diff -r 7759f1766189 -r 50c715579715 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -201,10 +201,6 @@
 
 lemmas push_mods = push_mods' [THEN eq_reflection]
 lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
-lemmas mod_simps = 
-  mod_mult_self2_is_0 [THEN eq_reflection]
-  mod_mult_self1_is_0 [THEN eq_reflection]
-  mod_mod_trivial [THEN eq_reflection]
 
 lemma nat_mod_eq:
   "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" 
diff -r 7759f1766189 -r 50c715579715 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/ex/Word_Type.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -57,7 +57,7 @@
 
 lemma bitrunc_plus:
   "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
-  by (simp add: bitrunc_eq_mod mod_add_eq [symmetric])
+  by (simp add: bitrunc_eq_mod mod_add_eq)
 
 lemma bitrunc_of_1_eq_0_iff [simp]:
   "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
@@ -74,12 +74,12 @@
 lemma bitrunc_uminus:
   fixes k :: int
   shows "bitrunc n (- (bitrunc n k)) = bitrunc n (- k)"
-  by (simp add: bitrunc_eq_mod mod_minus_eq [symmetric])
+  by (simp add: bitrunc_eq_mod mod_minus_eq)
 
 lemma bitrunc_minus:
   fixes k l :: int
   shows "bitrunc n (bitrunc n k - bitrunc n l) = bitrunc n (k - l)"
-  by (simp add: bitrunc_eq_mod mod_diff_eq [symmetric])
+  by (simp add: bitrunc_eq_mod mod_diff_eq)
 
 lemma bitrunc_nonnegative [simp]:
   fixes k :: int
@@ -279,7 +279,7 @@
 
 lemma of_int_signed [simp]:
   "of_int (signed a) = a"
-  by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod zdiff_zmod_left)
+  by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod mod_simps)
 
 
 subsubsection \<open>Properties\<close>