eliminated irregular aliasses
authorhaftmann
Sun Oct 16 09:31:06 2016 +0200 (2016-10-16)
changeset 6424615d1ee6e847b
parent 64245 3d00821444fc
child 64247 f537616459e6
child 64261 fb3bc899fd51
eliminated irregular aliasses
NEWS
src/HOL/Algebra/IntRing.thy
src/HOL/Code_Numeral.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Hoare/Arith2.thy
src/HOL/Library/Float.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Old_Number_Theory/Int2.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Presburger.thy
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/SPARK/Manual/Example_Verification.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:06 2016 +0200
     1.3 @@ -272,6 +272,11 @@
     1.4      minus_mod_eq_div2 ~> minus_mod_eq_mult_div
     1.5      div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
     1.6      mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
     1.7 +    zmod_zdiv_equality ~> mult_div_mod_eq [symmetric]
     1.8 +    zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric]
     1.9 +    Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    1.10 +    mult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    1.11 +    zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric]
    1.12      div_1 ~> div_by_Suc_0
    1.13      mod_1 ~> mod_by_Suc_0
    1.14  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Oct 16 09:31:05 2016 +0200
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Sun Oct 16 09:31:06 2016 +0200
     2.3 @@ -342,7 +342,7 @@
     2.4      apply (simp add: int_Idl a_r_coset_defs)
     2.5    proof -
     2.6      have "a = m * (a div m) + (a mod m)"
     2.7 -      by (simp add: zmod_zdiv_equality)
     2.8 +      by (simp add: mult_div_mod_eq [symmetric])
     2.9      then have "a = (a div m) * m + (a mod m)"
    2.10        by simp
    2.11      then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
     3.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:05 2016 +0200
     3.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:06 2016 +0200
     3.3 @@ -534,7 +534,7 @@
     3.4      show "k = integer_of_int (int_of_integer k)" by simp
     3.5    qed
     3.6    moreover have "2 * (j div 2) = j - j mod 2"
     3.7 -    by (simp add: zmult_div_cancel mult.commute)
     3.8 +    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
     3.9    ultimately show ?thesis
    3.10      by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
    3.11        nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    3.12 @@ -548,7 +548,7 @@
    3.13         (l, j) = divmod_integer k 2;
    3.14         l' = 2 * int_of_integer l
    3.15       in if j = 0 then l' else l' + 1)"
    3.16 -  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
    3.17 +  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
    3.18  
    3.19  lemma integer_of_int_code [code]:
    3.20    "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
    3.21 @@ -557,7 +557,7 @@
    3.22         l = 2 * integer_of_int (k div 2);
    3.23         j = k mod 2
    3.24       in if j = 0 then l else l + 1)"
    3.25 -  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
    3.26 +  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
    3.27  
    3.28  hide_const (open) Pos Neg sub dup divmod_abs
    3.29  
     4.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:05 2016 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Oct 16 09:31:06 2016 +0200
     4.3 @@ -4408,7 +4408,7 @@
     4.4    "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j"
     4.5    "i < j \<longleftrightarrow> real_of_int i < real_of_int j"
     4.6    "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}"
     4.7 -  by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality')
     4.8 +  by (simp_all add: floor_divide_of_int_eq minus_div_mult_eq_mod [symmetric])
     4.9  
    4.10  lemma approximation_preproc_nat[approximation_preproc]:
    4.11    "real 0 = real_of_float 0"
     5.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 16 09:31:05 2016 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 16 09:31:06 2016 +0200
     5.3 @@ -1735,7 +1735,7 @@
     5.4    have "c * (l div c) = c * (l div c) + l mod c"
     5.5      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     5.6    then have cl: "c * (l div c) =l"
     5.7 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
     5.8 +    using mult_div_mod_eq [where a="l" and b="c"] by simp
     5.9    then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
    5.10        ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
    5.11      by simp
    5.12 @@ -1762,7 +1762,7 @@
    5.13    have "c * (l div c) = c * (l div c) + l mod c"
    5.14      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.15    then have cl: "c * (l div c) = l"
    5.16 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
    5.17 +    using mult_div_mod_eq [where a="l" and b="c"] by simp
    5.18    then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
    5.19        (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
    5.20      by simp
    5.21 @@ -1787,7 +1787,7 @@
    5.22    have "c * (l div c) = c * (l div c) + l mod c"
    5.23      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.24    then have cl: "c * (l div c) = l"
    5.25 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
    5.26 +    using mult_div_mod_eq [where a="l" and b="c"] by simp
    5.27    then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
    5.28        (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
    5.29      by simp
    5.30 @@ -1814,7 +1814,7 @@
    5.31    have "c * (l div c) = c * (l div c) + l mod c"
    5.32      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.33    then have cl: "c * (l div c) =l"
    5.34 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    5.35 +    using mult_div_mod_eq [where a="l" and b="c"]
    5.36      by simp
    5.37    then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
    5.38        (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
    5.39 @@ -1841,7 +1841,7 @@
    5.40      by (simp add: div_self[OF cnz])
    5.41    have "c * (l div c) = c * (l div c) + l mod c"
    5.42      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.43 -  then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    5.44 +  then have cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    5.45      by simp
    5.46    then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
    5.47        (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
    5.48 @@ -1869,7 +1869,7 @@
    5.49    have "c * (l div c) = c * (l div c) + l mod c"
    5.50      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.51    then have cl: "c * (l div c) = l"
    5.52 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
    5.53 +    using mult_div_mod_eq [where a="l" and b="c"] by simp
    5.54    then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
    5.55        (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
    5.56      by simp
    5.57 @@ -1895,7 +1895,7 @@
    5.58    have "c * (l div c) = c * (l div c) + l mod c"
    5.59      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.60    then have cl: "c * (l div c) = l"
    5.61 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
    5.62 +    using mult_div_mod_eq [where a="l" and b="c"] by simp
    5.63    then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
    5.64        (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
    5.65      by simp
    5.66 @@ -1925,7 +1925,7 @@
    5.67    have "c * (l div c) = c* (l div c) + l mod c"
    5.68      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    5.69    then have cl:"c * (l div c) =l"
    5.70 -    using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    5.71 +    using mult_div_mod_eq [where a="l" and b="c"]
    5.72      by simp
    5.73    then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
    5.74        (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
     6.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:05 2016 +0200
     6.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 16 09:31:06 2016 +0200
     6.3 @@ -2419,7 +2419,7 @@
     6.4      then have ldcp:"0 < l div c"
     6.5        by (simp add: div_self[OF cnz])
     6.6      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     6.7 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
     6.8 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
     6.9        by simp
    6.10      hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e < (0::real)) =
    6.11            (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)"
    6.12 @@ -2437,7 +2437,7 @@
    6.13      then have ldcp:"0 < l div c"
    6.14        by (simp add: div_self[OF cnz])
    6.15      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.16 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.17 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.18        by simp
    6.19      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)) =
    6.20            (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)"
    6.21 @@ -2455,7 +2455,7 @@
    6.22      then have ldcp:"0 < l div c"
    6.23        by (simp add: div_self[OF cnz])
    6.24      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.25 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.26 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.27        by simp
    6.28      hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e > (0::real)) =
    6.29            (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)"
    6.30 @@ -2473,7 +2473,7 @@
    6.31      then have ldcp:"0 < l div c"
    6.32        by (simp add: div_self[OF cnz])
    6.33      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.34 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.35 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.36        by simp
    6.37      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)) =
    6.38            (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)"
    6.39 @@ -2491,7 +2491,7 @@
    6.40      then have ldcp:"0 < l div c"
    6.41        by (simp add: div_self[OF cnz])
    6.42      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.43 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.44 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.45        by simp
    6.46      hence "(real_of_int l * real_of_int x + real_of_int (l div c) * Inum (real_of_int x # bs) e = (0::real)) =
    6.47            (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)"
    6.48 @@ -2509,7 +2509,7 @@
    6.49      then have ldcp:"0 < l div c"
    6.50        by (simp add: div_self[OF cnz])
    6.51      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.52 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.53 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.54        by simp
    6.55      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)) =
    6.56            (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)"
    6.57 @@ -2527,7 +2527,7 @@
    6.58      then have ldcp:"0 < l div c"
    6.59        by (simp add: div_self[OF cnz])
    6.60      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.61 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.62 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.63        by simp
    6.64      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
    6.65      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)
    6.66 @@ -2544,7 +2544,7 @@
    6.67      then have ldcp:"0 < l div c"
    6.68        by (simp add: div_self[OF cnz])
    6.69      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    6.70 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
    6.71 +    hence cl:"c * (l div c) =l" using mult_div_mod_eq [where a="l" and b="c"]
    6.72        by simp
    6.73      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
    6.74      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)
     7.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     7.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:06 2016 +0200
     7.3 @@ -565,17 +565,6 @@
     7.4  
     7.5  begin
     7.6  
     7.7 -lemma mult_div_cancel:
     7.8 -  "b * (a div b) = a - a mod b"
     7.9 -proof -
    7.10 -  have "b * (a div b) + a mod b = a"
    7.11 -    using div_mult_mod_eq [of a b] by (simp add: ac_simps)
    7.12 -  then have "b * (a div b) + a mod b - a mod b = a - a mod b"
    7.13 -    by simp
    7.14 -  then show ?thesis
    7.15 -    by simp
    7.16 -qed
    7.17 -
    7.18  subclass semiring_div_parity
    7.19  proof
    7.20    fix a
    7.21 @@ -617,7 +606,7 @@
    7.22      by (auto simp add: mod_w) (insert mod_less, auto)
    7.23    with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
    7.24    have "2 * (a div (2 * b)) = a div b - w"
    7.25 -    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
    7.26 +    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
    7.27    with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
    7.28    then show ?P and ?Q
    7.29      by (simp_all add: div mod add_implies_diff [symmetric])
    7.30 @@ -642,7 +631,7 @@
    7.31    ultimately have "w = 0" by auto
    7.32    with mod_w have mod: "a mod (2 * b) = a mod b" by simp
    7.33    have "2 * (a div (2 * b)) = a div b - w"
    7.34 -    by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
    7.35 +    by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
    7.36    with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
    7.37    then show ?P and ?Q
    7.38      by (simp_all add: div mod)
    7.39 @@ -1120,10 +1109,6 @@
    7.40  lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
    7.41  by (induct m) (simp_all add: mod_geq)
    7.42  
    7.43 -(* a simple rearrangement of div_mult_mod_eq: *)
    7.44 -lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
    7.45 -  using mult_div_mod_eq [of n m] by arith
    7.46 -
    7.47  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
    7.48    apply (drule mod_less_divisor [where m = m])
    7.49    apply simp
    7.50 @@ -1329,7 +1314,7 @@
    7.51    shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
    7.52  proof
    7.53    assume ?rhs
    7.54 -  with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
    7.55 +  with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
    7.56    then have A: "n * q \<le> m" by simp
    7.57    have "n - (m mod n) > 0" using mod_less_divisor assms by auto
    7.58    then have "m < m + (n - (m mod n))" by simp
    7.59 @@ -1387,8 +1372,6 @@
    7.60    qed
    7.61  qed
    7.62  
    7.63 -declare minus_div_mult_eq_mod [symmetric, where ?'a = nat, nitpick_unfold]
    7.64 -
    7.65  lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
    7.66    apply rule
    7.67    apply (cases "b = 0")
    7.68 @@ -1806,9 +1789,6 @@
    7.69    
    7.70  text\<open>Basic laws about division and remainder\<close>
    7.71  
    7.72 -lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
    7.73 -  by (fact mult_div_mod_eq [symmetric])
    7.74 -
    7.75  lemma zdiv_int: "int (a div b) = int a div int b"
    7.76    by (simp add: divide_int_def)
    7.77  
    7.78 @@ -1932,16 +1912,18 @@
    7.79  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
    7.80  
    7.81  lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
    7.82 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
    7.83 -apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
    7.84 +using mult_div_mod_eq [symmetric, of a b]
    7.85 +using mult_div_mod_eq [symmetric, of a' b]
    7.86 +apply -
    7.87  apply (rule unique_quotient_lemma)
    7.88  apply (erule subst)
    7.89  apply (erule subst, simp_all)
    7.90  done
    7.91  
    7.92  lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
    7.93 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
    7.94 -apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
    7.95 +using mult_div_mod_eq [symmetric, of a b]
    7.96 +using mult_div_mod_eq [symmetric, of a' b]
    7.97 +apply -
    7.98  apply (rule unique_quotient_lemma_neg)
    7.99  apply (erule subst)
   7.100  apply (erule subst, simp_all)
   7.101 @@ -1974,9 +1956,10 @@
   7.102  lemma zdiv_mono2:
   7.103       "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
   7.104  apply (subgoal_tac "b \<noteq> 0")
   7.105 - prefer 2 apply arith
   7.106 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
   7.107 -apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
   7.108 +  prefer 2 apply arith
   7.109 +using mult_div_mod_eq [symmetric, of a b]
   7.110 +using mult_div_mod_eq [symmetric, of a b']
   7.111 +apply -
   7.112  apply (rule zdiv_mono2_lemma)
   7.113  apply (erule subst)
   7.114  apply (erule subst, simp_all)
   7.115 @@ -2002,8 +1985,9 @@
   7.116  
   7.117  lemma zdiv_mono2_neg:
   7.118       "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
   7.119 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
   7.120 -apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
   7.121 +using mult_div_mod_eq [symmetric, of a b]
   7.122 +using mult_div_mod_eq [symmetric, of a b']
   7.123 +apply -
   7.124  apply (rule zdiv_mono2_neg_lemma)
   7.125  apply (erule subst)
   7.126  apply (erule subst, simp_all)
   7.127 @@ -2044,10 +2028,6 @@
   7.128  (* REVISIT: should this be generalized to all semiring_div types? *)
   7.129  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   7.130  
   7.131 -lemma zmod_zdiv_equality' [nitpick_unfold]:
   7.132 -  "(m::int) mod n = m - (m div n) * n"
   7.133 -  using div_mult_mod_eq [of m n] by arith
   7.134 -
   7.135  
   7.136  subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
   7.137  
   7.138 @@ -2350,11 +2330,6 @@
   7.139  apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
   7.140  done
   7.141  
   7.142 -lemma zmult_div_cancel:
   7.143 -  "(n::int) * (m div n) = m - (m mod n)"
   7.144 -  using zmod_zdiv_equality [where a="m" and b="n"]
   7.145 -  by (simp add: algebra_simps) (* FIXME: generalize *)
   7.146 -
   7.147  
   7.148  subsubsection \<open>Computation of Division and Remainder\<close>
   7.149  
   7.150 @@ -2690,6 +2665,8 @@
   7.151    "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   7.152    by (fact dvd_eq_mod_eq_0)
   7.153  
   7.154 +declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
   7.155 +
   7.156  hide_fact (open) div_0 div_by_0
   7.157  
   7.158  end
     8.1 --- a/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:05 2016 +0200
     8.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Oct 16 09:31:06 2016 +0200
     8.3 @@ -56,7 +56,7 @@
     8.4  declare mod_mod_trivial[algebra]
     8.5  declare div_by_0[algebra]
     8.6  declare mod_by_0[algebra]
     8.7 -declare zmod_zdiv_equality[symmetric,algebra]
     8.8 +declare mult_div_mod_eq[algebra]
     8.9  declare div_mod_equality2[symmetric, algebra]
    8.10  declare div_minus_minus[algebra]
    8.11  declare mod_minus_minus[algebra]
     9.1 --- a/src/HOL/Hoare/Arith2.thy	Sun Oct 16 09:31:05 2016 +0200
     9.2 +++ b/src/HOL/Hoare/Arith2.thy	Sun Oct 16 09:31:06 2016 +0200
     9.3 @@ -83,7 +83,7 @@
     9.4  
     9.5  lemma sq_pow_div2 [simp]:
     9.6      "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m"
     9.7 -  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] mult_div_cancel)
     9.8 +  apply (simp add: power2_eq_square [symmetric] power_mult [symmetric] minus_mod_eq_mult_div [symmetric])
     9.9    done
    9.10  
    9.11  end
    10.1 --- a/src/HOL/Library/Float.thy	Sun Oct 16 09:31:05 2016 +0200
    10.2 +++ b/src/HOL/Library/Float.thy	Sun Oct 16 09:31:06 2016 +0200
    10.3 @@ -1816,7 +1816,7 @@
    10.4    assumes "b > 0"
    10.5    shows "a \<ge> b * (a div b)"
    10.6  proof -
    10.7 -  from zmod_zdiv_equality'[of a b] have "a = b * (a div b) + a mod b"
    10.8 +  from minus_div_mult_eq_mod [symmetric, of a b] have "a = b * (a div b) + a mod b"
    10.9      by simp
   10.10    also have "\<dots> \<ge> b * (a div b) + 0"
   10.11      apply (rule add_left_mono)
    11.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
    11.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:06 2016 +0200
    11.3 @@ -1240,7 +1240,7 @@
    11.4        case True
    11.5        hence "length (snd (rbtreeify_f n kvs)) = 
    11.6          length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
    11.7 -        by(metis minus_nat.diff_0 mult_div_cancel)
    11.8 +        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
    11.9        also from "1.prems" False obtain k v kvs' 
   11.10          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   11.11        also have "0 < n div 2" using False by(simp) 
   11.12 @@ -1260,7 +1260,7 @@
   11.13        have "length (snd (rbtreeify_g (n div 2) kvs'')) = 
   11.14          Suc (length kvs'') - n div 2" by(rule IH)
   11.15        finally show ?thesis using len[unfolded kvs''] "1.prems" True
   11.16 -        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   11.17 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
   11.18      next
   11.19        case False
   11.20        hence "length (snd (rbtreeify_f n kvs)) = 
   11.21 @@ -1303,7 +1303,7 @@
   11.22        case True
   11.23        hence "length (snd (rbtreeify_g n kvs)) =
   11.24          length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
   11.25 -        by(metis minus_nat.diff_0 mult_div_cancel)
   11.26 +        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
   11.27        also from "2.prems" True obtain k v kvs' 
   11.28          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   11.29        also have "0 < n div 2" using \<open>1 < n\<close> by(simp) 
   11.30 @@ -1324,7 +1324,7 @@
   11.31        have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   11.32          by(rule IH)
   11.33        finally show ?thesis using len[unfolded kvs''] "2.prems" True
   11.34 -        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
   11.35 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
   11.36      next
   11.37        case False
   11.38        hence "length (snd (rbtreeify_g n kvs)) = 
   11.39 @@ -1431,7 +1431,7 @@
   11.40          moreover note fodd[unfolded fodd_def]
   11.41          ultimately have "P (Suc (2 * (n div 2))) kvs" by -
   11.42          thus ?thesis using False 
   11.43 -          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   11.44 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
   11.45        qed
   11.46      qed
   11.47    next
   11.48 @@ -1478,7 +1478,7 @@
   11.49          moreover note godd[unfolded godd_def]
   11.50          ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
   11.51          thus ?thesis using False 
   11.52 -          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
   11.53 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
   11.54        qed
   11.55      qed
   11.56    qed
    12.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Sun Oct 16 09:31:05 2016 +0200
    12.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Sun Oct 16 09:31:06 2016 +0200
    12.3 @@ -51,7 +51,7 @@
    12.4    have "(x div z) * z \<le> (x div z) * z" by simp
    12.5    then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
    12.6    also have "\<dots> = x"
    12.7 -    by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps)
    12.8 +    by (auto simp add: mult_div_mod_eq ac_simps)
    12.9    also note \<open>x < y * z\<close>
   12.10    finally show ?thesis
   12.11      apply (auto simp add: mult_less_cancel_right)
   12.12 @@ -73,7 +73,7 @@
   12.13  
   12.14  lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)"
   12.15  proof-
   12.16 -  from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
   12.17 +  from mult_div_mod_eq [symmetric] have "x = y * (x div y) + x mod y" by auto
   12.18    moreover have "0 \<le> x mod y" by (auto simp add: assms)
   12.19    ultimately show ?thesis by arith
   12.20  qed
    13.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:05 2016 +0200
    13.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Sun Oct 16 09:31:06 2016 +0200
    13.3 @@ -236,7 +236,7 @@
    13.4     prefer 2 apply (metis zcong_sym zcong_trans zcong_zless_imp_eq)
    13.5    apply (unfold zcong_def dvd_def)
    13.6    apply (rule_tac x = "a mod m" in exI, auto)
    13.7 -  apply (metis zmult_div_cancel)
    13.8 +  apply (metis minus_mod_eq_mult_div [symmetric])
    13.9    done
   13.10  
   13.11  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
    14.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:05 2016 +0200
    14.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Sun Oct 16 09:31:06 2016 +0200
    14.3 @@ -26,7 +26,7 @@
    14.4    also have "setsum (%x. x * a) A = setsum id B"
    14.5      by (simp add: B_def setsum.reindex [OF inj_on_xa_A])
    14.6    also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
    14.7 -    by (auto simp add: StandardRes_def zmod_zdiv_equality)
    14.8 +    by (auto simp add: StandardRes_def mult_div_mod_eq [symmetric])
    14.9    also have "... = setsum (%x. p * (x div p)) B + setsum (StandardRes p) B"
   14.10      by (rule setsum.distrib)
   14.11    also have "setsum (StandardRes p) B = setsum id C"
    15.1 --- a/src/HOL/Presburger.thy	Sun Oct 16 09:31:05 2016 +0200
    15.2 +++ b/src/HOL/Presburger.thy	Sun Oct 16 09:31:06 2016 +0200
    15.3 @@ -186,7 +186,7 @@
    15.4  proof
    15.5    assume ?LHS
    15.6    then obtain x where P: "P x" ..
    15.7 -  have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality ac_simps eq_diff_eq)
    15.8 +  have "x mod d = x - (x div d)*d" by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq)
    15.9    hence Pmod: "P x = P(x mod d)" using modd by simp
   15.10    show ?RHS
   15.11    proof (cases)
    16.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Oct 16 09:31:05 2016 +0200
    16.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Oct 16 09:31:06 2016 +0200
    16.3 @@ -16,10 +16,10 @@
    16.4  proof -
    16.5    from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
    16.6    with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
    16.7 -    by (simp add: sdiv_pos_pos zmod_zdiv_equality')
    16.8 +    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
    16.9  next
   16.10    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
   16.11 -    by (simp add: sdiv_pos_pos zmod_zdiv_equality' gcd_non_0_int)
   16.12 +    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
   16.13  qed
   16.14  
   16.15  spark_vc procedure_g_c_d_11
    17.1 --- a/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Oct 16 09:31:05 2016 +0200
    17.2 +++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Oct 16 09:31:06 2016 +0200
    17.3 @@ -172,9 +172,9 @@
    17.4  just becomes \<open>c - c sdiv d * d\<close> in Isabelle. The first conclusion of
    17.5  \<open>procedure_g_c_d_4\<close> requires us to prove that the remainder of \<open>c\<close>
    17.6  and \<open>d\<close> is greater than \<open>0\<close>. To do this, we use the theorem
    17.7 -\<open>zmod_zdiv_equality'\<close> describing the correspondence between \<open>div\<close>
    17.8 +\<open>minus_div_mult_eq_mod [symmetric]\<close> describing the correspondence between \<open>div\<close>
    17.9  and \<open>mod\<close>
   17.10 -@{thm [display] zmod_zdiv_equality'}
   17.11 +@{thm [display] minus_div_mult_eq_mod [symmetric]}
   17.12  together with the theorem \<open>pos_mod_sign\<close> saying that the result of the
   17.13  \<open>mod\<close> operator is non-negative when applied to a non-negative divisor:
   17.14  @{thm [display] pos_mod_sign}
   17.15 @@ -194,7 +194,7 @@
   17.16  which is the actual \emph{invariant} of the procedure. This is a consequence
   17.17  of theorem \<open>gcd_non_0_int\<close>
   17.18  @{thm [display] gcd_non_0_int}
   17.19 -Again, we also need theorems \<open>zmod_zdiv_equality'\<close> and \<open>sdiv_pos_pos\<close>
   17.20 +Again, we also need theorems \<open>minus_div_mult_eq_mod [symmetric]\<close> and \<open>sdiv_pos_pos\<close>
   17.21  to justify that \SPARK{}'s \textbf{rem} operator is equivalent to Isabelle's
   17.22  \<open>mod\<close> operator for non-negative operands.
   17.23  The VC \<open>procedure_g_c_d_11\<close> says that if the loop invariant holds before
   17.24 @@ -227,7 +227,7 @@
   17.25  numbers are non-negative by construction, the values computed by the algorithm
   17.26  are trivially proved to be non-negative. Since we are working with non-negative
   17.27  numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
   17.28 -\textbf{rem}, which spares us an application of theorems \<open>zmod_zdiv_equality'\<close>
   17.29 +\textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>
   17.30  and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
   17.31  we can simplify matters by placing the \textbf{assert} statement between
   17.32  \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
    18.1 --- a/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:05 2016 +0200
    18.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sun Oct 16 09:31:06 2016 +0200
    18.3 @@ -314,7 +314,7 @@
    18.4     apply arith
    18.5    apply (simp add: bin_last_def bin_rest_def Bit_def)
    18.6    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
    18.7 -         zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    18.8 +         mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    18.9    apply (rule trans [symmetric, OF _ emep1])
   18.10    apply auto
   18.11    done
    19.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:05 2016 +0200
    19.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 16 09:31:06 2016 +0200
    19.3 @@ -255,7 +255,7 @@
    19.4     (x - y) mod z = (if y <= x then x - y else x - y + z)"
    19.5    by (auto intro: int_mod_eq)
    19.6  
    19.7 -lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]
    19.8 +lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
    19.9  lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
   19.10  
   19.11  (* already have this for naturals, div_mult_self1/2, but not for ints *)
   19.12 @@ -331,7 +331,7 @@
   19.13     apply (drule mult.commute [THEN xtr1])
   19.14     apply (frule (1) td_gal_lt [THEN iffD1])
   19.15     apply (clarsimp simp: le_simps)
   19.16 -   apply (rule mult_div_cancel [THEN [2] xtr4])
   19.17 +   apply (rule minus_mod_eq_mult_div [symmetric, THEN [2] xtr4])
   19.18     apply (rule mult_mono)
   19.19        apply auto
   19.20    done