--- a/NEWS Thu Feb 22 14:51:05 2024 +0100
+++ b/NEWS Thu Feb 22 16:31:58 2024 +0100
@@ -48,7 +48,11 @@
* Theory "HOL.Transitive_Closure":
- Added lemmas.
+ relpow_left_unique
+ relpow_right_unique
relpow_trans[trans]
+ relpowp_left_unique
+ relpowp_right_unique
relpowp_trans[trans]
* Theory "HOL-Library.Multiset":
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Feb 22 16:31:58 2024 +0100
@@ -2379,8 +2379,7 @@
by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
lemma powr_times_real:
- "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
- \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
+ "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk> \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
lemma Re_powr_le: "r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> Re (r powr z) \<le> Re r powr Re z"
@@ -2392,6 +2391,12 @@
shows Reals_powr [simp]: "w powr z \<in> \<real>" and nonneg_Reals_powr [simp]: "w powr z \<in> \<real>\<^sub>\<ge>\<^sub>0"
using assms by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
+lemma exp_powr_complex:
+ fixes x::complex
+ assumes "-pi < Im(x)" "Im(x) \<le> pi"
+ shows "exp x powr y = exp (x*y)"
+ using assms by (simp add: powr_def mult.commute)
+
lemma powr_neg_real_complex:
fixes w::complex
shows "(- of_real x) powr w = (-1) powr (of_real (sgn x) * w) * of_real x powr w"
--- a/src/HOL/Analysis/Convex.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Analysis/Convex.thy Thu Feb 22 16:31:58 2024 +0100
@@ -583,7 +583,6 @@
and f :: "'b \<Rightarrow> real"
assumes "finite S" "S \<noteq> {}"
and "convex_on C f"
- and "convex C"
and "(\<Sum> i \<in> S. a i) = 1"
and "\<And>i. i \<in> S \<Longrightarrow> a i \<ge> 0"
and "\<And>i. i \<in> S \<Longrightarrow> y i \<in> C"
@@ -624,6 +623,8 @@
using i0 by auto
then have a1: "(\<Sum> j \<in> S. ?a j) = 1"
unfolding sum_divide_distrib by simp
+ have "convex C"
+ using \<open>convex_on C f\<close> by (simp add: convex_on_def)
have asum: "(\<Sum> j \<in> S. ?a j *\<^sub>R y j) \<in> C"
using insert convex_sum [OF \<open>finite S\<close> \<open>convex C\<close> a1 a_nonneg] by auto
have asum_le: "f (\<Sum> j \<in> S. ?a j *\<^sub>R y j) \<le> (\<Sum> j \<in> S. ?a j * f (y j))"
@@ -648,6 +649,26 @@
qed
qed
+lemma concave_on_sum:
+ fixes a :: "'a \<Rightarrow> real"
+ and y :: "'a \<Rightarrow> 'b::real_vector"
+ and f :: "'b \<Rightarrow> real"
+ assumes "finite S" "S \<noteq> {}"
+ and "concave_on C f"
+ and "(\<Sum>i \<in> S. a i) = 1"
+ and "\<And>i. i \<in> S \<Longrightarrow> a i \<ge> 0"
+ and "\<And>i. i \<in> S \<Longrightarrow> y i \<in> C"
+ shows "f (\<Sum>i \<in> S. a i *\<^sub>R y i) \<ge> (\<Sum>i \<in> S. a i * f (y i))"
+proof -
+ have "(uminus \<circ> f) (\<Sum>i\<in>S. a i *\<^sub>R y i) \<le> (\<Sum>i\<in>S. a i * (uminus \<circ> f) (y i))"
+ proof (intro convex_on_sum)
+ show "convex_on C (uminus \<circ> f)"
+ by (simp add: assms convex_on_iff_concave)
+ qed (use assms in auto)
+ then show ?thesis
+ by (simp add: sum_negf o_def)
+qed
+
lemma convex_on_alt:
fixes C :: "'a::real_vector set"
shows "convex_on C f \<longleftrightarrow> convex C \<and>
@@ -865,6 +886,39 @@
lemma exp_convex: "convex_on UNIV exp"
by (intro f''_ge0_imp_convex derivative_eq_intros | simp)+
+text \<open>The AM-GM inequality: the arithmetic mean exceeds the geometric mean.\<close>
+lemma arith_geom_mean:
+ fixes x :: "'a \<Rightarrow> real"
+ assumes "finite S" "S \<noteq> {}"
+ and x: "\<And>i. i \<in> S \<Longrightarrow> x i \<ge> 0"
+ shows "(\<Sum>i \<in> S. x i / card S) \<ge> (\<Prod>i \<in> S. x i) powr (1 / card S)"
+proof (cases "\<exists>i\<in>S. x i = 0")
+ case True
+ then have "(\<Prod>i \<in> S. x i) = 0"
+ by (simp add: \<open>finite S\<close>)
+ moreover have "(\<Sum>i \<in> S. x i / card S) \<ge> 0"
+ by (simp add: sum_nonneg x)
+ ultimately show ?thesis
+ by simp
+next
+ case False
+ have "ln (\<Sum>i \<in> S. (1 / card S) *\<^sub>R x i) \<ge> (\<Sum>i \<in> S. (1 / card S) * ln (x i))"
+ proof (intro concave_on_sum)
+ show "concave_on {0<..} ln"
+ by (simp add: ln_concave)
+ show "\<And>i. i\<in>S \<Longrightarrow> x i \<in> {0<..}"
+ using False x by fastforce
+ qed (use assms False in auto)
+ moreover have "(\<Sum>i \<in> S. (1 / card S) *\<^sub>R x i) > 0"
+ using False assms by (simp add: card_gt_0_iff less_eq_real_def sum_pos)
+ ultimately have "(\<Sum>i \<in> S. (1 / card S) *\<^sub>R x i) \<ge> exp (\<Sum>i \<in> S. (1 / card S) * ln (x i))"
+ using ln_ge_iff by blast
+ then have "(\<Sum>i \<in> S. x i / card S) \<ge> exp (\<Sum>i \<in> S. ln (x i) / card S)"
+ by (simp add: divide_simps)
+ then show ?thesis
+ using assms False
+ by (smt (verit, ccfv_SIG) divide_inverse exp_ln exp_powr_real exp_sum inverse_eq_divide prod.cong prod_powr_distrib)
+qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>Convexity of real functions\<close>
--- a/src/HOL/Analysis/Retracts.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Analysis/Retracts.thy Thu Feb 22 16:31:58 2024 +0100
@@ -1178,7 +1178,7 @@
if "openin (top_of_set U) V" "T retract_of V" "U \<noteq> {}" for V
using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
obtain Ta where "(openin (top_of_set U) Ta \<and> T retract_of Ta)"
- using ANR_def UT \<open>S homeomorphic T\<close> assms by moura
+ using ANR_def UT \<open>S homeomorphic T\<close> assms by atomize_elim (auto simp: choice)
then show ?thesis
using S \<open>U \<noteq> {}\<close> by blast
qed
--- a/src/HOL/Bit_Operations.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Bit_Operations.thy Thu Feb 22 16:31:58 2024 +0100
@@ -14,9 +14,9 @@
\<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
\<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
\<Longrightarrow> P a\<close>
- assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
+ assumes bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
+ and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
- and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
begin
@@ -382,24 +382,6 @@
with rec [of n True] show ?case
by simp
qed
- show \<open>even (q mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (q div 2 ^ n)\<close> for q m n :: nat
- proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define r where \<open>r = n - m\<close>
- ultimately have \<open>n = m + r\<close>
- by simp
- with True show ?thesis
- by (simp add: power_add div_mult2_eq)
- next
- case False
- moreover define r where \<open>r = m - Suc n\<close>
- ultimately have \<open>m = n + Suc r\<close>
- by simp
- moreover have \<open>even (q mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (q div 2 ^ n)\<close>
- by (simp only: power_add) (simp add: mod_mult2_eq dvd_mod_iff)
- ultimately show ?thesis
- by simp
- qed
qed (auto simp add: div_mult2_eq bit_nat_def)
end
@@ -539,24 +521,6 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
- show \<open>even (k mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (k div 2 ^ n)\<close> for k :: int and m n :: nat
- proof (cases \<open>m \<le> n\<close>)
- case True
- moreover define r where \<open>r = n - m\<close>
- ultimately have \<open>n = m + r\<close>
- by simp
- with True show ?thesis
- by (simp add: power_add zdiv_zmult2_eq)
- next
- case False
- moreover define r where \<open>r = m - Suc n\<close>
- ultimately have \<open>m = n + Suc r\<close>
- by simp
- moreover have \<open>even (k mod 2 ^ (n + Suc r) div 2 ^ n) \<longleftrightarrow> even (k div 2 ^ n)\<close>
- by (simp only: power_add) (simp add: zmod_zmult2_eq dvd_mod_iff)
- ultimately show ?thesis
- by simp
- qed
qed (auto simp add: zdiv_zmult2_eq bit_int_def)
end
@@ -879,13 +843,96 @@
\<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
+lemma bit_drop_bit_eq [bit_simps]:
+ \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
+ by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
+
+lemma disjunctive_xor_eq_or:
+ \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
+ using that by (auto simp add: bit_eq_iff bit_simps)
+
+lemma disjunctive_add_eq_or:
+ \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
+proof (rule bit_eqI)
+ fix n
+ assume \<open>possible_bit TYPE('a) n\<close>
+ moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
+ by simp
+ then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+ by (simp add: bit_simps)
+ ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
+ proof (induction n arbitrary: a b)
+ case 0
+ from "0"(2)[of 0] show ?case
+ by (auto simp add: even_or_iff bit_0)
+ next
+ case (Suc n)
+ from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
+ by (auto simp add: bit_0)
+ have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+ using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+ from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
+ using possible_bit_less_imp by force
+ with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
+ have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (simp add: bit_Suc)
+ have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+ using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+ also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+ using even by (auto simp add: algebra_simps mod2_eq_if)
+ finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+ using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
+ also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
+ by (rule IH)
+ finally show ?case
+ by (simp add: bit_simps flip: bit_Suc)
+ qed
+qed
+
+lemma disjunctive_add_eq_xor:
+ \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
+ using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
+
lemma take_bit_0 [simp]:
"take_bit 0 a = 0"
by (simp add: take_bit_eq_mod)
lemma bit_take_bit_iff [bit_simps]:
\<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
- by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le)
+proof -
+ have \<open>push_bit m (drop_bit m a) AND take_bit m a = 0\<close> (is \<open>?lhs = _\<close>)
+ proof (rule bit_eqI)
+ fix n
+ show \<open>bit ?lhs n \<longleftrightarrow> bit 0 n\<close>
+ proof (cases \<open>m \<le> n\<close>)
+ case False
+ then show ?thesis
+ by (simp add: bit_simps)
+ next
+ case True
+ moreover define q where \<open>q = n - m\<close>
+ ultimately have \<open>n = m + q\<close> by simp
+ moreover have \<open>\<not> bit (take_bit m a) (m + q)\<close>
+ by (simp add: take_bit_eq_mod bit_iff_odd flip: div_exp_eq)
+ ultimately show ?thesis
+ by (simp add: bit_simps)
+ qed
+ qed
+ then have \<open>push_bit m (drop_bit m a) XOR take_bit m a = push_bit m (drop_bit m a) + take_bit m a\<close>
+ by (simp add: disjunctive_add_eq_xor)
+ also have \<open>\<dots> = a\<close>
+ by (simp add: bits_ident)
+ finally have \<open>bit (push_bit m (drop_bit m a) XOR take_bit m a) n \<longleftrightarrow> bit a n\<close>
+ by simp
+ also have \<open>\<dots> \<longleftrightarrow> (m \<le> n \<or> n < m) \<and> bit a n\<close>
+ by auto
+ also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
+ by auto
+ also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
+ by (auto simp add: bit_simps bit_imp_possible_bit)
+ finally show ?thesis
+ by (auto simp add: bit_simps)
+qed
lemma take_bit_Suc:
\<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
@@ -915,10 +962,6 @@
\<open>take_bit n 1 = of_bool (n > 0)\<close>
by (cases n) (simp_all add: take_bit_Suc)
-lemma bit_drop_bit_eq [bit_simps]:
- \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
- by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)
-
lemma drop_bit_of_0 [simp]:
\<open>drop_bit n 0 = 0\<close>
by (rule bit_eqI) (simp add: bit_simps)
@@ -1245,52 +1288,6 @@
\<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
-lemma disjunctive_xor_eq_or:
- \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
- using that by (auto simp add: bit_eq_iff bit_simps)
-
-lemma disjunctive_add_eq_or:
- \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
-proof (rule bit_eqI)
- fix n
- assume \<open>possible_bit TYPE('a) n\<close>
- moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
- by simp
- then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
- by (simp add: bit_simps)
- ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
- proof (induction n arbitrary: a b)
- case 0
- from "0"(2)[of 0] show ?case
- by (auto simp add: even_or_iff bit_0)
- next
- case (Suc n)
- from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
- by (auto simp add: bit_0)
- have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
- using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
- from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
- using possible_bit_less_imp by force
- with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
- have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
- by (simp add: bit_Suc)
- have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
- using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
- also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
- using even by (auto simp add: algebra_simps mod2_eq_if)
- finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
- using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
- also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
- by (rule IH)
- finally show ?case
- by (simp add: bit_simps flip: bit_Suc)
- qed
-qed
-
-lemma disjunctive_add_eq_xor:
- \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
- using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)
-
lemma set_bit_eq:
\<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
proof -
@@ -3921,6 +3918,10 @@
\<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
by (rule disjunctive_add_eq_or) (use that in \<open>simp add: bit_eq_iff bit_simps\<close>)
+lemma even_mod_exp_div_exp_iff [no_atp]:
+ \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
+ by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
+
end
context ring_bit_operations
--- a/src/HOL/Code_Numeral.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Feb 22 16:31:58 2024 +0100
@@ -349,7 +349,7 @@
instance by (standard; transfer)
(fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
- half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
and_rec or_rec xor_rec mask_eq_exp_minus_1
set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
@@ -1109,7 +1109,7 @@
instance by (standard; transfer)
(fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
- half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
and_rec or_rec xor_rec mask_eq_exp_minus_1
set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
--- a/src/HOL/Computational_Algebra/Polynomial.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Feb 22 16:31:58 2024 +0100
@@ -464,7 +464,7 @@
by (simp add: is_zero_def null_def)
-subsubsection \<open>Reconstructing the polynomial from the list\<close>
+text \<open>Reconstructing the polynomial from the list\<close>
\<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
@@ -1296,6 +1296,15 @@
"lead_coeff (of_int k) = of_int k"
by (simp add: of_int_poly)
+lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n"
+ by (simp add: of_nat_poly)
+
+lemma poly_of_int [simp]: "poly (of_int n) x = of_int n"
+ by (simp add: of_int_poly)
+
+lemma poly_numeral [simp]: "poly (numeral n) x = numeral n"
+ by (metis of_nat_numeral poly_of_nat)
+
lemma numeral_poly: "numeral n = [:numeral n:]"
proof -
have "numeral n = of_nat (numeral n)"
@@ -1841,6 +1850,12 @@
by simp
qed
+lemma order_gt_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p > 0 \<longleftrightarrow> poly p x = 0"
+ by (subst order_root) auto
+
+lemma order_eq_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p = 0 \<longleftrightarrow> poly p x \<noteq> 0"
+ by (subst order_root) auto
+
text \<open>Next three lemmas contributed by Wenda Li\<close>
lemma order_1_eq_0 [simp]:"order x 1 = 0"
by (metis order_root poly_1 zero_neq_one)
@@ -2176,6 +2191,68 @@
qed
qed
+lemma coeff_pcompose_monom_linear [simp]:
+ fixes p :: "'a :: comm_ring_1 poly"
+ shows "coeff (pcompose p (monom c (Suc 0))) k = c ^ k * coeff p k"
+ by (induction p arbitrary: k)
+ (auto simp: coeff_pCons coeff_monom_mult pcompose_pCons split: nat.splits)
+
+lemma of_nat_mult_conv_smult: "of_nat n * P = smult (of_nat n) P"
+ by (simp add: monom_0 of_nat_monom)
+
+lemma numeral_mult_conv_smult: "numeral n * P = smult (numeral n) P"
+ by (simp add: numeral_poly)
+
+lemma sum_order_le_degree:
+ assumes "p \<noteq> 0"
+ shows "(\<Sum>x | poly p x = 0. order x p) \<le> degree p"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case (less p)
+ show ?case
+ proof (cases "\<exists>x. poly p x = 0")
+ case False
+ thus ?thesis
+ by auto
+ next
+ case True
+ then obtain x where x: "poly p x = 0"
+ by auto
+ have "[:-x, 1:] ^ order x p dvd p"
+ by (simp add: order_1)
+ then obtain q where q: "p = [:-x, 1:] ^ order x p * q"
+ by (elim dvdE)
+ have [simp]: "q \<noteq> 0"
+ using q less.prems by auto
+ have "order x p = order x p + order x q"
+ by (subst q, subst order_mult) (auto simp: order_power_n_n)
+ hence "order x q = 0"
+ by auto
+ hence [simp]: "poly q x \<noteq> 0"
+ by (simp add: order_root)
+ have deg_p: "degree p = degree q + order x p"
+ by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq)
+ moreover have "order x p > 0"
+ using x less.prems by (simp add: order_root)
+ ultimately have "degree q < degree p"
+ by linarith
+ hence "(\<Sum>x | poly q x = 0. order x q) \<le> degree q"
+ by (intro less.hyps) auto
+ hence "order x p + (\<Sum>x | poly q x = 0. order x q) \<le> degree p"
+ by (simp add: deg_p)
+ also have "{y. poly q y = 0} = {y. poly p y = 0} - {x}"
+ by (subst q) auto
+ also have "(\<Sum>y \<in> {y. poly p y = 0} - {x}. order y q) =
+ (\<Sum>y \<in> {y. poly p y = 0} - {x}. order y p)"
+ by (intro sum.cong refl, subst q)
+ (auto simp: order_mult order_power_n_n intro!: order_0I)
+ also have "order x p + \<dots> = (\<Sum>y \<in> insert x ({y. poly p y = 0} - {x}). order y p)"
+ using \<open>p \<noteq> 0\<close> by (subst sum.insert) (auto simp: poly_roots_finite)
+ also have "insert x ({y. poly p y = 0} - {x}) = {y. poly p y = 0}"
+ using \<open>poly p x = 0\<close> by auto
+ finally show ?thesis .
+ qed
+qed
subsection \<open>Closure properties of coefficients\<close>
@@ -2858,6 +2935,12 @@
by (simp add: rsquarefree_def order_root)
qed
+lemma has_field_derivative_poly [derivative_intros]:
+ assumes "(f has_field_derivative f') (at x within A)"
+ shows "((\<lambda>x. poly p (f x)) has_field_derivative
+ (f' * poly (pderiv p) (f x))) (at x within A)"
+ using DERIV_chain[OF poly_DERIV assms, of p] by (simp add: o_def mult_ac)
+
subsection \<open>Algebraic numbers\<close>
@@ -5138,7 +5221,6 @@
by (simp_all add: content_mult mult_ac)
qed (auto simp: content_mult)
-
no_notation cCons (infixr "##" 65)
end
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Thu Feb 22 16:31:58 2024 +0100
@@ -9,6 +9,7 @@
"HOL-Library.Pattern_Aliases"
Complex_Main
Priority_Queue_Specs
+ Define_Time_Function
begin
text \<open>
@@ -471,21 +472,19 @@
subsubsection \<open>Timing Functions\<close>
-text \<open>
- We define timing functions for each operation, and provide
- estimations of their complexity.
-\<close>
-definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
-[simp]: "T_link _ _ = 0"
+define_time_fun link
+
+lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0"
+by(cases t\<^sub>1; cases t\<^sub>2, auto)
+
+define_time_fun rank
-fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a trees \<Rightarrow> nat" where
- "T_ins_tree t [] = 1"
-| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = 1 +
- (if rank t\<^sub>1 < rank t\<^sub>2 then 0
- else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
+lemma T_rank[simp]: "T_rank t = 0"
+by(cases t, auto)
-definition T_insert :: "'a::linorder \<Rightarrow> 'a trees \<Rightarrow> nat" where
-"T_insert x ts = T_ins_tree (Node 0 x []) ts"
+define_time_fun ins_tree
+
+define_time_fun insert
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
by (induction t ts rule: T_ins_tree.induct) auto
@@ -497,7 +496,7 @@
shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 1"
proof -
have "real (T_insert x ts) \<le> real (length ts) + 1"
- unfolding T_insert_def using T_ins_tree_simple_bound
+ unfolding T_insert.simps using T_ins_tree_simple_bound
by (metis of_nat_1 of_nat_add of_nat_mono)
also note size_mset_trees[OF \<open>invar ts\<close>]
finally show ?thesis by simp
@@ -505,20 +504,11 @@
subsubsection \<open>\<open>T_merge\<close>\<close>
-context
-includes pattern_aliases
-begin
+define_time_fun merge
-fun T_merge :: "'a::linorder trees \<Rightarrow> 'a trees \<Rightarrow> nat" where
- "T_merge ts\<^sub>1 [] = 1"
-| "T_merge [] ts\<^sub>2 = 1"
-| "T_merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + (
- if rank t\<^sub>1 < rank t\<^sub>2 then T_merge ts\<^sub>1 h\<^sub>2
- else if rank t\<^sub>2 < rank t\<^sub>1 then T_merge h\<^sub>1 ts\<^sub>2
- else T_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2
- )"
-
-end
+(* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>,
+apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated.
+*)
text \<open>A crucial idea is to estimate the time in correlation with the
result length, as each carry reduces the length of the result.\<close>
@@ -529,7 +519,7 @@
lemma T_merge_length:
"T_merge ts\<^sub>1 ts\<^sub>2 + length (merge ts\<^sub>1 ts\<^sub>2) \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
-by (induction ts\<^sub>1 ts\<^sub>2 rule: T_merge.induct)
+by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
(auto simp: T_ins_tree_length algebra_simps)
text \<open>Finally, we get the desired logarithmic bound\<close>
@@ -557,9 +547,14 @@
subsubsection \<open>\<open>T_get_min\<close>\<close>
-fun T_get_min :: "'a::linorder trees \<Rightarrow> nat" where
- "T_get_min [t] = 1"
-| "T_get_min (t#ts) = 1 + T_get_min ts"
+define_time_fun root
+
+lemma T_root[simp]: "T_root t = 0"
+by(cases t)(simp_all)
+
+define_time_fun min
+
+define_time_fun get_min
lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts"
by (induction ts rule: T_get_min.induct) auto
@@ -576,9 +571,10 @@
subsubsection \<open>\<open>T_del_min\<close>\<close>
-fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
+define_time_fun get_min_rest
+(*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where
"T_get_min_rest [t] = 1"
-| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"
+| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*)
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
by (induction ts rule: T_get_min_rest.induct) auto
@@ -599,9 +595,7 @@
definition "T_rev xs = length xs + 1"
-definition T_del_min :: "'a::linorder trees \<Rightarrow> nat" where
- "T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
- \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2)"
+define_time_fun del_min
lemma T_del_min_bound:
fixes ts
@@ -624,7 +618,7 @@
by (auto simp: mset_trees_def)
have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
- unfolding T_del_min_def GM
+ unfolding T_del_min.simps GM
by simp
also have "T_get_min_rest ts \<le> log 2 (n+1)"
using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp
--- a/src/HOL/Data_Structures/Define_Time_Function.ML Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Thu Feb 22 16:31:58 2024 +0100
@@ -360,7 +360,7 @@
casec = casec,
letc = letc
}
-fun top_converter is_rec _ _ = opt_term o (plus (if is_rec then SOME one else NONE))
+fun top_converter is_rec _ _ = opt_term o (fn exp => plus exp (if is_rec then SOME one else NONE))
(* Use converter to convert right side of a term *)
fun to_time ctxt origin converter top_converter term =
--- a/src/HOL/Groups_Big.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Groups_Big.thy Thu Feb 22 16:31:58 2024 +0100
@@ -1596,10 +1596,10 @@
context linordered_semidom
begin
-lemma prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
+lemma prod_nonneg: "(\<And>a. a\<in>A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
by (induct A rule: infinite_finite_induct) simp_all
-lemma prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
+lemma prod_pos: "(\<And>a. a\<in>A \<Longrightarrow> 0 < f a) \<Longrightarrow> 0 < prod f A"
by (induct A rule: infinite_finite_induct) simp_all
lemma prod_mono:
@@ -1738,14 +1738,13 @@
case empty
then show ?case by auto
next
- case (insert x F)
- from insertI1 have "0 \<le> g (f x)" by (rule insert)
- hence 1: "sum g (f ` F) \<le> g (f x) + sum g (f ` F)" using add_increasing by blast
- have 2: "sum g (f ` F) \<le> sum (g \<circ> f) F" using insert by blast
- have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
- also have "\<dots> \<le> g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if)
- also from 2 have "\<dots> \<le> g (f x) + sum (g \<circ> f) F" by (rule add_left_mono)
- also from insert(1, 2) have "\<dots> = sum (g \<circ> f) (insert x F)" by (simp add: sum.insert_if)
+ case (insert i I)
+ hence *: "sum g (f ` I) \<le> g (f i) + sum g (f ` I)"
+ "sum g (f ` I) \<le> sum (g \<circ> f) I" using add_increasing by blast+
+ have "sum g (f ` insert i I) = sum g (insert (f i) (f ` I))" by simp
+ also have "\<dots> \<le> g (f i) + sum g (f ` I)" by (simp add: * insert sum.insert_if)
+ also from * have "\<dots> \<le> g (f i) + sum (g \<circ> f) I" by (intro add_left_mono)
+ also from insert have "\<dots> = sum (g \<circ> f) (insert i I)" by (simp add: sum.insert_if)
finally show ?case .
qed
--- a/src/HOL/Library/Multiset_Order.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Thu Feb 22 16:31:58 2024 +0100
@@ -652,7 +652,7 @@
by (metis image_mset_Diff image_mset_union)
next
obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
- using ex_y by moura
+ using ex_y by metis
show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
proof (intro allI impI)
--- a/src/HOL/Library/Word.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Library/Word.thy Thu Feb 22 16:31:58 2024 +0100
@@ -667,6 +667,32 @@
end
+lemma unat_div_distrib:
+ \<open>unat (v div w) = unat v div unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule div_le_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
+qed
+
+lemma unat_mod_distrib:
+ \<open>unat (v mod w) = unat v mod unat w\<close>
+proof transfer
+ fix k l
+ have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
+ by (rule mod_less_eq_dividend)
+ also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
+ by (simp add: nat_less_iff)
+ finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
+ (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
+ by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
+qed
+
instance word :: (len) semiring_parity
by (standard; transfer)
(auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
@@ -838,6 +864,9 @@
show \<open>0 div a = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
+ show \<open>a mod b div b = 0\<close>
+ for a b :: \<open>'a word\<close>
+ by (simp add: word_eq_iff_unsigned [where ?'a = nat] unat_div_distrib unat_mod_distrib)
show \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
for a :: \<open>'a word\<close> and m n :: nat
apply transfer
@@ -849,10 +878,6 @@
for a :: \<open>'a word\<close> and n :: nat
using that by transfer
(simp add: even_drop_bit_iff_not_bit bit_simps flip: drop_bit_eq_div del: power.simps)
- show \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
- for a :: \<open>'a word\<close> and m n :: nat
- by transfer
- (auto simp flip: take_bit_eq_mod drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_simps)
qed
end
@@ -1301,32 +1326,6 @@
by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
(simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)
-lemma unat_div_distrib:
- \<open>unat (v div w) = unat v div unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule div_le_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff)
-qed
-
-lemma unat_mod_distrib:
- \<open>unat (v mod w) = unat v mod unat w\<close>
-proof transfer
- fix k l
- have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
- by (rule mod_less_eq_dividend)
- also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
- by (simp add: nat_less_iff)
- finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
- (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
- by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff)
-qed
-
lemma uint_div_distrib:
\<open>uint (v div w) = uint v div uint w\<close>
proof -
--- a/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy Thu Feb 22 16:31:58 2024 +0100
@@ -409,10 +409,6 @@
and "\<forall>x. l x > 0 \<longrightarrow> f x \<in> {l x..u x} \<longrightarrow> g x \<le> 0 \<longrightarrow> f x powr g x \<in> {u x powr g x..l x powr g x}"
by (auto intro: powr_mono2 powr_mono2')
-(* TODO Move *)
-lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
- using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
-
qualified lemma powr_left_bounds:
fixes f g :: "real \<Rightarrow> real"
shows "\<forall>x. f x > 0 \<longrightarrow> g x \<in> {l x..u x} \<longrightarrow> f x \<ge> 1 \<longrightarrow> f x powr g x \<in> {f x powr l x..f x powr u x}"
--- a/src/HOL/Transcendental.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Transcendental.thy Thu Feb 22 16:31:58 2024 +0100
@@ -2450,6 +2450,10 @@
shows "continuous_on s (\<lambda>x. log (f x) (g x))"
using assms unfolding continuous_on_def by (fast intro: tendsto_log)
+lemma exp_powr_real:
+ fixes x::real shows "exp x powr y = exp (x*y)"
+ by (simp add: powr_def)
+
lemma powr_one_eq_one [simp]: "1 powr a = 1"
by (simp add: powr_def)
@@ -2469,6 +2473,13 @@
for a x y :: real
by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
+lemma prod_powr_distrib:
+ fixes x :: "'a \<Rightarrow> real"
+ assumes "\<And>i. i\<in>I \<Longrightarrow> x i \<ge> 0"
+ shows "(prod x I) powr r = (\<Prod>i\<in>I. x i powr r)"
+ using assms
+ by (induction I rule: infinite_finite_induct) (auto simp add: powr_mult prod_nonneg)
+
lemma powr_ge_pzero [simp]: "0 \<le> x powr y"
for x y :: real
by (simp add: powr_def)
@@ -2546,6 +2557,14 @@
shows "x powr real_of_int n = power_int x n"
by (metis assms exp_ln_iff exp_power_int nless_le power_int_eq_0_iff powr_def)
+lemma exp_minus_ge:
+ fixes x::real shows "1 - x \<le> exp (-x)"
+ by (smt (verit) exp_ge_add_one_self)
+
+lemma exp_minus_greater:
+ fixes x::real shows "1 - x < exp (-x) \<longleftrightarrow> x \<noteq> 0"
+ by (smt (verit) exp_minus_ge exp_eq_one_iff exp_gt_zero ln_eq_minus_one ln_exp)
+
lemma log_ln: "ln x = log (exp(1)) x"
by (simp add: log_def)
@@ -2945,6 +2964,17 @@
for x :: real
using less_eq_real_def powr_less_mono2 that by auto
+lemma powr01_less_one:
+ fixes a::real
+ assumes "0 < a" "a < 1"
+ shows "a powr e < 1 \<longleftrightarrow> e>0"
+proof
+ show "a powr e < 1 \<Longrightarrow> e>0"
+ using assms not_less_iff_gr_or_eq powr_less_mono2_neg by fastforce
+ show "e>0 \<Longrightarrow> a powr e < 1"
+ by (metis assms less_eq_real_def powr_less_mono2 powr_one_eq_one)
+qed
+
lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
for x :: real
using powr_mono2 by fastforce
@@ -2966,6 +2996,14 @@
shows "x powr a \<le> y powr b"
by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
+lemma powr_mono': "a \<le> (b::real) \<Longrightarrow> x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr b \<le> x powr a"
+ using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
+
+lemma powr_less_mono':
+ assumes "(x::real) > 0" "x < 1" "a < b"
+ shows "x powr b < x powr a"
+ by (metis assms log_powr_cancel order.strict_iff_order powr_mono')
+
lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
for x :: real
unfolding powr_def exp_inj_iff by simp
@@ -2973,6 +3011,9 @@
lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
by (simp add: powr_def root_powr_inverse sqrt_def)
+lemma powr_half_sqrt_powr: "0 \<le> x \<Longrightarrow> x powr (a/2) = sqrt(x powr a)"
+ by (metis divide_inverse mult.left_neutral powr_ge_pzero powr_half_sqrt powr_powr)
+
lemma square_powr_half [simp]:
fixes x::real shows "x\<^sup>2 powr (1/2) = \<bar>x\<bar>"
by (simp add: powr_half_sqrt)
@@ -3108,6 +3149,23 @@
by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
qed
+lemma has_derivative_const_powr [derivative_intros]:
+ assumes "\<And>x. (f has_derivative f') (at x)" "a \<noteq> (0::real)"
+ shows "((\<lambda>x. a powr (f x)) has_derivative (\<lambda>y. f' y * ln a * a powr (f x))) (at x)"
+ using assms
+ apply (simp add: powr_def)
+ apply (rule assms derivative_eq_intros refl)+
+ done
+
+lemma has_real_derivative_const_powr [derivative_intros]:
+ assumes "\<And>x. (f has_real_derivative f' x) (at x)"
+ "a \<noteq> (0::real)"
+ shows "((\<lambda>x. a powr (f x)) has_real_derivative (f' x * ln a * a powr (f x))) (at x)"
+ using assms
+ apply (simp add: powr_def)
+ apply (rule assms derivative_eq_intros refl | simp)+
+ done
+
lemma DERIV_powr:
fixes r :: real
assumes g: "DERIV g x :> m"
@@ -5462,6 +5520,35 @@
unfolding filterlim_at_bot_mirror arctan_minus
by (intro tendsto_minus tendsto_arctan_at_top)
+lemma sin_multiple_reduce:
+ "sin (x * numeral n :: 'a :: {real_normed_field, banach}) =
+ sin x * cos (x * of_nat (pred_numeral n)) + cos x * sin (x * of_nat (pred_numeral n))"
+proof -
+ have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+ by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+ also have "sin (x * \<dots>) = sin (x * of_nat (pred_numeral n) + x)"
+ unfolding of_nat_Suc by (simp add: ring_distribs)
+ finally show ?thesis
+ by (simp add: sin_add)
+qed
+
+lemma cos_multiple_reduce:
+ "cos (x * numeral n :: 'a :: {real_normed_field, banach}) =
+ cos (x * of_nat (pred_numeral n)) * cos x - sin (x * of_nat (pred_numeral n)) * sin x"
+proof -
+ have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+ by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+ also have "cos (x * \<dots>) = cos (x * of_nat (pred_numeral n) + x)"
+ unfolding of_nat_Suc by (simp add: ring_distribs)
+ finally show ?thesis
+ by (simp add: cos_add)
+qed
+
+lemma arccos_eq_pi_iff: "x \<in> {-1..1} \<Longrightarrow> arccos x = pi \<longleftrightarrow> x = -1"
+ by (metis arccos arccos_minus_1 atLeastAtMost_iff cos_pi)
+
+lemma arccos_eq_0_iff: "x \<in> {-1..1} \<Longrightarrow> arccos x = 0 \<longleftrightarrow> x = 1"
+ by (metis arccos arccos_1 atLeastAtMost_iff cos_zero)
subsection \<open>Prove Totality of the Trigonometric Functions\<close>
@@ -7161,6 +7248,133 @@
finally show ?thesis .
qed
+lemma cosh_double_cosh: "cosh (2 * x :: 'a :: {banach, real_normed_field}) = 2 * (cosh x)\<^sup>2 - 1"
+ using cosh_double[of x] by (simp add: sinh_square_eq)
+
+lemma sinh_multiple_reduce:
+ "sinh (x * numeral n :: 'a :: {real_normed_field, banach}) =
+ sinh x * cosh (x * of_nat (pred_numeral n)) + cosh x * sinh (x * of_nat (pred_numeral n))"
+proof -
+ have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+ by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+ also have "sinh (x * \<dots>) = sinh (x * of_nat (pred_numeral n) + x)"
+ unfolding of_nat_Suc by (simp add: ring_distribs)
+ finally show ?thesis
+ by (simp add: sinh_add)
+qed
+
+lemma cosh_multiple_reduce:
+ "cosh (x * numeral n :: 'a :: {real_normed_field, banach}) =
+ cosh (x * of_nat (pred_numeral n)) * cosh x + sinh (x * of_nat (pred_numeral n)) * sinh x"
+proof -
+ have "numeral n = of_nat (pred_numeral n) + (1 :: 'a)"
+ by (metis add.commute numeral_eq_Suc of_nat_Suc of_nat_numeral)
+ also have "cosh (x * \<dots>) = cosh (x * of_nat (pred_numeral n) + x)"
+ unfolding of_nat_Suc by (simp add: ring_distribs)
+ finally show ?thesis
+ by (simp add: cosh_add)
+qed
+
+lemma cosh_arcosh_real [simp]:
+ assumes "x \<ge> (1 :: real)"
+ shows "cosh (arcosh x) = x"
+proof -
+ have "eventually (\<lambda>t::real. cosh t \<ge> x) at_top"
+ using cosh_real_at_top by (simp add: filterlim_at_top)
+ then obtain t where "t \<ge> 1" "cosh t \<ge> x"
+ by (metis eventually_at_top_linorder linorder_not_le order_le_less)
+ moreover have "isCont cosh (y :: real)" for y
+ by (intro continuous_intros)
+ ultimately obtain y where "y \<ge> 0" "x = cosh y"
+ using IVT[of cosh 0 x t] assms by auto
+ thus ?thesis
+ by (simp add: arcosh_cosh_real)
+qed
+
+lemma arcosh_eq_0_iff_real [simp]: "x \<ge> 1 \<Longrightarrow> arcosh x = 0 \<longleftrightarrow> x = (1 :: real)"
+ using cosh_arcosh_real by fastforce
+
+lemma arcosh_nonneg_real [simp]:
+ assumes "x \<ge> 1"
+ shows "arcosh (x :: real) \<ge> 0"
+proof -
+ have "1 + 0 \<le> x + (x\<^sup>2 - 1) powr (1 / 2)"
+ using assms by (intro add_mono) auto
+ thus ?thesis unfolding arcosh_def by simp
+qed
+
+lemma arcosh_real_strict_mono:
+ fixes x y :: real
+ assumes "1 \<le> x" "x < y"
+ shows "arcosh x < arcosh y"
+proof -
+ have "cosh (arcosh x) < cosh (arcosh y)"
+ by (subst (1 2) cosh_arcosh_real) (use assms in auto)
+ thus ?thesis
+ using assms by (subst (asm) cosh_real_nonneg_less_iff) auto
+qed
+
+lemma arcosh_less_iff_real [simp]:
+ fixes x y :: real
+ assumes "1 \<le> x" "1 \<le> y"
+ shows "arcosh x < arcosh y \<longleftrightarrow> x < y"
+ using arcosh_real_strict_mono[of x y] arcosh_real_strict_mono[of y x] assms
+ by (cases x y rule: linorder_cases) auto
+
+lemma arcosh_real_gt_1_iff [simp]: "x \<ge> 1 \<Longrightarrow> arcosh x > 0 \<longleftrightarrow> x \<noteq> (1 :: real)"
+ using arcosh_less_iff_real[of 1 x] by (auto simp del: arcosh_less_iff_real)
+
+lemma sinh_arcosh_real: "x \<ge> 1 \<Longrightarrow> sinh (arcosh x) = sqrt (x\<^sup>2 - 1)"
+ by (rule sym, rule real_sqrt_unique) (auto simp: sinh_square_eq)
+
+
+lemma sinh_arsinh_real [simp]: "sinh (arsinh x :: real) = x"
+proof -
+ have "eventually (\<lambda>t::real. sinh t \<ge> x) at_top"
+ using sinh_real_at_top by (simp add: filterlim_at_top)
+ then obtain t where "sinh t \<ge> x"
+ by (metis eventually_at_top_linorder linorder_not_le order_le_less)
+ moreover have "eventually (\<lambda>t::real. sinh t \<le> x) at_bot"
+ using sinh_real_at_bot by (simp add: filterlim_at_bot)
+ then obtain t' where "t' \<le> t" "sinh t' \<le> x"
+ by (metis eventually_at_bot_linorder nle_le)
+ moreover have "isCont sinh (y :: real)" for y
+ by (intro continuous_intros)
+ ultimately obtain y where "x = sinh y"
+ using IVT[of sinh t' x t] by auto
+ thus ?thesis
+ by (simp add: arsinh_sinh_real)
+qed
+
+lemma arsinh_real_strict_mono:
+ fixes x y :: real
+ assumes "x < y"
+ shows "arsinh x < arsinh y"
+proof -
+ have "sinh (arsinh x) < sinh (arsinh y)"
+ by (subst (1 2) sinh_arsinh_real) (use assms in auto)
+ thus ?thesis
+ using assms by (subst (asm) sinh_real_less_iff) auto
+qed
+
+lemma arsinh_less_iff_real [simp]:
+ fixes x y :: real
+ shows "arsinh x < arsinh y \<longleftrightarrow> x < y"
+ using arsinh_real_strict_mono[of x y] arsinh_real_strict_mono[of y x]
+ by (cases x y rule: linorder_cases) auto
+
+lemma arsinh_real_eq_0_iff [simp]: "arsinh x = 0 \<longleftrightarrow> x = (0 :: real)"
+ by (metis arsinh_0 sinh_arsinh_real)
+
+lemma arsinh_real_pos_iff [simp]: "arsinh x > 0 \<longleftrightarrow> x > (0 :: real)"
+ using arsinh_less_iff_real[of 0 x] by (simp del: arsinh_less_iff_real)
+
+lemma arsinh_real_neg_iff [simp]: "arsinh x < 0 \<longleftrightarrow> x < (0 :: real)"
+ using arsinh_less_iff_real[of x 0] by (simp del: arsinh_less_iff_real)
+
+lemma cosh_arsinh_real: "cosh (arsinh x) = sqrt (x\<^sup>2 + 1)"
+ by (rule sym, rule real_sqrt_unique) (auto simp: cosh_square_eq)
+
lemma continuous_on_arsinh [continuous_intros]: "continuous_on A (arsinh :: real \<Rightarrow> real)"
by (rule DERIV_continuous_on derivative_intros)+
--- a/src/HOL/Transitive_Closure.thy Thu Feb 22 14:51:05 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy Thu Feb 22 16:31:58 2024 +0100
@@ -936,6 +936,64 @@
lemma relpow_trans[trans]: "(x, y) \<in> R ^^ i \<Longrightarrow> (y, z) \<in> R ^^ j \<Longrightarrow> (x, z) \<in> R ^^ (i + j)"
using relpowp_trans[to_set] .
+lemma relpowp_left_unique:
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and n :: nat and x y z :: 'a
+ assumes lunique: "\<And>x y z. R x z \<Longrightarrow> R y z \<Longrightarrow> x = y"
+ shows "(R ^^ n) x z \<Longrightarrow> (R ^^ n) y z \<Longrightarrow> x = y"
+proof (induction n arbitrary: x y z)
+ case 0
+ thus ?case
+ by simp
+next
+ case (Suc n')
+ then obtain x' y' :: 'a where
+ "(R ^^ n') x x'" and "R x' z" and
+ "(R ^^ n') y y'" and "R y' z"
+ by auto
+
+ have "x' = y'"
+ using lunique[OF \<open>R x' z\<close> \<open>R y' z\<close>] .
+
+ show "x = y"
+ proof (rule Suc.IH)
+ show "(R ^^ n') x x'"
+ using \<open>(R ^^ n') x x'\<close> .
+ next
+ show "(R ^^ n') y x'"
+ using \<open>(R ^^ n') y y'\<close>
+ unfolding \<open>x' = y'\<close> .
+ qed
+qed
+
+lemma relpow_left_unique:
+ fixes R :: "('a \<times> 'a) set" and n :: nat and x y z :: 'a
+ shows "(\<And>x y z. (x, z) \<in> R \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> x = y) \<Longrightarrow>
+ (x, z) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> x = y"
+ using relpowp_left_unique[to_set] .
+
+lemma relpowp_right_unique:
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and n :: nat and x y z :: 'a
+ assumes runique: "\<And>x y z. R x y \<Longrightarrow> R x z \<Longrightarrow> y = z"
+ shows "(R ^^ n) x y \<Longrightarrow> (R ^^ n) x z \<Longrightarrow> y = z"
+proof (induction n arbitrary: x y z)
+ case 0
+ thus ?case
+ by simp
+next
+ case (Suc n')
+ then obtain x' :: 'a where
+ "(R ^^ n') x x'" and "R x' y" and "R x' z"
+ by auto
+ thus "y = z"
+ using runique by simp
+qed
+
+lemma relpow_right_unique:
+ fixes R :: "('a \<times> 'a) set" and n :: nat and x y z :: 'a
+ shows "(\<And>x y z. (x, y) \<in> R \<Longrightarrow> (x, z) \<in> R \<Longrightarrow> y = z) \<Longrightarrow>
+ (x, y) \<in> (R ^^ n) \<Longrightarrow> (x, z) \<in> (R ^^ n) \<Longrightarrow> y = z"
+ using relpowp_right_unique[to_set] .
+
lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
by (induct n) auto