--- a/src/Doc/Codegen/Adaptation.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Tue Apr 22 17:35:13 2025 +0100
@@ -190,6 +190,16 @@
Part of \<open>HOL-Main\<close>.
+ \item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close>
+ isomorphic to lists but implemented by (effectively immutable)
+ arrays \emph{in SML only}.
+
+ \end{description}
+
+ \noindent Using these adaptation setups the following extensions are provided:
+
+ \begin{description}
+
\item[\<open>Code_Target_Int\<close>] implements type \<^typ>\<open>int\<close>
by \<^typ>\<open>integer\<close> and thus by target-language built-in integers.
@@ -207,14 +217,14 @@
\item[\<open>Code_Target_Numeral\<close>] is a convenience theory
containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
+ \item[\<open>Code_Bit_Shifts_for_Arithmetic\<close>] uses the preprocessor to
+ replace arithmetic operations on numeric types by target-language
+ built-in bit shifts whenever feasible.
+
\item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language
integers, sacrificing pattern patching in exchange for dramatically
increased performance for comparisons.
- \item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close>
- isomorphic to lists but implemented by (effectively immutable)
- arrays \emph{in SML only}.
-
\end{description}
\<close>
--- a/src/HOL/Analysis/Derivative.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Analysis/Derivative.thy Tue Apr 22 17:35:13 2025 +0100
@@ -1742,7 +1742,7 @@
using islimpt_approachable_real[of x S] not_bot
by (auto simp add: trivial_limit_within)
then show ?thesis
- using eq_iff_diff_eq_0 by fastforce
+ using eq_iff_diff_eq_0 by (metis add.commute diff_add_cancel)
qed
qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
then show ?thesis
@@ -1777,6 +1777,17 @@
by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
(auto simp: differentiable_def has_vector_derivative_def)
+lemma vector_derivative_translate [simp]:
+ "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
+proof -
+ have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
+ if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
+ unfolding o_def using that by (auto intro!: derivative_eq_intros)
+ from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
+ unfolding vector_derivative_def
+ by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
+qed
+
lemma deriv_of_real [simp]:
"at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
by (auto intro!: vector_derivative_within derivative_eq_intros)
@@ -2256,6 +2267,43 @@
definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
"deriv f x \<equiv> SOME D. DERIV f x :> D"
+lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+proof -
+ have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
+ if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
+ proof -
+ have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
+ by (rule DERIV_chain that derivative_eq_intros refl)+ auto
+ thus ?thesis by simp
+ qed
+ have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
+ using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
+ thus ?thesis
+ by (simp add: deriv_def)
+qed
+
+lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+ by (rule deriv_shift_0)
+
+lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+proof (induction n arbitrary: f)
+ case (Suc n)
+ have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
+ by (subst funpow_Suc_right) auto
+ also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
+ by (subst Suc) (auto simp: o_def)
+ also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
+ by (subst deriv_shift_0) (auto simp: o_def)
+ also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
+ by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
+ also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
+ by (subst funpow_Suc_right) (auto simp: o_def)
+ finally show ?case .
+qed auto
+
+lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+ by (rule higher_deriv_shift_0)
+
lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
unfolding deriv_def by (metis some_equality DERIV_unique)
--- a/src/HOL/Analysis/FPS_Convergence.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Tue Apr 22 17:35:13 2025 +0100
@@ -61,6 +61,9 @@
lemma open_eball [simp, intro]: "open (eball z r)"
by (cases r) auto
+lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
+ by (cases r) auto
+
subsection \<open>Basic properties of convergent power series\<close>
@@ -843,6 +846,17 @@
with radius show ?thesis by (auto simp: has_fps_expansion_def)
qed
+lemma has_fps_expansion_sum [fps_expansion_intros]:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x has_fps_expansion F x"
+ shows "(\<lambda>z. \<Sum>x\<in>A. f x z) has_fps_expansion (\<Sum>x\<in>A. F x)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: fps_expansion_intros)
+
+lemma has_fps_expansion_prod [fps_expansion_intros]:
+ fixes F :: "'a \<Rightarrow> 'b :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x has_fps_expansion F x"
+ shows "(\<lambda>z. \<Prod>x\<in>A. f x z) has_fps_expansion (\<Prod>x\<in>A. F x)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: fps_expansion_intros)
+
lemma has_fps_expansion_exp [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field}"
shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c"
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Tue Apr 22 17:35:13 2025 +0100
@@ -846,11 +846,16 @@
by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
next
assume cg: "convergent_prod g"
- have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"
- by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)
+ have **: "eventually (\<lambda>n. prod g {..n} = prod f {..n} / C) sequentially"
+ using * by eventually_elim (use \<open>C \<noteq> 0\<close> in auto)
+ from cg and g have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
+ by simp
+ then have "\<not> (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+ using ** \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
then show "convergent_prod f"
- using "*" tendsto_mult_left filterlim_cong
- by (fastforce simp add: convergent_prod_iff_nz_lim f)
+ by (metis \<open>C \<noteq> 0\<close> cg convergent_LIMSEQ_iff
+ convergent_mult_const_iff convergent_prod_iff_convergent
+ convergent_prod_imp_convergent f local.cong)
qed
qed
@@ -953,8 +958,14 @@
lemma convergent_prod_If_finite[simp, intro]:
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
- shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"
- using convergent_prod_def has_prod_If_finite has_prod_def by fastforce
+ assumes "finite {r. P r}"
+ shows "convergent_prod (\<lambda>r. if P r then f r else 1)"
+proof -
+ have "(\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
+ by (rule has_prod_If_finite) fact
+ thus ?thesis
+ by (meson convergent_prod_def has_prod_def)
+qed
lemma has_prod_single:
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Tue Apr 22 17:35:13 2025 +0100
@@ -27,6 +27,7 @@
Elementary_Topology
"HOL-Library.Extended_Nonnegative_Real"
"HOL-Library.Complex_Order"
+ "HOL-Computational_Algebra.Formal_Power_Series"
begin
subsection \<open>Definition and syntax\<close>
@@ -3578,5 +3579,79 @@
shows "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. -f x) has_sum (-S)) A"
using has_sum_cmult_right[of f A S "-1"] by simp
+
+subsection \<open>Infinite sums of formal power series\<close>
+
+text \<open>
+ Consequently, a family $(f_x)_{x\in A}$ of formal power series sums to a series $s$ iff for
+ any $n\geq 0$, the set $A_n = \{x\in A \mid [X^n]\,f_x \neq 0\}$ is finite and
+ $[X^n]\,s = \sum_{x\in A_n} [X^n]\,f_x$.
+
+ The first condition can be rephrased as follows: for any $n\geq 0$, for all but finitely many
+ $x$, the series $f_x$ has subdegree ${>}\,n$.
+\<close>
+lemma has_sum_fpsI:
+ assumes "\<And>n. finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ assumes "\<And>n. fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+ shows "(F has_sum S) A"
+ unfolding has_sum_def
+proof (rule tendsto_fpsI)
+ fix n :: nat
+ define B where "B = {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ from assms(1) have [intro]: "finite B"
+ unfolding B_def by auto
+ moreover have "B \<subseteq> A"
+ by (auto simp: B_def)
+ ultimately have "eventually (\<lambda>X. finite X \<and> B \<subseteq> X \<and> X \<subseteq> A) (finite_subsets_at_top A)"
+ by (subst eventually_finite_subsets_at_top) blast
+ thus "eventually (\<lambda>X. fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n) (finite_subsets_at_top A)"
+ proof eventually_elim
+ case (elim X)
+ have "fps_nth (\<Sum>x\<in>X. F x) n = (\<Sum>x\<in>X. fps_nth (F x) n)"
+ by (simp add: fps_sum_nth)
+ also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+ by (rule sum.mono_neutral_right) (use \<open>finite B\<close> \<open>B \<subseteq> A\<close> elim in \<open>auto simp: B_def\<close>)
+ also have "\<dots> = fps_nth S n"
+ using assms(2)[of n] by (simp add: B_def)
+ finally show "fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n" .
+ qed
+qed
+
+lemma has_sum_fpsD:
+ fixes F :: "'a \<Rightarrow> 'b :: ab_group_add fps"
+ assumes "(F has_sum S) A"
+ shows "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+proof -
+ from assms have "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) k = fps_nth S k" for k
+ unfolding has_sum_def tendsto_fps_iff by blast
+ hence "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) n = fps_nth S n"
+ by eventually_elim force
+ then obtain B where [intro, simp]: "finite B" and B: "B \<subseteq> A"
+ "\<And>X. finite X \<Longrightarrow> B \<subseteq> X \<Longrightarrow> X \<subseteq> A \<Longrightarrow> fps_nth (sum F X) n = fps_nth S n"
+ unfolding eventually_finite_subsets_at_top by metis
+
+ have subset: "{x\<in>A. fps_nth (F x) n \<noteq> 0} \<subseteq> B"
+ proof safe
+ fix x assume x: "x \<in> A" "fps_nth (F x) n \<noteq> 0"
+ have "fps_nth (sum F B) n = fps_nth S n"
+ by (rule B(2)) (use B(1) in auto)
+ moreover have "fps_nth (sum F (insert x B)) n = fps_nth S n"
+ by (rule B(2)) (use B(1) x in auto)
+ ultimately show "x \<in> B"
+ using x by (auto simp: sum.insert_if split: if_splits)
+ qed
+ thus finite: "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ by (rule finite_subset) auto
+
+ have "fps_nth S n = fps_nth (\<Sum>x\<in>B. F x) n"
+ by (rule sym, rule B(2)) (use B(1) in auto)
+ also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+ by (simp add: fps_sum_nth)
+ also have "\<dots> = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+ by (rule sum.mono_neutral_right) (use subset B(1) in auto)
+ finally show "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)" .
+qed
+
end
--- a/src/HOL/Bit_Operations.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Bit_Operations.thy Tue Apr 22 17:35:13 2025 +0100
@@ -778,6 +778,14 @@
by (simp add: mask_eq_exp_minus_1)
qed
+lemma mask_eq_iff_eq_exp:
+ \<open>mask n = a \<longleftrightarrow> a + 1 = 2 ^ n\<close>
+ by (auto simp flip: inc_mask_eq_exp)
+
+lemma eq_mask_iff_eq_exp:
+ \<open>a = mask n \<longleftrightarrow> a + 1 = 2 ^ n\<close>
+ by (auto simp flip: inc_mask_eq_exp)
+
lemma mask_Suc_double:
\<open>mask (Suc n) = 1 OR 2 * mask n\<close>
proof -
@@ -3832,6 +3840,10 @@
using that take_bit_int_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
by (simp add: signed_take_bit_eq_take_bit_shift)
+lemma signed_take_bit_Suc_sgn_eq [simp]:
+ \<open>signed_take_bit (Suc n) (sgn k) = sgn k\<close> for k :: int
+ by (simp add: sgn_if)
+
lemma signed_take_bit_Suc_bit0 [simp]:
\<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
by (simp add: signed_take_bit_Suc)
--- a/src/HOL/Code_Numeral.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Code_Numeral.thy Tue Apr 22 17:35:13 2025 +0100
@@ -837,6 +837,12 @@
in if j = 0 then l' else l' + 1)"
by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
+lemma int_of_integer_code_nbe [code nbe]:
+ "int_of_integer 0 = 0"
+ "int_of_integer (Pos n) = Int.Pos n"
+ "int_of_integer (Neg n) = Int.Neg n"
+ by simp_all
+
lemma integer_of_int_code [code]:
"integer_of_int k = (if k < 0 then - (integer_of_int (- k))
else if k = 0 then 0
@@ -846,6 +852,12 @@
in if j = 0 then l else l + 1)"
by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
+lemma integer_of_int_code_nbe [code nbe]:
+ "integer_of_int 0 = 0"
+ "integer_of_int (Int.Pos n) = Pos n"
+ "integer_of_int (Int.Neg n) = Neg n"
+ by simp_all
+
hide_const (open) Pos Neg sub dup divmod_abs
context
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Tue Apr 22 17:35:13 2025 +0100
@@ -1266,6 +1266,58 @@
finally show ?thesis .
qed
+lemma deriv_complex_uniform_limit:
+ assumes ulim: "uniform_limit A f g F"
+ and f_holo: "eventually (\<lambda>n. f n holomorphic_on A) F"
+ and F: "F \<noteq> bot"
+ and A: "open A" "z \<in> A"
+ shows "((\<lambda>n. deriv (f n) z) \<longlongrightarrow> deriv g z) F"
+ using higher_deriv_complex_uniform_limit[OF assms, of 1] by simp
+
+lemma logderiv_prodinf_complex_uniform_limit:
+ fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+ assumes lim: "uniform_limit A (\<lambda>n x. \<Prod>k<n. f k x) P sequentially"
+ assumes holo: "\<And>k. f k holomorphic_on A"
+ assumes nz: "P z \<noteq> 0"
+ assumes A: "open A" "z \<in> A"
+ shows "(\<lambda>k. deriv (f k) z / f k z) sums (deriv P z / P z)"
+proof -
+ define f' where "f' = (\<lambda>k. deriv (f k))"
+ note [derivative_intros] = has_field_derivative_prod'
+ have [derivative_intros]:
+ "(f k has_field_derivative f' k z) (at z within B)" if "z \<in> A" for B z k
+ using that holomorphic_derivI[OF holo[of k], of z B] A unfolding f'_def by auto
+ have lim': "(\<lambda>n. \<Prod>k<n. f k z) \<longlonglongrightarrow> P z"
+ using lim by (rule tendsto_uniform_limitI) fact+
+
+ have nz': "f k z \<noteq> 0" for k
+ proof
+ assume "f k z = 0"
+ have "eventually (\<lambda>n. (\<Prod>k<n. f k z) = 0) sequentially"
+ using eventually_gt_at_top[of k] by eventually_elim (use \<open>f k z = 0\<close> in auto)
+ hence "(\<lambda>n. (\<Prod>k<n. f k z)) \<longlonglongrightarrow> 0"
+ by (rule tendsto_eventually)
+ with lim' have "P z = 0"
+ using tendsto_unique sequentially_bot by blast
+ with nz show False
+ by simp
+ qed
+
+ from lim have "(\<lambda>n. deriv (\<lambda>x. \<Prod>k<n. f k x) z) \<longlonglongrightarrow> deriv P z"
+ by (rule deriv_complex_uniform_limit)
+ (use A in \<open>auto intro!: always_eventually holomorphic_intros holo\<close>)
+ also have "(\<lambda>n. deriv (\<lambda>x. \<Prod>k<n. f k x) z) = (\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z))"
+ using \<open>z \<in> A\<close> by (auto intro!: ext DERIV_imp_deriv derivative_eq_intros simp: nz')
+ finally have "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z)) \<longlonglongrightarrow> deriv P z" .
+ hence "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z) / (\<Prod>k<n. f k z)) \<longlonglongrightarrow> deriv P z / P z"
+ by (intro tendsto_intros) (use nz lim' in auto)
+ also have "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z) / (\<Prod>k<n. f k z)) =
+ (\<lambda>n. (\<Sum>k<n. f' k z / f k z))"
+ by (simp add: nz')
+ finally show "(\<lambda>k. f' k z / f k z) sums (deriv P z / P z)"
+ unfolding sums_def .
+qed
+
text\<open> Version showing that the limit is the limit of the derivatives.\<close>
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy Tue Apr 22 17:35:13 2025 +0100
@@ -52,6 +52,26 @@
with assms show ?thesis by simp
qed
+lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
+proof -
+ define Q where
+ "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
+ define P where
+ "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
+ have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
+ by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
+ have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
+ using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
+ have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
+ using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
+ by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
+ thus ?thesis
+ by (simp add: residue_def P_def Q_def)
+qed
+
+lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
+ by (rule residue_shift_0)
+
lemma contour_integral_circlepath_eq:
assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
and e2_cball:"cball z e2 \<subseteq> s"
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Tue Apr 22 17:35:13 2025 +0100
@@ -68,6 +68,18 @@
using has_integral_unique
by (auto simp: has_contour_integral_def)
+lemma has_contour_integral_translate:
+ "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
+ by (simp add: has_contour_integral_def add_ac)
+
+lemma contour_integrable_translate:
+ "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
+ by (simp add: contour_integrable_on_def has_contour_integral_translate)
+
+lemma contour_integral_translate:
+ "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
+ by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
+
lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
using contour_integrable_on_def by blast
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Tue Apr 22 17:35:13 2025 +0100
@@ -4,80 +4,6 @@
begin
-instance fps :: (semiring_char_0) semiring_char_0
-proof
- show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
- proof
- fix m n :: nat
- assume "of_nat m = (of_nat n :: 'a fps)"
- hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
- by (simp only: )
- thus "m = n"
- by simp
- qed
-qed
-
-instance fls :: (semiring_char_0) semiring_char_0
-proof
- show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
- by (metis fls_regpart_of_nat injI of_nat_eq_iff)
-qed
-
-lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \<longleftrightarrow> c = 0"
- using fls_const_0 fls_const_nonzero by blast
-
-lemma fls_subdegree_add_eq1:
- assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
- shows "fls_subdegree (f + g) = fls_subdegree f"
-proof (intro antisym)
- from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
- by auto
- from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
- by (rule fls_subdegree_leI)
- from * have "f + g \<noteq> 0"
- using fls_nonzeroI by blast
- thus "fls_subdegree f \<le> fls_subdegree (f + g)"
- using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_add_eq2:
- assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
- shows "fls_subdegree (f + g) = fls_subdegree g"
-proof (intro antisym)
- from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
- by auto
- from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
- by (rule fls_subdegree_leI)
- from * have "f + g \<noteq> 0"
- using fls_nonzeroI by blast
- thus "fls_subdegree g \<le> fls_subdegree (f + g)"
- using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_diff_eq1:
- assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
- shows "fls_subdegree (f - g) = fls_subdegree f"
- using fls_subdegree_add_eq1[of f "-g"] assms by simp
-
-lemma fls_subdegree_diff_eq2:
- assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
- shows "fls_subdegree (f - g) = fls_subdegree g"
- using fls_subdegree_add_eq2[of "-g" f] assms by simp
-
-lemma nat_minus_fls_subdegree_plus_const_eq:
- "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
-proof (cases "fls_subdegree F < 0")
- case True
- hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
- by (intro fls_subdegree_add_eq1) auto
- thus ?thesis
- by simp
-next
- case False
- thus ?thesis
- by (auto simp: fls_subdegree_ge0I)
-qed
-
definition%important fls_conv_radius :: "complex fls \<Rightarrow> ereal" where
"fls_conv_radius f = fps_conv_radius (fls_regpart f)"
@@ -139,12 +65,6 @@
and eval_fps_of_int [simp]: "eval_fps (of_int m) z = of_int m"
by (simp_all flip: fps_of_nat fps_of_int)
-lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
- by (metis fls_subdegree_of_nat of_nat_numeral)
-
-lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
- by (metis fls_regpart_of_nat of_nat_numeral)
-
lemma fps_conv_radius_of_nat [simp]: "fps_conv_radius (of_nat n) = \<infinity>"
and fps_conv_radius_of_int [simp]: "fps_conv_radius (of_int m) = \<infinity>"
by (simp_all flip: fps_of_nat fps_of_int)
@@ -486,9 +406,6 @@
lemmas has_field_derivative_eval_fps' [derivative_intros] =
DERIV_chain2[OF has_field_derivative_eval_fps]
-lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
- by (intro fps_ext) (auto simp: add_ac)
-
(* TODO: generalise for nonneg subdegree *)
lemma has_field_derivative_eval_fls:
assumes "z \<in> eball 0 (fls_conv_radius f) - {0}"
@@ -1186,43 +1103,6 @@
shows "f has_fps_expansion fps_expansion f 0"
using assms has_fps_expansion_fps_expansion analytic_at by fast
-lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
-proof -
- have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
- if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
- proof -
- have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
- by (rule DERIV_chain that derivative_eq_intros refl)+ auto
- thus ?thesis by simp
- qed
- have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
- using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
- thus ?thesis
- by (simp add: deriv_def)
-qed
-
-lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
- by (rule deriv_shift_0)
-
-lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
-proof (induction n arbitrary: f)
- case (Suc n)
- have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
- by (subst funpow_Suc_right) auto
- also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
- by (subst Suc) (auto simp: o_def)
- also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
- by (subst deriv_shift_0) (auto simp: o_def)
- also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
- by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
- also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
- by (subst funpow_Suc_right) (auto simp: o_def)
- finally show ?case .
-qed auto
-
-lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
- by (rule higher_deriv_shift_0)
-
lemma analytic_at_imp_has_fps_expansion:
assumes "f analytic_on {z}"
shows "(\<lambda>x. f (z + x)) has_fps_expansion fps_expansion f z"
@@ -1624,49 +1504,6 @@
by (simp add: field_simps)
qed
-lemma vector_derivative_translate [simp]:
- "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
-proof -
- have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
- if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
- unfolding o_def using that by (auto intro!: derivative_eq_intros)
- from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
- unfolding vector_derivative_def
- by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
-qed
-
-lemma has_contour_integral_translate:
- "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
- by (simp add: has_contour_integral_def add_ac)
-
-lemma contour_integrable_translate:
- "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
- by (simp add: contour_integrable_on_def has_contour_integral_translate)
-
-lemma contour_integral_translate:
- "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
- by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
-
-lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
-proof -
- define Q where
- "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
- define P where
- "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
- have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
- by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
- have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
- using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
- have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
- using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
- by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
- thus ?thesis
- by (simp add: residue_def P_def Q_def)
-qed
-
-lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
- by (rule residue_shift_0)
-
lemma has_laurent_expansion_residue_0:
assumes "f has_laurent_expansion F"
shows "residue f 0 = fls_residue F"
@@ -1768,9 +1605,6 @@
by (simp add: fls_conv_radius_altdef G_def)
qed
-lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
- by (cases r) auto
-
lemma eval_fls_eqI:
assumes "f has_laurent_expansion F" "f holomorphic_on eball 0 r - {0}"
assumes "z \<in> eball 0 r - {0}"
@@ -1821,7 +1655,7 @@
lemma tendsto_0_subdegree_iff_0:
assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
- shows "(f \<midarrow>0\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+ shows "(f \<midarrow>0\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
proof -
have ?thesis if "is_pole f 0"
proof -
@@ -1872,15 +1706,15 @@
qed
lemma tendsto_0_subdegree_iff:
- assumes F:"(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F\<noteq>0"
- shows "(f \<midarrow>z\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+ assumes F: "(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F \<noteq> 0"
+ shows "(f \<midarrow>z\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
apply (subst Lim_at_zero)
apply (rule tendsto_0_subdegree_iff_0)
using assms by auto
lemma is_pole_0_deriv_divide_iff:
- assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
- shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow>0)"
+ assumes F: "f has_laurent_expansion F" and "F \<noteq> 0"
+ shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow> 0)"
proof -
have "(\<lambda>x. deriv f x / f x) has_laurent_expansion fls_deriv F / F"
using F by (auto intro:laurent_expansion_intros)
@@ -2396,43 +2230,6 @@
qed
qed
-lemma subdegree_fps_compose [simp]:
- fixes F G :: "'a :: idom fps"
- assumes [simp]: "fps_nth G 0 = 0"
- shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
-proof (cases "G = 0"; cases "F = 0")
- assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
- define m where "m = subdegree F"
- define F' where "F' = fps_shift m F"
- have F_eq: "F = F' * fps_X ^ m"
- unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
- have [simp]: "F' \<noteq> 0"
- using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
- have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
- by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
- also have "subdegree (fps_compose F' G) = 0"
- by (intro subdegree_eq_0) (auto simp: F'_def m_def)
- finally show ?thesis by (simp add: m_def)
-qed auto
-
-lemma fls_subdegree_power_int [simp]:
- fixes F :: "'a :: field fls"
- shows "fls_subdegree (F powi n) = n * fls_subdegree F"
- by (auto simp: power_int_def fls_subdegree_pow)
-
-lemma subdegree_fls_compose_fps [simp]:
- fixes G :: "'a :: field fps"
- assumes [simp]: "fps_nth G 0 = 0"
- shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
-proof (cases "F = 0"; cases "G = 0")
- assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
- have nz1: "fls_base_factor_to_fps F \<noteq> 0"
- using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
- show ?thesis
- unfolding fls_compose_fps_def using nz1
- by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
-qed (auto simp: fls_compose_fps_0_right)
-
lemma zorder_compose_aux:
assumes "isolated_singularity_at f 0" "not_essential f 0"
assumes G: "g has_fps_expansion G" "G \<noteq> 0" "g 0 = 0"
@@ -2595,4 +2392,64 @@
shows "(\<lambda>y. \<Prod>x\<in>#I. f x y) has_laurent_expansion (\<Prod>x\<in>#I. F x)"
using assms by (induction I) (auto intro!: laurent_expansion_intros)
+
+subsection \<open>Formal convergence versus analytic convergence\<close>
+
+
+text \<open>
+ The convergence of a sequence of formal power series and the convergence of the functions
+ in the complex plane do not imply each other:
+
+ \<^item> If we have the sequence of constant power series $(1/n)_{n\geq 0}$, this clearly converges
+ to the zero function analytically, but as a series of formal power series it is divergent
+ (since the 0-th coefficient never stabilises).
+
+ \<^item> Conversely, the sequence of series $(n! x^n)_{n\geq 0}$ converges formally to $0$,
+ but the corresponding sequence of functions diverges for every $x \neq 0$.
+
+ However, if the sequence of series converges to some limit series $h$ and the corresponding
+ series of functions converges uniformly to some limit function $g(x)$, then $h$ is also a
+ series expansion of $g(x)$, i.e.\ in that case, formal and analytic convergence agree.
+\<close>
+proposition uniform_limit_imp_fps_expansion_eq:
+ fixes f :: "'a \<Rightarrow> complex fps"
+ assumes lim1: "(f \<longlongrightarrow> h) F"
+ assumes lim2: "uniform_limit A (\<lambda>x z. f' x z) g' F"
+ assumes expansions: "eventually (\<lambda>x. f' x has_fps_expansion f x) F" "g' has_fps_expansion g"
+ assumes holo: "eventually (\<lambda>x. f' x holomorphic_on A) F"
+ assumes A: "open A" "0 \<in> A"
+ assumes nontriv [simp]: "F \<noteq> bot"
+ shows "g = h"
+proof (rule fps_ext)
+ fix n :: nat
+ have "eventually (\<lambda>x. fps_nth (f x) n = fps_nth h n) F"
+ using lim1 unfolding tendsto_fps_iff by blast
+ hence "eventually (\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n = fps_nth h n) F"
+ using expansions(1)
+ proof eventually_elim
+ case (elim x)
+ have "fps_nth (f x) n = (deriv ^^ n) (f' x) 0 / fact n"
+ by (rule fps_nth_fps_expansion) (use elim in auto)
+ with elim show ?case
+ by simp
+ qed
+ hence "((\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n) \<longlongrightarrow> fps_nth h n) F"
+ by (simp add: tendsto_eventually)
+
+ moreover have "((\<lambda>x. (deriv ^^ n) (f' x) 0) \<longlongrightarrow> (deriv ^^ n) g' 0) F"
+ using lim2
+ proof (rule higher_deriv_complex_uniform_limit)
+ show "eventually (\<lambda>x. f' x holomorphic_on A) F"
+ using holo by eventually_elim auto
+ qed (use A in auto)
+ hence "((\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n) \<longlongrightarrow> (deriv ^^ n) g' 0 / fact n) F"
+ by (intro tendsto_divide) auto
+
+ ultimately have "fps_nth h n = (deriv ^^ n) g' 0 / fact n"
+ using tendsto_unique[OF nontriv] by blast
+ also have "\<dots> = fps_nth g n"
+ by (rule fps_nth_fps_expansion [symmetric]) fact
+ finally show "fps_nth g n = fps_nth h n" ..
+qed
+
end
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Tue Apr 22 17:35:13 2025 +0100
@@ -1165,6 +1165,58 @@
shows "fls_const x * fls_const y = fls_const (x*y)"
by (intro fls_eqI) simp
+lemma fls_subdegree_add_eq1:
+ assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+ shows "fls_subdegree (f + g) = fls_subdegree f"
+proof (intro antisym)
+ from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
+ by auto
+ from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
+ by (rule fls_subdegree_leI)
+ from * have "f + g \<noteq> 0"
+ using fls_nonzeroI by blast
+ thus "fls_subdegree f \<le> fls_subdegree (f + g)"
+ using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_add_eq2:
+ assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+ shows "fls_subdegree (f + g) = fls_subdegree g"
+proof (intro antisym)
+ from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
+ by auto
+ from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
+ by (rule fls_subdegree_leI)
+ from * have "f + g \<noteq> 0"
+ using fls_nonzeroI by blast
+ thus "fls_subdegree g \<le> fls_subdegree (f + g)"
+ using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_diff_eq1:
+ assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+ shows "fls_subdegree (f - g) = fls_subdegree f"
+ using fls_subdegree_add_eq1[of f "-g"] assms by simp
+
+lemma fls_subdegree_diff_eq2:
+ assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+ shows "fls_subdegree (f - g) = fls_subdegree g"
+ using fls_subdegree_add_eq2[of "-g" f] assms by simp
+
+lemma nat_minus_fls_subdegree_plus_const_eq:
+ "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
+proof (cases "fls_subdegree F < 0")
+ case True
+ hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
+ by (intro fls_subdegree_add_eq1) auto
+ thus ?thesis
+ by simp
+next
+ case False
+ thus ?thesis
+ by (auto simp: fls_subdegree_ge0I)
+qed
+
lemma fls_mult_subdegree_ge:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f*g \<noteq> 0"
@@ -1705,6 +1757,13 @@
by standard
+lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
+ by (metis fls_subdegree_of_nat of_nat_numeral)
+
+lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
+ by (metis fls_regpart_of_nat of_nat_numeral)
+
+
subsubsection \<open>Powers\<close>
lemma fls_subdegree_prod:
@@ -2946,6 +3005,20 @@
instance fls :: ("{field_prime_char,comm_semiring_1}") field_prime_char
by (rule field_prime_charI') auto
+instance fls :: (semiring_char_0) semiring_char_0
+proof
+ show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
+ by (metis fls_regpart_of_nat injI of_nat_eq_iff)
+qed
+
+instance fls :: (field_char_0) field_char_0 ..
+
+
+lemma fls_subdegree_power_int [simp]:
+ fixes F :: "'a :: field fls"
+ shows "fls_subdegree (F powi n) = n * fls_subdegree F"
+ by (auto simp: power_int_def fls_subdegree_pow)
+
subsubsection \<open>Division\<close>
@@ -3440,45 +3513,6 @@
shows "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H"
using fls_compose_fps_add[of H F "-G"] by simp
-lemma fps_compose_eq_0_iff:
- fixes F G :: "'a :: idom fps"
- assumes "fps_nth G 0 = 0"
- shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
-proof safe
- assume *: "fps_compose F G = 0" "F \<noteq> 0"
- have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
- by simp
- also have "fps_compose F G = 0"
- by (simp add: *)
- finally show "fps_nth F 0 = 0"
- by simp
- show "G = 0"
- proof (rule ccontr)
- assume "G \<noteq> 0"
- hence "subdegree G > 0" using assms
- using subdegree_eq_0_iff by blast
- define N where "N = subdegree F * subdegree G"
- have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
- unfolding fps_compose_def by (simp add: N_def)
- also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
- proof (intro sum.mono_neutral_right ballI)
- fix i assume i: "i \<in> {0..N} - {subdegree F}"
- show "fps_nth F i * fps_nth (G ^ i) N = 0"
- proof (cases i "subdegree F" rule: linorder_cases)
- assume "i > subdegree F"
- hence "fps_nth (G ^ i) N = 0"
- using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
- thus ?thesis by simp
- qed (use i in \<open>auto simp: N_def\<close>)
- qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
- also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
- by simp
- also have "\<dots> \<noteq> 0"
- using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
- finally show False using * by auto
- qed
-qed auto
-
lemma fls_compose_fps_eq_0_iff:
assumes "H \<noteq> 0" "fps_nth H 0 = 0"
shows "fls_compose_fps F H = 0 \<longleftrightarrow> F = 0"
@@ -3588,7 +3622,7 @@
assumes "d > 0"
shows "fls_compose_power f d $$ n = (if int d dvd n then f $$ (n div int d) else 0)"
by (simp add: assms fls_compose_power.rep_eq)
-
+
lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0"
by transfer auto
@@ -3680,6 +3714,20 @@
"d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_compose_power f d $$ int n = f $$ int (n div d)"
by (transfer; force; fail)+
+lemma subdegree_fls_compose_fps [simp]:
+ fixes G :: "'a :: field fps"
+ assumes [simp]: "fps_nth G 0 = 0"
+ shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
+proof (cases "F = 0"; cases "G = 0")
+ assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+ have nz1: "fls_base_factor_to_fps F \<noteq> 0"
+ using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
+ show ?thesis
+ unfolding fls_compose_fps_def using nz1
+ by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
+qed (auto simp: fls_compose_fps_0_right)
+
+
subsection \<open>Formal differentiation and integration\<close>
subsubsection \<open>Derivative\<close>
@@ -3747,6 +3795,9 @@
shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"
by (auto intro: fls_subdegree_deriv' simp: assms)
+lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
+ by (intro fps_ext) (auto simp: add_ac)
+
text \<open>
Shifting is like multiplying by a power of the implied variable, and so satisfies a product-like
rule.
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Apr 22 17:35:13 2025 +0100
@@ -11,6 +11,8 @@
Complex_Main
Euclidean_Algorithm
Primes
+ "HOL-Library.FuncSet"
+ "HOL-Library.Multiset"
begin
@@ -748,6 +750,19 @@
from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
qed
+instance fps :: (semiring_char_0) semiring_char_0
+proof
+ show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
+ proof
+ fix m n :: nat
+ assume "of_nat m = (of_nat n :: 'a fps)"
+ hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
+ by (simp only: )
+ thus "m = n"
+ by simp
+ qed
+qed
+
lemma subdegree_power_ge:
"f^n \<noteq> 0 \<Longrightarrow> subdegree (f^n) \<ge> n * subdegree f"
proof (induct n)
@@ -801,6 +816,12 @@
"subdegree ((f :: ('a :: semiring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
by (cases "f = 0"; induction n) simp_all
+lemma subdegree_prod:
+ fixes f :: "'a \<Rightarrow> 'b :: idom fps"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "subdegree (\<Prod>x\<in>A. f x) = (\<Sum>x\<in>A. subdegree (f x))"
+ using assms by (induction A rule: infinite_finite_induct) auto
+
lemma minus_one_power_iff: "(- (1::'a::ring_1)) ^ n = (if even n then 1 else - 1)"
by (induct n) auto
@@ -1325,6 +1346,15 @@
"k < n \<Longrightarrow> (fps_cutoff n f * g) $ k = (f * g) $ k"
by (simp add: fps_mult_nth)
+lemma fps_cutoff_add: "fps_cutoff n (f + g :: 'a :: monoid_add fps) = fps_cutoff n f + fps_cutoff n g"
+ by (auto simp: fps_eq_iff)
+
+lemma fps_cutoff_diff: "fps_cutoff n (f - g :: 'a :: group_add fps) = fps_cutoff n f - fps_cutoff n g"
+ by (auto simp: fps_eq_iff)
+
+lemma fps_cutoff_uminus: "fps_cutoff n (-f :: 'a :: group_add fps) = -fps_cutoff n f"
+ by (auto simp: fps_eq_iff)
+
lemma fps_cutoff_right_mult_nth:
assumes "k < n"
shows "(f * fps_cutoff n g) $ k = (f * g) $ k"
@@ -1333,6 +1363,22 @@
thus ?thesis by (simp add: fps_mult_nth)
qed
+lemma fps_cutoff_eq_fps_cutoff_iff:
+ "fps_cutoff n f = fps_cutoff n g \<longleftrightarrow> (\<forall>k<n. fps_nth f k = fps_nth g k)"
+ by (subst fps_eq_iff) auto
+
+lemma fps_conv_fps_X_power_mult_fps_shift:
+ assumes "f = 0 \<or> subdegree f \<ge> n"
+ shows "f = fps_X ^ n * fps_shift n f"
+proof -
+ have "f = fps_X ^ n * fps_shift n f + fps_cutoff n f"
+ by (auto simp: fps_eq_iff fps_X_power_mult_nth)
+ also have "fps_cutoff n f = 0"
+ by (subst fps_cutoff_zero_iff) (use assms in auto)
+ finally show ?thesis by simp
+qed
+
+
subsection \<open>Metrizability\<close>
instantiation fps :: ("{minus,zero}") dist
@@ -1402,6 +1448,156 @@
lemma open_fps_def: "open (S :: 'a::group_add fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)"
unfolding open_dist subset_eq by simp
+
+text \<open>Topology\<close>
+
+subsection \<open>The topology of formal power series\<close>
+
+text \<open>
+ A set of formal power series is open iff for any power series $f$ in it, there exists some
+ number $n$ such that all power series that agree with $f$ on the first $n$ components are
+ also in it.
+\<close>
+lemma open_fps_iff:
+ "open A \<longleftrightarrow> (\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A)"
+proof
+ assume "open A"
+ show "\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
+ proof
+ fix F :: "'a fps"
+ assume F: "F \<in> A"
+ with \<open>open A\<close> obtain e where e: "e > 0" "\<And>G. dist G F < e \<Longrightarrow> G \<in> A"
+ by (force simp: open_fps_def)
+ thm dist_fps_def
+ have "filterlim (\<lambda>n. (1/2)^n :: real) (nhds 0) at_top"
+ by (intro LIMSEQ_realpow_zero) auto
+ from order_tendstoD(2)[OF this e(1)] have "eventually (\<lambda>n. 1 / 2 ^ n < e) at_top"
+ by (simp add: power_divide)
+ then obtain n where n: "1 / 2 ^ n < e"
+ by (auto simp: eventually_sequentially)
+ show "\<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
+ proof (rule exI[of _ n], safe)
+ fix G assume *: "fps_cutoff n G = fps_cutoff n F"
+ show "G \<in> A"
+ proof (cases "G = F")
+ case False
+ hence "dist G F = inverse (2 ^ subdegree (G - F))"
+ by (auto simp: dist_fps_def)
+ also have "subdegree (G - F) \<ge> n"
+ proof (rule subdegree_geI)
+ fix i assume "i < n"
+ hence "fps_nth (G - F) i = fps_nth (fps_cutoff n G - fps_cutoff n F) i"
+ by (auto simp: fps_eq_iff)
+ also from * have "\<dots> = 0"
+ by simp
+ finally show "fps_nth (G - F) i = 0" .
+ qed (use False in auto)
+ hence "inverse (2 ^ subdegree (G - F) :: real) \<le> inverse (2 ^ n)"
+ by (intro le_imp_inverse_le power_increasing) auto
+ also have "\<dots> < e"
+ using n by (simp add: field_simps)
+ finally show "G \<in> A"
+ using e(2)[of G] by auto
+ qed (use \<open>F \<in> A\<close> in auto)
+ qed
+ qed
+next
+ assume *: "\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
+ show "open A"
+ unfolding open_fps_def
+ proof safe
+ fix F assume F: "F \<in> A"
+ with * obtain n where n: "\<And>G. fps_cutoff n G = fps_cutoff n F \<Longrightarrow> G \<in> A"
+ by blast
+ show "\<exists>r>0. {G. dist G F < r} \<subseteq> A"
+ proof (rule exI[of _ "1 / 2 ^ n"], safe)
+ fix G assume dist: "dist G F < 1 / 2 ^ n"
+ show "G \<in> A"
+ proof (cases "G = F")
+ case False
+ hence "dist G F = inverse (2 ^ subdegree (F - G))"
+ by (simp add: dist_fps_def)
+ with dist have "n < subdegree (F - G)"
+ by (auto simp: field_simps)
+ hence "fps_nth (F - G) i = 0" if "i \<le> n" for i
+ using that nth_less_subdegree_zero[of i "F - G"] by simp
+ hence "fps_cutoff n G = fps_cutoff n F"
+ by (auto simp: fps_eq_iff fps_cutoff_def)
+ thus "G \<in> A"
+ by (rule n)
+ qed (use \<open>F \<in> A\<close> in auto)
+ qed auto
+ qed
+qed
+
+lemma open_fps_cutoff: "open {H. fps_cutoff N H = fps_cutoff N G}"
+ unfolding open_fps_iff
+proof safe
+ fix F assume F: "fps_cutoff N F = fps_cutoff N G"
+ show "\<exists>n. {G. fps_cutoff n G = fps_cutoff n F}
+ \<subseteq> {H. fps_cutoff N H = fps_cutoff N G}"
+ by (rule exI[of _ N]) (use F in \<open>auto simp: fps_eq_iff\<close>)
+qed
+
+lemma eventually_fps_nth_eq_nhds_fps_strong:
+ "eventually (\<lambda>g. \<forall>k\<le>n. fps_nth g k = fps_nth f k) (nhds f)"
+proof -
+ have "eventually (\<lambda>g. g \<in> {g. fps_cutoff (n+1) g = fps_cutoff (n+1) f}) (nhds f)"
+ by (rule eventually_nhds_in_open, rule open_fps_cutoff) auto
+ thus ?thesis
+ by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff)
+qed
+
+lemma eventually_fps_nth_eq_nhds_fps: "eventually (\<lambda>g. fps_nth g k = fps_nth f k) (nhds f)"
+ using eventually_fps_nth_eq_nhds_fps_strong[of k] by eventually_elim auto
+
+text \<open>
+ A family of formal power series $f_x$ tends to a limit series $g$ at some filter $F$
+ iff for any $N\geq 0$, the set of $x$ for which $f_x$ and $G$ agree on the first $N$ coefficients
+ is in $F$.
+
+ For a sequence $(f_i)_{n\geq 0}$ this means that $f_i \longrightarrow G$ iff for any
+ $N\geq 0$, $f_x$ and $G$ agree for all but finitely many $x$.
+\<close>
+
+lemma tendsto_fps_iff:
+ "filterlim f (nhds (g :: 'a :: group_add fps)) F \<longleftrightarrow>
+ (\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F)"
+proof safe
+ assume lim: "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+ show "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F" for n
+ proof -
+ define S where "S = {H. fps_cutoff (n+1) H = fps_cutoff (n+1) g}"
+ have S: "open S" "g \<in> S"
+ unfolding S_def using open_fps_cutoff[of "n+1" g] by (auto simp: S_def)
+ from lim and S have "eventually (\<lambda>x. f x \<in> S) F"
+ using topological_tendstoD by blast
+ thus "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+ by eventually_elim (auto simp: S_def fps_cutoff_eq_fps_cutoff_iff)
+ qed
+next
+ assume *: "\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+ show "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+ proof (rule topological_tendstoI)
+ fix S :: "'a fps set"
+ assume S: "open S" "g \<in> S"
+ then obtain N where N: "{H. fps_cutoff N H = fps_cutoff N g} \<subseteq> S"
+ unfolding open_fps_iff by blast
+ have "eventually (\<lambda>x. \<forall>n\<in>{..<N}. fps_nth (f x) n = fps_nth g n) F"
+ by (subst eventually_ball_finite_distrib) (use * in auto)
+ hence "eventually (\<lambda>x. f x \<in> {H. fps_cutoff N H = fps_cutoff N g}) F"
+ by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff)
+ thus "eventually (\<lambda>x. f x \<in> S) F"
+ by eventually_elim (use N in auto)
+ qed
+qed
+
+lemma tendsto_fpsI:
+ assumes "\<And>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth G n) F"
+ shows "filterlim f (nhds (G :: 'a :: group_add fps)) F"
+ unfolding tendsto_fps_iff using assms by blast
+
+
text \<open>The infinite sums and justification of the notation in textbooks.\<close>
lemma reals_power_lt_ex:
@@ -2030,6 +2226,9 @@
lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g"
by (simp add: fps_inverse_mult_divring)
+lemma inverse_prod_fps: "inverse (prod f A) = (\<Prod>x\<in>A. inverse (f x) :: 'a :: field fps)"
+ by (induction A rule: infinite_finite_induct) (auto simp: fps_inverse_mult)
+
lemma fps_lr_inverse_gp_ring1:
fixes ones ones_inv :: "'a :: ring_1 fps"
defines "ones \<equiv> Abs_fps (\<lambda>n. 1)"
@@ -2252,6 +2451,92 @@
using subdegree_lr_inverse(2)
by (simp add: fps_inverse_def)
+lemma fps_right_inverse_constructor_rec:
+ "n > 0 \<Longrightarrow> fps_right_inverse_constructor f a n =
+ -a * sum (\<lambda>i. fps_nth f i * fps_right_inverse_constructor f a (n - i)) {1..n}"
+ by (cases n) auto
+
+lemma fps_right_inverse_constructor_cong:
+ assumes "\<And>k. k \<le> n \<Longrightarrow> fps_nth f k = fps_nth g k"
+ shows "fps_right_inverse_constructor f c n = fps_right_inverse_constructor g c n"
+ using assms
+proof (induction n rule: less_induct)
+ case (less n)
+ show ?case
+ proof (cases "n > 0")
+ case n: True
+ have "fps_right_inverse_constructor f c n =
+ -c * sum (\<lambda>i. fps_nth f i * fps_right_inverse_constructor f c (n - i)) {1..n}"
+ by (subst fps_right_inverse_constructor_rec) (use n in auto)
+ also have "sum (\<lambda>i. fps_nth f i * fps_right_inverse_constructor f c (n - i)) {1..n} =
+ sum (\<lambda>i. fps_nth g i * fps_right_inverse_constructor g c (n - i)) {1..n}"
+ by (intro sum.cong refl arg_cong2[of _ _ _ _ "(*)"] less) (use assms in auto)
+ also have "-c * \<dots> = fps_right_inverse_constructor g c n"
+ by (subst (2) fps_right_inverse_constructor_rec) (use n in auto)
+ finally show ?thesis .
+ qed auto
+qed
+
+lemma fps_cutoff_inverse:
+ fixes f :: "'a :: field fps"
+ assumes "fps_nth f 0 \<noteq> 0"
+ shows "fps_cutoff n (inverse (fps_cutoff n f)) = fps_cutoff n (inverse f)"
+proof (cases "n = 0")
+ case True
+ show ?thesis
+ by (simp add: True)
+next
+ case False
+ show ?thesis
+ proof (subst fps_cutoff_eq_fps_cutoff_iff, safe)
+ fix k assume "k < n"
+ have "fps_nth (inverse (fps_cutoff n f)) k =
+ fps_right_inverse_constructor (fps_cutoff n f) (inverse (fps_nth f 0)) k"
+ using False by (simp add: fps_inverse_def)
+ also have "\<dots> = fps_right_inverse_constructor f (inverse (fps_nth f 0)) k"
+ by (rule fps_right_inverse_constructor_cong) (use \<open>k < n\<close> in auto)
+ also have "\<dots> = fps_nth (inverse f) k"
+ using False by (simp add: fps_inverse_def)
+ finally show "fps_nth (inverse (fps_cutoff n f)) k = fps_nth (inverse f) k" .
+ qed
+qed
+
+lemma tendsto_inverse_fps_aux:
+ fixes f :: "'a :: field fps"
+ assumes "fps_nth f 0 \<noteq> 0"
+ shows "((\<lambda>f. inverse f) \<longlongrightarrow> inverse f) (at f)"
+ unfolding tendsto_fps_iff
+proof
+ fix n :: nat
+ have "eventually (\<lambda>g. \<forall>k\<le>n. fps_nth g k = fps_nth f k) (nhds f)"
+ by (rule eventually_fps_nth_eq_nhds_fps_strong)
+ hence "eventually (\<lambda>g. \<forall>k\<le>n. fps_nth g k = fps_nth f k) (at f)"
+ using eventually_nhds_conv_at by blast
+ thus "eventually (\<lambda>g. fps_nth (inverse g) n = fps_nth (inverse f) n) (at f)"
+ proof eventually_elim
+ case (elim g)
+ from elim have "fps_nth g 0 = fps_nth f 0"
+ by auto
+ with assms have [simp]: "fps_nth g 0 \<noteq> 0"
+ by simp
+ have "fps_cutoff (n+1) (inverse f) = fps_cutoff (n+1) (inverse (fps_cutoff (n+1) f))"
+ by (rule fps_cutoff_inverse [symmetric]) fact
+ also have "fps_cutoff (n+1) f = fps_cutoff (n+1) g"
+ by (subst fps_cutoff_eq_fps_cutoff_iff) (use elim in auto)
+ also have "fps_cutoff (n+1) (inverse \<dots>) = fps_cutoff (n+1) (inverse g)"
+ by (rule fps_cutoff_inverse) auto
+ finally show ?case
+ by (subst (asm) fps_cutoff_eq_fps_cutoff_iff) auto
+ qed
+qed
+
+lemma tendsto_inverse_fps [tendsto_intros]:
+ fixes g :: "'a :: field fps"
+ assumes "(f \<longlongrightarrow> g) F"
+ assumes "fps_nth g 0 \<noteq> 0"
+ shows "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse g) F"
+ by (rule tendsto_compose[OF tendsto_inverse_fps_aux assms(1)]) fact
+
lemma fps_div_zero [simp]:
"0 div (g :: 'a :: {comm_monoid_add,inverse,mult_zero,uminus} fps) = 0"
by (simp add: fps_divide_def)
@@ -2863,6 +3148,105 @@
end
+subsection \<open>Computing reciprocals via Hensel lifting\<close>
+
+lemma inverse_fps_hensel_lifting:
+ fixes F G :: "'a :: field fps" and n :: nat
+ assumes G_eq: "fps_cutoff n G = fps_cutoff n (inverse F)"
+ assumes unit: "fps_nth F 0 \<noteq> 0"
+ shows "fps_cutoff (2*n) (inverse F) = fps_cutoff (2*n) (G * (2 - F * G))"
+proof -
+ define R where "R = inverse F - G"
+ have eq: "G = inverse F - R"
+ by (simp add: R_def)
+ from assms have "fps_cutoff n R = 0"
+ by (simp add: R_def fps_cutoff_diff)
+ hence R: "R = 0 \<or> subdegree R \<ge> n"
+ by (simp add: fps_cutoff_zero_iff)
+
+ have "G * (2 - F * G) - inverse F =
+ inverse F + F * inverse F * R * 2 - F * R\<^sup>2 - R * 2 - F * inverse F * inverse F"
+ by (simp add: eq algebra_simps power2_eq_square)
+ also have "F * inverse F = 1"
+ using unit by (simp add: inverse_mult_eq_1')
+ also have "inverse F + 1 * R * 2 - F * R\<^sup>2 - R * 2 - 1 * inverse F = -F * R\<^sup>2"
+ by (simp add: algebra_simps)
+ finally have "fps_cutoff (2*n) (G * (2 - F * G) - inverse F) = fps_cutoff (2*n) (-F * R\<^sup>2)"
+ by (rule arg_cong)
+ also have "\<dots> = 0"
+ proof (cases "-F * R\<^sup>2 = 0")
+ case False
+ have "2 * n \<le> subdegree (-F * R\<^sup>2)"
+ using False R unit by simp
+ thus ?thesis
+ by (simp add: fps_cutoff_zero_iff)
+ qed auto
+ finally show ?thesis
+ by (simp add: fps_cutoff_diff)
+qed
+
+lemma inverse_fps_hensel_lifting':
+ fixes F G :: "'a :: field fps" and n :: nat
+ assumes G_eq: "fps_cutoff n G = fps_cutoff n (inverse F)"
+ assumes unit: "fps_nth F 0 \<noteq> 0"
+ defines "P \<equiv> fps_shift n (F * G - 1)"
+ shows "fps_cutoff (2*n) (inverse F) = fps_cutoff (2*n) (G * (1 - fps_X ^ n * P))"
+proof -
+ define R where "R = inverse F - G"
+ have eq: "G = inverse F - R"
+ by (simp add: R_def)
+ from assms have "fps_cutoff n R = 0"
+ by (simp add: R_def fps_cutoff_diff)
+ hence R: "R = 0 \<or> subdegree R \<ge> n"
+ by (simp add: fps_cutoff_zero_iff)
+
+ have FG_eq: "F * G = 1 + fps_X ^ n * P"
+ proof (cases "F * G - 1 = 0")
+ case False
+ have eq: "F * G - 1 = F * (G - inverse F)"
+ using unit by (simp add: inverse_mult_eq_1' ring_distribs)
+ have "subdegree (F * (G - inverse F)) \<ge> n"
+ proof -
+ have "fps_cutoff n (G - inverse F) = 0"
+ using G_eq by (simp add: fps_cutoff_diff)
+ hence "n \<le> subdegree (G - inverse F)"
+ using False unfolding eq by (simp add: fps_cutoff_zero_iff)
+ also have "subdegree (G - inverse F) = subdegree (F * (G - inverse F))"
+ by (subst subdegree_mult) (use unit False in \<open>auto simp: eq\<close>)
+ finally have "n \<le> subdegree (F * (G - inverse F))" .
+ thus ?thesis
+ by blast
+ qed
+ hence "F * G - 1 = fps_X ^ n * P"
+ unfolding eq P_def by (intro fps_conv_fps_X_power_mult_fps_shift) auto
+ thus ?thesis
+ by (simp add: algebra_simps)
+ qed (auto simp: P_def)
+
+ have "G * (1 - fps_X ^ n * P) - inverse F = G * (2 - F * G) - inverse F"
+ by (auto simp: FG_eq)
+ also have "G * (2 - F * G) - inverse F =
+ inverse F + F * inverse F * R * 2 - F * R\<^sup>2 - R * 2 - F * inverse F * inverse F"
+ by (simp add: eq algebra_simps power2_eq_square)
+ also have "F * inverse F = 1"
+ using unit by (simp add: inverse_mult_eq_1')
+ also have "inverse F + 1 * R * 2 - F * R\<^sup>2 - R * 2 - 1 * inverse F = -F * R\<^sup>2"
+ by (simp add: algebra_simps)
+ finally have "fps_cutoff (2*n) (G * (1 - fps_X ^ n * P) - inverse F) = fps_cutoff (2*n) (-F * R\<^sup>2)"
+ by (rule arg_cong)
+ also have "\<dots> = 0"
+ proof (cases "-F * R\<^sup>2 = 0")
+ case False
+ have "2 * n \<le> subdegree (-F * R\<^sup>2)"
+ using False R unit by simp
+ thus ?thesis
+ by (simp add: fps_cutoff_zero_iff)
+ qed auto
+ finally show ?thesis
+ by (simp add: fps_cutoff_diff)
+qed
+
+
subsection \<open>Euclidean division\<close>
instantiation fps :: (field) euclidean_ring_cancel
@@ -3447,6 +3831,165 @@
by (simp add: fps_deriv_power' fps_of_nat)
+subsection \<open>Finite and infinite products\<close>
+
+lemma fps_prod_nth':
+ assumes "finite A"
+ shows "fps_nth (\<Prod>x\<in>A. f x) n = (\<Sum>X\<in>multisets_of_size A n. \<Prod>x\<in>A. fps_nth (f x) (count X x))"
+ using assms
+proof (induction A arbitrary: n rule: finite_induct)
+ case (insert a A n)
+ note [simp] = \<open>a \<notin> A\<close>
+ note [intro, simp] = \<open>finite A\<close>
+ have "(\<Sum>X\<in>multisets_of_size (insert a A) n. \<Prod>x\<in>insert a A. fps_nth (f x) (count X x)) =
+ (\<Sum>(m,X)\<in>(SIGMA m:{0..n}. multisets_of_size A (n-m)).
+ \<Prod>x\<in>insert a A. fps_nth (f x) (count (X + replicate_mset m a) x))"
+ by (subst sum.reindex_bij_betw[OF bij_betw_multisets_of_size_insert, symmetric])
+ (simp_all add: case_prod_unfold)
+ also have "\<dots> = (\<Sum>m=0..n. \<Sum>X\<in>multisets_of_size A (n-m).
+ \<Prod>x\<in>insert a A. fps_nth (f x) (count (X + replicate_mset m a) x))"
+ by (rule sum.Sigma [symmetric]) auto
+ also have "\<dots> = (\<Sum>m=0..n. fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m))"
+ proof (rule sum.cong)
+ fix m
+ assume m: "m \<in> {0..n}"
+ have "(\<Sum>X\<in>multisets_of_size A (n-m).
+ \<Prod>x\<in>insert a A. fps_nth (f x) (count (X + replicate_mset m a) x)) =
+ (\<Sum>X\<in>multisets_of_size A (n-m). fps_nth (f a) (count X a + m) *
+ (\<Prod>x\<in>A. fps_nth (f x) (count (X + replicate_mset m a) x)))"
+ by simp
+ also have "\<dots> = (\<Sum>X\<in>multisets_of_size A (n-m). fps_nth (f a) m *
+ (\<Prod>x\<in>A. fps_nth (f x) (count (X + replicate_mset m a) x)))"
+ by (intro sum.cong arg_cong2[of _ _ _ _ "(*)"] arg_cong2[of _ _ _ _ fps_nth] refl)
+ (auto simp: multisets_of_size_def simp flip: not_in_iff)
+ also have "\<dots> = fps_nth (f a) m * (\<Sum>X\<in>multisets_of_size A (n-m).
+ (\<Prod>x\<in>A. fps_nth (f x) (count (X + replicate_mset m a) x)))"
+ by (simp add: sum_distrib_left)
+ also have "(\<Sum>X\<in>multisets_of_size A (n-m). \<Prod>x\<in>A. fps_nth (f x) (count (X + replicate_mset m a) x)) =
+ (\<Sum>X\<in>multisets_of_size A (n-m). \<Prod>x\<in>A. fps_nth (f x) (count X x))"
+ by (intro sum.cong prod.cong) auto
+ also have "\<dots> = fps_nth (\<Prod>x\<in>A. f x) (n - m)"
+ by (rule insert.IH [symmetric])
+ finally show "(\<Sum>X\<in>multisets_of_size A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) (count (X + replicate_mset m a) x)) =
+ fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m)" .
+ qed auto
+ also have "\<dots> = fps_nth (\<Prod>x\<in>insert a A. f x) n"
+ by (simp add: fps_mult_nth)
+ finally show ?case ..
+qed auto
+
+theorem tendsto_prod_fps:
+ fixes f :: "nat \<Rightarrow> 'a :: {idom, t2_space} fps"
+ assumes [simp]: "\<And>k. f k \<noteq> 0"
+ assumes g: "\<And>n k. k > g n \<Longrightarrow> subdegree (f k - 1) > n"
+ defines "P \<equiv> Abs_fps (\<lambda>n. (\<Sum>X\<in>multisets_of_size {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (count X i)))"
+ shows "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> P"
+proof (rule tendsto_fpsI)
+ fix n :: nat
+ show "eventually (\<lambda>N. fps_nth (prod f {..N}) n = fps_nth P n) at_top"
+ using eventually_ge_at_top[of "g n"]
+ proof eventually_elim
+ case (elim N)
+ have "fps_nth (prod f {..N}) n = (\<Sum>X\<in>multisets_of_size {..N} n. \<Prod>x\<le>N. fps_nth (f x) (count X x))"
+ by (subst fps_prod_nth') auto
+ also have "\<dots> = (\<Sum>X | X \<in> multisets_of_size {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0).
+ \<Prod>x\<le>N. fps_nth (f x) (count X x))"
+ by (intro sum.mono_neutral_right) auto
+
+ also have "{X. X \<in> multisets_of_size {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0)} =
+ {X. X \<in> multisets_of_size {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0)}"
+ (is "?lhs = ?rhs")
+ proof (intro equalityI subsetI)
+ fix X assume "X \<in> ?rhs"
+ thus "X \<in> ?lhs" using elim multisets_of_size_mono[of "{..g n}" "{..N}"] by auto
+ next
+ fix X assume "X \<in> ?lhs"
+ hence X: "set_mset X \<subseteq> {..N}" "size X = n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (count X x) \<noteq> 0"
+ by (auto simp: multisets_of_size_def)
+ have "set_mset X \<subseteq> {..g n}"
+ proof
+ fix x assume *: "x \<in> set_mset X"
+ show "x \<in> {..g n}"
+ proof (rule ccontr)
+ assume "x \<notin> {..g n}"
+ hence x: "x > g n" "x \<le> N"
+ using X(1) * by auto
+ have "count X x \<le> n"
+ using X x count_le_size[of X x] by (auto simp: Pi_def)
+ also have "n < subdegree (f x - 1)"
+ by (rule g) (use x in auto)
+ finally have "fps_nth (f x - 1) (count X x) = 0"
+ by blast
+ hence "fps_nth (f x) (count X x) = 0"
+ using * by simp
+ moreover have "fps_nth (f x) (count X x) \<noteq> 0"
+ by (intro X(3)) (use x in auto)
+ ultimately show False by contradiction
+ qed
+ qed
+ thus "X \<in> ?rhs" using X
+ by (auto simp: multisets_of_size_def)
+ qed
+
+ also have "(\<Sum>X | X \<in> multisets_of_size {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0).
+ \<Prod>x\<le>N. fps_nth (f x) (count X x)) =
+ (\<Sum>X | X \<in> multisets_of_size {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0).
+ \<Prod>i\<le>g n. fps_nth (f i) (count X i))"
+ proof (intro sum.cong prod.mono_neutral_right ballI)
+ fix X i
+ assume i: "i \<in> {..N} - {..g n}"
+ assume "X \<in> {X. X \<in> multisets_of_size {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0)}"
+ hence h: "X \<in> multisets_of_size {..g n} n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (count X x) \<noteq> 0"
+ by blast+
+ have "i \<notin># X"
+ using i h unfolding multisets_of_size_def by auto
+ have "n < subdegree (f i - 1)"
+ by (intro g) (use i in auto)
+ moreover have "count X i \<le> n"
+ using \<open>i \<notin># X\<close> by (simp add: not_in_iff)
+ ultimately have "fps_nth (f i - 1) (count X i) = 0"
+ by (intro nth_less_subdegree_zero) auto
+ thus "fps_nth (f i) (count X i) = 1"
+ using h(2) i \<open>i \<notin># X\<close> by (auto split: if_splits)
+ qed (use elim in auto)
+
+ also have "(\<Sum>X | X \<in> multisets_of_size {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0).
+ \<Prod>i\<le>g n. fps_nth (f i) (count X i)) =
+ (\<Sum>X \<in> multisets_of_size {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (count X i))"
+ proof (intro sum.mono_neutral_left ballI)
+ fix X assume "X \<in> multisets_of_size {..g n} n -
+ {X\<in>multisets_of_size {..g n} n. \<forall>x\<le>N. fps_nth (f x) (count X x) \<noteq> 0}"
+ then obtain i
+ where h: "X \<in> multisets_of_size {..g n} n"
+ and i: "i \<le> N" "fps_nth (f i) (count X i) = 0"
+ by blast
+ have "\<not>(i > g n)"
+ proof
+ assume i': "i > g n"
+ hence "count X i = 0"
+ using h by (auto simp: multisets_of_size_def simp flip: not_in_iff)
+ have "subdegree (f i - 1) > n"
+ by (intro g) (use i' in auto)
+ hence "subdegree (f i - 1) > 0"
+ by simp
+ hence "fps_nth (f i - 1) 0 = 0"
+ by blast
+ hence "fps_nth (f i) (count X i) = 1"
+ using \<open>count X i = 0\<close> by simp
+ thus False using i by simp
+ qed
+ thus " (\<Prod>x\<le>g n. fps_nth (f x) (count X x)) = 0"
+ using i by auto
+ qed auto
+
+ also have "\<dots> = fps_nth P n"
+ by (simp add: P_def)
+ finally show "fps_nth (\<Prod>k\<le>N. f k) n = fps_nth P n" .
+ qed
+qed
+
+
+
subsection \<open>Integration\<close>
definition fps_integral :: "'a::{semiring_1,inverse} fps \<Rightarrow> 'a \<Rightarrow> 'a fps"
@@ -4911,6 +5454,64 @@
lemma fps_X_fps_compose: "fps_X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left)
+lemma fps_compose_eq_0_iff:
+ fixes F G :: "'a :: idom fps"
+ assumes "fps_nth G 0 = 0"
+ shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
+proof safe
+ assume *: "fps_compose F G = 0" "F \<noteq> 0"
+ have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
+ by simp
+ also have "fps_compose F G = 0"
+ by (simp add: *)
+ finally show "fps_nth F 0 = 0"
+ by simp
+ show "G = 0"
+ proof (rule ccontr)
+ assume "G \<noteq> 0"
+ hence "subdegree G > 0" using assms
+ using subdegree_eq_0_iff by blast
+ define N where "N = subdegree F * subdegree G"
+ have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
+ unfolding fps_compose_def by (simp add: N_def)
+ also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
+ proof (intro sum.mono_neutral_right ballI)
+ fix i assume i: "i \<in> {0..N} - {subdegree F}"
+ show "fps_nth F i * fps_nth (G ^ i) N = 0"
+ proof (cases i "subdegree F" rule: linorder_cases)
+ assume "i > subdegree F"
+ hence "fps_nth (G ^ i) N = 0"
+ using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
+ thus ?thesis by simp
+ qed (use i in \<open>auto simp: N_def\<close>)
+ qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
+ also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
+ by simp
+ also have "\<dots> \<noteq> 0"
+ using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
+ finally show False using * by auto
+ qed
+qed auto
+
+lemma subdegree_fps_compose [simp]:
+ fixes F G :: "'a :: idom fps"
+ assumes [simp]: "fps_nth G 0 = 0"
+ shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
+proof (cases "G = 0"; cases "F = 0")
+ assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+ define m where "m = subdegree F"
+ define F' where "F' = fps_shift m F"
+ have F_eq: "F = F' * fps_X ^ m"
+ unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
+ have [simp]: "F' \<noteq> 0"
+ using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
+ have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
+ by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
+ also have "subdegree (fps_compose F' G) = 0"
+ by (intro subdegree_eq_0) (auto simp: F'_def m_def)
+ finally show ?thesis by (simp add: m_def)
+qed auto
+
lemma fps_inverse_compose:
assumes b0: "(b$0 :: 'a::field) = 0"
and a0: "a$0 \<noteq> 0"
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy Tue Apr 22 17:35:13 2025 +0100
@@ -313,4 +313,48 @@
end
+
+text \<open>
+ Truncation of formal power series: all monomials $cx^k$ with $k\geq n$ are removed;
+ the remainder is a polynomial of degree at most $n-1$.
+\<close>
+lift_definition truncate_fps :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a :: zero poly" is
+ "\<lambda>n F k. if k \<ge> n then 0 else fps_nth F k"
+proof goal_cases
+ case (1 n F)
+ have "eventually (\<lambda>k. (if n \<le> k then 0 else fps_nth F k) = 0) at_top"
+ using eventually_ge_at_top[of n] by eventually_elim auto
+ thus ?case
+ by (simp add: cofinite_eq_sequentially)
+qed
+
+lemma coeff_truncate_fps' [simp]:
+ "k \<ge> n \<Longrightarrow> coeff (truncate_fps n F) k = 0"
+ "k < n \<Longrightarrow> coeff (truncate_fps n F) k = fps_nth F k"
+ by (transfer; simp; fail)+
+
+lemma coeff_truncate_fps: "coeff (truncate_fps n F) k = (if k < n then fps_nth F k else 0)"
+ by auto
+
+lemma truncate_0_fps [simp]: "truncate_fps 0 F = 0"
+ by (rule poly_eqI) auto
+
+lemma degree_truncate_fps: "n > 0 \<Longrightarrow> degree (truncate_fps n F) < n"
+ by (rule degree_lessI) auto
+
+lemma truncate_fps_0 [simp]: "truncate_fps n 0 = 0"
+ by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_add: "truncate_fps n (f + g) = truncate_fps n f + truncate_fps n g"
+ by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_diff: "truncate_fps n (f - g) = truncate_fps n f - truncate_fps n g"
+ by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_uminus: "truncate_fps n (-f) = -truncate_fps n f"
+ by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma fps_of_poly_truncate [simp]: "fps_of_poly (truncate_fps n f) = fps_cutoff n f"
+ by (rule fps_ext) auto
+
end
--- a/src/HOL/Deriv.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Deriv.thy Tue Apr 22 17:35:13 2025 +0100
@@ -1156,6 +1156,35 @@
((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
by (rule DERIV_chain')
+text \<open>Derivative of a finite product\<close>
+
+lemma has_field_derivative_prod:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> (f x has_field_derivative f' x) (at z)"
+ shows "((\<lambda>u. \<Prod>x\<in>A. f x u) has_field_derivative (\<Sum>x\<in>A. f' x * (\<Prod>y\<in>A-{x}. f y z))) (at z)"
+ using assms
+proof (induction A rule: infinite_finite_induct)
+ case (insert x A)
+ have eq: "insert x A - {y} = insert x (A - {y})" if "y \<in> A" for y
+ using insert.hyps that by auto
+ show ?case
+ using insert.hyps
+ by (auto intro!: derivative_eq_intros insert.prems insert.IH sum.cong
+ simp: sum_distrib_left sum_distrib_right eq)
+qed auto
+
+lemma has_field_derivative_prod':
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x z \<noteq> 0"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> (f x has_field_derivative f' x) (at z)"
+ defines "P \<equiv> (\<lambda>A u. \<Prod>x\<in>A. f x u)"
+ shows "(P A has_field_derivative (P A z * (\<Sum>x\<in>A. f' x / f x z))) (at z)"
+proof (cases "finite A")
+ case True
+ note [derivative_intros] = has_field_derivative_prod
+ show ?thesis using assms True
+ by (auto intro!: derivative_eq_intros
+ simp: prod_diff1 sum_distrib_left sum_distrib_right mult_ac)
+qed (auto simp: P_def)
+
text \<open>Standard version\<close>
lemma DERIV_chain:
--- a/src/HOL/Groups_Big.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Groups_Big.thy Tue Apr 22 17:35:13 2025 +0100
@@ -1792,4 +1792,74 @@
finally show ?case .
qed
+lemma prod_add:
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_semiring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x + f2 x) = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ using assms
+proof (induction A rule: finite_induct)
+ case (insert x A)
+ have "(\<Sum>X\<in>Pow (insert x A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) +
+ (\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x))"
+ unfolding Pow_insert by (rule sum.union_disjoint) (use insert.hyps in auto)
+ also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ proof (rule sum.cong)
+ fix X assume X: "X \<in> Pow A"
+ have "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x (A-X). f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+ by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in \<open>auto simp: mult_ac\<close>)
+ also have "insert x (A - X) = insert x A - X"
+ using insert.hyps X by auto
+ finally show "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)" .
+ qed auto
+ also have "(\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x))"
+ by (subst sum.reindex) (use insert.hyps in \<open>auto intro!: inj_onI simp: o_def\<close>)
+ also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x)) =
+ (\<Sum>X\<in>Pow A. f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ proof (rule sum.cong)
+ fix X assume X: "X \<in> Pow A"
+ show "(\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x) =
+ f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+ by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in auto)
+ qed auto
+ also have "(\<Sum>X\<in>Pow A. f2 x * prod f1 X * prod f2 (A - X)) +
+ (\<Sum>X\<in>Pow A. f1 x * prod f1 X * prod f2 (A - X)) =
+ (f1 x + f2 x) * (\<Sum>X\<in>Pow A. prod f1 X * prod f2 (A - X))"
+ by (simp add: algebra_simps flip: sum_distrib_left sum_distrib_right)
+ finally show ?case
+ by (subst (asm) insert.IH [symmetric]) (use insert.hyps in simp)
+qed auto
+
+lemma prod_diff_conv_sum:
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * (\<Prod>x\<in>A-X. f1 x))"
+proof -
+ have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. -f2 x + f1 x)"
+ by simp
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. - f2 x) * prod f1 (A - X))"
+ by (rule prod_add) fact+
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * prod f1 (A - X))"
+ by (simp add: prod_uminus)
+ finally show ?thesis .
+qed
+
+lemma prod_diff_conv_sum':
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+proof -
+ have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. f1 x + (-f2 x))"
+ by simp
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. -f2 x))"
+ by (rule prod_add) fact+
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card (A - X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ by (simp add: prod_uminus mult_ac)
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ using finite_subset[OF _ assms] by (intro sum.cong refl, subst card_Diff_subset) auto
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Library/FuncSet.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Library/FuncSet.thy Tue Apr 22 17:35:13 2025 +0100
@@ -810,4 +810,37 @@
by blast
qed
+subsection \<open>Products of sums\<close>
+
+lemma prod_sum_PiE:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: comm_semiring_1"
+ assumes finite: "finite A" and finite: "\<And>x. x \<in> A \<Longrightarrow> finite (B x)"
+ shows "(\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y) = (\<Sum>g\<in>PiE A B. \<Prod>x\<in>A. f x (g x))"
+ using assms
+proof (induction A rule: finite_induct)
+ case empty
+ thus ?case by auto
+next
+ case (insert x A)
+ have "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. \<Prod>x\<in>insert x A. f x (g x)) =
+ (\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * (\<Prod>x'\<in>A. f x' (g x')))"
+ using insert by simp
+ also have "(\<lambda>g. \<Prod>x'\<in>A. f x' (g x')) = (\<lambda>g. \<Prod>x'\<in>A. f x' (if x' = x then undefined else g x'))"
+ using insert by (intro ext prod.cong) auto
+ also have "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * \<dots> g) =
+ (\<Sum>(y,g)\<in>B x \<times> Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+ using insert.prems insert.hyps
+ by (intro sum.reindex_bij_witness[of _ "\<lambda>(y,g). g(x := y)" "\<lambda>g. (g x, g(x := undefined))"])
+ (auto simp: PiE_def extensional_def)
+ also have "\<dots> = (\<Sum>y\<in>B x. \<Sum>g\<in>Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+ by (subst sum.cartesian_product) auto
+ also have "\<dots> = (\<Sum>y\<in>B x. f x y) * (\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x'))"
+ using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right)
+ also have "(\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x')) = (\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y)"
+ using insert.prems by (intro insert.IH [symmetric]) auto
+ also have "(\<Sum>y\<in>B x. f x y) * \<dots> = (\<Prod>x\<in>insert x A. \<Sum>y\<in>B x. f x y)"
+ using insert.hyps by simp
+ finally show ?case ..
+qed
+
end
--- a/src/HOL/Library/Multiset.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Apr 22 17:35:13 2025 +0100
@@ -4834,4 +4834,185 @@
hide_const (open) wcount
+
+subsection \<open>The set of multisets of a given size\<close>
+
+(* contributed by Manuel Eberl *)
+
+text \<open>
+ The following operator gives the set of all multisets consisting of $n$ elements drawn from
+ the set $A$. In other words: all the different ways to put $n$ unlabelled balls into
+ the labelled bins $A$.
+\<close>
+definition multisets_of_size :: "'a set \<Rightarrow> nat \<Rightarrow> 'a multiset set" where
+ "multisets_of_size A n = {X. set_mset X \<subseteq> A \<and> size X = n}"
+
+lemma
+ assumes "X \<in> multisets_of_size A n"
+ shows multisets_of_size_subset: "set_mset X \<subseteq> A"
+ and multisets_of_size_size: "size X = n"
+ using assms by (auto simp: multisets_of_size_def)
+
+lemma multisets_of_size_mono:
+ assumes "A \<subseteq> B"
+ shows "multisets_of_size A n \<subseteq> multisets_of_size B n"
+ unfolding multisets_of_size_def
+ by (intro Collect_mono) (use assms in auto)
+
+lemma multisets_of_size_0 [simp]: "multisets_of_size A 0 = {{#}}"
+proof (intro equalityI subsetI)
+ fix h :: "'a multiset" assume "h \<in> {{#}}"
+ thus "h \<in> multisets_of_size A 0"
+ by (auto simp: multisets_of_size_def)
+qed (auto simp: multisets_of_size_def fun_eq_iff)
+
+lemma multisets_of_size_empty [simp]: "n > 0 \<Longrightarrow> multisets_of_size {} n = {}"
+ by (auto simp: multisets_of_size_def fun_eq_iff)
+
+lemma count_le_size: "count X x \<le> size X"
+ by (induction X) auto
+
+lemma bij_betw_multisets_of_size_insert:
+ assumes "a \<notin> A"
+ shows "bij_betw (\<lambda>(m,X). X + replicate_mset m a)
+ (SIGMA m:{0..n}. multisets_of_size A (n - m)) (multisets_of_size (insert a A) n)"
+proof -
+ define B where "B = (SIGMA m:{0..n}. multisets_of_size A (n - m))"
+ define C where "C = (multisets_of_size (insert a A) n)"
+ define f where "f = (\<lambda>(m,X). X + replicate_mset m a)"
+ define g where "g = (\<lambda>X. (count X a, filter_mset (\<lambda>x. x \<noteq> a) X))"
+ note defs = B_def C_def f_def g_def
+
+ have *: "size (filter_mset (\<lambda>x. x \<noteq> a) X) = size X - count X a" for X
+ proof -
+ have "size X = size (filter_mset (\<lambda>x. x \<noteq> a) X) + count X a"
+ by (induction X) auto
+ thus ?thesis
+ by linarith
+ qed
+
+ have 1: "f mX \<in> C" if "mX \<in> B" for mX
+ using that by (auto simp: multisets_of_size_def defs split: if_splits)
+
+ have 2: "g X \<in> B" if "X \<in> C" for X
+ using that by (auto simp: multisets_of_size_def count_le_size * defs)
+
+ have 3: "g (f mX) = mX" if "mX \<in> B" for mX
+ using that assms
+ by (auto simp: multisets_of_size_def multiset_eq_iff defs simp flip: not_in_iff)
+
+ have 4: "f (g X) = X" if "X \<in> C" for X
+ using that
+ by (auto simp: multisets_of_size_def multiset_eq_iff defs simp flip: not_in_iff)
+
+ have "f ` B = C"
+ using 1 2 4 unfolding set_eq_iff image_iff by metis
+ moreover have "inj_on f B"
+ using 3 unfolding inj_on_def by metis
+ ultimately show ?thesis
+ unfolding bij_betw_def defs by metis
+qed
+
+lemma multisets_of_size_insert:
+ assumes "a \<notin> A"
+ shows "multisets_of_size (insert a A) n =
+ (\<Union>m\<le>n. (\<lambda>X. X + replicate_mset m a) ` multisets_of_size A (n - m))"
+proof -
+ have "multisets_of_size (insert a A) n =
+ (\<lambda>(m,X). X + replicate_mset m a) ` (SIGMA m:{0..n}. multisets_of_size A (n - m))"
+ using bij_betw_multisets_of_size_insert[OF assms, of n] unfolding bij_betw_def by simp
+ also have "\<dots> = (\<Union>m\<le>n. (\<lambda>X. X + replicate_mset m a) ` multisets_of_size A (n - m))"
+ unfolding Sigma_def image_UN atLeast0AtMost image_insert image_empty prod.case
+ UNION_singleton_eq_range image_image by (rule refl)
+ finally show ?thesis .
+qed
+
+primrec multisets_of_size_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list list" where
+ "multisets_of_size_list [] n = (if n = 0 then [[]] else [])"
+| "multisets_of_size_list (x # xs) n =
+ [replicate m x @ ys . m \<leftarrow> [0..<n+1], ys \<leftarrow> multisets_of_size_list xs (n - m)]"
+
+lemma multisets_of_size_list_correct:
+ assumes "distinct xs"
+ shows "mset ` set (multisets_of_size_list xs n) = multisets_of_size (set xs) n"
+ using assms
+proof (induction xs arbitrary: n)
+ case Nil
+ thus ?case
+ by (cases "n = 0") auto
+next
+ case (Cons x xs n)
+ have IH: "multisets_of_size (set xs) n = mset ` set (multisets_of_size_list xs n)" for n
+ by (rule Cons.IH [symmetric]) (use Cons.prems in auto)
+ from Cons.prems have "x \<notin> set xs"
+ by auto
+ thus ?case
+ by (simp add: multisets_of_size_insert image_UN atLeastLessThanSuc_atLeastAtMost image_image
+ add_ac atLeast0AtMost IH del: upt_Suc)
+qed
+
+lemma multisets_of_size_code [code]:
+ "multisets_of_size (set xs) n = set (map mset (multisets_of_size_list (remdups xs) n))"
+ using multisets_of_size_list_correct[of "remdups xs"] by simp
+
+lemma finite_multisets_of_size [intro]:
+ assumes "finite A"
+ shows "finite (multisets_of_size A n)"
+ using assms
+proof (induction arbitrary: n rule: finite_induct)
+ case empty
+ thus ?case
+ by (cases "n = 0") auto
+next
+ case (insert x A n)
+ have "finite (SIGMA m:{0..n}. multisets_of_size A (n - m))"
+ by (auto intro: insert.IH)
+ also have "?this \<longleftrightarrow> finite (multisets_of_size (insert x A) n)"
+ by (rule bij_betw_finite, rule bij_betw_multisets_of_size_insert) fact
+ finally show ?case .
+qed
+
+lemma card_multisets_of_size:
+ assumes "finite A"
+ shows "card (multisets_of_size A n) = (card A + n - 1) choose n"
+ using assms
+proof (induction A arbitrary: n rule: finite_induct)
+ case empty
+ thus ?case
+ by (cases "n = 0") auto
+next
+ case (insert a A n)
+ have "card (multisets_of_size (insert a A) n) = card (SIGMA m:{0..n}. multisets_of_size A (n - m))"
+ using bij_betw_same_card[OF bij_betw_multisets_of_size_insert[of a A], of n] insert.hyps
+ by simp
+ also have "\<dots> = (\<Sum>m=0..n. card (multisets_of_size A (n - m)))"
+ by (intro card_SigmaI) (use insert.hyps in auto)
+ also have "\<dots> = (\<Sum>m=0..n. (card A + (n - m) - 1) choose (n - m))"
+ by (intro sum.cong insert.IH refl)
+ also have "\<dots> = (\<Sum>m=0..n. (card A + m - 1) choose m)"
+ by (intro sum.reindex_bij_witness[of _ "\<lambda>m. n - m" "\<lambda>m. n - m"]) auto
+ also have "\<dots> = (card A + n) choose n"
+ proof (cases "card A = 0")
+ case True
+ have "(\<Sum>m=0..n. (card A + m - 1) choose m) = (\<Sum>m\<in>{0}. (m-1) choose m)"
+ by (intro sum.mono_neutral_cong_right) (use True in auto)
+ also have "\<dots> = 1"
+ by simp
+ also have "\<dots> = (card A + n) choose n"
+ using True by simp
+ finally show ?thesis .
+ next
+ case False
+ have "(\<Sum>m=0..n. (card A + m - 1) choose m) = (\<Sum>m\<le>n. ((card A - 1) + m) choose m)"
+ by (intro sum.cong) (use False in \<open>auto simp: algebra_simps\<close>)
+ also have "\<dots> = (\<Sum>m\<le>n. ((card A - 1) + m) choose (card A - 1))"
+ by (subst binomial_symmetric) auto
+ also have "\<dots> = (card A + n) choose n"
+ using choose_rising_sum(2)[of "card A - 1" n] False by simp
+ finally show ?thesis .
+ qed
+ finally show ?case
+ using insert.hyps by simp
+qed
+
end
--- a/src/HOL/Library/Type_Length.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Library/Type_Length.thy Tue Apr 22 17:35:13 2025 +0100
@@ -101,10 +101,22 @@
end
+lemma length_less_eq_Suc_0_iff [simp]:
+ \<open>LENGTH('a::len) \<le> Suc 0 \<longleftrightarrow> LENGTH('a) = Suc 0\<close>
+ by (simp add: le_Suc_eq)
+
lemma length_not_greater_eq_2_iff [simp]:
- \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+ \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = Suc 0\<close>
by (auto simp add: not_le dest: less_2_cases)
+lemma less_eq_decr_length_iff [simp]:
+ \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
+
+lemma decr_length_less_iff [simp]:
+ \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
+ by (cases \<open>LENGTH('a)\<close>) auto
+
context linordered_idom
begin
@@ -115,12 +127,4 @@
end
-lemma less_eq_decr_length_iff [simp]:
- \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
- by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
-
-lemma decr_length_less_iff [simp]:
- \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
- by (cases \<open>LENGTH('a)\<close>) auto
-
end
--- a/src/HOL/Library/Word.thy Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/Library/Word.thy Tue Apr 22 17:35:13 2025 +0100
@@ -511,6 +511,27 @@
by transfer simp
+subsection \<open>Elementary case distinctions\<close>
+
+lemma word_length_one [case_names zero minus_one length_beyond]:
+ fixes w :: \<open>'a::len word\<close>
+ obtains (zero) \<open>LENGTH('a) = Suc 0\<close> \<open>w = 0\<close>
+ | (minus_one) \<open>LENGTH('a) = Suc 0\<close> \<open>w = - 1\<close>
+ | (length_beyond) \<open>2 \<le> LENGTH('a)\<close>
+proof (cases \<open>2 \<le> LENGTH('a)\<close>)
+ case True
+ with length_beyond show ?thesis .
+next
+ case False
+ then have \<open>LENGTH('a) = Suc 0\<close>
+ by simp
+ then have \<open>w = 0 \<or> w = - 1\<close>
+ by transfer auto
+ with \<open>LENGTH('a) = Suc 0\<close> zero minus_one show ?thesis
+ by blast
+qed
+
+
subsubsection \<open>Basic ordering\<close>
instantiation word :: (len) linorder
@@ -759,10 +780,8 @@
for a :: \<open>'a::len word\<close>
proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
case False
- have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
- by auto
- with False that show ?thesis
- by transfer (simp add: eq_iff)
+ with that show ?thesis
+ by transfer simp
next
case True
obtain n where length: \<open>LENGTH('a) = Suc n\<close>
@@ -1245,9 +1264,7 @@
lemma signed_push_bit_eq:
\<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
for w :: \<open>'b::len word\<close>
- apply (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
- apply (cases n, simp_all add: min_def)
- done
+ by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj) auto
lemma signed_take_bit_eq:
\<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
@@ -1729,6 +1746,22 @@
\<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
by (fact signed.less_le)
+lemma minus_1_sless_0 [simp]:
+ \<open>- 1 <s 0\<close>
+ by transfer simp
+
+lemma not_0_sless_minus_1 [simp]:
+ \<open>\<not> 0 <s - 1\<close>
+ by transfer simp
+
+lemma minus_1_sless_eq_0 [simp]:
+ \<open>- 1 \<le>s 0\<close>
+ by transfer simp
+
+lemma not_0_sless_eq_minus_1 [simp]:
+ \<open>\<not> 0 \<le>s - 1\<close>
+ by transfer simp
+
subsection \<open>Bit-wise operations\<close>
@@ -1746,7 +1779,7 @@
lemma bit_word_of_int_iff:
\<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
- by (metis Word_eq_word_of_int bit_word.abs_eq)
+ by (simp add: bit_simps)
lemma bit_uint_iff:
\<open>bit (uint w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w n\<close>
@@ -1761,13 +1794,13 @@
lemma bit_word_ucast_iff:
\<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
- by (meson bit_imp_possible_bit bit_unsigned_iff possible_bit_word)
+ by (auto simp add: bit_unsigned_iff bit_imp_le_length)
lemma bit_word_scast_iff:
\<open>bit (scast w :: 'b::len word) n \<longleftrightarrow>
n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close>
for w :: \<open>'a::len word\<close>
- by (metis One_nat_def bit_sint_iff bit_word_of_int_iff of_int_sint)
+ by (auto simp add: bit_signed_iff bit_imp_le_length min_def le_less dest: bit_imp_possible_bit)
lemma bit_word_iff_drop_bit_and [code]:
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
@@ -1859,10 +1892,7 @@
lemma bit_signed_drop_bit_iff [bit_simps]:
\<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
- apply transfer
- apply (simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
- by (metis add.commute add_lessD1 le_antisym less_diff_conv less_eq_decr_length_iff
- nat_less_le)
+ by transfer (simp add: bit_drop_bit_eq bit_signed_take_bit_iff min_def le_less not_less, auto)
lemma [code]:
\<open>Word.the_int (signed_drop_bit n w) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))\<close>
@@ -1896,19 +1926,13 @@
lemma sint_signed_drop_bit_eq:
\<open>sint (signed_drop_bit n w) = drop_bit n (sint w)\<close>
-proof (cases \<open>LENGTH('a) = 0 \<or> n=0\<close>)
- case False
- then show ?thesis
- apply simp
- apply (rule bit_eqI)
- by (auto simp: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
-qed auto
+ by (rule bit_eqI; cases n) (auto simp add: bit_simps not_less)
subsection \<open>Single-bit operations\<close>
lemma set_bit_eq_idem_iff:
- \<open>Bit_Operations.set_bit n w = w \<longleftrightarrow> bit w n \<or> n \<ge> LENGTH('a)\<close>
+ \<open>set_bit n w = w \<longleftrightarrow> bit w n \<or> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
unfolding bit_eq_iff
by (auto simp: bit_simps not_le)
--- a/src/HOL/ROOT Tue Apr 22 17:35:02 2025 +0100
+++ b/src/HOL/ROOT Tue Apr 22 17:35:13 2025 +0100
@@ -108,6 +108,7 @@
"HOL-Real_Asymp"
theories
Analysis
+ Finite_Function_Topology (* not part of main file because it imports problematic Sum_any notation *)
document_files
"root.tex"
"root.bib"