: ?goal when "x-k*2*pi \ 0" diff -r 05ad117ee3fb -r 386b1b33785c src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Feb 15 12:48:53 2023 +0000 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Feb 16 10:42:28 2023 +0000 @@ -332,6 +332,9 @@ lemma fls_shift_eq0_iff: "fls_shift m f = 0 \ f = 0" using fls_shift_eq_iff[of m f 0] by simp +lemma fls_shift_eq_1_iff: "fls_shift n f = 1 \ f = fls_shift (-n) 1" + by (metis add_minus_cancel fls_shift_eq_iff fls_shift_fls_shift) + lemma fls_shift_nonneg_subdegree: "m \ fls_subdegree f \ fls_subdegree (fls_shift m f) \ 0" by (cases "f=0") (auto intro: fls_subdegree_geI) @@ -699,6 +702,9 @@ thus "f $ n = g $ n" by simp qed +lemma fps_to_fls_eq_iff [simp]: "fps_to_fls f = fps_to_fls g \ f = g" + using fps_to_fls_eq_imp_fps_eq by blast + lemma fps_zero_to_fls [simp]: "fps_to_fls 0 = 0" by (intro fls_zero_eqI) simp @@ -723,9 +729,12 @@ lemma fps_X_to_fls [simp]: "fps_to_fls fps_X = fls_X" by (fastforce intro: fls_eqI) -lemma fps_to_fls_eq_zero_iff: "(fps_to_fls f = 0) \ (f=0)" +lemma fps_to_fls_eq_0_iff [simp]: "(fps_to_fls f = 0) \ (f=0)" using fps_to_fls_nonzeroI by auto +lemma fps_to_fls_eq_1_iff [simp]: "fps_to_fls f = 1 \ f = 1" + using fps_to_fls_eq_iff by fastforce + lemma fls_subdegree_fls_to_fps_gt0: "fls_subdegree (fps_to_fls f) \ 0" proof (cases "f=0") case False show ?thesis @@ -780,6 +789,25 @@ using fls_base_factor_fps_to_fls[of f] fls_regpart_fps_trivial[of "unit_factor f"] by simp +lemma fls_as_fps: + fixes f :: "'a :: zero fls" and n :: int + assumes n: "n \ -fls_subdegree f" + obtains f' where "f = fls_shift n (fps_to_fls f')" +proof - + have "fls_subdegree (fls_shift (- n) f) \ 0" + by (rule fls_shift_nonneg_subdegree) (use n in simp) + hence "f = fls_shift n (fps_to_fls (fls_regpart (fls_shift (-n) f)))" + by (subst fls_regpart_to_fls_trivial) simp_all + thus ?thesis + by (rule that) +qed + +lemma fls_as_fps': + fixes f :: "'a :: zero fls" and n :: int + assumes n: "n \ -fls_subdegree f" + shows "\f'. f = fls_shift n (fps_to_fls f')" + using fls_as_fps[OF assms] by metis + abbreviation "fls_regpart_as_fls f \ fps_to_fls (fls_regpart f)" abbreviation @@ -1719,10 +1747,12 @@ by (simp add: fls_times_conv_fps_times) qed simp +lemma fps_to_fls_power: "fps_to_fls (f ^ n) = fps_to_fls f ^ n" + by (simp add: fls_pow_conv_fps_pow fls_subdegree_fls_to_fps_gt0) + lemma fls_pow_conv_regpart: "fls_subdegree f \ 0 \ fls_regpart (f ^ n) = (fls_regpart f) ^ n" - using fls_pow_subdegree_ge0[of f n] fls_pow_conv_fps_pow[of f n] - by (intro fps_to_fls_eq_imp_fps_eq) simp + by (simp add: fls_pow_conv_fps_pow) text \These two lemmas show that shifting 1 is equivalent to powers of the implied variable.\ @@ -1995,17 +2025,7 @@ lemma fls_lr_inverse_eq0_imp_starting0: "fls_left_inverse f x = 0 \ x = 0" "fls_right_inverse f x = 0 \ x = 0" -proof- - assume "fls_left_inverse f x = 0" - hence "fps_left_inverse (fls_base_factor_to_fps f) x = 0" - using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce - thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(1) by fast -next - assume "fls_right_inverse f x = 0" - hence "fps_right_inverse (fls_base_factor_to_fps f) x = 0" - using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce - thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(2) by fast -qed + by (metis fls_lr_inverse_base fls_nonzeroI)+ lemma fls_lr_inverse_eq_0_iff: fixes x :: "'a::{comm_monoid_add,mult_zero,uminus}" @@ -3231,10 +3251,146 @@ thus "\g. 1 = g * f" by fast qed +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) + +lemma fls_const_transfer [transfer_rule]: + "rel_fun (=) (pcr_fls (=)) + (\c n. if n = 0 then c else 0) fls_const" + by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def) + +lemma fls_shift_transfer [transfer_rule]: + "rel_fun (=) (rel_fun (pcr_fls (=)) (pcr_fls (=))) + (\n f k. f (k+n)) fls_shift" + by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def) + +lift_definition fls_compose_power :: "'a :: zero fls \ nat \ 'a fls" is + "\f d n. if d > 0 \ int d dvd n then f (n div int d) else 0" +proof - + fix f :: "int \ 'a" and d :: nat + assume *: "eventually (\n. f (-int n) = 0) cofinite" + show "eventually (\n. (if d > 0 \ int d dvd -int n then f (-int n div int d) else 0) = 0) cofinite" + proof (cases "d = 0") + case False + from * have "eventually (\n. f (-int n) = 0) at_top" + by (simp add: cofinite_eq_sequentially) + hence "eventually (\n. f (-int (n div d)) = 0) at_top" + by (rule eventually_compose_filterlim[OF _ filterlim_at_top_div_const_nat]) (use False in auto) + hence "eventually (\n. (if d > 0 \ int d dvd -int n then f (-int n div int d) else 0) = 0) at_top" + by eventually_elim (auto simp: zdiv_int dvd_neg_div) + thus ?thesis + by (simp add: cofinite_eq_sequentially) + qed auto +qed + +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 + + +lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0" + by transfer auto + +lemma fls_compose_power_1_left [simp]: "d > 0 \ fls_compose_power 1 d = 1" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_const_left [simp]: + "d > 0 \ fls_compose_power (fls_const c) d = fls_const c" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_shift [simp]: + "d > 0 \ fls_compose_power (fls_shift n f) d = fls_shift (d * n) (fls_compose_power f d)" + by transfer (auto simp: fun_eq_iff add_ac mult_ac) + +lemma fls_compose_power_X_intpow [simp]: + "d > 0 \ fls_compose_power (fls_X_intpow n) d = fls_X_intpow (int d * n)" + by simp + +lemma fls_compose_power_X [simp]: + "d > 0 \ fls_compose_power fls_X d = fls_X_intpow (int d)" + by transfer (auto simp: fun_eq_iff) + +lemma fls_compose_power_X_inv [simp]: + "d > 0 \ fls_compose_power fls_X_inv d = fls_X_intpow (-int d)" + by (simp add: fls_X_inv_conv_shift_1) + +lemma fls_compose_power_0_right [simp]: "fls_compose_power f 0 = 0" + by transfer auto + +lemma fls_compose_power_add [simp]: + "fls_compose_power (f + g) d = fls_compose_power f d + fls_compose_power g d" + by transfer auto + +lemma fls_compose_power_diff [simp]: + "fls_compose_power (f - g) d = fls_compose_power f d - fls_compose_power g d" + by transfer auto + +lemma fls_compose_power_uminus [simp]: + "fls_compose_power (-f) d = -fls_compose_power f d" + by transfer auto + +lemma fps_nth_compose_X_power: + "fps_nth (f oo (fps_X ^ d)) n = (if d dvd n then fps_nth f (n div d) else 0)" +proof - + have "fps_nth (f oo (fps_X ^ d)) n = (\i = 0..n. f $ i * (fps_X ^ (d * i)) $ n)" + unfolding fps_compose_def by (simp add: power_mult) + also have "\ = (\i\(if d dvd n then {n div d} else {}). f $ i * (fps_X ^ (d * i)) $ n)" + by (intro sum.mono_neutral_right) auto + also have "\ = (if d dvd n then fps_nth f (n div d) else 0)" + by auto + finally show ?thesis . +qed + +lemma fls_compose_power_fps_to_fls: + assumes "d > 0" + shows "fls_compose_power (fps_to_fls f) d = fps_to_fls (fps_compose f (fps_X ^ d))" + using assms + by (intro fls_eqI) (auto simp: fls_nth_compose_power fps_nth_compose_X_power + pos_imp_zdiv_neg_iff div_neg_pos_less0 nat_div_distrib + simp flip: int_dvd_int_iff) + +lemma fls_compose_power_mult [simp]: + "fls_compose_power (f * g :: 'a :: idom fls) d = fls_compose_power f d * fls_compose_power g d" +proof (cases "d > 0") + case True + define n where "n = nat (max 0 (max (- fls_subdegree f) (- fls_subdegree g)))" + have n_ge: "-fls_subdegree f \ int n" "-fls_subdegree g \ int n" + unfolding n_def by auto + obtain f' where f': "f = fls_shift n (fps_to_fls f')" + using fls_as_fps[OF n_ge(1)] by (auto simp: n_def) + obtain g' where g': "g = fls_shift n (fps_to_fls g')" + using fls_as_fps[OF n_ge(2)] by (auto simp: n_def) + show ?thesis using \d > 0\ + by (simp add: f' g' fls_shifted_times_simps mult_ac fls_compose_power_fps_to_fls + fps_compose_mult_distrib flip: fls_times_fps_to_fls) +qed auto + +lemma fls_compose_power_power [simp]: + assumes "d > 0 \ n > 0" + shows "fls_compose_power (f ^ n :: 'a :: idom fls) d = fls_compose_power f d ^ n" +proof (cases "d > 0") + case True + thus ?thesis by (induction n) auto +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)" + by (transfer; force; fail)+ subsection \Formal differentiation and integration\ - subsubsection \Derivative definition and basic properties\ definition "fls_deriv f = Abs_fls (\n. of_int (n+1) * f$$(n+1))" diff -r 05ad117ee3fb -r 386b1b33785c src/HOL/Filter.thy --- a/src/HOL/Filter.thy Wed Feb 15 12:48:53 2023 +0000 +++ b/src/HOL/Filter.thy Thu Feb 16 10:42:28 2023 +0000 @@ -1511,7 +1511,21 @@ fixes f :: "'a \ ('b::unbounded_dense_linorder)" and c :: "'b" shows "(LIM x F. f x :> at_bot) \ (\Zx. Z \ f x) F)" by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans) - + +lemma filterlim_at_top_div_const_nat: + assumes "c > 0" + shows "filterlim (\x::nat. x div c) at_top at_top" + unfolding filterlim_at_top +proof + fix C :: nat + have *: "n div c \ C" if "n \ C * c" for n + using assms that by (metis div_le_mono div_mult_self_is_m) + have "eventually (\n. n \ C * c) at_top" + by (rule eventually_ge_at_top) + thus "eventually (\n. n div c \ C) at_top" + by eventually_elim (use * in auto) +qed + lemma filterlim_finite_subsets_at_top: "filterlim f (finite_subsets_at_top A) F \ (\X. finite X \ X \ A \ eventually (\y. finite (f y) \ X \ f y \ f y \ A) F)"