# HG changeset patch
# User haftmann
# Date 1476603066 -7200
# Node ID 15d1ee6e847beeccf9133eaab206e0aeeb9421d6
# Parent  3d00821444fcdb2ce6d0280bb6df7a8e15f77dc5
eliminated irregular aliasses

diff -r 3d00821444fc -r 15d1ee6e847b NEWS
--- a/NEWS	Sun Oct 16 09:31:05 2016 +0200
+++ b/NEWS	Sun Oct 16 09:31:06 2016 +0200
@@ -272,6 +272,11 @@
     minus_mod_eq_div2 ~> minus_mod_eq_mult_div
     div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
     mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
+    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
+    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
+    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
+    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
+    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
     div_1 ~> div_by_Suc_0
     mod_1 ~> mod_by_Suc_0
 INCOMPATIBILITY.
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -342,7 +342,7 @@
     apply (simp add: int_Idl a_r_coset_defs)
   proof -
     have "a = m * (a div m) + (a mod m)"
-      by (simp add: zmod_zdiv_equality)
+      by (simp add: mult_div_mod_eq [symmetric])
     then have "a = (a div m) * m + (a mod m)"
       by simp
     then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -534,7 +534,7 @@
     show "k = integer_of_int (int_of_integer k)" by simp
   qed
   moreover have "2 * (j div 2) = j - j mod 2"
-    by (simp add: zmult_div_cancel mult.commute)
+    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
   ultimately show ?thesis
     by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
       nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
@@ -548,7 +548,7 @@
        (l, j) = divmod_integer k 2;
        l' = 2 * int_of_integer l
      in if j = 0 then l' else l' + 1)"
-  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
+  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
 lemma integer_of_int_code [code]:
   "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
@@ -557,7 +557,7 @@
        l = 2 * integer_of_int (k div 2);
        j = k mod 2
      in if j = 0 then l else l + 1)"
-  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
+  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
 
 hide_const (open) Pos Neg sub dup divmod_abs
 
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -4408,7 +4408,7 @@
   "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j"
   "i < j \<longleftrightarrow> real_of_int i < real_of_int j"
   "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}"
-  by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality')
+  by (simp_all add: floor_divide_of_int_eq minus_div_mult_eq_mod [symmetric])
 
 lemma approximation_preproc_nat[approximation_preproc]:
   "real 0 = real_of_float 0"
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -1735,7 +1735,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
     by simp
@@ -1762,7 +1762,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
     by simp
@@ -1787,7 +1787,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
     by simp
@@ -1814,7 +1814,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
@@ -1841,7 +1841,7 @@
     by (simp add: div_self[OF cnz])
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+  then have cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
@@ -1869,7 +1869,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
     by simp
@@ -1895,7 +1895,7 @@
   have "c * (l div c) = c * (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl: "c * (l div c) = l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
+    using mult_div_mod_eq [where a="l" and b="c"] by simp
   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     by simp
@@ -1925,7 +1925,7 @@
   have "c * (l div c) = c* (l div c) + l mod c"
     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   then have cl:"c * (l div c) =l"
-    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    using mult_div_mod_eq [where a="l" and b="c"]
     by simp
   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -2419,7 +2419,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e < (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e < 0)"
@@ -2437,7 +2437,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<le> (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<le> 0)"
@@ -2455,7 +2455,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e > (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e > 0)"
@@ -2473,7 +2473,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<ge> (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<ge> 0)"
@@ -2491,7 +2491,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = 0)"
@@ -2509,7 +2509,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<noteq> (0::real)) =
           (real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e \<noteq> 0)"
@@ -2527,7 +2527,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(\<exists> (k::int). real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (real_of_int (l div c) * real_of_int j) * real_of_int k) = (\<exists> (k::int). real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (real_of_int (l div c) * real_of_int j) * real_of_int k)"  by simp
     also have "\<dots> = (\<exists> (k::int). real_of_int (l div c) * (real_of_int c * real_of_int x + Inum (real_of_int x # bs) e - real_of_int j * real_of_int k) = real_of_int (l div c)*0)" by (simp add: algebra_simps)
@@ -2544,7 +2544,7 @@
     then have ldcp:"0 < l div c"
       by (simp add: div_self[OF cnz])
     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
-    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
+    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
       by simp
     hence "(\<exists> (k::int). real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (real_of_int (l div c) * real_of_int j) * real_of_int k) = (\<exists> (k::int). real_of_int (c * (l div c)) * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (real_of_int (l div c) * real_of_int j) * real_of_int k)"  by simp
     also have "\<dots> = (\<exists> (k::int). real_of_int (l div c) * (real_of_int c * real_of_int x + Inum (real_of_int x # bs) e - real_of_int j * real_of_int k) = real_of_int (l div c)*0)" by (simp add: algebra_simps)
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -565,17 +565,6 @@
 
 begin
 
-lemma mult_div_cancel:
-  "b * (a div b) = a - a mod b"
-proof -
-  have "b * (a div b) + a mod b = a"
-    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
-  then have "b * (a div b) + a mod b - a mod b = a - a mod b"
-    by simp
-  then show ?thesis
-    by simp
-qed
-
 subclass semiring_div_parity
 proof
   fix a
@@ -617,7 +606,7 @@
     by (auto simp add: mod_w) (insert mod_less, auto)
   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   then show ?P and ?Q
     by (simp_all add: div mod add_implies_diff [symmetric])
@@ -642,7 +631,7 @@
   ultimately have "w = 0" by auto
   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
-    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
+    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
   then show ?P and ?Q
     by (simp_all add: div mod)
@@ -1120,10 +1109,6 @@
 lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
 by (induct m) (simp_all add: mod_geq)
 
-(* a simple rearrangement of div_mult_mod_eq: *)
-lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
-  using mult_div_mod_eq [of n m] by arith
-
 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   apply (drule mod_less_divisor [where m = m])
   apply simp
@@ -1329,7 +1314,7 @@
   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
-  with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
+  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
   then have A: "n * q \<le> m" by simp
   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
   then have "m < m + (n - (m mod n))" by simp
@@ -1387,8 +1372,6 @@
   qed
 qed
 
-declare minus_div_mult_eq_mod [symmetric, where ?'a = nat, nitpick_unfold]
-
 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
   apply rule
   apply (cases "b = 0")
@@ -1806,9 +1789,6 @@
   
 text\<open>Basic laws about division and remainder\<close>
 
-lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
-  by (fact mult_div_mod_eq [symmetric])
-
 lemma zdiv_int: "int (a div b) = int a div int b"
   by (simp add: divide_int_def)
 
@@ -1932,16 +1912,18 @@
 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
 
 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
+using mult_div_mod_eq [symmetric, of a b]
+using mult_div_mod_eq [symmetric, of a' b]
+apply -
 apply (rule unique_quotient_lemma)
 apply (erule subst)
 apply (erule subst, simp_all)
 done
 
 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
+using mult_div_mod_eq [symmetric, of a b]
+using mult_div_mod_eq [symmetric, of a' b]
+apply -
 apply (rule unique_quotient_lemma_neg)
 apply (erule subst)
 apply (erule subst, simp_all)
@@ -1974,9 +1956,10 @@
 lemma zdiv_mono2:
      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
 apply (subgoal_tac "b \<noteq> 0")
- prefer 2 apply arith
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
+  prefer 2 apply arith
+using mult_div_mod_eq [symmetric, of a b]
+using mult_div_mod_eq [symmetric, of a b']
+apply -
 apply (rule zdiv_mono2_lemma)
 apply (erule subst)
 apply (erule subst, simp_all)
@@ -2002,8 +1985,9 @@
 
 lemma zdiv_mono2_neg:
      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
-apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
+using mult_div_mod_eq [symmetric, of a b]
+using mult_div_mod_eq [symmetric, of a b']
+apply -
 apply (rule zdiv_mono2_neg_lemma)
 apply (erule subst)
 apply (erule subst, simp_all)
@@ -2044,10 +2028,6 @@
 (* REVISIT: should this be generalized to all semiring_div types? *)
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
-lemma zmod_zdiv_equality' [nitpick_unfold]:
-  "(m::int) mod n = m - (m div n) * n"
-  using div_mult_mod_eq [of m n] by arith
-
 
 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
 
@@ -2350,11 +2330,6 @@
 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
 done
 
-lemma zmult_div_cancel:
-  "(n::int) * (m div n) = m - (m mod n)"
-  using zmod_zdiv_equality [where a="m" and b="n"]
-  by (simp add: algebra_simps) (* FIXME: generalize *)
-
 
 subsubsection \<open>Computation of Division and Remainder\<close>
 
@@ -2690,6 +2665,8 @@
   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   by (fact dvd_eq_mod_eq_0)
 
+declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
+
 hide_fact (open) div_0 div_by_0
 
 end
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -56,7 +56,7 @@
 declare mod_mod_trivial[algebra]
 declare div_by_0[algebra]
 declare mod_by_0[algebra]
-declare zmod_zdiv_equality[symmetric,algebra]
+declare mult_div_mod_eq[algebra]
 declare div_mod_equality2[symmetric, algebra]
 declare div_minus_minus[algebra]
 declare mod_minus_minus[algebra]
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -83,7 +83,7 @@
 
 lemma sq_pow_div2 [simp]:
     "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"
-  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] mult_div_cancel)
+  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] minus_mod_eq_mult_div [symmetric])
   done
 
 end
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -1816,7 +1816,7 @@
   assumes "b > 0"
   shows "a \<ge> b * (a div b)"
 proof -
-  from zmod_zdiv_equality'[of a b] have "a = b * (a div b) + a mod b"
+  from minus_div_mult_eq_mod [symmetric, of a b] have "a = b * (a div b) + a mod b"
     by simp
   also have "\<dots> \<ge> b * (a div b) + 0"
     apply (rule add_left_mono)
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -1240,7 +1240,7 @@
       case True
       hence "length (snd (rbtreeify_f n kvs)) = 
         length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
-        by(metis minus_nat.diff_0 mult_div_cancel)
+        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
       also from "1.prems" False obtain k v kvs' 
         where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
       also have "0 < n div 2" using False by(simp) 
@@ -1260,7 +1260,7 @@
       have "length (snd (rbtreeify_g (n div 2) kvs'')) = 
         Suc (length kvs'') - n div 2" by(rule IH)
       finally show ?thesis using len[unfolded kvs''] "1.prems" True
-        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
+        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
     next
       case False
       hence "length (snd (rbtreeify_f n kvs)) = 
@@ -1303,7 +1303,7 @@
       case True
       hence "length (snd (rbtreeify_g n kvs)) =
         length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
-        by(metis minus_nat.diff_0 mult_div_cancel)
+        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
       also from "2.prems" True obtain k v kvs' 
         where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
       also have "0 < n div 2" using \<open>1 < n\<close> by(simp) 
@@ -1324,7 +1324,7 @@
       have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
         by(rule IH)
       finally show ?thesis using len[unfolded kvs''] "2.prems" True
-        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
+        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
     next
       case False
       hence "length (snd (rbtreeify_g n kvs)) = 
@@ -1431,7 +1431,7 @@
         moreover note fodd[unfolded fodd_def]
         ultimately have "P (Suc (2 * (n div 2))) kvs" by -
         thus ?thesis using False 
-          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
+          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
       qed
     qed
   next
@@ -1478,7 +1478,7 @@
         moreover note godd[unfolded godd_def]
         ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
         thus ?thesis using False 
-          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
+          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
       qed
     qed
   qed
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -51,7 +51,7 @@
   have "(x div z) * z \<le> (x div z) * z" by simp
   then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
   also have "\<dots> = x"
-    by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
+    by (auto simp add: mult_div_mod_eq ac_simps)
   also note \<open>x < y * z\<close>
   finally show ?thesis
     apply (auto simp add: mult_less_cancel_right)
@@ -73,7 +73,7 @@
 
 lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)"
 proof-
-  from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
+  from mult_div_mod_eq [symmetric] have "x = y * (x div y) + x mod y" by auto
   moreover have "0 \<le> x mod y" by (auto simp add: assms)
   ultimately show ?thesis by arith
 qed
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -236,7 +236,7 @@
    prefer 2 apply (metis zcong_sym zcong_trans zcong_zless_imp_eq)
   apply (unfold zcong_def dvd_def)
   apply (rule_tac x = "a mod m" in exI, auto)
-  apply (metis zmult_div_cancel)
+  apply (metis minus_mod_eq_mult_div [symmetric])
   done
 
 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -26,7 +26,7 @@
   also have "setsum (%x. x * a) A = setsum id B"
     by (simp add: B_def setsum.reindex [OF inj_on_xa_A])
   also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
-    by (auto simp add: StandardRes_def zmod_zdiv_equality)
+    by (auto simp add: StandardRes_def mult_div_mod_eq [symmetric])
   also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
     by (rule setsum.distrib)
   also have "setsum (StandardRes p) B = setsum id C"
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -186,7 +186,7 @@
 proof
   assume ?LHS
   then obtain x where P: "P x" ..
-  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
+  have "x mod d = x - (x div d)*d" by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq)
   hence Pmod: "P x = P(x mod d)" using modd by simp
   show ?RHS
   proof (cases)
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -16,10 +16,10 @@
 proof -
   from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
   with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
-    by (simp add: sdiv_pos_pos zmod_zdiv_equality')
+    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
 next
   from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
-    by (simp add: sdiv_pos_pos zmod_zdiv_equality' gcd_non_0_int)
+    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
 qed
 
 spark_vc procedure_g_c_d_11
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/SPARK/Manual/Example_Verification.thy
--- a/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -172,9 +172,9 @@
 just becomes \<open>c - c sdiv d * d\<close> in Isabelle. The first conclusion of
 \<open>procedure_g_c_d_4\<close> requires us to prove that the remainder of \<open>c\<close>
 and \<open>d\<close> is greater than \<open>0\<close>. To do this, we use the theorem
-\<open>zmod_zdiv_equality'\<close> describing the correspondence between \<open>div\<close>
+\<open>minus_div_mult_eq_mod [symmetric]\<close> describing the correspondence between \<open>div\<close>
 and \<open>mod\<close>
-@{thm [display] zmod_zdiv_equality'}
+@{thm [display] minus_div_mult_eq_mod [symmetric]}
 together with the theorem \<open>pos_mod_sign\<close> saying that the result of the
 \<open>mod\<close> operator is non-negative when applied to a non-negative divisor:
 @{thm [display] pos_mod_sign}
@@ -194,7 +194,7 @@
 which is the actual \emph{invariant} of the procedure. This is a consequence
 of theorem \<open>gcd_non_0_int\<close>
 @{thm [display] gcd_non_0_int}
-Again, we also need theorems \<open>zmod_zdiv_equality'\<close> and \<open>sdiv_pos_pos\<close>
+Again, we also need theorems \<open>minus_div_mult_eq_mod [symmetric]\<close> and \<open>sdiv_pos_pos\<close>
 to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
 \<open>mod\<close> operator for non-negative operands.
 The VC \<open>procedure_g_c_d_11\<close> says that if the loop invariant holds before
@@ -227,7 +227,7 @@
 numbers are non-negative by construction, the values computed by the algorithm
 are trivially proved to be non-negative. Since we are working with non-negative
 numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
-\textbf{rem}, which spares us an application of theorems \<open>zmod_zdiv_equality'\<close>
+\textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>
 and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
 we can simplify matters by placing the \textbf{assert} statement between
 \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -314,7 +314,7 @@
    apply arith
   apply (simp add: bin_last_def bin_rest_def Bit_def)
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
-         zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
+         mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
   apply auto
   done
diff -r 3d00821444fc -r 15d1ee6e847b src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:06 2016 +0200
@@ -255,7 +255,7 @@
    (x - y) mod z = (if y <= x then x - y else x - y + z)"
   by (auto intro: int_mod_eq)
 
-lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]
+lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
 lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
 
 (* already have this for naturals, div_mult_self1/2, but not for ints *)
@@ -331,7 +331,7 @@
    apply (drule mult.commute [THEN xtr1])
    apply (frule (1) td_gal_lt [THEN iffD1])
    apply (clarsimp simp: le_simps)
-   apply (rule mult_div_cancel [THEN [2] xtr4])
+   apply (rule minus_mod_eq_mult_div [symmetric, THEN [2] xtr4])
    apply (rule mult_mono)
       apply auto
   done