--- a/NEWS Sun Oct 16 09:31:05 2016 +0200
+++ b/NEWS Sun Oct 16 09:31:05 2016 +0200
@@ -270,6 +270,8 @@
minus_div_eq_mod2 ~> minus_mult_div_eq_mod
minus_mod_eq_div ~> minus_mod_eq_div_mult
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]
INCOMPATIBILITY.
* Dedicated syntax LENGTH('a) for length of types.
--- 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:05 2016 +0200
@@ -4426,7 +4426,7 @@
"n \<le> m \<longleftrightarrow> real n \<le> real m"
"n < m \<longleftrightarrow> real n < real m"
"n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
- by (simp_all add: real_div_nat_eq_floor_of_divide div_mult_mod_eq')
+ by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric])
ML_file "approximation.ML"
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200
@@ -56,7 +56,7 @@
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms div_mult_mod_eq' Suc_eq_plus1 simp_thms}
+ addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
|> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max}
(* Simp rules for changing (n::int) to int n *)
val simpset1 =
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200
@@ -31,7 +31,6 @@
@{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
-val div_mult_mod_eq' = @{thm "div_mult_mod_eq'"};
val mod_add_eq = @{thm "mod_add_eq"} RS sym;
fun prepare_for_mir q fm =
@@ -80,7 +79,7 @@
addsimps @{thms add.assoc add.commute add.left_commute}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 = put_simpset HOL_basic_ss ctxt
- addsimps [div_mult_mod_eq', @{thm Suc_eq_plus1}]
+ addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
addsimps comp_ths
|> fold Splitter.add_split
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
--- a/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200
@@ -1387,12 +1387,7 @@
qed
qed
-theorem div_mult_mod_eq' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
- using div_mult_mod_eq [of m n] by arith
-
-lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
- using div_mult_mod_eq [of m n] by arith
-(* FIXME: very similar to mult_div_cancel *)
+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
--- 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:05 2016 +0200
@@ -1416,7 +1416,7 @@
moreover note feven[unfolded feven_def]
(* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
ultimately have "P (2 * (n div 2)) kvs" by -
- thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute)
+ thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
next
case False note ge0
moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
@@ -1462,7 +1462,7 @@
moreover note geven[unfolded geven_def]
ultimately have "Q (2 * (n div 2)) kvs" by -
thus ?thesis using True
- by(metis div_mod_equality' minus_nat.diff_0 mult.commute)
+ by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute)
next
case False note ge0
moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
--- a/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 09:31:05 2016 +0200
@@ -143,7 +143,7 @@
then have "u + (w - u mod w) = w + (u - u mod w)"
by simp
then have "u + (w - u mod w) = w + u div w * w"
- by (simp add: div_mod_equality' [symmetric])
+ by (simp add: minus_mod_eq_div_mult)
}
then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)"
by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v]
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200
@@ -510,7 +510,7 @@
also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
by (simp add: algebra_simps)
finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
- qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
+ qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric])
finally show ?thesis .
qed
qed
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 09:31:05 2016 +0200
@@ -1241,8 +1241,8 @@
unfolding mod_eq_0_iff by blast
hence eq0: "(a^((n - 1) div p))^p = (n*s)^p" by simp
from qrn[symmetric] have qn1: "q dvd n - 1" unfolding dvd_def by auto
- from dvd_trans[OF p(2) qn1] div_mod_equality'[of "n - 1" p]
- have npp: "(n - 1) div p * p = n - 1" by (simp add: dvd_eq_mod_eq_0)
+ with p(2) have npp: "(n - 1) div p * p = n - 1"
+ by (auto intro: dvd_div_mult_self dvd_trans)
with eq0 have "a^ (n - 1) = (n*s)^p"
by (simp add: power_mult[symmetric])
hence "1 = (n*s)^(Suc (p - 1)) mod n" using bqn p01 by simp
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
@@ -835,7 +835,7 @@
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
val splits_ss =
simpset_of (put_simpset comp_ss @{context}
- addsimps [@{thm "div_mult_mod_eq'"}]
+ addsimps [@{thm minus_div_mult_eq_mod [symmetric]}]
|> fold Splitter.add_split
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
--- a/src/HOL/Word/Word.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Word/Word.thy Sun Oct 16 09:31:05 2016 +0200
@@ -3867,7 +3867,7 @@
apply clarsimp
apply (clarsimp simp add : nth_append size_rcat_lem)
apply (simp (no_asm_use) only: mult_Suc [symmetric]
- td_gal_lt_len less_Suc_eq_le div_mult_mod_eq')
+ td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
apply clarsimp
done