# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1706873111 0
# Node ID f783490c6c995a6494d8fed680a9581809e732df
# Parent  76ad72736e9ed3f1ee5d76a82383942209211d10
A small number of new lemmas

diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -2374,7 +2374,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 mult_le_cancel_iff1 that(1))
+        by (metis B(1) dist_norm mem_cball mult_le_cancel_right_pos 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"
@@ -2396,7 +2396,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 mult_le_cancel_iff1)
+      by (metis B(1) z dist_norm mem_cball norm_minus_commute mult_le_cancel_right_pos)
     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"
@@ -2435,7 +2435,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 mult_le_cancel_iff1 z(1))
+      by (metis B(1) dist_norm mem_cball norm_minus_commute mult_le_cancel_right_pos 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 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -749,7 +749,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, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_iff2)
+              by (metis (no_types, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_left_pos)
             then show "False"
               using less.hyps by linarith
           qed
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Feb 02 11:25:11 2024 +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 mult_le_cancel_iff1)
+          by (metis C(1) \<open>y \<in> T\<close> d0 fg mult_le_cancel_right_pos)
       qed
       also have "\<dots> \<le> e * norm (g z - g y)"
         using C by (auto simp add: field_simps)
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -3191,7 +3191,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 mult_less_iff1)
+        using \<open>C>0\<close> \<open>D>0\<close> by (metis mult_zero_left mult_less_cancel_right_pos)
     qed
   qed
 qed
@@ -4321,7 +4321,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 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_right_pos 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 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -4354,7 +4354,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 mult_less_iff1 zero_less_norm_iff)
+        by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_cancel_right_pos zero_less_norm_iff)
     qed
     then have conn_fS: "connected (f ` S)"
       by (meson S connected_continuous_image continuous_on_subset hull_subset)
@@ -4424,7 +4424,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 mult_less_iff1 zero_less_norm_iff)
+      by (metis \<open>z \<noteq> 0\<close> mult_pos_pos mult_less_cancel_right_pos 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 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -2215,7 +2215,7 @@
           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 mult_le_cancel_iff2)
+          by (metis bjaj mult.commute of_nat_1 of_nat_add mult_le_cancel_left_pos)
         then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
           by (rule dd)
         then have "m \<le> n"
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Analysis/Vitali_Covering_Theorem.thy
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -616,7 +616,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 mult_le_cancel_iff1 \<open>e > 0\<close> le1)
+              by (metis mult.commute mult.left_neutral mult_le_cancel_right_pos \<open>e > 0\<close> le1)
             finally show ?thesis .
           qed
           have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Binomial.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -269,6 +269,13 @@
   shows "fact k * of_nat (n choose k) = (fact n / fact (n - k) :: 'a::field_char_0)"
   unfolding binomial_fact [OF assms] by (simp add: field_simps)
 
+lemma binomial_fact_pow: "(n choose s) * fact s \<le> n^s"
+proof (cases "s \<le> n")
+  case True
+  then show ?thesis
+    by (smt (verit) binomial_fact_lemma mult.assoc mult.commute fact_div_fact_le_pow fact_nonzero nonzero_mult_div_cancel_right) 
+qed (simp add: binomial_eq_0)
+
 lemma choose_two: "n choose 2 = n * (n - 1) div 2"
 proof (cases "n \<ge> 2")
   case False
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Factorial.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -417,17 +417,4 @@
     (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 76ad72736e9e -r f783490c6c99 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -1935,9 +1935,6 @@
 lemma ennreal_plus_if: "ennreal a + ennreal b = ennreal (if 0 \<le> a then (if 0 \<le> b then a + b else a) else b)"
   by (auto simp: ennreal_neg)
 
-lemma power_le_one_iff: "0 \<le> (a::real) \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
-  by (metis (mono_tags, opaque_lifting) le_less neq0_conv not_le one_le_power power_0 power_eq_imp_eq_base power_le_one zero_le_one)
-
 lemma ennreal_diff_le_mono_left: "a \<le> b \<Longrightarrow> a - c \<le> (b::ennreal)"
   using ennreal_mono_minus[of 0 c a, THEN order_trans, of b] by simp
 
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Power.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -836,9 +836,23 @@
 
 subsection \<open>Miscellaneous rules\<close>
 
-lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
+context linordered_semidom
+begin
+
+lemma self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   using power_increasing [of 1 n a] power_one_right [of a] by auto
 
+lemma power_le_one_iff: "0 \<le> a \<Longrightarrow> a ^ n \<le> 1 \<longleftrightarrow> (n = 0 \<or> a \<le> 1)"
+  by (metis (mono_tags) gr0I nle_le one_le_power power_le_one self_le_power power_0)
+
+lemma power_less1_D: "a^n < 1 \<Longrightarrow> a < 1"
+  using not_le one_le_power by blast
+
+lemma power_less_one_iff: "0 \<le> a \<Longrightarrow> a ^ n < 1 \<longleftrightarrow> (n > 0 \<and> a < 1)"
+  by (metis (mono_tags) power_one power_strict_mono power_less1_D less_le_not_le neq0_conv power_0)
+
+end
+
 lemma power2_ge_1_iff: "x ^ 2 \<ge> 1 \<longleftrightarrow> x \<ge> 1 \<or> x \<le> (-1 :: 'a :: linordered_idom)"
   using abs_le_square_iff[of 1 x] by (auto simp: abs_if split: if_splits)
 
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Rings.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -2378,6 +2378,18 @@
 lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
   by (auto simp: mult_less_cancel_left)
 
+lemma mult_le_cancel_right_pos: "0 < c \<Longrightarrow> a * c \<le> b * c \<longleftrightarrow> a \<le> b"
+  by (auto simp: mult_le_cancel_right)
+
+lemma mult_le_cancel_right_neg: "c < 0 \<Longrightarrow> a * c \<le> b * c \<longleftrightarrow> b \<le> a"
+  by (auto simp: mult_le_cancel_right)
+
+lemma mult_less_cancel_right_pos: "0 < c \<Longrightarrow> a * c < b * c \<longleftrightarrow> a < b"
+  by (auto simp: mult_less_cancel_right)
+
+lemma mult_less_cancel_right_neg: "c < 0 \<Longrightarrow> a * c < b * c \<longleftrightarrow> b < a"
+  by (auto simp: mult_less_cancel_right)
+
 end
 
 lemmas mult_sign_intros =
@@ -2784,7 +2796,6 @@
 
 end
 
-
 subsection \<open>Dioids\<close>
 
 text \<open>
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Set.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -1920,6 +1920,9 @@
 lemma disjnt_self_iff_empty [simp]: "disjnt S S \<longleftrightarrow> S = {}"
   by (auto simp: disjnt_def)
 
+lemma disjnt_commute: "disjnt A B = disjnt B A"
+  by (auto simp: disjnt_def)
+
 lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
   by (force simp: disjnt_def)
 
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -2231,27 +2231,24 @@
 lemma sum_diff_split:
   fixes f:: "nat \<Rightarrow> 'a::ab_group_add"
   assumes "m \<le> n"
-  shows "(\<Sum>i\<le>n - m. f(n - i)) = (\<Sum>i\<le>n. f i) - (\<Sum>i<m. f i)"
+  shows "(\<Sum>i\<le>n. f i) - (\<Sum>i<m. f i) = (\<Sum>i\<le>n - m. f(n - i))"
 proof -
-  have inj: "inj_on ((-) n) {m..n}"
+  have "\<And>i. i \<le> n-m \<Longrightarrow> \<exists>k\<ge>m. k \<le> n \<and> i = n-k"
+    by (metis Nat.le_diff_conv2 add.commute \<open>m\<le>n\<close> diff_diff_cancel diff_le_self order.trans)
+  then have eq: "{..n-m} = (-)n ` {m..n}"
+    by force
+  have inj: "inj_on ((-)n) {m..n}"
     by (auto simp: inj_on_def)
-  have "(\<Sum>i\<le>n - m. f(n - i)) = (\<Sum>i\<in>(-) n ` {m..n}. f(n - i))"
-  proof (rule sum.cong)
-    have "\<And>x. x \<le> n - m \<Longrightarrow> \<exists>k\<ge>m. k \<le> n \<and> x = n - k"
-      by (metis assms diff_diff_cancel diff_le_mono2 diff_le_self le_trans)
-    then show "{..n - m} = (-) n ` {m..n}"
-      by (auto simp: image_iff Bex_def)
-  qed auto
-  also have "\<dots> = (\<Sum>i=m..n. f i)"
-    by (simp add: sum.reindex_cong [OF inj])
+  have "(\<Sum>i\<le>n - m. f(n - i)) = (\<Sum>i=m..n. f i)"
+    by (simp add: eq sum.reindex_cong [OF inj])
   also have "\<dots> = (\<Sum>i\<le>n. f i) - (\<Sum>i<m. f i)"
-    using sum_diff_nat_ivl[of 0 "m" "Suc n" f] assms 
+    using sum_diff_nat_ivl[of 0 "m" "Suc n" f] assms
     by (simp only: atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost)
-  finally show ?thesis .
+  finally show ?thesis by metis
 qed
 
 
-subsubsection \<open>Telescoping\<close>
+subsubsection \<open>Telescoping sums\<close>
 
 lemma sum_telescope:
   fixes f::"nat \<Rightarrow> 'a::ab_group_add"
@@ -2601,6 +2598,34 @@
     by auto
 qed
 
+subsubsection \<open>Telescoping products\<close>
+
+lemma prod_telescope:
+  fixes f::"nat \<Rightarrow> 'a::field"
+  assumes "\<And>i. i\<le>n \<Longrightarrow> f (Suc i) \<noteq> 0"
+  shows "(\<Prod>i\<le>n. f i / f (Suc i)) = f 0 / f (Suc n)"
+  using assms by (induction n) auto
+
+lemma prod_telescope'':
+  fixes f::"nat \<Rightarrow> 'a::field"
+  assumes "m \<le> n"
+  assumes "\<And>i. i \<in> {m..n} \<Longrightarrow> f i \<noteq> 0"
+  shows   "(\<Prod>i = Suc m..n. f i / f (i - 1)) = f n / f m"
+  by (rule dec_induct[OF \<open>m \<le> n\<close>]) (auto simp add: assms)
+
+lemma prod_lessThan_telescope:
+  fixes f::"nat \<Rightarrow> 'a::field"
+  assumes "\<And>i. i\<le>n \<Longrightarrow> f i \<noteq> 0"
+  shows "(\<Prod>i<n. f (Suc i) / f i) = f n / f 0"
+  using assms by (induction n) auto
+
+lemma prod_lessThan_telescope':
+  fixes f::"nat \<Rightarrow> 'a::field"
+  assumes "\<And>i. i\<le>n \<Longrightarrow> f i \<noteq> 0"
+  shows "(\<Prod>i<n. f i / f (Suc i)) = f 0 / f n"
+  using assms by (induction n) auto
+
+
 subsection \<open>Efficient folding over intervals\<close>
 
 function fold_atLeastAtMost_nat where
diff -r 76ad72736e9e -r f783490c6c99 src/HOL/ex/BigO.thy
--- a/src/HOL/ex/BigO.thy	Wed Jan 31 22:36:12 2024 +0100
+++ b/src/HOL/ex/BigO.thy	Fri Feb 02 11:25:11 2024 +0000
@@ -49,7 +49,7 @@
 
 lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
   apply (auto simp add: bigo_alt_def)
-  by (metis (no_types, opaque_lifting) mult.assoc mult_le_cancel_iff2 order.trans
+  by (metis (no_types, opaque_lifting) mult.assoc mult_le_cancel_left_pos order.trans
       zero_less_mult_iff)
 
 lemma bigo_refl [intro]: "f \<in> O(f)"
@@ -77,7 +77,7 @@
   apply (rule conjI)
    apply (rule_tac x = "c + c" in exI)
    apply (clarsimp)
-  apply (smt (verit, ccfv_threshold) mult.commute abs_triangle_ineq add_le_cancel_left dual_order.trans mult.left_commute mult_2 mult_le_cancel_iff2)
+  apply (smt (verit, ccfv_threshold) mult.commute abs_triangle_ineq add_le_cancel_left dual_order.trans mult.left_commute mult_2 mult_le_cancel_left_pos)
   apply (simp add: order_less_le)
   apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
   apply (rule conjI)