# HG changeset patch # User paulson # Date 1697110569 -3600 # Node ID 80b4f6a0808dcfbfe4058d544ad4034175d2e9b5 # Parent f229090cb8a3be70b0801dbac61d231d93306496 Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts diff -r f229090cb8a3 -r 80b4f6a0808d src/HOL/Complex_Analysis/Laurent_Convergence.thy --- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Wed Oct 11 17:02:33 2023 +0100 +++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Thu Oct 12 12:36:09 2023 +0100 @@ -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 \ 0 \ fls_nth (numeral n) k = 0" - by (subst fls_const_numeral [symmetric], subst fls_const_nth, simp)+ - -lemma fls_subdegree_prod: - fixes F :: "'a \ 'b :: field_char_0 fls" - assumes "\x. x \ I \ F x \ 0" - shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" - using assms by (induction I rule: infinite_finite_induct) auto - -lemma fls_subdegree_prod': - fixes F :: "'a \ 'b :: field_char_0 fls" - assumes "\x. x \ I \ fls_subdegree (F x) \ 0" - shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" -proof (intro fls_subdegree_prod) - show "F x \ 0" if "x \ I" for x - using assms[OF that] by auto -qed - instance fps :: (semiring_char_0) semiring_char_0 proof show "inj (of_nat :: nat \ 'a fps)" @@ -2187,211 +2151,6 @@ by simp qed -hide_const (open) fls_compose_fps - -definition fls_compose_fps :: "'a :: field fls \ 'a fps \ '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 \ 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 \ 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 \ 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' \ 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 \ 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 \ 0" "G \ 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 "\ = 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 "\ = 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 \ 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 \ 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 \ G = 0") - case False - hence [simp]: "F \ 0" "G \ 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 \ 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 "\ = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n" - by (subst fls_compose_fps_to_fls) auto - also have "\ = 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 \ 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 \ F = 0 \ (G = 0 \ fps_nth F 0 = 0)" -proof safe - assume *: "fps_compose F G = 0" "F \ 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 \ 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 = (\i = 0..N. fps_nth F i * fps_nth (G ^ i) N)" - unfolding fps_compose_def by (simp add: N_def) - also have "\ = (\i\{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)" - proof (intro sum.mono_neutral_right ballI) - fix i assume i: "i \ {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 \subdegree G > 0\ by (intro fps_pow_nth_below_subdegree) (auto simp: N_def) - thus ?thesis by simp - qed (use i in \auto simp: N_def\) - qed (use \subdegree G > 0\ in \auto simp: N_def\) - also have "\ = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N" - by simp - also have "\ \ 0" - using \G \ 0\ \F \ 0\ by (auto simp: N_def) - finally show False using * by auto - qed -qed auto - -lemma fls_compose_fps_eq_0_iff: - assumes "H \ 0" "fps_nth H 0 = 0" - shows "fls_compose_fps F H = 0 \ 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 \ 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 \ 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 \ 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 \ 0" "fps_nth G 0 = 0" "H \ 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 \ F \ 0 \ 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 \ 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 \ 0" - shows "fls_nth (fls_compose_fps F (fps_const c * fps_X)) n = fls_nth F n * c powi n" -proof - - { - assume *: "n \ 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 "\ * 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 "\ = 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 (\z. f z * g z \ 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 diff -r f229090cb8a3 -r 80b4f6a0808d src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 11 17:02:33 2023 +0100 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Oct 12 12:36:09 2023 +0100 @@ -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 \ 0 \ 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 \Powers\ +lemma fls_subdegree_prod: + fixes F :: "'a \ 'b :: field_char_0 fls" + assumes "\x. x \ I \ F x \ 0" + shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" + using assms by (induction I rule: infinite_finite_induct) auto + +lemma fls_subdegree_prod': + fixes F :: "'a \ 'b :: field_char_0 fls" + assumes "\x. x \ I \ fls_subdegree (F x) \ 0" + shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" +proof (intro fls_subdegree_prod) + show "F x \ 0" if "x \ I" for x + using assms[OF that] by auto +qed + lemma fls_pow_subdegree_ge: "f^n \ 0 \ fls_subdegree (f^n) \ n * fls_subdegree f" proof (induct n) @@ -3254,15 +3287,236 @@ subsection \Composition\ definition fls_compose_fps :: "'a :: field fls \ 'a fps \ 'a fls" where - "fls_compose_fps f g = - (if f = 0 then 0 - else if fls_subdegree f \ 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 \ 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 \ 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 \ 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' \ 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 \ 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 \ 0" "G \ 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 "\ = 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 "\ = 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 \ 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 \ 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 \ G = 0") + case False + hence [simp]: "F \ 0" "G \ 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 \ 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 "\ = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n" + by (subst fls_compose_fps_to_fls) auto + also have "\ = 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 \ 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 \ F = 0 \ (G = 0 \ fps_nth F 0 = 0)" +proof safe + assume *: "fps_compose F G = 0" "F \ 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 \ 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 = (\i = 0..N. fps_nth F i * fps_nth (G ^ i) N)" + unfolding fps_compose_def by (simp add: N_def) + also have "\ = (\i\{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)" + proof (intro sum.mono_neutral_right ballI) + fix i assume i: "i \ {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 \subdegree G > 0\ by (intro fps_pow_nth_below_subdegree) (auto simp: N_def) + thus ?thesis by simp + qed (use i in \auto simp: N_def\) + qed (use \subdegree G > 0\ in \auto simp: N_def\) + also have "\ = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N" + by simp + also have "\ \ 0" + using \G \ 0\ \F \ 0\ by (auto simp: N_def) + finally show False using * by auto + qed +qed auto + +lemma fls_compose_fps_eq_0_iff: + assumes "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps F H = 0 \ 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 \ 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 \ 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 \ 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 \ 0" "fps_nth G 0 = 0" "H \ 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 \ F \ 0 \ 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 \ 0" + shows "fls_compose_fps F (fps_const c * fps_X) $$ n = F $$ n * c powi n" +proof - + { + assume *: "n \ 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 "\ * 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 "\ = 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 \ \d dvd n \ fls_nth (fls_compose_power f d) n = 0" - "d dvd n \ d > 0 \ fls_nth (fls_compose_power f d) n = fls_nth f (n div d)" + "d = 0 \ \d dvd n \ fls_compose_power f d $$ int n = 0" + "d dvd n \ d > 0 \ fls_compose_power f d $$ int n = f $$ int (n div d)" by (transfer; force; fail)+ subsection \Formal differentiation and integration\ @@ -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 \ 0" shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"