--- a/NEWS Sun Oct 16 09:31:03 2016 +0200
+++ b/NEWS Sun Oct 16 09:31:04 2016 +0200
@@ -249,6 +249,21 @@
*** 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
+INCOMPATIBILITY.
+
* Dedicated syntax LENGTH('a) for length of types.
* New proof method "argo" using the built-in Argo solver based on SMT
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Binomial.thy Sun Oct 16 09:31:04 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/Decision_Procs/Approximation.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Oct 16 09:31:04 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
--- a/src/HOL/Decision_Procs/Ferrack.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Oct 16 09:31:04 2016 +0200
@@ -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 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Oct 16 09:31:04 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/mir_tac.ML Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:04 2016 +0200
@@ -25,7 +25,7 @@
@{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"}]
--- a/src/HOL/Divides.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Divides.thy Sun Oct 16 09:31:04 2016 +0200
@@ -26,18 +26,6 @@
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"
@@ -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
@@ -1817,7 +1805,7 @@
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
@@ -2707,4 +2695,6 @@
"numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
by (fact dvd_eq_mod_eq_0)
+hide_fact (open) div_0 div_by_0
+
end
--- a/src/HOL/GCD.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/GCD.thy Sun Oct 16 09:31:04 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"
--- a/src/HOL/Library/Float.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Float.thy Sun Oct 16 09:31:04 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" .
--- a/src/HOL/Library/Formal_Power_Series.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sun Oct 16 09:31:04 2016 +0200
@@ -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 09:31:03 2016 +0200
+++ b/src/HOL/Library/Normalized_Fraction.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Sun Oct 16 09:31:04 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)
--- a/src/HOL/Library/Stirling.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Library/Stirling.thy Sun Oct 16 09:31:04 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/Nonstandard_Analysis/HDeriv.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy Sun Oct 16 09:31:04 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/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:04 2016 +0200
@@ -26,7 +26,7 @@
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
begin
-lemma zero_mod_left [simp]: "0 mod a = 0"
+lemma mod_0 [simp]: "0 mod a = 0"
using mod_div_equality [of 0 a] by simp
lemma dvd_mod_iff:
--- a/src/HOL/Number_Theory/Gauss.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Sun Oct 16 09:31:04 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/Old_Number_Theory/EvenOdd.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Sun Oct 16 09:31:04 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/IntPrimes.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Sun Oct 16 09:31:04 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:
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Oct 16 09:31:04 2016 +0200
@@ -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/Probability/SPMF.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Rat.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Oct 16 09:31:04 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 09:31:03 2016 +0200
+++ b/src/HOL/Rings.thy Sun Oct 16 09:31:04 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
@@ -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"
--- a/src/HOL/Tools/numeral_simprocs.ML Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sun Oct 16 09:31:04 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/ex/Simproc_Tests.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Sun Oct 16 09:31:04 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