--- 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.
--- 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"
--- 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
--- 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"
--- 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)"
--- 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)
--- 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
--- 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]
--- 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
--- 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)
--- 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
--- 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
--- 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)"
--- 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"
--- 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)
--- 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
--- 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}.
--- 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
--- 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