mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Nov 11 14:27:17 2020 +0000
@@ -2432,7 +2432,7 @@
also have "\<dots> \<le> norm (f x - y) * B"
by (metis B(2) g'.diff)
also have "\<dots> \<le> e * B"
- by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
+ by (metis B(1) dist_norm mem_cball mult_le_cancel_iff1 that(1))
also have "\<dots> \<le> e1"
using B(1) e(3) pos_less_divide_eq by fastforce
finally have "z \<in> cball x e1"
@@ -2454,7 +2454,7 @@
have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
using B by auto
also have "\<dots> \<le> e * B"
- by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
+ by (metis B(1) z dist_norm mem_cball norm_minus_commute mult_le_cancel_iff1)
also have "\<dots> < e0"
using B(1) e(2) pos_less_divide_eq by blast
finally have *: "norm (x + g' (z - f x) - x) < e0"
@@ -2493,7 +2493,7 @@
using B
by (auto simp add: field_simps)
also have "\<dots> \<le> e * B"
- by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
+ by (metis B(1) dist_norm mem_cball norm_minus_commute mult_le_cancel_iff1 z(1))
also have "\<dots> \<le> e1"
using e B unfolding less_divide_eq by auto
finally have "x + g'(z - f x) \<in> T"
--- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Nov 11 14:27:17 2020 +0000
@@ -170,7 +170,7 @@
have "norm (\<chi> k. m k * x $ k) \<le> norm (Max (range (\<lambda>k. \<bar>m k\<bar>)) *\<^sub>R x)"
by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono)
also have "\<dots> < ?C"
- using x by simp (metis \<open>B > 0\<close> \<open>?C > 0\<close> mult.commute real_mult_less_iff1 zero_less_mult_pos)
+ using x \<open>0 < (MAX k. \<bar>m k\<bar>) * B\<close> \<open>0 < B\<close> zero_less_mult_pos2 by fastforce
finally have "norm (\<chi> k. m k * x $ k) < ?C" .
then show "x \<in> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
using stretch_Galois [of "inverse \<circ> m"] True by (auto simp: image_iff field_simps)
@@ -764,7 +764,7 @@
fix x
assume "e > 0" "m < n" "n * e \<le> \<bar>det (matrix (f' x))\<bar>" "\<bar>det (matrix (f' x))\<bar> < (1 + real m) * e"
then have "n < 1 + real m"
- by (metis (no_types, hide_lams) less_le_trans mult.commute not_le real_mult_le_cancel_iff2)
+ by (metis (no_types, hide_lams) less_le_trans mult.commute not_le mult_le_cancel_iff2)
then show "False"
using less.hyps by linarith
qed
@@ -780,7 +780,7 @@
have False if "T n \<subseteq> T m" "x \<in> T n" for x
using \<open>e > 0\<close> \<open>m < n\<close> that
apply (auto simp: T_def mult.commute intro: less_le_trans dest!: subsetD)
- by (metis add.commute less_le_trans nat_less_real_le not_le real_mult_le_cancel_iff2)
+ by (metis add.commute less_le_trans nat_less_real_le not_le mult_le_cancel_iff2)
then show ?case
using less.prems by blast
qed auto
@@ -2161,7 +2161,7 @@
show "\<exists>t. norm (f y - f x - f' x t) \<le> d * norm (v - u)"
apply (rule_tac x="y-x" in exI)
using \<open>d > 0\<close> yx_le le_dyx mult_left_mono [where c=d]
- by (meson order_trans real_mult_le_cancel_iff2)
+ by (meson order_trans mult_le_cancel_iff2)
qed
with subT show "f ` (K \<inter> S) \<subseteq> T" by blast
show "?\<mu> T \<le> e / (2*c) ^ ?m * ?\<mu> K"
--- a/src/HOL/Analysis/Derivative.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Derivative.thy Wed Nov 11 14:27:17 2020 +0000
@@ -1116,7 +1116,7 @@
have "norm (g z - g y) < d0"
by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) \<open>0 < d0\<close> d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff)
then show ?thesis
- by (metis C(1) \<open>y \<in> T\<close> d0 fg real_mult_le_cancel_iff1)
+ by (metis C(1) \<open>y \<in> T\<close> d0 fg mult_le_cancel_iff1)
qed
also have "\<dots> \<le> e * norm (g z - g y)"
using C by (auto simp add: field_simps)
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Nov 11 14:27:17 2020 +0000
@@ -1092,7 +1092,7 @@
proof (cases "d = 0")
case True
from \<open>1 - c > 0\<close> have "(1 - c) * x \<le> 0 \<longleftrightarrow> x \<le> 0" for x
- by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1)
+ by (simp add: mult_le_0_iff)
with c cf_z2[of 0] True have "z n = z0" for n
by (simp add: z_def)
with \<open>e > 0\<close> show ?thesis by simp
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Nov 11 14:27:17 2020 +0000
@@ -3157,7 +3157,7 @@
then show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
f ` S \<inter> cbox a b \<in> lmeasurable \<and>
\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> < e"
- using \<open>C>0\<close> \<open>D>0\<close> by (metis mult_zero_left real_mult_less_iff1)
+ using \<open>C>0\<close> \<open>D>0\<close> by (metis mult_zero_left mult_less_iff1)
qed
qed
qed
@@ -4224,7 +4224,7 @@
moreover have "0 \<le> m"
using False m_def by force
ultimately show ?thesis
- by (metis abs_of_nonneg floor_mono le_floor_iff m_def of_int_0_le_iff power2_eq_square power_mult real_mult_le_cancel_iff1 zero_less_numeral mult.commute zero_less_power)
+ by (metis abs_of_nonneg floor_mono le_floor_iff m_def of_int_0_le_iff power2_eq_square power_mult mult_le_cancel_iff1 zero_less_numeral mult.commute zero_less_power)
qed
then have "?g n x = m/2^n"
by (rule indicator_sum_eq) (auto simp add: m_def field_split_simps, linarith)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Nov 11 14:27:17 2020 +0000
@@ -6323,7 +6323,7 @@
obtain u v where "K = cbox u v"
using \<open>(x, K) \<in> \<D>\<close> p(1) by blast
moreover have "content K * norm (f x) \<le> content K * g x"
- by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
+ by (meson K(1) K(2) content_pos_le mult_left_mono nle subsetD)
then show ?thesis
by simp
qed
--- a/src/HOL/Analysis/Homeomorphism.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy Wed Nov 11 14:27:17 2020 +0000
@@ -1483,7 +1483,7 @@
by blast+
have neq: "{0..n/N} \<union> {n/N..(1 + real n) / N} = {0..(1 + real n) / N}"
apply (auto simp: field_split_simps)
- by (metis mult_zero_left of_nat_0_le_iff of_nat_0_less_iff order_trans real_mult_le_cancel_iff1)
+ by (metis not_less of_nat_0_le_iff of_nat_0_less_iff order_trans zero_le_mult_iff)
then have neqQ': "{0..n/N} \<times> Q' \<union> {n/N..(1 + real n) / N} \<times> Q' = {0..(1 + real n) / N} \<times> Q'"
by blast
have cont: "continuous_on ({0..(1 + real n) / N} \<times> Q') (\<lambda>x. if x \<in> {0..n/N} \<times> Q' then k x else (p' \<circ> h) x)"
--- a/src/HOL/Analysis/Line_Segment.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Line_Segment.thy Wed Nov 11 14:27:17 2020 +0000
@@ -580,7 +580,7 @@
apply (simp add: dist_norm algebra_simps x)
by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
also have *: "... < dist a b"
- by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
+ using assms mult_less_cancel_right2 u(2) by fastforce
finally show "dist x a < dist a b" .
have ab_ne0: "dist a b \<noteq> 0"
using * by fastforce
--- a/src/HOL/Analysis/Poly_Roots.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Poly_Roots.thy Wed Nov 11 14:27:17 2020 +0000
@@ -92,7 +92,8 @@
(e + norm (c (Suc n))) * (norm z * norm z ^ n)"
by (simp add: norm_mult norm_power algebra_simps)
also have "... \<le> (e * norm z) * (norm z * norm z ^ n)"
- using norm2 by (metis real_mult_le_cancel_iff1)
+ using norm2
+ using assms mult_mono by fastforce
also have "... = e * (norm z * (norm z * norm z ^ n))"
by (simp add: algebra_simps)
finally have "e * (norm z * norm z ^ n) + norm (c (Suc n) * (z * z ^ n))
--- a/src/HOL/Analysis/Polytope.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Polytope.thy Wed Nov 11 14:27:17 2020 +0000
@@ -2816,7 +2816,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
have "?n * a \<le> a + x"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis assms(2) floor_divide_lower mult.commute)
also have "... < y"
by (rule 1)
finally have "?n * a < y" .
@@ -2829,7 +2829,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
have "?n * a \<le> a + y"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis assms(2) floor_divide_lower mult.commute)
also have "... < x"
by (rule 2)
finally have "?n * a < x" .
--- a/src/HOL/Analysis/Starlike.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Starlike.thy Wed Nov 11 14:27:17 2020 +0000
@@ -4142,7 +4142,7 @@
have cont_f: "continuous_on (affine hull S) f"
proof (clarsimp simp: dist_norm continuous_on_iff diff)
show "\<And>x e. 0 < e \<Longrightarrow> \<exists>d>0. \<forall>y \<in> affine hull S. \<bar>f y - f x\<bar> * norm z < d \<longrightarrow> \<bar>f y - f x\<bar> < e"
- by (metis \<open>z \<noteq> 0\<close> mult_pos_pos real_mult_less_iff1 zero_less_norm_iff)
+ by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_iff1 zero_less_norm_iff)
qed
then have conn_fS: "connected (f ` S)"
by (meson S connected_continuous_image continuous_on_subset hull_subset)
@@ -4212,7 +4212,7 @@
have cont_f: "continuous_on (affine hull S) f"
proof (clarsimp simp: dist_norm continuous_on_iff diff)
show "\<And>x e. 0 < e \<Longrightarrow> \<exists>d>0. \<forall>y \<in> affine hull S. \<bar>f y - f x\<bar> * norm z < d \<longrightarrow> \<bar>f y - f x\<bar> < e"
- by (metis \<open>z \<noteq> 0\<close> mult_pos_pos real_mult_less_iff1 zero_less_norm_iff)
+ by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_iff1 zero_less_norm_iff)
qed
then have "connected (f ` S)"
by (meson \<open>connected S\<close> connected_continuous_image continuous_on_subset hull_subset)
--- a/src/HOL/Analysis/Tagged_Division.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy Wed Nov 11 14:27:17 2020 +0000
@@ -2495,8 +2495,8 @@
(((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
using that \<open>j \<in> Basis\<close> by (simp add: subset_box field_split_simps aibi)
then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
- ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
- by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
+ ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
+ by (metis bjaj mult.commute of_nat_1 of_nat_add mult_le_cancel_iff2)
then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
by (rule dd)
then have "m \<le> n"
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Wed Nov 11 14:27:17 2020 +0000
@@ -615,7 +615,7 @@
apply (subst measure_UNION')
using that pwC by (auto simp: case_prod_unfold elim: pairwise_mono)
also have "\<dots> \<le> e"
- by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
+ by (metis mult.commute mult.left_neutral mult_le_cancel_iff1 \<open>e > 0\<close> le1)
finally show ?thesis .
qed
have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
--- a/src/HOL/Factorial.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Factorial.thy Wed Nov 11 14:27:17 2020 +0000
@@ -435,4 +435,17 @@
(simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
atLeastLessThanSuc_atLeastAtMost)
+
+lemma mult_less_iff1: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y"
+ for x y z :: "'a::linordered_idom"
+ by simp
+
+lemma mult_le_cancel_iff1: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y"
+ for x y z :: "'a::linordered_idom"
+ by simp
+
+lemma mult_le_cancel_iff2: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y"
+ for x y z :: "'a::linordered_idom"
+ by simp
+
end
--- a/src/HOL/Real.thy Wed Nov 11 11:27:44 2020 +0000
+++ b/src/HOL/Real.thy Wed Nov 11 14:27:17 2020 +0000
@@ -950,24 +950,6 @@
lifting_forget real.lifting
-subsection \<open>More Lemmas\<close>
-
-text \<open>BH: These lemmas should not be necessary; they should be
- covered by existing simp rules and simplification procedures.\<close>
-
-lemma real_mult_less_iff1 [simp]: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y"
- for x y z :: real
- by simp (* solved by linordered_ring_less_cancel_factor simproc *)
-
-lemma real_mult_le_cancel_iff1 [simp]: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y"
- for x y z :: real
- by simp (* solved by linordered_ring_le_cancel_factor simproc *)
-
-lemma real_mult_le_cancel_iff2 [simp]: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y"
- for x y z :: real
- by simp (* solved by linordered_ring_le_cancel_factor simproc *)
-
-
subsection \<open>Embedding numbers into the Reals\<close>
abbreviation real_of_nat :: "nat \<Rightarrow> real"