--- a/src/HOL/Analysis/Abstract_Limits.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Limits.thy Thu Oct 12 21:13:22 2023 +0200
@@ -9,9 +9,14 @@
where "nhdsin X a =
(if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"
-definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
- where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
+definition atin_within :: "['a topology, 'a, 'a set] \<Rightarrow> 'a filter"
+ where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \<inter> S - {a}))"
+abbreviation atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
+ where "atin X a \<equiv> atin_within X a UNIV"
+
+lemma atin_def: "atin X a = inf (nhdsin X a) (principal (topspace X - {a}))"
+ by (simp add: atin_within_def)
lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
@@ -28,18 +33,23 @@
finally show ?thesis using True by simp
qed auto
+lemma eventually_atin_within:
+ "eventually P (atin_within X a S) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+proof (cases "a \<in> topspace X")
+ case True
+ hence "eventually P (atin_within X a S) \<longleftrightarrow>
+ (\<exists>T. openin X T \<and> a \<in> T \<and>
+ (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+ by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
+ also have "\<dots> \<longleftrightarrow> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+ using openin_subset by (intro ex_cong) auto
+ finally show ?thesis by (simp add: True)
+qed (simp add: atin_within_def)
+
lemma eventually_atin:
"eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
(\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
-proof (cases "a \<in> topspace X")
- case True
- hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
- a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
- by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
- also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
- using openin_subset by (intro ex_cong) auto
- finally show ?thesis by (simp add: True)
-qed auto
+ by (auto simp add: eventually_atin_within)
lemma nontrivial_limit_atin:
"atin X a \<noteq> bot \<longleftrightarrow> a \<in> X derived_set_of topspace X"
@@ -64,12 +74,50 @@
qed
qed
+lemma eventually_atin_subtopology:
+ assumes "a \<in> topspace X"
+ shows "eventually P (atin (subtopology X S) a) \<longleftrightarrow>
+ (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
+ using assms by (simp add: eventually_atin)
+
+lemma eventually_within_imp:
+ "eventually P (atin_within X a S) \<longleftrightarrow> eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) (atin X a)"
+ by (auto simp add: eventually_atin_within eventually_atin)
+
+lemma atin_subtopology_within:
+ assumes "a \<in> S"
+ shows "atin (subtopology X S) a = atin_within X a S"
+proof -
+ have "eventually P (atin (subtopology X S) a) \<longleftrightarrow> eventually P (atin_within X a S)" for P
+ unfolding eventually_atin eventually_atin_within openin_subtopology
+ using assms by auto
+ then show ?thesis
+ by (meson le_filter_def order.eq_iff)
+qed
+
+lemma atin_subtopology_within_if:
+ shows "atin (subtopology X S) a = (if a \<in> S then atin_within X a S else bot)"
+ by (simp add: atin_subtopology_within)
+
+lemma trivial_limit_atpointof_within:
+ "trivial_limit(atin_within X a S) \<longleftrightarrow>
+ (a \<notin> X derived_set_of S)"
+ by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)
+
+lemma derived_set_of_trivial_limit:
+ "a \<in> X derived_set_of S \<longleftrightarrow> \<not> trivial_limit(atin_within X a S)"
+ by (simp add: trivial_limit_atpointof_within)
+
subsection\<open>Limits in a topological space\<close>
definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
"limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
+lemma limit_within_subset:
+ "\<lbrakk>limitin X f l (atin_within Y a S); T \<subseteq> S\<rbrakk> \<Longrightarrow> limitin X f l (atin_within Y a T)"
+ by (smt (verit) eventually_atin_within limitin_def subset_eq)
+
lemma limitinD: "\<lbrakk>limitin X f l F; openin X U; l \<in> U\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. f x \<in> U) F"
by (simp add: limitin_def)
@@ -217,10 +265,7 @@
assume R: ?rhs
then show ?lhs
apply (auto simp: continuous_map_def topcontinuous_at_def)
- apply (subst openin_subopen, safe)
- apply (drule bspec, assumption)
- using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
- done
+ by (smt (verit, del_insts) mem_Collect_eq openin_subopen openin_subset subset_eq)
qed
lemma continuous_map_atin:
@@ -231,6 +276,11 @@
"\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limitin Y f b (atin X a)"
by (auto simp: continuous_map_atin)
+lemma limit_continuous_map_within:
+ "\<lbrakk>continuous_map (subtopology X S) Y f; a \<in> S; a \<in> topspace X\<rbrakk>
+ \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
+ by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)
+
subsection\<open>Combining theorems for continuous functions into the reals\<close>
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Thu Oct 12 21:13:22 2023 +0200
@@ -2562,12 +2562,12 @@
lemma derived_set_of_infinite_mball:
"mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mball x e)}"
unfolding derived_set_of_infinite_openin_metric
- by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+ by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
lemma derived_set_of_infinite_mcball:
"mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mcball x e)}"
unfolding derived_set_of_infinite_openin_metric
- by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+ by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
end
@@ -2671,7 +2671,8 @@
proof -
have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
- by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology Pi_iff)
+ unfolding continuous_map_def Pi_iff topspace_mtopology
+ by (smt (verit, del_insts) eventually_mono)
then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
by metis
show thesis
@@ -3370,74 +3371,6 @@
using empty_completely_metrizable_space by auto
qed
-
-subsection \<open>The "atin-within" filter for topologies\<close>
-
-(*FIXME: replace original definition of atin to be an abbreviation, like at / at_within
- ("atin (_) (_)/ within (_)" [1000, 60] 60)*)
-definition atin_within :: "['a topology, 'a, 'a set] \<Rightarrow> 'a filter"
- where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \<inter> S - {a}))"
-
-lemma atin_within_UNIV [simp]:
- shows "atin_within X a UNIV = atin X a"
- by (simp add: atin_def atin_within_def)
-
-lemma eventually_atin_subtopology:
- assumes "a \<in> topspace X"
- shows "eventually P (atin (subtopology X S) a) \<longleftrightarrow>
- (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
- using assms by (simp add: eventually_atin)
-
-lemma eventually_atin_within:
- "eventually P (atin_within X a S) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
-proof (cases "a \<in> topspace X")
- case True
- hence "eventually P (atin_within X a S) \<longleftrightarrow>
- (\<exists>T. openin X T \<and> a \<in> T \<and>
- (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
- by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
- also have "\<dots> \<longleftrightarrow> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
- using openin_subset by (intro ex_cong) auto
- finally show ?thesis by (simp add: True)
-qed (simp add: atin_within_def)
-
-lemma eventually_within_imp:
- "eventually P (atin_within X a S) \<longleftrightarrow> eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) (atin X a)"
- by (auto simp add: eventually_atin_within eventually_atin)
-
-lemma limit_within_subset:
- "\<lbrakk>limitin X f l (atin_within Y a S); T \<subseteq> S\<rbrakk> \<Longrightarrow> limitin X f l (atin_within Y a T)"
- by (smt (verit) eventually_atin_within limitin_def subset_eq)
-
-lemma atin_subtopology_within:
- assumes "a \<in> S"
- shows "atin (subtopology X S) a = atin_within X a S"
-proof -
- have "eventually P (atin (subtopology X S) a) \<longleftrightarrow> eventually P (atin_within X a S)" for P
- unfolding eventually_atin eventually_atin_within openin_subtopology
- using assms by auto
- then show ?thesis
- by (meson le_filter_def order.eq_iff)
-qed
-
-lemma limit_continuous_map_within:
- "\<lbrakk>continuous_map (subtopology X S) Y f; a \<in> S; a \<in> topspace X\<rbrakk>
- \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
- by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)
-
-lemma atin_subtopology_within_if:
- shows "atin (subtopology X S) a = (if a \<in> S then atin_within X a S else bot)"
- by (simp add: atin_subtopology_within)
-
-lemma trivial_limit_atpointof_within:
- "trivial_limit(atin_within X a S) \<longleftrightarrow>
- (a \<notin> X derived_set_of S)"
- by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)
-
-lemma derived_set_of_trivial_limit:
- "a \<in> X derived_set_of S \<longleftrightarrow> \<not> trivial_limit(atin_within X a S)"
- by (simp add: trivial_limit_atpointof_within)
-
subsection\<open>More sequential characterizations in a metric space\<close>
@@ -3992,7 +3925,8 @@
lemma uniformly_continuous_map_compose:
assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g"
shows "uniformly_continuous_map m1 m3 (g \<circ> f)"
- by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff uniformly_continuous_map_def)
+ using f g unfolding uniformly_continuous_map_def comp_apply Pi_iff
+ by metis
lemma uniformly_continuous_map_real_const [simp]:
"uniformly_continuous_map m euclidean_metric (\<lambda>x. c)"
@@ -5109,7 +5043,6 @@
by (metis (full_types) completely_metrizable_space_def)
qed
-
proposition metrizable_space_product_topology:
"metrizable_space (product_topology X I) \<longleftrightarrow>
(product_topology X I) = trivial_topology \<or>
--- a/src/HOL/Analysis/Urysohn.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Analysis/Urysohn.thy Thu Oct 12 21:13:22 2023 +0200
@@ -4562,8 +4562,7 @@
with that \<open>a \<in> topspace X\<close>
obtain U where U: "openin X U" "a \<in> U" "l \<in> M"
and Uless: "\<forall>x\<in>U - {a}. x \<in> S \<longrightarrow> f x \<in> M \<and> d (f x) l < \<epsilon>/2"
- unfolding limitin_metric eventually_within_imp eventually_atin
- using half_gt_zero by blast
+ unfolding limitin_metric eventually_atin_within by (metis Diff_iff insertI1 half_gt_zero [OF \<open>\<epsilon>>0\<close>])
show "\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x\<in>S \<inter> U - {a}. \<forall>y\<in>S \<inter> U - {a}. d (f x) (f y) < \<epsilon>)"
proof (intro exI strip conjI)
fix x y
@@ -4653,7 +4652,7 @@
qed
ultimately show "\<forall>\<^sub>F x in atin_within X a S. f x \<in> M \<and> d (f x) b < \<epsilon>"
using fim U
- apply (simp add: eventually_atin eventually_within_imp del: divide_const_simps flip: image_subset_iff_funcset)
+ apply (simp add: eventually_atin_within del: divide_const_simps flip: image_subset_iff_funcset)
by (smt (verit, del_insts) Diff_iff Int_iff imageI insertI1 openin_subset subsetD)
qed
then show ?thesis ..
--- a/src/HOL/Archimedean_Field.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Archimedean_Field.thy Thu Oct 12 21:13:22 2023 +0200
@@ -719,6 +719,57 @@
by (simp add: frac_def)
+subsection \<open>Fractional part arithmetic\<close>
+text \<open>Many thanks to Stepan Holub\<close>
+
+lemma frac_non_zero: "frac x \<noteq> 0 \<Longrightarrow> frac (-x) = 1 - frac x"
+ using frac_eq_0_iff frac_neg by metis
+
+lemma frac_add_simps [simp]:
+ "frac (frac a + b) = frac (a + b)"
+ "frac (a + frac b) = frac (a + b)"
+ by (simp_all add: frac_add)
+
+lemma frac_neg_frac: "frac (- frac x) = frac (-x)"
+ unfolding frac_neg frac_frac by force
+
+lemma frac_diff_simp: "frac (y - frac x) = frac (y - x)"
+ unfolding diff_conv_add_uminus frac_add frac_neg_frac..
+
+lemma frac_diff: "frac (a - b) = frac (frac a + (- frac b))"
+ unfolding frac_add_simps(1)
+ unfolding ab_group_add_class.ab_diff_conv_add_uminus[symmetric] frac_diff_simp..
+
+lemma frac_diff_pos: "frac x \<le> frac y \<Longrightarrow> frac (y - x) = frac y - frac x"
+ unfolding diff_conv_add_uminus frac_add frac_neg
+ using frac_lt_1 by force
+
+lemma frac_diff_neg: assumes "frac y < frac x"
+ shows "frac (y - x) = frac y + 1 - frac x"
+proof-
+ have "x \<notin> \<int>"
+ unfolding frac_gt_0_iff[symmetric]
+ using assms frac_ge_0[of y] by order
+ have "frac y + (1 + - frac x) < 1"
+ using frac_lt_1[of x] assms by fastforce
+ show ?thesis
+ unfolding diff_conv_add_uminus frac_add frac_neg
+ if_not_P[OF \<open>x \<notin> \<int>\<close>] if_P[OF \<open>frac y + (1 + - frac x) < 1\<close>]
+ by simp
+qed
+
+lemma frac_diff_eq: assumes "frac y = frac x"
+ shows "frac (y - x) = 0"
+ by (simp add: assms frac_diff_pos)
+
+lemma frac_diff_zero: assumes "frac (x - y) = 0"
+ shows "frac x = frac y"
+ using frac_add_simps(1)[of "x - y" y, symmetric]
+ unfolding assms add.group_left_neutral diff_add_cancel.
+
+lemma frac_neg_eq_iff: "frac (-x) = frac (-y) \<longleftrightarrow> frac x = frac y"
+ using add.inverse_inverse frac_neg_frac by metis
+
subsection \<open>Rounding to the nearest integer\<close>
definition round :: "'a::floor_ceiling \<Rightarrow> int"
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Thu Oct 12 21:13:22 2023 +0200
@@ -4,42 +4,6 @@
begin
-lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
- by (metis fps_to_fls_of_nat of_nat_numeral)
-
-lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b"
- by (induction b) (auto simp flip: fls_const_mult_const)
-
-lemma fls_deriv_numeral [simp]: "fls_deriv (numeral n) = 0"
- by (metis fls_deriv_of_int of_int_numeral)
-
-lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n"
- by (metis fls_of_nat of_nat_numeral)
-
-lemma fls_mult_of_int_nth [simp]:
- shows "fls_nth (numeral k * f) n = numeral k * fls_nth f n"
- and "fls_nth (f * numeral k) n = fls_nth f n * numeral k"
- by (metis fls_const_numeral fls_mult_const_nth)+
-
-lemma fls_nth_numeral' [simp]:
- "fls_nth (numeral n) 0 = numeral n" "k \<noteq> 0 \<Longrightarrow> fls_nth (numeral n) k = 0"
- by (subst fls_const_numeral [symmetric], subst fls_const_nth, simp)+
-
-lemma fls_subdegree_prod:
- fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
- assumes "\<And>x. x \<in> I \<Longrightarrow> F x \<noteq> 0"
- shows "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
- using assms by (induction I rule: infinite_finite_induct) auto
-
-lemma fls_subdegree_prod':
- fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
- assumes "\<And>x. x \<in> I \<Longrightarrow> fls_subdegree (F x) \<noteq> 0"
- shows "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
-proof (intro fls_subdegree_prod)
- show "F x \<noteq> 0" if "x \<in> I" for x
- using assms[OF that] by auto
-qed
-
instance fps :: (semiring_char_0) semiring_char_0
proof
show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
@@ -2187,211 +2151,6 @@
by simp
qed
-hide_const (open) fls_compose_fps
-
-definition fls_compose_fps :: "'a :: field fls \<Rightarrow> 'a fps \<Rightarrow> 'a fls" where
- "fls_compose_fps F G =
- fps_to_fls (fps_compose (fls_base_factor_to_fps F) G) * fps_to_fls G powi fls_subdegree F"
-
-lemma fps_compose_of_nat [simp]: "fps_compose (of_nat n :: 'a :: comm_ring_1 fps) H = of_nat n"
- and fps_compose_of_int [simp]: "fps_compose (of_int i) H = of_int i"
- unfolding fps_of_nat [symmetric] fps_of_int [symmetric] numeral_fps_const
- by (rule fps_const_compose)+
-
-lemmas [simp] = fps_to_fls_of_nat fps_to_fls_of_int
-
-lemma fls_compose_fps_0 [simp]: "fls_compose_fps 0 H = 0"
- and fls_compose_fps_1 [simp]: "fls_compose_fps 1 H = 1"
- and fls_compose_fps_const [simp]: "fls_compose_fps (fls_const c) H = fls_const c"
- and fls_compose_fps_of_nat [simp]: "fls_compose_fps (of_nat n) H = of_nat n"
- and fls_compose_fps_of_int [simp]: "fls_compose_fps (of_int i) H = of_int i"
- and fls_compose_fps_X [simp]: "fls_compose_fps fls_X F = fps_to_fls F"
- by (simp_all add: fls_compose_fps_def)
-
-lemma fls_compose_fps_0_right:
- "fls_compose_fps F 0 = (if fls_subdegree F \<ge> 0 then fls_const (fls_nth F 0) else 0)"
- by (cases "fls_subdegree F = 0") (simp_all add: fls_compose_fps_def)
-
-lemma fls_compose_fps_shift:
- assumes "H \<noteq> 0"
- shows "fls_compose_fps (fls_shift n F) H = fls_compose_fps F H * fps_to_fls H powi (-n)"
-proof (cases "F = 0")
- case False
- thus ?thesis
- using assms by (simp add: fls_compose_fps_def power_int_diff power_int_minus field_simps)
-qed auto
-
-lemma fls_compose_fps_to_fls [simp]:
- assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
- shows "fls_compose_fps (fps_to_fls F) G = fps_to_fls (fps_compose F G)"
-proof (cases "F = 0")
- case False
- define n where "n = subdegree F"
- define F' where "F' = fps_shift n F"
- have [simp]: "F' \<noteq> 0" "subdegree F' = 0"
- using False by (auto simp: F'_def n_def)
- have F_eq: "F = F' * fps_X ^ n"
- unfolding F'_def n_def using subdegree_decompose by blast
- have "fls_compose_fps (fps_to_fls F) G =
- fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F' * fls_X_intpow (int n))) oo G) * fps_to_fls (G ^ n)"
- unfolding F_eq fls_compose_fps_def
- by (simp add: fls_times_fps_to_fls fls_X_power_conv_shift_1 power_int_add
- fls_subdegree_fls_to_fps fps_to_fls_power fls_regpart_shift_conv_fps_shift
- flip: fls_times_both_shifted_simp)
- also have "fps_to_fls F' * fls_X_intpow (int n) = fps_to_fls F"
- by (simp add: F_eq fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1)
- also have "fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F)) oo G) * fps_to_fls (G ^ n) =
- fps_to_fls ((fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n) oo G)"
- by (simp add: fls_times_fps_to_fls flip: fps_compose_power add: fps_compose_mult_distrib)
- also have "fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n = F"
- by (simp add: F_eq)
- finally show ?thesis .
-qed (auto simp: fls_compose_fps_def)
-
-lemma fls_compose_fps_mult:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (F * G) H = fls_compose_fps F H * fls_compose_fps G H"
- using assms
-proof (cases "F * G = 0")
- case False
- hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
- by auto
- define n m where "n = fls_subdegree F" "m = fls_subdegree G"
- define F' where "F' = fls_regpart (fls_shift n F)"
- define G' where "G' = fls_regpart (fls_shift m G)"
- have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-m) (fps_to_fls G')"
- by (simp_all add: F'_def G'_def n_m_def)
- have "fls_compose_fps (F * G) H = fls_compose_fps (fls_shift (-(n + m)) (fps_to_fls (F' * G'))) H"
- by (simp add: fls_times_fps_to_fls F_eq G_eq fls_shifted_times_simps)
- also have "\<dots> = fps_to_fls ((F' oo H) * (G' oo H)) * fps_to_fls H powi (m + n)"
- by (simp add: fls_compose_fps_shift fps_compose_mult_distrib)
- also have "\<dots> = fls_compose_fps F H * fls_compose_fps G H"
- by (simp add: F_eq G_eq fls_compose_fps_shift fls_times_fps_to_fls power_int_add)
- finally show ?thesis .
-qed auto
-
-lemma fls_compose_fps_power:
- assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
- shows "fls_compose_fps (F ^ n) G = fls_compose_fps F G ^ n"
- by (induction n) (auto simp: fls_compose_fps_mult)
-
-lemma fls_compose_fps_add:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (F + G) H = fls_compose_fps F H + fls_compose_fps G H"
-proof (cases "F = 0 \<or> G = 0")
- case False
- hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
- by auto
- define n where "n = min (fls_subdegree F) (fls_subdegree G)"
- define F' where "F' = fls_regpart (fls_shift n F)"
- define G' where "G' = fls_regpart (fls_shift n G)"
- have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-n) (fps_to_fls G')"
- unfolding n_def by (simp_all add: F'_def G'_def n_def)
- have "F + G = fls_shift (-n) (fps_to_fls (F' + G'))"
- by (simp add: F_eq G_eq)
- also have "fls_compose_fps \<dots> H = fls_compose_fps (fps_to_fls (F' + G')) H * fps_to_fls H powi n"
- by (subst fls_compose_fps_shift) auto
- also have "\<dots> = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n"
- by (subst fls_compose_fps_to_fls) auto
- also have "\<dots> = fls_compose_fps F H + fls_compose_fps G H"
- by (simp add: F_eq G_eq fls_compose_fps_shift fps_compose_add_distrib algebra_simps)
- finally show ?thesis .
-qed auto
-
-lemma fls_compose_fps_uminus [simp]: "fls_compose_fps (-F) H = -fls_compose_fps F H"
- by (simp add: fls_compose_fps_def fps_compose_uminus)
-
-lemma fls_compose_fps_diff:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- 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"
- using assms fls_base_factor_to_fps_nonzero[of F]
- by (cases "F = 0") (auto simp: fls_compose_fps_def fps_compose_eq_0_iff)
-
-lemma fls_compose_fps_inverse:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (inverse F) H = inverse (fls_compose_fps F H)"
-proof (cases "F = 0")
- case False
- have "fls_compose_fps (inverse F) H * fls_compose_fps F H =
- fls_compose_fps (inverse F * F) H"
- by (subst fls_compose_fps_mult) auto
- also have "inverse F * F = 1"
- using False by simp
- finally show ?thesis
- using False by (simp add: field_simps fls_compose_fps_eq_0_iff)
-qed auto
-
-lemma fls_compose_fps_divide:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (F / G) H = fls_compose_fps F H / fls_compose_fps G H"
- using fls_compose_fps_mult[of H F "inverse G"] fls_compose_fps_inverse[of H G]
- by (simp add: field_simps)
-
-lemma fls_compose_fps_powi:
- assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (F powi n) H = fls_compose_fps F H powi n"
- by (simp add: power_int_def fls_compose_fps_power fls_compose_fps_inverse)
-
-lemma fls_compose_fps_assoc:
- assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0" "H \<noteq> 0" "fps_nth H 0 = 0"
- shows "fls_compose_fps (fls_compose_fps F G) H = fls_compose_fps F (fps_compose G H)"
-proof (cases "F = 0")
- case [simp]: False
- define n where "n = fls_subdegree F"
- define F' where "F' = fls_regpart (fls_shift n F)"
- have F_eq: "F = fls_shift (-n) (fps_to_fls F')"
- by (simp add: F'_def n_def)
- show ?thesis
- by (simp add: F_eq fls_compose_fps_shift fls_compose_fps_mult fls_compose_fps_powi
- fps_compose_eq_0_iff fps_compose_assoc)
-qed auto
-
-lemma subdegree_pos_iff: "subdegree F > 0 \<longleftrightarrow> F \<noteq> 0 \<and> fps_nth F 0 = 0"
- using subdegree_eq_0_iff[of F] by auto
lemma has_fps_expansion_fps_to_fls:
assumes "f has_laurent_expansion fps_to_fls F"
@@ -2404,7 +2163,6 @@
by (auto simp: has_fps_expansion_to_laurent)
qed
-
lemma has_laurent_expansion_compose [laurent_expansion_intros]:
fixes f g :: "complex \<Rightarrow> complex"
assumes F: "f has_laurent_expansion F"
@@ -2455,34 +2213,6 @@
using has_laurent_expansion_inverse[OF has_laurent_expansion_fps_X]
by (simp add: fls_inverse_X)
-lemma fls_X_power_int [simp]: "fls_X powi n = (fls_X_intpow n :: 'a :: division_ring fls)"
- by (auto simp: power_int_def fls_X_power_conv_shift_1 fls_inverse_X fls_inverse_shift
- simp flip: fls_inverse_X_power)
-
-lemma fls_const_power_int: "fls_const (c powi n) = fls_const (c :: 'a :: division_ring) powi n"
- by (auto simp: power_int_def fls_const_power fls_inverse_const)
-
-lemma fls_nth_fls_compose_fps_linear:
- fixes c :: "'a :: field"
- assumes [simp]: "c \<noteq> 0"
- shows "fls_nth (fls_compose_fps F (fps_const c * fps_X)) n = fls_nth F n * c powi n"
-proof -
- {
- assume *: "n \<ge> fls_subdegree F"
- hence "c ^ nat (n - fls_subdegree F) = c powi int (nat (n - fls_subdegree F))"
- by (simp add: power_int_def)
- also have "\<dots> * c powi fls_subdegree F = c powi (int (nat (n - fls_subdegree F)) + fls_subdegree F)"
- using * by (subst power_int_add) auto
- also have "\<dots> = c powi n"
- using * by simp
- finally have "c ^ nat (n - fls_subdegree F) * c powi fls_subdegree F = c powi n" .
- }
- thus ?thesis
- by (simp add: fls_compose_fps_def fps_compose_linear fls_times_fps_to_fls power_int_mult_distrib
- fls_shifted_times_simps
- flip: fls_const_power_int)
-qed
-
lemma zorder_times_analytic:
assumes "f analytic_on {z}" "g analytic_on {z}"
assumes "eventually (\<lambda>z. f z * g z \<noteq> 0) (at z)"
@@ -2787,7 +2517,6 @@
by (auto simp: eq_commute)
qed
-
lemma has_laurent_expansion_sin' [laurent_expansion_intros]:
"sin has_laurent_expansion fps_to_fls (fps_sin 1)"
using has_fps_expansion_sin' has_fps_expansion_to_laurent by blast
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Oct 12 21:11:59 2023 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Oct 12 21:13:22 2023 +0200
@@ -1587,6 +1587,24 @@
thus ?thesis by (simp add: fls_of_nat)
qed
+lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
+ by (metis fps_to_fls_of_nat of_nat_numeral)
+
+lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b"
+ by (induction b) (auto simp flip: fls_const_mult_const)
+
+lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n"
+ by (metis fls_of_nat of_nat_numeral)
+
+lemma fls_mult_of_numeral_nth [simp]:
+ shows "(numeral k * f) $$ n = numeral k * f $$ n"
+ and "(f * numeral k) $$ n = f $$ n * numeral k"
+ by (metis fls_const_numeral fls_mult_const_nth)+
+
+lemma fls_nth_numeral' [simp]:
+ "numeral n $$ 0 = numeral n" "k \<noteq> 0 \<Longrightarrow> numeral n $$ k = 0"
+ by (metis fls_const_nth fls_const_numeral)+
+
instance fls :: (comm_semiring_1) comm_semiring_1
by standard simp
@@ -1668,6 +1686,21 @@
subsubsection \<open>Powers\<close>
+lemma fls_subdegree_prod:
+ fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
+ assumes "\<And>x. x \<in> I \<Longrightarrow> F x \<noteq> 0"
+ shows "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
+ using assms by (induction I rule: infinite_finite_induct) auto
+
+lemma fls_subdegree_prod':
+ fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
+ assumes "\<And>x. x \<in> I \<Longrightarrow> fls_subdegree (F x) \<noteq> 0"
+ shows "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
+proof (intro fls_subdegree_prod)
+ show "F x \<noteq> 0" if "x \<in> I" for x
+ using assms[OF that] by auto
+qed
+
lemma fls_pow_subdegree_ge:
"f^n \<noteq> 0 \<Longrightarrow> fls_subdegree (f^n) \<ge> n * fls_subdegree f"
proof (induct n)
@@ -3254,15 +3287,236 @@
subsection \<open>Composition\<close>
definition fls_compose_fps :: "'a :: field fls \<Rightarrow> 'a fps \<Rightarrow> 'a fls" where
- "fls_compose_fps f g =
- (if f = 0 then 0
- else if fls_subdegree f \<ge> 0 then fps_to_fls (fps_compose (fls_regpart f) g)
- else fps_to_fls (fps_compose (fls_base_factor_to_fps f) g) /
- fps_to_fls g ^ nat (-fls_subdegree f))"
-
-lemma fls_compose_fps_fps [simp]:
- "fls_compose_fps (fps_to_fls f) g = fps_to_fls (fps_compose f g)"
- by (simp add: fls_compose_fps_def fls_subdegree_fls_to_fps_gt0 fps_to_fls_eq_0_iff)
+ "fls_compose_fps F G =
+ fps_to_fls (fps_compose (fls_base_factor_to_fps F) G) * fps_to_fls G powi fls_subdegree F"
+
+lemma fps_compose_of_nat [simp]: "fps_compose (of_nat n :: 'a :: comm_ring_1 fps) H = of_nat n"
+ and fps_compose_of_int [simp]: "fps_compose (of_int i) H = of_int i"
+ unfolding fps_of_nat [symmetric] fps_of_int [symmetric] numeral_fps_const
+ by (rule fps_const_compose)+
+
+lemmas [simp] = fps_to_fls_of_nat fps_to_fls_of_int
+
+lemma fls_compose_fps_0 [simp]: "fls_compose_fps 0 H = 0"
+ and fls_compose_fps_1 [simp]: "fls_compose_fps 1 H = 1"
+ and fls_compose_fps_const [simp]: "fls_compose_fps (fls_const c) H = fls_const c"
+ and fls_compose_fps_of_nat [simp]: "fls_compose_fps (of_nat n) H = of_nat n"
+ and fls_compose_fps_of_int [simp]: "fls_compose_fps (of_int i) H = of_int i"
+ and fls_compose_fps_X [simp]: "fls_compose_fps fls_X F = fps_to_fls F"
+ by (simp_all add: fls_compose_fps_def)
+
+lemma fls_compose_fps_0_right:
+ "fls_compose_fps F 0 = (if 0 \<le> fls_subdegree F then fls_const (F $$ 0) else 0)"
+ by (cases "fls_subdegree F = 0") (simp_all add: fls_compose_fps_def)
+
+lemma fls_compose_fps_shift:
+ assumes "H \<noteq> 0"
+ shows "fls_compose_fps (fls_shift n F) H = fls_compose_fps F H * fps_to_fls H powi (-n)"
+proof (cases "F = 0")
+ case False
+ thus ?thesis
+ using assms by (simp add: fls_compose_fps_def power_int_diff power_int_minus field_simps)
+qed auto
+
+lemma fls_compose_fps_to_fls [simp]:
+ assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
+ shows "fls_compose_fps (fps_to_fls F) G = fps_to_fls (fps_compose F G)"
+proof (cases "F = 0")
+ case False
+ define n where "n = subdegree F"
+ define F' where "F' = fps_shift n F"
+ have [simp]: "F' \<noteq> 0" "subdegree F' = 0"
+ using False by (auto simp: F'_def n_def)
+ have F_eq: "F = F' * fps_X ^ n"
+ unfolding F'_def n_def using subdegree_decompose by blast
+ have "fls_compose_fps (fps_to_fls F) G =
+ fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F' * fls_X_intpow (int n))) oo G) * fps_to_fls (G ^ n)"
+ unfolding F_eq fls_compose_fps_def
+ by (simp add: fls_times_fps_to_fls fls_X_power_conv_shift_1 power_int_add
+ fls_subdegree_fls_to_fps fps_to_fls_power fls_regpart_shift_conv_fps_shift
+ flip: fls_times_both_shifted_simp)
+ also have "fps_to_fls F' * fls_X_intpow (int n) = fps_to_fls F"
+ by (simp add: F_eq fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1)
+ also have "fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F)) oo G) * fps_to_fls (G ^ n) =
+ fps_to_fls ((fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n) oo G)"
+ by (simp add: fls_times_fps_to_fls flip: fps_compose_power add: fps_compose_mult_distrib)
+ also have "fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n = F"
+ by (simp add: F_eq)
+ finally show ?thesis .
+qed (auto simp: fls_compose_fps_def)
+
+lemma fls_compose_fps_mult:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (F * G) H = fls_compose_fps F H * fls_compose_fps G H"
+ using assms
+proof (cases "F * G = 0")
+ case False
+ hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
+ by auto
+ define n m where "n = fls_subdegree F" "m = fls_subdegree G"
+ define F' where "F' = fls_regpart (fls_shift n F)"
+ define G' where "G' = fls_regpart (fls_shift m G)"
+ have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-m) (fps_to_fls G')"
+ by (simp_all add: F'_def G'_def n_m_def)
+ have "fls_compose_fps (F * G) H = fls_compose_fps (fls_shift (-(n + m)) (fps_to_fls (F' * G'))) H"
+ by (simp add: fls_times_fps_to_fls F_eq G_eq fls_shifted_times_simps)
+ also have "\<dots> = fps_to_fls ((F' oo H) * (G' oo H)) * fps_to_fls H powi (m + n)"
+ by (simp add: fls_compose_fps_shift fps_compose_mult_distrib)
+ also have "\<dots> = fls_compose_fps F H * fls_compose_fps G H"
+ by (simp add: F_eq G_eq fls_compose_fps_shift fls_times_fps_to_fls power_int_add)
+ finally show ?thesis .
+qed auto
+
+lemma fls_compose_fps_power:
+ assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
+ shows "fls_compose_fps (F ^ n) G = fls_compose_fps F G ^ n"
+ by (induction n) (auto simp: fls_compose_fps_mult)
+
+lemma fls_compose_fps_add:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (F + G) H = fls_compose_fps F H + fls_compose_fps G H"
+proof (cases "F = 0 \<or> G = 0")
+ case False
+ hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
+ by auto
+ define n where "n = min (fls_subdegree F) (fls_subdegree G)"
+ define F' where "F' = fls_regpart (fls_shift n F)"
+ define G' where "G' = fls_regpart (fls_shift n G)"
+ have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-n) (fps_to_fls G')"
+ unfolding n_def by (simp_all add: F'_def G'_def n_def)
+ have "F + G = fls_shift (-n) (fps_to_fls (F' + G'))"
+ by (simp add: F_eq G_eq)
+ also have "fls_compose_fps \<dots> H = fls_compose_fps (fps_to_fls (F' + G')) H * fps_to_fls H powi n"
+ by (subst fls_compose_fps_shift) auto
+ also have "\<dots> = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n"
+ by (subst fls_compose_fps_to_fls) auto
+ also have "\<dots> = fls_compose_fps F H + fls_compose_fps G H"
+ by (simp add: F_eq G_eq fls_compose_fps_shift fps_compose_add_distrib algebra_simps)
+ finally show ?thesis .
+qed auto
+
+lemma fls_compose_fps_uminus [simp]: "fls_compose_fps (-F) H = -fls_compose_fps F H"
+ by (simp add: fls_compose_fps_def fps_compose_uminus)
+
+lemma fls_compose_fps_diff:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ 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"
+ using assms fls_base_factor_to_fps_nonzero[of F]
+ by (cases "F = 0") (auto simp: fls_compose_fps_def fps_compose_eq_0_iff)
+
+lemma fls_compose_fps_inverse:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (inverse F) H = inverse (fls_compose_fps F H)"
+proof (cases "F = 0")
+ case False
+ have "fls_compose_fps (inverse F) H * fls_compose_fps F H =
+ fls_compose_fps (inverse F * F) H"
+ by (subst fls_compose_fps_mult) auto
+ also have "inverse F * F = 1"
+ using False by simp
+ finally show ?thesis
+ using False by (simp add: field_simps fls_compose_fps_eq_0_iff)
+qed auto
+
+lemma fls_compose_fps_divide:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (F / G) H = fls_compose_fps F H / fls_compose_fps G H"
+ using fls_compose_fps_mult[of H F "inverse G"] fls_compose_fps_inverse[of H G]
+ by (simp add: field_simps)
+
+lemma fls_compose_fps_powi:
+ assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (F powi n) H = fls_compose_fps F H powi n"
+ by (simp add: power_int_def fls_compose_fps_power fls_compose_fps_inverse)
+
+lemma fls_compose_fps_assoc:
+ assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0" "H \<noteq> 0" "fps_nth H 0 = 0"
+ shows "fls_compose_fps (fls_compose_fps F G) H = fls_compose_fps F (fps_compose G H)"
+proof (cases "F = 0")
+ case [simp]: False
+ define n where "n = fls_subdegree F"
+ define F' where "F' = fls_regpart (fls_shift n F)"
+ have F_eq: "F = fls_shift (-n) (fps_to_fls F')"
+ by (simp add: F'_def n_def)
+ show ?thesis
+ by (simp add: F_eq fls_compose_fps_shift fls_compose_fps_mult fls_compose_fps_powi
+ fps_compose_eq_0_iff fps_compose_assoc)
+qed auto
+
+lemma subdegree_pos_iff: "subdegree F > 0 \<longleftrightarrow> F \<noteq> 0 \<and> fps_nth F 0 = 0"
+ using subdegree_eq_0_iff[of F] by auto
+
+lemma fls_X_power_int [simp]: "fls_X powi n = (fls_X_intpow n :: 'a :: division_ring fls)"
+ by (auto simp: power_int_def fls_X_power_conv_shift_1 fls_inverse_X fls_inverse_shift
+ simp flip: fls_inverse_X_power)
+
+lemma fls_const_power_int: "fls_const (c powi n) = fls_const (c :: 'a :: division_ring) powi n"
+ by (auto simp: power_int_def fls_const_power fls_inverse_const)
+
+lemma fls_nth_fls_compose_fps_linear:
+ fixes c :: "'a :: field"
+ assumes [simp]: "c \<noteq> 0"
+ shows "fls_compose_fps F (fps_const c * fps_X) $$ n = F $$ n * c powi n"
+proof -
+ {
+ assume *: "n \<ge> fls_subdegree F"
+ hence "c ^ nat (n - fls_subdegree F) = c powi int (nat (n - fls_subdegree F))"
+ by (simp add: power_int_def)
+ also have "\<dots> * c powi fls_subdegree F = c powi (int (nat (n - fls_subdegree F)) + fls_subdegree F)"
+ using * by (subst power_int_add) auto
+ also have "\<dots> = c powi n"
+ using * by simp
+ finally have "c ^ nat (n - fls_subdegree F) * c powi fls_subdegree F = c powi n" .
+ }
+ thus ?thesis
+ by (simp add: fls_compose_fps_def fps_compose_linear fls_times_fps_to_fls power_int_mult_distrib
+ fls_shifted_times_simps
+ flip: fls_const_power_int)
+qed
lemma fls_const_transfer [transfer_rule]:
"rel_fun (=) (pcr_fls (=))
@@ -3295,8 +3549,8 @@
lemma fls_nth_compose_power:
assumes "d > 0"
- shows "fls_nth (fls_compose_power f d) n = (if int d dvd n then fls_nth f (n div int d) else 0)"
- using assms by transfer auto
+ 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"
@@ -3385,8 +3639,8 @@
qed (use assms in auto)
lemma fls_nth_compose_power' [simp]:
- "d = 0 \<or> \<not>d dvd n \<Longrightarrow> fls_nth (fls_compose_power f d) n = 0"
- "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_nth (fls_compose_power f d) n = fls_nth f (n div d)"
+ "d = 0 \<or> \<not>d dvd n \<Longrightarrow> fls_compose_power f d $$ int n = 0"
+ "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_compose_power f d $$ int n = f $$ int (n div d)"
by (transfer; force; fail)+
subsection \<open>Formal differentiation and integration\<close>
@@ -3423,6 +3677,9 @@
lemma fls_deriv_one[simp]: "fls_deriv 1 = 0"
using fls_deriv_const[of 1] by simp
+lemma fls_deriv_numeral [simp]: "fls_deriv (numeral n) = 0"
+ by (metis fls_deriv_of_int of_int_numeral)
+
lemma fls_deriv_subdegree':
assumes "of_int (fls_subdegree f) * f $$ fls_subdegree f \<noteq> 0"
shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"