# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1605104837 0
# Node ID d56e4eeae96749b6d1d0589aa35464ccd71f5066
# Parent  bac8921e2901c495b0bad47ad04b4ffe5f1f1d7d
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions

diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- 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"
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Change_Of_Vars.thy
--- 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"
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Derivative.thy
--- 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)
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- 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
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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)
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Homeomorphism.thy
--- 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)"
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Line_Segment.thy
--- 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
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Poly_Roots.thy
--- 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))
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Polytope.thy
--- 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" .
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Starlike.thy
--- 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)
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Tagged_Division.thy
--- 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"
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Analysis/Vitali_Covering_Theorem.thy
--- 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"
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Factorial.thy
--- 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
diff -r bac8921e2901 -r d56e4eeae967 src/HOL/Real.thy
--- 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"