--- a/NEWS Sun Oct 16 18:16:49 2016 +0200
+++ b/NEWS Sun Oct 16 18:22:19 2016 +0200
@@ -249,6 +249,38 @@
*** HOL ***
+* Sligthly more standardized theorem names:
+ sgn_times ~> sgn_mult
+ sgn_mult' ~> Real_Vector_Spaces.sgn_mult
+ divide_zero_left ~> div_0
+ zero_mod_left ~> mod_0
+ divide_zero ~> div_by_0
+ divide_1 ~> div_by_1
+ nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
+ div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
+ nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
+ div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
+ is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
+ is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
+ mod_div_equality ~> div_mult_mod_eq
+ mod_div_equality2 ~> mult_div_mod_eq
+ mod_div_equality3 ~> mod_div_mult_eq
+ mod_div_equality4 ~> mod_mult_div_eq
+ minus_div_eq_mod ~> minus_div_mult_eq_mod
+ 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]
+ 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.
+
* Dedicated syntax LENGTH('a) for length of types.
* New proof method "argo" using the built-in Argo solver based on SMT
--- a/src/Doc/Tutorial/Rules/Force.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/Doc/Tutorial/Rules/Force.thy Sun Oct 16 18:22:19 2016 +0200
@@ -6,7 +6,7 @@
lemma div_mult_self_is_m:
"0<n \<Longrightarrow> (m*n) div n = (m::nat)"
-apply (insert mod_div_equality [of "m*n" n])
+apply (insert div_mult_mod_eq [of "m*n" n])
apply simp
done
--- a/src/Doc/Tutorial/Rules/Forward.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/Doc/Tutorial/Rules/Forward.thy Sun Oct 16 18:22:19 2016 +0200
@@ -183,8 +183,8 @@
Another example of "insert"
-@{thm[display] mod_div_equality}
-\rulename{mod_div_equality}
+@{thm[display] div_mult_mod_eq}
+\rulename{div_mult_mod_eq}
*}
(*MOVED to Force.thy, which now depends only on Divides.thy
--- a/src/Doc/Tutorial/Types/Numbers.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/Doc/Tutorial/Types/Numbers.thy Sun Oct 16 18:22:19 2016 +0200
@@ -86,8 +86,8 @@
@{thm[display] mod_if[no_vars]}
\rulename{mod_if}
-@{thm[display] mod_div_equality[no_vars]}
-\rulename{mod_div_equality}
+@{thm[display] div_mult_mod_eq[no_vars]}
+\rulename{div_mult_mod_eq}
@{thm[display] div_mult1_eq[no_vars]}
--- a/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 18:16:49 2016 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 18:22:19 2016 +0200
@@ -143,7 +143,7 @@
m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
\rulename{mod_if}\isanewline
m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
-\rulenamedx{mod_div_equality}
+\rulenamedx{div_mult_mod_eq}
\end{isabelle}
Many less obvious facts about quotient and remainder are also provided.
--- a/src/Doc/Tutorial/document/rules.tex Sun Oct 16 18:16:49 2016 +0200
+++ b/src/Doc/Tutorial/document/rules.tex Sun Oct 16 18:22:19 2016 +0200
@@ -2175,7 +2175,7 @@
remainder obey a well-known law:
\begin{isabelle}
(?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
-\rulename{mod_div_equality}
+\rulename{div_mult_mod_eq}
\end{isabelle}
We refer to this law explicitly in the following proof:
@@ -2183,7 +2183,7 @@
\isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
(m::nat)"\isanewline
-\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
+\isacommand{apply}\ (insert\ div_mult_mod_eq\ [of\ "m*n"\ n])\isanewline
\isacommand{apply}\ (simp)\isanewline
\isacommand{done}
\end{isabelle}
--- a/src/HOL/Algebra/IntRing.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy Sun Oct 16 18:22:19 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/Analysis/Cauchy_Integral_Theorem.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Oct 16 18:22:19 2016 +0200
@@ -5106,7 +5106,7 @@
and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
proof -
have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
- by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_divide_cancel_left eq)
+ by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Oct 16 18:22:19 2016 +0200
@@ -1315,7 +1315,7 @@
case False
then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
using Arg [of z]
- by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
+ by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
using cis_conv_exp cis_pi
by (auto simp: exp_diff algebra_simps)
@@ -1918,7 +1918,7 @@
shows "csqrt z = exp(Ln(z) / 2)"
proof -
have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
- by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
+ by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
also have "... = z"
using assms exp_Ln by blast
finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 16 18:22:19 2016 +0200
@@ -11985,7 +11985,7 @@
have "UNIV \<subseteq> {x. a \<bullet> x = b} \<Longrightarrow> a = 0 \<and> b = 0"
apply (drule_tac c = "((b+1) / (a \<bullet> a)) *\<^sub>R a" in subsetD)
apply simp_all
- by (metis add_cancel_right_right divide_1 zero_neq_one)
+ by (metis add_cancel_right_right div_by_1 zero_neq_one)
then show ?thesis by force
qed
--- a/src/HOL/Analysis/Derivative.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy Sun Oct 16 18:22:19 2016 +0200
@@ -698,7 +698,7 @@
"(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
then show ?thesis
by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
- zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
+ zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero
times_divide_eq_left)
qed
--- a/src/HOL/Analysis/Polytope.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy Sun Oct 16 18:22:19 2016 +0200
@@ -2603,7 +2603,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
have "?n * a \<le> a + x"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
also have "... < y"
by (rule 1)
finally have "?n * a < y" .
@@ -2616,7 +2616,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
have "?n * a \<le> a + y"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
also have "... < x"
by (rule 2)
finally have "?n * a < x" .
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 16 18:22:19 2016 +0200
@@ -3668,7 +3668,7 @@
apply (cases "e < 0")
apply (simp add: divide_simps)
apply (rule subset_cball)
- apply (metis divide_1 frac_le not_le order_refl zero_less_one)
+ apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
done
lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
--- a/src/HOL/Binomial.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Binomial.thy Sun Oct 16 18:22:19 2016 +0200
@@ -407,7 +407,7 @@
assumes "k \<le> n"
shows "n choose k = fact n div (fact k * fact (n - k))"
using binomial_fact_lemma [OF assms]
- by (metis fact_nonzero mult_eq_0_iff nonzero_mult_divide_cancel_left)
+ by (metis fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left)
lemma binomial_fact:
assumes kn: "k \<le> n"
--- a/src/HOL/Code_Numeral.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Oct 16 18:22:19 2016 +0200
@@ -75,6 +75,12 @@
end
+instance integer :: Rings.dvd ..
+
+lemma [transfer_rule]:
+ "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
+ unfolding dvd_def by transfer_prover
+
lemma [transfer_rule]:
"rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
by (rule transfer_rule_of_nat) transfer_prover+
@@ -528,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)
@@ -542,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))
@@ -551,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
@@ -716,6 +722,12 @@
end
+instance natural :: Rings.dvd ..
+
+lemma [transfer_rule]:
+ "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
+ unfolding dvd_def by transfer_prover
+
lemma [transfer_rule]:
"rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
proof -
--- a/src/HOL/Data_Structures/RBT_Set.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Oct 16 18:22:19 2016 +0200
@@ -419,7 +419,7 @@
next
case (2 h t t')
with RB_mod obtain n where "2*n + 1 = h"
- by (metis color.distinct(1) mod_div_equality2 parity)
+ by (metis color.distinct(1) mult_div_mod_eq parity)
with 2 balB_h RB_h show ?case by auto
next
case (3 h t t')
--- a/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 18:22:19 2016 +0200
@@ -2224,7 +2224,7 @@
proof -
have "x \<noteq> 0" using assms by auto
have "x + y = x * (1 + y / x)"
- unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF \<open>x \<noteq> 0\<close>]
+ unfolding distrib_left times_divide_eq_right nonzero_mult_div_cancel_left[OF \<open>x \<noteq> 0\<close>]
by auto
moreover
have "0 < y / x" using assms by auto
@@ -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"
@@ -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 mod_div_equality')
+ 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.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Oct 16 18:22:19 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/Ferrack.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Oct 16 18:22:19 2016 +0200
@@ -1596,7 +1596,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0"
by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
@@ -1606,7 +1606,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
@@ -1616,7 +1616,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0"
by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
@@ -1626,7 +1626,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0"
by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
@@ -1637,7 +1637,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0"
by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
next
@@ -1647,7 +1647,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0"
by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])
--- a/src/HOL/Decision_Procs/MIR.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Oct 16 18:22:19 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)
@@ -4412,7 +4412,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) < 0)"
by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) < 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4423,7 +4423,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4434,7 +4434,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) > 0)"
by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) > 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4445,7 +4445,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<ge> 0)"
by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<ge> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4457,7 +4457,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) = 0)"
by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) = 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
@@ -4469,7 +4469,7 @@
using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<noteq> 0)"
by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
- and b="0", simplified divide_zero_left]) (simp only: algebra_simps)
+ and b="0", simplified div_0]) (simp only: algebra_simps)
also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<noteq> 0)"
using np by simp
finally show ?case using nbt nb by (simp add: algebra_simps)
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Oct 16 18:22:19 2016 +0200
@@ -2704,7 +2704,7 @@
using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
- using nonzero_mult_divide_cancel_left [OF cd2] cd
+ using nonzero_mult_div_cancel_left [OF cd2] cd
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
using cd
@@ -2811,7 +2811,7 @@
using cd mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
- using nonzero_mult_divide_cancel_left[OF cd2] cd
+ using nonzero_mult_div_cancel_left[OF cd2] cd
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
using cd
@@ -2899,7 +2899,7 @@
mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
- using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
+ using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
using cd c d nc nd cd2'
@@ -2923,7 +2923,7 @@
mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
- using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
+ using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
using cd c d nc nd
@@ -2946,7 +2946,7 @@
order_less_not_sym[OF c'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
- using nonzero_mult_divide_cancel_left[OF c'] \<open>?c > 0\<close>
+ using nonzero_mult_div_cancel_left[OF c'] \<open>?c > 0\<close>
by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally show ?thesis
using cd nc nd
@@ -2969,7 +2969,7 @@
mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a*?t - 2*?c *?r < 0"
- using nonzero_mult_divide_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
+ using nonzero_mult_div_cancel_left[OF c'] cd(1) order_less_not_sym[OF c'']
less_imp_neq[OF c''] c''
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
@@ -2993,7 +2993,7 @@
order_less_not_sym[OF d'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?s+ 2 * ?d * ?r < 0"
- using nonzero_mult_divide_cancel_left[OF d'] cd(2)
+ using nonzero_mult_div_cancel_left[OF d'] cd(2)
by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally show ?thesis
using cd nc nd
@@ -3016,7 +3016,7 @@
mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a * ?s - 2 * ?d * ?r < 0"
- using nonzero_mult_divide_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
+ using nonzero_mult_div_cancel_left[OF d'] cd(2) order_less_not_sym[OF d'']
less_imp_neq[OF d''] d''
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally show ?thesis
@@ -3108,7 +3108,7 @@
mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
- using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
+ using nonzero_mult_div_cancel_left[of "2*?c*?d"] c d
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd dc'
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
@@ -3133,7 +3133,7 @@
mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
- using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
+ using nonzero_mult_div_cancel_left[of "2 * ?c * ?d"] c d
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
@@ -3157,7 +3157,7 @@
order_less_not_sym[OF c'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a*?t+ 2*?c *?r \<le> 0"
- using nonzero_mult_divide_cancel_left[OF c'] c
+ using nonzero_mult_div_cancel_left[OF c'] c
by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
@@ -3181,7 +3181,7 @@
mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
- using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
+ using nonzero_mult_div_cancel_left[OF c'] c order_less_not_sym[OF c'']
less_imp_neq[OF c''] c''
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
@@ -3206,7 +3206,7 @@
order_less_not_sym[OF d'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
- using nonzero_mult_divide_cancel_left[OF d'] d
+ using nonzero_mult_div_cancel_left[OF d'] d
by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
@@ -3230,7 +3230,7 @@
mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
by simp
also have "\<dots> \<longleftrightarrow> ?a * ?s - 2 * ?d * ?r \<le> 0"
- using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
+ using nonzero_mult_div_cancel_left[OF d'] d order_less_not_sym[OF d'']
less_imp_neq[OF d''] d''
by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 18:22:19 2016 +0200
@@ -50,13 +50,13 @@
div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0
- div_by_1 mod_by_1 div_1 mod_1
+ div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
Suc_eq_plus1}
addsimps @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
val simpset0 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms mod_div_equality' 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 18:16:49 2016 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 18:22:19 2016 +0200
@@ -25,13 +25,12 @@
@{thm of_nat_numeral},
@{thm "of_nat_Suc"}, @{thm "of_nat_1"},
@{thm "of_int_0"}, @{thm "of_nat_0"},
- @{thm "divide_zero"},
+ @{thm "div_by_0"},
@{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
val comp_ths = distinct Thm.eq_thm (ths @ comp_arith @ @{thms simp_thms});
-val mod_div_equality' = @{thm "mod_div_equality'"};
val mod_add_eq = @{thm "mod_add_eq"} RS sym;
fun prepare_for_mir q fm =
@@ -75,12 +74,12 @@
addsimps [refl, mod_add_eq,
@{thm mod_self},
@{thm div_0}, @{thm mod_0},
- @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
@{thm "Suc_eq_plus1"}]
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 [mod_div_equality', @{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 18:16:49 2016 +0200
+++ b/src/HOL/Divides.thy Sun Oct 16 18:22:19 2016 +0200
@@ -26,31 +26,19 @@
using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
qed (simp add: div_by_0)
-lemma div_by_1:
- "a div 1 = a"
- by (fact divide_1)
-
-lemma div_mult_self1_is_id:
- "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
- by (fact nonzero_mult_divide_cancel_left)
-
-lemma div_mult_self2_is_id:
- "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
- by (fact nonzero_mult_divide_cancel_right)
-
text \<open>@{const divide} and @{const modulo}\<close>
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
- by (simp add: mod_div_equality)
+ by (simp add: div_mult_mod_eq)
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
- by (simp add: mod_div_equality2)
+ by (simp add: mult_div_mod_eq)
lemma mod_by_0 [simp]: "a mod 0 = a"
- using mod_div_equality [of a zero] by simp
+ using div_mult_mod_eq [of a zero] by simp
lemma mod_0 [simp]: "0 mod a = 0"
- using mod_div_equality [of zero a] div_0 by simp
+ using div_mult_mod_eq [of zero a] div_0 by simp
lemma div_mult_self2 [simp]:
assumes "b \<noteq> 0"
@@ -73,14 +61,14 @@
next
case False
have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
- by (simp add: mod_div_equality)
+ by (simp add: div_mult_mod_eq)
also from False div_mult_self1 [of b a c] have
"\<dots> = (c + a div b) * b + (a + c * b) mod b"
by (simp add: algebra_simps)
finally have "a = a div b * b + (a + c * b) mod b"
by (simp add: add.commute [of a] add.assoc distrib_right)
then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
- by (simp add: mod_div_equality)
+ by (simp add: div_mult_mod_eq)
then show ?thesis by simp
qed
@@ -107,7 +95,7 @@
lemma mod_by_1 [simp]:
"a mod 1 = 0"
proof -
- from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
+ from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
then have "a + a mod 1 = a + 0" by simp
then show ?thesis by (rule add_left_imp_eq)
qed
@@ -150,7 +138,7 @@
then show "a mod b = 0" by simp
next
assume "a mod b = 0"
- with mod_div_equality [of a b] have "a div b * b = a" by simp
+ with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
then have "a = b * (a div b)" by (simp add: ac_simps)
then show "b dvd a" ..
qed
@@ -169,7 +157,7 @@
hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
by (rule div_mult_self1 [symmetric])
also have "\<dots> = a div b"
- by (simp only: mod_div_equality3)
+ by (simp only: mod_div_mult_eq)
also have "\<dots> = a div b + 0"
by simp
finally show ?thesis
@@ -182,7 +170,7 @@
have "a mod b mod b = (a mod b + a div b * b) mod b"
by (simp only: mod_mult_self1)
also have "\<dots> = a mod b"
- by (simp only: mod_div_equality3)
+ by (simp only: mod_div_mult_eq)
finally show ?thesis .
qed
@@ -192,7 +180,7 @@
proof -
from assms have "k dvd (m div n) * n + m mod n"
by (simp only: dvd_add dvd_mult)
- then show ?thesis by (simp add: mod_div_equality)
+ then show ?thesis by (simp add: div_mult_mod_eq)
qed
text \<open>Addition respects modular equivalence.\<close>
@@ -201,7 +189,7 @@
"(a + b) mod c = (a mod c + b) mod c"
proof -
have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
also have "\<dots> = (a mod c + b + a div c * c) mod c"
by (simp only: ac_simps)
also have "\<dots> = (a mod c + b) mod c"
@@ -213,7 +201,7 @@
"(a + b) mod c = (a + b mod c) mod c"
proof -
have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
also have "\<dots> = (a + b mod c + b div c * c) mod c"
by (simp only: ac_simps)
also have "\<dots> = (a + b mod c) mod c"
@@ -242,7 +230,7 @@
"(a * b) mod c = ((a mod c) * b) mod c"
proof -
have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
by (simp only: algebra_simps)
also have "\<dots> = (a mod c * b) mod c"
@@ -254,7 +242,7 @@
"(a * b) mod c = (a * (b mod c)) mod c"
proof -
have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
by (simp only: algebra_simps)
also have "\<dots> = (a * (b mod c)) mod c"
@@ -299,7 +287,7 @@
also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
by (simp only: ac_simps)
also have "\<dots> = a mod c"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
finally show ?thesis .
qed
@@ -317,11 +305,11 @@
case True then show ?thesis by simp
next
case False
- from mod_div_equality
+ from div_mult_mod_eq
have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
= c * a + c * (a mod b)" by (simp add: algebra_simps)
- with mod_div_equality show ?thesis by simp
+ with div_mult_mod_eq show ?thesis by simp
qed
lemma mod_mult_mult2:
@@ -369,7 +357,7 @@
lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
proof -
have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
- by (simp only: mod_div_equality)
+ by (simp only: div_mult_mod_eq)
also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
by (simp add: ac_simps)
also have "\<dots> = (- (a mod b)) mod b"
@@ -412,7 +400,7 @@
apply (auto simp add: dvd_def)
apply (subgoal_tac "-(y * k) = y * - k")
apply (simp only:)
- apply (erule div_mult_self1_is_id)
+ apply (erule nonzero_mult_div_cancel_left)
apply simp
done
@@ -420,7 +408,7 @@
apply (case_tac "y = 0") apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst, rule div_mult_self1_is_id)
+ apply (erule ssubst, rule nonzero_mult_div_cancel_left)
apply simp
apply simp
done
@@ -479,7 +467,7 @@
case True then show ?thesis by simp
next
case False
- from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
+ from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
then have "1 div 2 = 0 \<or> 2 = 0" by simp
@@ -514,7 +502,7 @@
next
fix a
assume "a mod 2 = 1"
- then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
+ then have "a = a div 2 * 2 + 1" using div_mult_mod_eq [of a 2] by simp
then show "\<exists>b. a = b + 1" ..
qed
@@ -540,7 +528,7 @@
lemma odd_two_times_div_two_succ [simp]:
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
- using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+ using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
end
@@ -577,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 mod_div_equality [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
@@ -629,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])
@@ -654,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)
@@ -1119,7 +1096,7 @@
fixes m n :: nat
shows "m mod n \<le> m"
proof (rule add_leD2)
- from mod_div_equality have "m div n * n + m mod n = m" .
+ from div_mult_mod_eq have "m div n * n + m mod n = m" .
then show "m div n * n + m mod n \<le> m" by auto
qed
@@ -1129,13 +1106,9 @@
lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
by (simp add: le_mod_geq)
-lemma mod_1 [simp]: "m mod Suc 0 = 0"
+lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
by (induct m) (simp_all add: mod_geq)
-(* a simple rearrangement of mod_div_equality: *)
-lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
- using mod_div_equality2 [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
@@ -1208,7 +1181,7 @@
subsubsection \<open>Further Facts about Quotient and Remainder\<close>
-lemma div_1 [simp]:
+lemma div_by_Suc_0 [simp]:
"m div Suc 0 = m"
using div_by_1 [of m] by simp
@@ -1291,7 +1264,7 @@
assumes "m mod d = r"
shows "\<exists>q. m = r + q * d"
proof -
- from mod_div_equality obtain q where "q * d + m mod d = m" by blast
+ from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
with assms have "m = r + q * d" by simp
then show ?thesis ..
qed
@@ -1341,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
@@ -1399,13 +1372,6 @@
qed
qed
-theorem mod_div_equality' [nitpick_unfold]: "(m::nat) mod n = m - (m div n) * n"
- using mod_div_equality [of m n] by arith
-
-lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
- using mod_div_equality [of m n] by arith
-(* FIXME: very similar to mult_div_cancel *)
-
lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
apply rule
apply (cases "b = 0")
@@ -1817,15 +1783,12 @@
by (cases "0::int" k rule: linorder_cases) simp_all
then show "is_unit (unit_factor k)"
by simp
-qed (simp_all add: sgn_times mult_sgn_abs)
+qed (simp_all add: sgn_mult mult_sgn_abs)
end
text\<open>Basic laws about division and remainder\<close>
-lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
- by (fact mod_div_equality2 [symmetric])
-
lemma zdiv_int: "int (a div b) = int a div int b"
by (simp add: divide_int_def)
@@ -1949,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)
@@ -1991,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)
@@ -2019,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)
@@ -2061,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 mod_div_equality [of m n] by arith
-
subsubsection \<open>Proving @{term "a div (b * c) = (a div b) div c"}\<close>
@@ -2219,8 +2182,6 @@
shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
using assms unfolding divmod_int_rel_def by auto
-declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
-
lemma neg_divmod_int_rel_mult_2:
assumes "b \<le> 0"
assumes "divmod_int_rel (a + 1) b (q, r)"
@@ -2296,7 +2257,7 @@
shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
proof -
have "i mod k = i \<longleftrightarrow> i div k = 0"
- by safe (insert mod_div_equality [of i k], auto)
+ by safe (insert div_mult_mod_eq [of i k], auto)
with zdiv_eq_0_iff
show ?thesis
by simp
@@ -2369,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>
@@ -2709,4 +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/GCD.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/GCD.thy Sun Oct 16 18:22:19 2016 +0200
@@ -356,7 +356,7 @@
then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
by (simp_all add: normalize_mult)
with \<open>lcm a b \<noteq> 0\<close> show ?thesis
- using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
+ using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
qed
lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
@@ -1920,7 +1920,7 @@
apply (simp add: bezw_non_0 gcd_non_0_nat)
apply (erule subst)
apply (simp add: field_simps)
- apply (subst mod_div_equality [of m n, symmetric])
+ apply (subst div_mult_mod_eq [of m n, symmetric])
(* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
done
--- a/src/HOL/Groebner_Basis.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Groebner_Basis.thy Sun Oct 16 18:22:19 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 18:16:49 2016 +0200
+++ b/src/HOL/Hoare/Arith2.thy Sun Oct 16 18:22:19 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/Hoare_Parallel/OG_Examples.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 16 18:22:19 2016 +0200
@@ -347,10 +347,10 @@
lemma mod_lemma: "\<lbrakk> (c::nat) \<le> a; a < b; b - c < n \<rbrakk> \<Longrightarrow> b mod n \<noteq> a mod n"
apply(subgoal_tac "b=b div n*n + b mod n" )
- prefer 2 apply (simp add: mod_div_equality [symmetric])
+ prefer 2 apply (simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "a=a div n*n + a mod n")
prefer 2
- apply(simp add: mod_div_equality [symmetric])
+ apply(simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "b - a \<le> b - c")
prefer 2 apply arith
apply(drule le_less_trans)
--- a/src/HOL/Library/Code_Target_Int.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy Sun Oct 16 18:22:19 2016 +0200
@@ -115,7 +115,7 @@
j = k mod 2
in if j = 0 then l else l + 1)"
proof -
- from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
+ from div_mult_mod_eq have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
show ?thesis
by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
qed
--- a/src/HOL/Library/Code_Target_Nat.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Sun Oct 16 18:22:19 2016 +0200
@@ -115,7 +115,7 @@
m' = 2 * of_nat m
in if q = 0 then m' else m' + 1)"
proof -
- from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
+ from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
show ?thesis
by (simp add: Let_def divmod_nat_div_mod of_nat_add [symmetric])
(simp add: * mult.commute of_nat_mult add.commute)
--- a/src/HOL/Library/Float.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Float.thy Sun Oct 16 18:22:19 2016 +0200
@@ -590,7 +590,7 @@
qualified lemma compute_float_sgn[code]:
"sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
- by transfer (simp add: sgn_times)
+ by transfer (simp add: sgn_mult)
lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
@@ -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/Formal_Power_Series.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sun Oct 16 18:22:19 2016 +0200
@@ -1302,13 +1302,13 @@
proof (cases "f div g * g = 0")
assume "f div g * g \<noteq> 0"
hence [simp]: "f div g \<noteq> 0" "g \<noteq> 0" by auto
- from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
+ from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
also from assms have "subdegree ... = subdegree f"
by (intro subdegree_diff_eq1) simp_all
finally show ?thesis .
next
assume zero: "f div g * g = 0"
- from mod_div_equality[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
+ from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
also note zero
finally show ?thesis by simp
qed
@@ -3013,7 +3013,7 @@
*)
lemma fps_divide_1 [simp]: "(a :: 'a::field fps) / 1 = a"
- by (fact divide_1)
+ by (fact div_by_1)
lemma radical_divide:
fixes a :: "'a::field_char_0 fps"
--- a/src/HOL/Library/Normalized_Fraction.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Normalized_Fraction.thy Sun Oct 16 18:22:19 2016 +0200
@@ -10,7 +10,7 @@
apply (auto simp add: dvd_def)
apply (subgoal_tac "-(y * k) = y * - k")
apply (simp only:)
-apply (erule nonzero_mult_divide_cancel_left)
+apply (erule nonzero_mult_div_cancel_left)
apply simp
done
--- a/src/HOL/Library/Polynomial_FPS.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Sun Oct 16 18:22:19 2016 +0200
@@ -100,7 +100,7 @@
also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q"
by (simp add: fps_of_poly_mult)
also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)"
- by (intro div_mult_self2_is_id) (auto simp: fps_of_poly_0)
+ by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0)
finally show ?thesis ..
qed simp
--- a/src/HOL/Library/Polynomial_Factorial.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Sun Oct 16 18:22:19 2016 +0200
@@ -331,7 +331,7 @@
from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
moreover {
have "smult c q = [:c:] * q" by simp
- also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
+ also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
finally have "smult c q div [:c:] = q" .
}
ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
@@ -1038,7 +1038,7 @@
thus "is_unit (unit_factor_field_poly p)"
by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult
- euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
+ euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
lemma field_poly_irreducible_imp_prime:
assumes "irreducible (p :: 'a :: field poly)"
@@ -1356,7 +1356,7 @@
"euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
instance
- by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
+ by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
end
--- a/src/HOL/Library/RBT_Impl.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Sun Oct 16 18:22:19 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)) =
@@ -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
@@ -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
@@ -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
@@ -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/Library/Stirling.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Stirling.thy Sun Oct 16 18:22:19 2016 +0200
@@ -108,7 +108,7 @@
using Suc.hyps[OF geq1]
by (simp only: stirling_Suc_n_1 of_nat_fact of_nat_add of_nat_mult)
also have "\<dots> = Suc n * (\<Sum>k=1..n. fact n div k) + Suc n * fact n div Suc n"
- by (metis nat.distinct(1) nonzero_mult_divide_cancel_left)
+ by (metis nat.distinct(1) nonzero_mult_div_cancel_left)
also have "\<dots> = (\<Sum>k=1..n. fact (Suc n) div k) + fact (Suc n) div Suc n"
by (simp add: setsum_distrib_left div_mult_swap dvd_fact)
also have "\<dots> = (\<Sum>k=1..Suc n. fact (Suc n) div k)"
--- a/src/HOL/Library/Stream.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Library/Stream.thy Sun Oct 16 18:22:19 2016 +0200
@@ -336,7 +336,7 @@
lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
- by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
+ by (subst div_mult_mod_eq[of n "length u", symmetric], unfold stake_add[symmetric]) auto
lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Sun Oct 16 18:22:19 2016 +0200
@@ -147,7 +147,7 @@
apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
apply (drule_tac c = "xa - star_of x" in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
- simp add: mult.assoc nonzero_mult_divide_cancel_right)
+ simp add: mult.assoc nonzero_mult_div_cancel_right)
apply (drule_tac x3=D in
HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult,
THEN mem_infmal_iff [THEN iffD1]])
@@ -417,7 +417,7 @@
have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow>
( *f* g) w * (w - star_of x) / (w - star_of x) \<approx>
star_of (g x)"
- by (simp add: isNSCont_def nonzero_mult_divide_cancel_right)
+ by (simp add: isNSCont_def nonzero_mult_div_cancel_right)
thus ?thesis using all
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
qed
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 16 18:22:19 2016 +0200
@@ -863,7 +863,7 @@
by (intro_classes; transfer) simp_all
instance star :: (semiring_div) semiring_div
- by (intro_classes; transfer) (simp_all add: mod_div_equality)
+ by (intro_classes; transfer) (simp_all add: div_mult_mod_eq)
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
--- a/src/HOL/Num.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Num.thy Sun Oct 16 18:22:19 2016 +0200
@@ -1217,7 +1217,7 @@
K (
Lin_Arith.add_simps
@{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
- arith_special numeral_One of_nat_simps}
+ arith_special numeral_One of_nat_simps uminus_numeral_One}
#> Lin_Arith.add_simps
@{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
--- a/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Sun Oct 16 18:22:19 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 18:16:49 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 18:22:19 2016 +0200
@@ -26,8 +26,8 @@
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
begin
-lemma zero_mod_left [simp]: "0 mod a = 0"
- using mod_div_equality [of 0 a] by simp
+lemma mod_0 [simp]: "0 mod a = 0"
+ using div_mult_mod_eq [of 0 a] by simp
lemma dvd_mod_iff:
assumes "k dvd n"
@@ -36,7 +36,7 @@
from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
by (simp add: dvd_add_right_iff)
also have "(m div n) * n + m mod n = m"
- using mod_div_equality [of m n] by simp
+ using div_mult_mod_eq [of m n] by simp
finally show ?thesis .
qed
@@ -46,7 +46,7 @@
proof -
have "b dvd ((a div b) * b)" by simp
also have "(a div b) * b = a"
- using mod_div_equality [of a b] by (simp add: assms)
+ using div_mult_mod_eq [of a b] by (simp add: assms)
finally show ?thesis .
qed
@@ -72,7 +72,7 @@
obtains s and t where "a = s * b + t"
and "euclidean_size t < euclidean_size b"
proof -
- from mod_div_equality [of a b]
+ from div_mult_mod_eq [of a b]
have "a = a div b * b + a mod b" by simp
with that and assms show ?thesis by (auto simp add: mod_size_less)
qed
@@ -507,10 +507,10 @@
(s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
also have "s' * a + t' * b = r'" by fact
also have "s * a + t * b = r" by fact
- also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
+ 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/Number_Theory/Gauss.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Sun Oct 16 18:22:19 2016 +0200
@@ -52,7 +52,7 @@
qed
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
- using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]
+ using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"]
by simp
lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
--- a/src/HOL/Number_Theory/Pocklington.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Sun Oct 16 18:22:19 2016 +0200
@@ -227,7 +227,7 @@
{assume nm1: "(n - 1) mod m > 0"
from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
let ?y = "a^ ((n - 1) div m * m)"
- note mdeq = mod_div_equality[of "(n - 1)" m]
+ note mdeq = div_mult_mod_eq[of "(n - 1)" m]
have yn: "coprime ?y n"
by (metis an(1) coprime_exp gcd.commute)
have "?y mod n = (a^m)^((n - 1) div m) mod n"
@@ -239,7 +239,7 @@
finally have th3: "?y mod n = 1" .
have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
using an1[unfolded cong_nat_def onen] onen
- mod_div_equality[of "(n - 1)" m, symmetric]
+ div_mult_mod_eq[of "(n - 1)" m, symmetric]
by (simp add:power_add[symmetric] cong_nat_def th3 del: One_nat_def)
have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)"
by (metis cong_mult_rcancel_nat mult.commute th2 yn)
@@ -362,7 +362,7 @@
by (metis cong_exp_nat ord power_one)
from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
hence op: "?o > 0" by simp
- from mod_div_equality[of d "ord n a"] lh
+ from div_mult_mod_eq[of d "ord n a"] lh
have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: cong_nat_def mult.commute)
hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
by (simp add: cong_nat_def power_mult[symmetric] power_add[symmetric])
@@ -618,7 +618,7 @@
{assume b0: "b = 0"
from p(2) nqr have "(n - 1) mod p = 0"
by (metis mod_0 mod_mod_cancel mod_mult_self1_is_0)
- with mod_div_equality[of "n - 1" p]
+ with div_mult_mod_eq[of "n - 1" p]
have "(n - 1) div p * p= n - 1" by auto
hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
by (simp only: power_mult[symmetric])
@@ -720,7 +720,7 @@
unfolding arnb[symmetric] power_mod
by (simp_all add: power_mult[symmetric] algebra_simps)
from n have n0: "n > 0" by arith
- from mod_div_equality[of "a^(n - 1)" n]
+ from div_mult_mod_eq[of "a^(n - 1)" n]
mod_less_divisor[OF n0, of "a^(n - 1)"]
have an1: "[a ^ (n - 1) = 1] (mod n)"
by (metis bqn cong_nat_def mod_mod_trivial)
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Oct 16 18:22:19 2016 +0200
@@ -14,6 +14,13 @@
definition zEven :: "int set"
where "zEven = {x. \<exists>k. x = 2 * k}"
+lemma in_zEven_zOdd_iff:
+ fixes k :: int
+ shows "k \<in> zEven \<longleftrightarrow> even k"
+ and "k \<in> zOdd \<longleftrightarrow> odd k"
+ by (auto simp add: zEven_def zOdd_def elim: evenE oddE)
+
+
subsection \<open>Some useful properties about even and odd\<close>
lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
--- a/src/HOL/Old_Number_Theory/Gauss.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Sun Oct 16 18:22:19 2016 +0200
@@ -46,16 +46,11 @@
qed
lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
- using div_mult_self1_is_id [of 2 "p - 1"] by auto
+ using nonzero_mult_div_cancel_left [of 2 "p - 1"] by auto
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
- apply (frule odd_minus_one_even)
- apply (simp add: zEven_def)
- apply (subgoal_tac "2 \<noteq> 0")
- apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
- apply (auto simp add: even_div_2_prop2)
- done
+ by (simp add: in_zEven_zOdd_iff)
lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
--- a/src/HOL/Old_Number_Theory/Int2.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy Sun Oct 16 18:22:19 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 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Sun Oct 16 18:22:19 2016 +0200
@@ -227,7 +227,7 @@
lemma zcong_zless_0:
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
apply (unfold zcong_def dvd_def, auto)
- apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id)
+ apply (metis div_pos_pos_trivial linorder_not_less nonzero_mult_div_cancel_left)
done
lemma zcong_zless_unique:
@@ -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/Pocklington.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Sun Oct 16 18:22:19 2016 +0200
@@ -744,7 +744,7 @@
{assume nm1: "(n - 1) mod m > 0"
from mod_less_divisor[OF m(1)] have th0:"(n - 1) mod m < m" by blast
let ?y = "a^ ((n - 1) div m * m)"
- note mdeq = mod_div_equality[of "(n - 1)" m]
+ note mdeq = div_mult_mod_eq[of "(n - 1)" m]
from coprime_exp[OF an(1)[unfolded coprime_commute[of a n]],
of "(n - 1) div m * m"]
have yn: "coprime ?y n" by (simp add: coprime_commute)
@@ -757,7 +757,7 @@
finally have th3: "?y mod n = 1" .
have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)"
using an1[unfolded modeq_def onen] onen
- mod_div_equality[of "(n - 1)" m, symmetric]
+ div_mult_mod_eq[of "(n - 1)" m, symmetric]
by (simp add:power_add[symmetric] modeq_def th3 del: One_nat_def)
from cong_mult_lcancel[of ?y n "a^((n - 1) mod m)" 1, OF yn th2]
have th1: "[a ^ ((n - 1) mod m) = 1] (mod n)" .
@@ -855,7 +855,7 @@
have eqo: "[(a^?o)^?q = 1] (mod n)" by (simp add: modeq_def power_Suc0)
from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
hence op: "?o > 0" by simp
- from mod_div_equality[of d "ord n a"] lh
+ from div_mult_mod_eq[of d "ord n a"] lh
have "[a^(?o*?q + ?r) = 1] (mod n)" by (simp add: modeq_def mult.commute)
hence "[(a^?o)^?q * (a^?r) = 1] (mod n)"
by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
@@ -1108,7 +1108,7 @@
{assume b0: "b = 0"
from p(2) nqr have "(n - 1) mod p = 0"
apply (simp only: dvd_eq_mod_eq_0[symmetric]) by (rule dvd_mult2, simp)
- with mod_div_equality[of "n - 1" p]
+ with div_mult_mod_eq[of "n - 1" p]
have "(n - 1) div p * p= n - 1" by auto
hence eq: "(a^((n - 1) div p))^p = a^(n - 1)"
by (simp only: power_mult[symmetric])
@@ -1196,7 +1196,7 @@
lemma mod_le: assumes n: "n \<noteq> (0::nat)" shows "m mod n \<le> m"
proof-
- from mod_div_equality[of m n]
+ from div_mult_mod_eq[of m n]
have "\<exists>x. x + m mod n = m" by blast
then show ?thesis by auto
qed
@@ -1214,7 +1214,7 @@
and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps" unfolding arnb[symmetric] power_mod
by (simp_all add: power_mult[symmetric] algebra_simps)
from n have n0: "n > 0" by arith
- from mod_div_equality[of "a^(n - 1)" n]
+ from div_mult_mod_eq[of "a^(n - 1)" n]
mod_less_divisor[OF n0, of "a^(n - 1)"]
have an1: "[a ^ (n - 1) = 1] (mod n)"
unfolding nat_mod bqn
@@ -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/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Oct 16 18:22:19 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"
@@ -315,7 +315,7 @@
by (rule zdiv_mono1) (insert p_g_2, auto)
then show "b \<le> (q * a) div p"
apply (subgoal_tac "p \<noteq> 0")
- apply (frule div_mult_self1_is_id, force)
+ apply (frule nonzero_mult_div_cancel_left, force)
apply (insert p_g_2, auto)
done
qed
@@ -349,7 +349,7 @@
by (rule zdiv_mono1) (insert q_g_2, auto)
then show "a \<le> (p * b) div q"
apply (subgoal_tac "q \<noteq> 0")
- apply (frule div_mult_self1_is_id, force)
+ apply (frule nonzero_mult_div_cancel_left, force)
apply (insert q_g_2, auto)
done
qed
--- a/src/HOL/Presburger.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Presburger.thy Sun Oct 16 18:22:19 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)
@@ -411,7 +411,7 @@
\<close> "Cooper's algorithm for Presburger arithmetic"
declare dvd_eq_mod_eq_0 [symmetric, presburger]
-declare mod_1 [presburger]
+declare mod_by_Suc_0 [presburger]
declare mod_0 [presburger]
declare mod_by_1 [presburger]
declare mod_self [presburger]
@@ -420,8 +420,8 @@
declare mod_div_trivial [presburger]
declare div_mod_equality2 [presburger]
declare div_mod_equality [presburger]
-declare mod_div_equality2 [presburger]
-declare mod_div_equality [presburger]
+declare mult_div_mod_eq [presburger]
+declare div_mult_mod_eq [presburger]
declare mod_mult_self1 [presburger]
declare mod_mult_self2 [presburger]
declare mod2_Suc_Suc[presburger]
--- a/src/HOL/Probability/SPMF.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Sun Oct 16 18:22:19 2016 +0200
@@ -2363,7 +2363,7 @@
apply(cases "weight_spmf p > 0")
apply(auto simp add: scale_scale_spmf min_def max_def field_simps not_le weight_spmf_lt_0 weight_spmf_eq_0 not_less weight_spmf_le_0)
apply(subgoal_tac "1 = r'")
- apply (metis (no_types) divide_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
+ apply (metis (no_types) div_by_1 eq_iff measure_spmf.subprob_measure_le_1 mult.commute mult_cancel_right1)
apply(meson eq_iff le_divide_eq_1_pos measure_spmf.subprob_measure_le_1 mult_imp_div_pos_le order.trans)
done
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Sun Oct 16 18:22:19 2016 +0200
@@ -258,7 +258,7 @@
fix a b :: int
assume "b \<noteq> 0"
then have "a * b \<le> (a div b + 1) * b * b"
- by (metis mult.commute div_mult_self1_is_id less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
+ by (metis mult.commute nonzero_mult_div_cancel_left less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
then show "\<exists>z::int. a * b \<le> z * b * b" by auto
qed
qed
--- a/src/HOL/Rat.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Rat.thy Sun Oct 16 18:22:19 2016 +0200
@@ -295,10 +295,10 @@
(q * gcd r s) * (sgn (q * s) * r * gcd p q)"
by simp
with assms show ?thesis
- by (auto simp add: ac_simps sgn_times sgn_0_0)
+ by (auto simp add: ac_simps sgn_mult sgn_0_0)
qed
from assms show ?thesis
- by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times
+ by (auto simp: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_mult
split: if_splits intro: *)
qed
@@ -651,7 +651,7 @@
@{thm True_implies_equals},
@{thm distrib_left [where a = "numeral v" for v]},
@{thm distrib_left [where a = "- numeral v" for v]},
- @{thm divide_1}, @{thm divide_zero_left},
+ @{thm div_by_1}, @{thm div_0},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
@{thm add_divide_distrib}, @{thm diff_divide_distrib},
--- a/src/HOL/Real_Vector_Spaces.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Oct 16 18:22:19 2016 +0200
@@ -1325,6 +1325,8 @@
for x y :: "'a::real_normed_div_algebra"
by (simp add: sgn_div_norm norm_mult mult.commute)
+hide_fact (open) sgn_mult
+
lemma real_sgn_eq: "sgn x = x / \<bar>x\<bar>"
for x :: real
by (simp add: sgn_div_norm divide_inverse)
--- a/src/HOL/Rings.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Rings.thy Sun Oct 16 18:22:19 2016 +0200
@@ -574,12 +574,12 @@
text \<open>Algebraic classes with division\<close>
class semidom_divide = semidom + divide +
- assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
- assumes divide_zero [simp]: "a div 0 = 0"
+ assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
+ assumes div_by_0 [simp]: "a div 0 = 0"
begin
-lemma nonzero_mult_divide_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
- using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
+ using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)
subclass semiring_no_zero_divisors_cancel
proof
@@ -603,21 +603,21 @@
qed
lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
- using nonzero_mult_divide_cancel_left [of a 1] by simp
+ using nonzero_mult_div_cancel_left [of a 1] by simp
-lemma divide_zero_left [simp]: "0 div a = 0"
+lemma div_0 [simp]: "0 div a = 0"
proof (cases "a = 0")
case True
then show ?thesis by simp
next
case False
then have "a * 0 div a = 0"
- by (rule nonzero_mult_divide_cancel_left)
+ by (rule nonzero_mult_div_cancel_left)
then show ?thesis by simp
qed
-lemma divide_1 [simp]: "a div 1 = a"
- using nonzero_mult_divide_cancel_left [of 1 a] by simp
+lemma div_by_1 [simp]: "a div 1 = a"
+ using nonzero_mult_div_cancel_left [of 1 a] by simp
end
@@ -952,7 +952,7 @@
unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
unit_eq_div1 unit_eq_div2
-lemma is_unit_divide_mult_cancel_left:
+lemma is_unit_div_mult_cancel_left:
assumes "a \<noteq> 0" and "is_unit b"
shows "a div (a * b) = 1 div b"
proof -
@@ -961,10 +961,10 @@
with assms show ?thesis by simp
qed
-lemma is_unit_divide_mult_cancel_right:
+lemma is_unit_div_mult_cancel_right:
assumes "a \<noteq> 0" and "is_unit b"
shows "a div (b * a) = 1 div b"
- using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
+ using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
end
@@ -1058,7 +1058,7 @@
next
case False
then have "normalize a \<noteq> 0" by simp
- with nonzero_mult_divide_cancel_right
+ with nonzero_mult_div_cancel_right
have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
then show ?thesis by simp
qed
@@ -1070,7 +1070,7 @@
next
case False
then have "unit_factor a \<noteq> 0" by simp
- with nonzero_mult_divide_cancel_left
+ with nonzero_mult_div_cancel_left
have "unit_factor a * normalize a div unit_factor a = normalize a"
by blast
then show ?thesis by simp
@@ -1085,7 +1085,7 @@
have "normalize a div a = normalize a div (unit_factor a * normalize a)"
by simp
also have "\<dots> = 1 div unit_factor a"
- using False by (subst is_unit_divide_mult_cancel_right) simp_all
+ using False by (subst is_unit_div_mult_cancel_right) simp_all
finally show ?thesis .
qed
@@ -1290,7 +1290,7 @@
text \<open>Arbitrary quotient and remainder partitions\<close>
class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
- assumes mod_div_equality: "a div b * b + a mod b = a"
+ assumes div_mult_mod_eq: "a div b * b + a mod b = a"
begin
lemma mod_div_decomp:
@@ -1298,35 +1298,35 @@
obtains q r where "q = a div b" and "r = a mod b"
and "a = q * b + r"
proof -
- from mod_div_equality have "a = a div b * b + a mod b" by simp
+ from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
moreover have "a div b = a div b" ..
moreover have "a mod b = a mod b" ..
note that ultimately show thesis by blast
qed
-lemma mod_div_equality2: "b * (a div b) + a mod b = a"
- using mod_div_equality [of a b] by (simp add: ac_simps)
+lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
+ using div_mult_mod_eq [of a b] by (simp add: ac_simps)
-lemma mod_div_equality3: "a mod b + a div b * b = a"
- using mod_div_equality [of a b] by (simp add: ac_simps)
+lemma mod_div_mult_eq: "a mod b + a div b * b = a"
+ using div_mult_mod_eq [of a b] by (simp add: ac_simps)
-lemma mod_div_equality4: "a mod b + b * (a div b) = a"
- using mod_div_equality [of a b] by (simp add: ac_simps)
+lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
+ using div_mult_mod_eq [of a b] by (simp add: ac_simps)
-lemma minus_div_eq_mod: "a - a div b * b = a mod b"
- by (rule add_implies_diff [symmetric]) (fact mod_div_equality3)
+lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
+ by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)
-lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b"
- by (rule add_implies_diff [symmetric]) (fact mod_div_equality4)
+lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
+ by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)
-lemma minus_mod_eq_div: "a - a mod b = a div b * b"
- by (rule add_implies_diff [symmetric]) (fact mod_div_equality)
+lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
+ by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)
-lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)"
- by (rule add_implies_diff [symmetric]) (fact mod_div_equality2)
+lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
+ by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
end
-
+
class ordered_semiring = semiring + ordered_comm_monoid_add +
assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -1906,7 +1906,7 @@
lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1"
by (simp only: sgn_1_neg)
-lemma sgn_times: "sgn (a * b) = sgn a * sgn b"
+lemma sgn_mult: "sgn (a * b) = sgn a * sgn b"
by (auto simp add: sgn_if zero_less_mult_iff)
lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
@@ -1918,6 +1918,10 @@
lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
unfolding sgn_if by auto
+lemma abs_sgn_eq_1 [simp]:
+ "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
+ by (simp add: abs_if)
+
lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
by (simp add: sgn_if)
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sun Oct 16 18:22:19 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 18:16:49 2016 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy Sun Oct 16 18:22:19 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/Tools/Qelim/cooper.ML Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 18:22:19 2016 +0200
@@ -829,13 +829,13 @@
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
@{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
- @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"},
+ @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}]
@ @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
val splits_ss =
simpset_of (put_simpset comp_ss @{context}
- addsimps [@{thm "mod_div_equality'"}]
+ 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/Tools/nat_numeral_simprocs.ML Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sun Oct 16 18:22:19 2016 +0200
@@ -350,7 +350,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Arith_Data.simplify_meta_eq
- [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_Suc_0}, @{thm numeral_1_eq_Suc_0}];
fun cancel_simplify_meta_eq ctxt cancel_th th =
simplify_one ctxt (([th, cancel_th]) MRS trans);
--- a/src/HOL/Tools/numeral_simprocs.ML Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sun Oct 16 18:22:19 2016 +0200
@@ -173,7 +173,7 @@
(*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
val add_0s = @{thms add_0_left add_0_right};
-val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
+val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1};
(* For post-simplification of the rhs of simproc-generated rules *)
val post_simps =
@@ -184,7 +184,7 @@
@{thm mult_minus1}, @{thm mult_minus1_right}]
val field_post_simps =
- post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
+ post_simps @ [@{thm div_0}, @{thm div_by_1}]
(*Simplify inverse Numeral1*)
val inverse_1s = [@{thm inverse_numeral_1}];
@@ -712,7 +712,7 @@
val ths =
[@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@{thm "divide_numeral_1"},
- @{thm "divide_zero"}, @{thm divide_zero_left},
+ @{thm "div_by_0"}, @{thm div_0},
@{thm "divide_divide_eq_left"},
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_times_eq"},
--- a/src/HOL/Word/Bit_Representation.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Sun Oct 16 18:22:19 2016 +0200
@@ -43,7 +43,7 @@
lemma bin_rl_simp [simp]:
"bin_rest w BIT bin_last w = w"
unfolding bin_rest_def bin_last_def Bit_def
- using mod_div_equality [of w 2]
+ using div_mult_mod_eq [of w 2]
by (cases "w mod 2 = 0", simp_all)
lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
@@ -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.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Word/Word.thy Sun Oct 16 18:22:19 2016 +0200
@@ -2161,7 +2161,7 @@
apply (unfold word_less_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
- apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
+ apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse)
apply simp
done
@@ -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 mod_div_equality')
+ td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
apply clarsimp
done
--- a/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sun Oct 16 18:22:19 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 *)
@@ -291,7 +291,7 @@
lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
-lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
+lemmas dme = div_mult_mod_eq
lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
@@ -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
--- a/src/HOL/ex/Simproc_Tests.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Sun Oct 16 18:22:19 2016 +0200
@@ -361,7 +361,7 @@
have "(k) / (k*y) = uu"
by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
next
- assume "(if b = 0 then 0 else a * c / 1) = uu"
+ assume "(if b = 0 then 0 else a * c) = uu"
have "(a*(b*c)) / b = uu"
by (tactic \<open>test @{context} [@{simproc divide_cancel_factor}]\<close>) fact
next
--- a/src/HOL/ex/Transfer_Ex.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/ex/Transfer_Ex.thy Sun Oct 16 18:22:19 2016 +0200
@@ -16,7 +16,7 @@
by (fact ex1 [untransferred])
lemma ex2: "(a::nat) div b * b + a mod b = a"
- by (rule mod_div_equality)
+ by (rule div_mult_mod_eq)
lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
by (fact ex2 [transferred])
--- a/src/HOL/ex/Word_Type.thy Sun Oct 16 18:16:49 2016 +0200
+++ b/src/HOL/ex/Word_Type.thy Sun Oct 16 18:22:19 2016 +0200
@@ -33,7 +33,7 @@
where "b = a div 2" and "c = a mod 2"
then have a: "a = b * 2 + c"
and "c = 0 \<or> c = 1"
- by (simp_all add: mod_div_equality parity)
+ by (simp_all add: div_mult_mod_eq parity)
from \<open>c = 0 \<or> c = 1\<close>
have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
proof