--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Feb 02 11:25:24 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"
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Feb 02 11:25:24 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
--- a/src/HOL/Analysis/Derivative.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Derivative.thy Fri Feb 02 11:25:24 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)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Feb 02 11:25:24 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)
--- a/src/HOL/Analysis/Starlike.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Starlike.thy Fri Feb 02 11:25:24 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)
--- a/src/HOL/Analysis/Tagged_Division.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy Fri Feb 02 11:25:24 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"
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Fri Feb 02 11:25:24 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"
--- a/src/HOL/Binomial.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Binomial.thy Fri Feb 02 11:25:24 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
--- a/src/HOL/Factorial.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Factorial.thy Fri Feb 02 11:25:24 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
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Feb 02 11:25:24 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
--- a/src/HOL/Power.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Power.thy Fri Feb 02 11:25:24 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)
--- a/src/HOL/Rings.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Rings.thy Fri Feb 02 11:25:24 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>
--- a/src/HOL/Set.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Set.thy Fri Feb 02 11:25:24 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)
--- a/src/HOL/Set_Interval.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/Set_Interval.thy Fri Feb 02 11:25:24 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
--- a/src/HOL/ex/BigO.thy Thu Feb 01 12:14:57 2024 +0000
+++ b/src/HOL/ex/BigO.thy Fri Feb 02 11:25:24 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)