HOL-Analysis: Convergent FPS and infinite sums
authorManuel Eberl <eberlm@in.tum.de>
Mon Aug 21 20:49:15 2017 +0200 (21 months ago)
changeset 664804b8d1df8933b
parent 66479 5c0a3f63057d
child 66481 d35f7a9f92e2
HOL-Analysis: Convergent FPS and infinite sums
CONTRIBUTORS
NEWS
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/FPS_Convergence.thy
src/HOL/Analysis/Infinite_Set_Sum.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Computational_Algebra/Polynomial_FPS.thy
     1.1 --- a/CONTRIBUTORS	Mon Aug 21 19:20:02 2017 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Aug 21 20:49:15 2017 +0200
     1.3 @@ -14,6 +14,11 @@
     1.4    Prover IDE improvements.
     1.5    Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
     1.6  
     1.7 +* August 2017: Manuel Eberl, TUM
     1.8 +  HOL-Analysis: infinite products over natural numbers,
     1.9 +  infinite sums over arbitrary sets, connection between formal
    1.10 +  power series and analytic complex functions
    1.11 +
    1.12  * March 2017: Alasdair Armstrong, University of Sheffield and
    1.13    Simon Foster, University of York
    1.14    Fixed-point theory and Galois Connections in HOL-Algebra.
     2.1 --- a/NEWS	Mon Aug 21 19:20:02 2017 +0200
     2.2 +++ b/NEWS	Mon Aug 21 20:49:15 2017 +0200
     2.3 @@ -215,8 +215,8 @@
     2.4  * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
     2.5  been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
     2.6  
     2.7 -* Theory "HOL-Library.Formal_Power_Series": constants E/L/F have been
     2.8 -renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
     2.9 +* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
    2.10 +renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
    2.11  space. INCOMPATIBILITY.
    2.12  
    2.13  * Theory "HOL-Library.FinFun" has been moved to AFP (again).
     3.1 --- a/src/HOL/Analysis/Analysis.thy	Mon Aug 21 19:20:02 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Analysis.thy	Mon Aug 21 20:49:15 2017 +0200
     3.3 @@ -11,6 +11,7 @@
     3.4    Bounded_Continuous_Function
     3.5    Function_Topology
     3.6    Infinite_Products
     3.7 +  Infinite_Set_Sum
     3.8    Weierstrass_Theorems
     3.9    Polytope
    3.10    Jordan_Curve
    3.11 @@ -18,6 +19,7 @@
    3.12    Great_Picard
    3.13    Poly_Roots
    3.14    Conformal_Mappings
    3.15 +  FPS_Convergence
    3.16    Generalised_Binomial_Theorem
    3.17    Gamma_Function
    3.18  begin
     4.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 19:20:02 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 20:49:15 2017 +0200
     4.3 @@ -73,6 +73,10 @@
     4.4  lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
     4.5    by (simp add: field_differentiable_within_exp holomorphic_on_def)
     4.6  
     4.7 +lemma holomorphic_on_exp' [holomorphic_intros]:
     4.8 +  "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
     4.9 +  using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
    4.10 +
    4.11  subsection\<open>Euler and de Moivre formulas.\<close>
    4.12  
    4.13  text\<open>The sine series times @{term i}\<close>
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Mon Aug 21 20:49:15 2017 +0200
     5.3 @@ -0,0 +1,1277 @@
     5.4 +(*  
     5.5 +  Title:    HOL/Analysis/FPS_Convergence.thy
     5.6 +  Author:   Manuel Eberl, TU München
     5.7 +
     5.8 +  Connection of formal power series and actual convergent power series on Banach spaces
     5.9 +  (most notably the complex numbers).
    5.10 +*)
    5.11 +section \<open>Convergence of formal power series\<close>
    5.12 +theory FPS_Convergence
    5.13 +imports
    5.14 +  Conformal_Mappings
    5.15 +  Generalised_Binomial_Theorem
    5.16 +  "HOL-Computational_Algebra.Formal_Power_Series"
    5.17 +begin
    5.18 +
    5.19 +subsection \<open>Balls with extended real radius\<close>
    5.20 +
    5.21 +text \<open>
    5.22 +  The following is a variant of @{const ball} that also allows an infinite radius.
    5.23 +\<close>
    5.24 +definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where
    5.25 +  "eball z r = {z'. ereal (dist z z') < r}"
    5.26 +
    5.27 +lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r"
    5.28 +  by (simp add: eball_def)
    5.29 +
    5.30 +lemma eball_ereal [simp]: "eball z (ereal r) = ball z r"
    5.31 +  by auto
    5.32 +
    5.33 +lemma eball_inf [simp]: "eball z \<infinity> = UNIV"
    5.34 +  by auto
    5.35 +
    5.36 +lemma eball_empty [simp]: "r \<le> 0 \<Longrightarrow> eball z r = {}"
    5.37 +proof safe
    5.38 +  fix x assume "r \<le> 0" "x \<in> eball z r"
    5.39 +  hence "dist z x < r" by simp
    5.40 +  also have "\<dots> \<le> ereal 0" using \<open>r \<le> 0\<close> by (simp add: zero_ereal_def)
    5.41 +  finally show "x \<in> {}" by simp
    5.42 +qed
    5.43 +
    5.44 +lemma eball_conv_UNION_balls:
    5.45 +  "eball z r = (\<Union>r'\<in>{r'. ereal r' < r}. ball z r')"
    5.46 +  by (cases r) (use dense gt_ex in force)+
    5.47 +
    5.48 +lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'"
    5.49 +  by auto
    5.50 +
    5.51 +lemma ball_eball_mono: "ereal r \<le> r' \<Longrightarrow> ball z r \<le> eball z r'"
    5.52 +  using eball_mono[of "ereal r" r'] by simp
    5.53 +
    5.54 +lemma open_eball [simp, intro]: "open (eball z r)" 
    5.55 +  by (cases r) auto
    5.56 +
    5.57 +
    5.58 +subsection \<open>Basic properties of convergent power series\<close>
    5.59 +
    5.60 +definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
    5.61 +  "fps_conv_radius f = conv_radius (fps_nth f)"
    5.62 +
    5.63 +definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
    5.64 +  "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
    5.65 +
    5.66 +definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
    5.67 +  "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
    5.68 +
    5.69 +lemma norm_summable_fps:
    5.70 +  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
    5.71 +  shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fps_nth f n * z ^ n))"
    5.72 +  by (rule abs_summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
    5.73 +
    5.74 +lemma summable_fps:
    5.75 +  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
    5.76 +  shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
    5.77 +  by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
    5.78 +
    5.79 +lemma sums_eval_fps:
    5.80 +  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
    5.81 +  assumes "norm z < fps_conv_radius f"
    5.82 +  shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
    5.83 +  using assms unfolding eval_fps_def fps_conv_radius_def
    5.84 +  by (intro summable_sums summable_in_conv_radius) simp_all
    5.85 +
    5.86 +lemma
    5.87 +  fixes r :: ereal
    5.88 +  assumes "f holomorphic_on eball z0 r"
    5.89 +  shows   conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r"
    5.90 +    and   eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z"
    5.91 +    and   eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)"
    5.92 +proof -
    5.93 +  have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
    5.94 +    if "z \<in> ball z0 r'" "ereal r' < r" for z r'
    5.95 +  proof -
    5.96 +    from that(2) have "ereal r' \<le> r" by simp
    5.97 +    from assms(1) and this have "f holomorphic_on ball z0 r'"
    5.98 +      by (rule holomorphic_on_subset[OF _ ball_eball_mono])
    5.99 +    from holomorphic_power_series [OF this that(1)] 
   5.100 +      show ?thesis by (simp add: fps_expansion_def)
   5.101 +  qed
   5.102 +  hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
   5.103 +    if "z \<in> eball z0 r" for z
   5.104 +    using that by (subst (asm) eball_conv_UNION_balls) blast
   5.105 +  show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def
   5.106 +  proof (rule conv_radius_geI_ex)
   5.107 +    fix r' :: real assume r': "r' > 0" "ereal r' < r"
   5.108 +    thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)"
   5.109 +      using *[of "z0 + of_real r'"]
   5.110 +      by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm)
   5.111 +  qed
   5.112 +  show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z
   5.113 +    using *[OF that] by (simp add: eval_fps_def sums_iff)
   5.114 +  show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z
   5.115 +    using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm)
   5.116 +qed
   5.117 +
   5.118 +lemma continuous_on_eval_fps:
   5.119 +  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
   5.120 +  shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)"
   5.121 +proof (subst continuous_on_eq_continuous_at [OF open_eball], safe)
   5.122 +  fix x :: 'a assume x: "x \<in> eball 0 (fps_conv_radius f)"
   5.123 +  define r where "r = (if fps_conv_radius f = \<infinity> then norm x + 1 else
   5.124 +                        (norm x + real_of_ereal (fps_conv_radius f)) / 2)"
   5.125 +  have r: "norm x < r \<and> ereal r < fps_conv_radius f"
   5.126 +    using x by (cases "fps_conv_radius f") 
   5.127 +               (auto simp: r_def eball_def split: if_splits)
   5.128 +
   5.129 +  have "continuous_on (cball 0 r) (\<lambda>x. \<Sum>i. fps_nth f i * (x - 0) ^ i)"
   5.130 +    by (rule powser_continuous_suminf) (insert r, auto simp: fps_conv_radius_def)
   5.131 +  hence "continuous_on (cball 0 r) (eval_fps f)"
   5.132 +    by (simp add: eval_fps_def)
   5.133 +  thus "isCont (eval_fps f) x"
   5.134 +    by (rule continuous_on_interior) (use r in auto)
   5.135 +qed
   5.136 +
   5.137 +lemma continuous_on_eval_fps' [continuous_intros]:
   5.138 +  assumes "continuous_on A g"
   5.139 +  assumes "g ` A \<subseteq> eball 0 (fps_conv_radius f)"
   5.140 +  shows   "continuous_on A (\<lambda>x. eval_fps f (g x))"
   5.141 +  using continuous_on_compose2[OF continuous_on_eval_fps assms] .
   5.142 +
   5.143 +lemma has_field_derivative_powser:
   5.144 +  fixes z :: "'a :: {banach, real_normed_field}"
   5.145 +  assumes "ereal (norm z) < conv_radius f"
   5.146 +  shows   "((\<lambda>z. \<Sum>n. f n * z ^ n) has_field_derivative (\<Sum>n. diffs f n * z ^ n)) (at z within A)"
   5.147 +proof -
   5.148 +  define K where "K = (if conv_radius f = \<infinity> then norm z + 1 
   5.149 +                         else (norm z + real_of_ereal (conv_radius f)) / 2)"
   5.150 +  have K: "norm z < K \<and> ereal K < conv_radius f"
   5.151 +    using assms by (cases "conv_radius f") (auto simp: K_def)
   5.152 +  have "0 \<le> norm z" by simp
   5.153 +  also from K have "\<dots> < K" by simp
   5.154 +  finally have K_pos: "K > 0" by simp
   5.155 +
   5.156 +  have "summable (\<lambda>n. f n * of_real K ^ n)"
   5.157 +    using K and K_pos by (intro summable_in_conv_radius) auto
   5.158 +  moreover from K and K_pos have "norm z < norm (of_real K :: 'a)" by auto
   5.159 +  ultimately show ?thesis
   5.160 +    by (rule has_field_derivative_at_within [OF termdiffs_strong])
   5.161 +qed
   5.162 +
   5.163 +lemma has_field_derivative_eval_fps:
   5.164 +  fixes z :: "'a :: {banach, real_normed_field}"
   5.165 +  assumes "norm z < fps_conv_radius f"
   5.166 +  shows   "(eval_fps f has_field_derivative eval_fps (fps_deriv f) z) (at z within A)"
   5.167 +proof -
   5.168 +  have "(eval_fps f has_field_derivative eval_fps (Abs_fps (diffs (fps_nth f))) z) (at z within A)"
   5.169 +    using assms unfolding eval_fps_def fps_nth_Abs_fps fps_conv_radius_def
   5.170 +    by (intro has_field_derivative_powser) auto
   5.171 +  also have "Abs_fps (diffs (fps_nth f)) = fps_deriv f"
   5.172 +    by (simp add: fps_eq_iff diffs_def)
   5.173 +  finally show ?thesis .
   5.174 +qed
   5.175 +
   5.176 +lemma holomorphic_on_eval_fps [holomorphic_intros]:
   5.177 +  fixes z :: "'a :: {banach, real_normed_field}"
   5.178 +  assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
   5.179 +  shows   "eval_fps f holomorphic_on A"
   5.180 +proof (rule holomorphic_on_subset [OF _ assms])
   5.181 +  show "eval_fps f holomorphic_on eball 0 (fps_conv_radius f)"
   5.182 +  proof (subst holomorphic_on_open [OF open_eball], safe, goal_cases)
   5.183 +    case (1 x)
   5.184 +    thus ?case
   5.185 +      by (intro exI[of _ "eval_fps (fps_deriv f) x"]) (auto intro: has_field_derivative_eval_fps)
   5.186 +  qed
   5.187 +qed
   5.188 +
   5.189 +lemma analytic_on_eval_fps:
   5.190 +  fixes z :: "'a :: {banach, real_normed_field}"
   5.191 +  assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
   5.192 +  shows   "eval_fps f analytic_on A"
   5.193 +proof (rule analytic_on_subset [OF _ assms])
   5.194 +  show "eval_fps f analytic_on eball 0 (fps_conv_radius f)"
   5.195 +    using holomorphic_on_eval_fps[of "eball 0 (fps_conv_radius f)"] 
   5.196 +    by (subst analytic_on_open) auto
   5.197 +qed
   5.198 +
   5.199 +
   5.200 +subsection \<open>Lower bounds on radius of convergence\<close>
   5.201 +
   5.202 +lemma fps_conv_radius_deriv:
   5.203 +  fixes f :: "'a :: {banach, real_normed_field} fps"
   5.204 +  shows "fps_conv_radius (fps_deriv f) \<ge> fps_conv_radius f"
   5.205 +  unfolding fps_conv_radius_def
   5.206 +proof (rule conv_radius_geI_ex)
   5.207 +  fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)"
   5.208 +  define K where "K = (if conv_radius (fps_nth f) = \<infinity> then r + 1 
   5.209 +                         else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)"
   5.210 +  have K: "r < K \<and> ereal K < conv_radius (fps_nth f)"
   5.211 +    using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def)
   5.212 +  have "summable (\<lambda>n. diffs (fps_nth f) n * of_real r ^ n)"
   5.213 +  proof (rule termdiff_converges)
   5.214 +    fix x :: 'a assume "norm x < K"
   5.215 +    hence "ereal (norm x) < ereal K" by simp
   5.216 +    also have "\<dots> < conv_radius (fps_nth f)" using K by simp
   5.217 +    finally show "summable (\<lambda>n. fps_nth f n * x ^ n)"
   5.218 +      by (intro summable_in_conv_radius) auto
   5.219 +  qed (insert K r, auto)
   5.220 +  also have "\<dots> = (\<lambda>n. fps_nth (fps_deriv f) n * of_real r ^ n)"
   5.221 +    by (simp add: fps_deriv_def diffs_def)
   5.222 +  finally show "\<exists>z::'a. norm z = r \<and> summable (\<lambda>n. fps_nth (fps_deriv f) n * z ^ n)"
   5.223 +    using r by (intro exI[of _ "of_real r"]) auto
   5.224 +qed
   5.225 +
   5.226 +lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"
   5.227 +  by (simp add: eval_fps_def)
   5.228 +
   5.229 +lemma fps_conv_radius_norm [simp]: 
   5.230 +  "fps_conv_radius (Abs_fps (\<lambda>n. norm (fps_nth f n))) = fps_conv_radius f"
   5.231 +  by (simp add: fps_conv_radius_def)
   5.232 +
   5.233 +lemma fps_conv_radius_const [simp]: "fps_conv_radius (fps_const c) = \<infinity>"
   5.234 +proof -
   5.235 +  have "fps_conv_radius (fps_const c) = conv_radius (\<lambda>_. 0 :: 'a)"
   5.236 +    unfolding fps_conv_radius_def
   5.237 +    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto
   5.238 +  thus ?thesis by simp
   5.239 +qed
   5.240 +
   5.241 +lemma fps_conv_radius_0 [simp]: "fps_conv_radius 0 = \<infinity>"
   5.242 +  by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const)
   5.243 +
   5.244 +lemma fps_conv_radius_1 [simp]: "fps_conv_radius 1 = \<infinity>"
   5.245 +  by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const)
   5.246 +
   5.247 +lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>"
   5.248 +  by (simp add: numeral_fps_const)
   5.249 +
   5.250 +lemma fps_conv_radius_fps_X_power [simp]: "fps_conv_radius (fps_X ^ n) = \<infinity>"
   5.251 +proof -
   5.252 +  have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (\<lambda>_. 0 :: 'a)"
   5.253 +    unfolding fps_conv_radius_def 
   5.254 +    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of n]]) 
   5.255 +       (auto simp: fps_X_power_iff)
   5.256 +  thus ?thesis by simp
   5.257 +qed
   5.258 +
   5.259 +lemma fps_conv_radius_fps_X [simp]: "fps_conv_radius fps_X = \<infinity>"
   5.260 +  using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right)
   5.261 +
   5.262 +lemma fps_conv_radius_shift [simp]:
   5.263 +  "fps_conv_radius (fps_shift n f) = fps_conv_radius f"
   5.264 +  by (simp add: fps_conv_radius_def fps_shift_def conv_radius_shift)
   5.265 +
   5.266 +lemma fps_conv_radius_cmult_left:
   5.267 +  "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (fps_const c * f) = fps_conv_radius f"
   5.268 +  unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_left)
   5.269 +
   5.270 +lemma fps_conv_radius_cmult_right:
   5.271 +  "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (f * fps_const c) = fps_conv_radius f"
   5.272 +  unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_right)
   5.273 +
   5.274 +lemma fps_conv_radius_uminus [simp]:
   5.275 +  "fps_conv_radius (-f) = fps_conv_radius f"
   5.276 +  using fps_conv_radius_cmult_left[of "-1" f]
   5.277 +  by (simp add: fps_const_neg [symmetric] del: fps_const_neg)
   5.278 +
   5.279 +lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
   5.280 +  unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
   5.281 +  by simp
   5.282 +
   5.283 +lemma fps_conv_radius_diff: "fps_conv_radius (f - g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
   5.284 +  using fps_conv_radius_add[of f "-g"] by simp
   5.285 +
   5.286 +lemma fps_conv_radius_mult: "fps_conv_radius (f * g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
   5.287 +  using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"]
   5.288 +  by (simp add: fps_mult_nth fps_conv_radius_def atLeast0AtMost)
   5.289 +
   5.290 +lemma fps_conv_radius_power: "fps_conv_radius (f ^ n) \<ge> fps_conv_radius f"
   5.291 +proof (induction n)
   5.292 +  case (Suc n)
   5.293 +  hence "fps_conv_radius f \<le> min (fps_conv_radius f) (fps_conv_radius (f ^ n))"
   5.294 +    by simp
   5.295 +  also have "\<dots> \<le> fps_conv_radius (f * f ^ n)" 
   5.296 +    by (rule fps_conv_radius_mult)
   5.297 +  finally show ?case by simp
   5.298 +qed simp_all
   5.299 +
   5.300 +context
   5.301 +begin
   5.302 +
   5.303 +lemma natfun_inverse_bound:
   5.304 +  fixes f :: "'a :: {real_normed_field} fps"
   5.305 +  assumes "fps_nth f 0 = 1" and "\<delta> > 0" 
   5.306 +      and summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
   5.307 +      and le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
   5.308 +  shows   "norm (natfun_inverse f n) \<le> inverse (\<delta> ^ n)"
   5.309 +proof (induction n rule: less_induct)
   5.310 +  case (less m)
   5.311 +  show ?case
   5.312 +  proof (cases m)
   5.313 +    case 0
   5.314 +    thus ?thesis using assms by (simp add: divide_simps norm_inverse norm_divide)
   5.315 +  next
   5.316 +    case [simp]: (Suc n)
   5.317 +    have "norm (natfun_inverse f (Suc n)) = 
   5.318 +            norm (\<Sum>i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))"
   5.319 +      (is "_ = norm ?S") using assms 
   5.320 +      by (simp add: field_simps norm_mult norm_divide del: sum_cl_ivl_Suc)
   5.321 +    also have "norm ?S \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))"
   5.322 +      by (rule norm_sum)
   5.323 +    also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (Suc n - i))"
   5.324 +    proof (intro sum_mono, goal_cases)
   5.325 +      case (1 i)
   5.326 +      have "norm (fps_nth f i * natfun_inverse f (Suc n - i)) =
   5.327 +              norm (fps_nth f i) * norm (natfun_inverse f (Suc n - i))"
   5.328 +        by (simp add: norm_mult)
   5.329 +      also have "\<dots> \<le> norm (fps_nth f i) * inverse (\<delta> ^ (Suc n - i))"
   5.330 +        using 1 by (intro mult_left_mono less.IH) auto
   5.331 +      also have "\<dots> = norm (fps_nth f i) / \<delta> ^ (Suc n - i)"
   5.332 +        by (simp add: divide_simps)
   5.333 +      finally show ?case .
   5.334 +    qed
   5.335 +    also have "\<dots> = (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) / \<delta> ^ Suc n"
   5.336 +      by (subst sum_divide_distrib, rule sum.cong)
   5.337 +         (insert \<open>\<delta> > 0\<close>, auto simp: field_simps power_diff)
   5.338 +    also have "(\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) =
   5.339 +                 (\<Sum>i=0..n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i))"
   5.340 +      by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all
   5.341 +    also have "{0..n} = {..<Suc n}" by auto
   5.342 +    also have "(\<Sum>i< Suc n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i)) \<le> 
   5.343 +                 (\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ (Suc n))"
   5.344 +      using \<open>\<delta> > 0\<close> by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto
   5.345 +    also have "\<dots> \<le> 1" by fact
   5.346 +    finally show ?thesis using \<open>\<delta> > 0\<close> 
   5.347 +      by (simp add: divide_right_mono divide_simps)
   5.348 +  qed
   5.349 +qed
   5.350 +
   5.351 +private lemma fps_conv_radius_inverse_pos_aux:
   5.352 +  fixes f :: "'a :: {banach, real_normed_field} fps"
   5.353 +  assumes "fps_nth f 0 = 1" "fps_conv_radius f > 0"
   5.354 +  shows   "fps_conv_radius (inverse f) > 0"
   5.355 +proof -
   5.356 +  let ?R = "fps_conv_radius f"
   5.357 +  define h where "h = Abs_fps (\<lambda>n. norm (fps_nth f n))"
   5.358 +  have [simp]: "fps_conv_radius h = ?R" by (simp add: h_def)
   5.359 +  have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)"
   5.360 +    by (intro continuous_on_eval_fps)
   5.361 +  hence *: "open (eval_fps h -` A \<inter> eball 0 ?R)" if "open A" for A
   5.362 +    using that by (subst (asm) continuous_on_open_vimage) auto
   5.363 +  have "open (eval_fps h -` {..<2} \<inter> eball 0 ?R)"
   5.364 +    by (rule *) auto
   5.365 +  moreover have "0 \<in> eval_fps h -` {..<2} \<inter> eball 0 ?R"
   5.366 +    using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def)
   5.367 +  ultimately obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "ball 0 \<epsilon> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R"
   5.368 +    by (subst (asm) open_contains_ball_eq) blast+
   5.369 +
   5.370 +  define \<delta> where "\<delta> = real_of_ereal (min (ereal \<epsilon> / 2) (?R / 2))"
   5.371 +  have \<delta>: "0 < \<delta> \<and> \<delta> < \<epsilon> \<and> ereal \<delta> < ?R"
   5.372 +    using \<open>\<epsilon> > 0\<close> and assms by (cases ?R) (auto simp: \<delta>_def min_def)
   5.373 +
   5.374 +  have summable: "summable (\<lambda>n. norm (fps_nth f n) * \<delta> ^ n)"
   5.375 +    using \<delta> by (intro summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
   5.376 +  hence "(\<lambda>n. norm (fps_nth f n) * \<delta> ^ n) sums eval_fps h \<delta>"
   5.377 +    by (simp add: eval_fps_def summable_sums h_def)
   5.378 +  hence "(\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) sums (eval_fps h \<delta> - 1)"
   5.379 +    by (subst sums_Suc_iff) (auto simp: assms)
   5.380 +  moreover {
   5.381 +    from \<delta> have "\<delta> \<in> ball 0 \<epsilon>" by auto
   5.382 +    also have "\<dots> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" by fact
   5.383 +    finally have "eval_fps h \<delta> < 2" by simp
   5.384 +  }
   5.385 +  ultimately have le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
   5.386 +    by (simp add: sums_iff)
   5.387 +  from summable have summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
   5.388 +    by (subst summable_Suc_iff)
   5.389 +
   5.390 +  have "0 < \<delta>" using \<delta> by blast
   5.391 +  also have "\<delta> = inverse (limsup (\<lambda>n. ereal (inverse \<delta>)))"
   5.392 +    using \<delta> by (subst Limsup_const) auto
   5.393 +  also have "\<dots> \<le> conv_radius (natfun_inverse f)"
   5.394 +    unfolding conv_radius_def
   5.395 +  proof (intro ereal_inverse_antimono Limsup_mono
   5.396 +           eventually_mono[OF eventually_gt_at_top[of 0]])
   5.397 +    fix n :: nat assume n: "n > 0"
   5.398 +    have "root n (norm (natfun_inverse f n)) \<le> root n (inverse (\<delta> ^ n))"
   5.399 +      using n assms \<delta> le summable 
   5.400 +      by (intro real_root_le_mono natfun_inverse_bound) auto
   5.401 +    also have "\<dots> = inverse \<delta>"
   5.402 +      using n \<delta> by (simp add: power_inverse [symmetric] real_root_pos2)
   5.403 +    finally show "ereal (inverse \<delta>) \<ge> ereal (root n (norm (natfun_inverse f n)))" 
   5.404 +      by (subst ereal_less_eq)
   5.405 +  next
   5.406 +    have "0 = limsup (\<lambda>n. 0::ereal)" 
   5.407 +      by (rule Limsup_const [symmetric]) auto
   5.408 +    also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (natfun_inverse f n))))"
   5.409 +      by (intro Limsup_mono) (auto simp: real_root_ge_zero)
   5.410 +    finally show "0 \<le> \<dots>" by simp
   5.411 +  qed
   5.412 +  also have "\<dots> = fps_conv_radius (inverse f)"
   5.413 +    using assms by (simp add: fps_conv_radius_def fps_inverse_def)
   5.414 +  finally show ?thesis by (simp add: zero_ereal_def)
   5.415 +qed
   5.416 +
   5.417 +lemma fps_conv_radius_inverse_pos:
   5.418 +  fixes f :: "'a :: {banach, real_normed_field} fps"
   5.419 +  assumes "fps_nth f 0 \<noteq> 0" and "fps_conv_radius f > 0"
   5.420 +  shows   "fps_conv_radius (inverse f) > 0"
   5.421 +proof -
   5.422 +  let ?c = "fps_nth f 0"
   5.423 +  have "fps_conv_radius (inverse f) = fps_conv_radius (fps_const ?c * inverse f)"
   5.424 +    using assms by (subst fps_conv_radius_cmult_left) auto
   5.425 +  also have "fps_const ?c * inverse f = inverse (fps_const (inverse ?c) * f)"
   5.426 +    using assms by (simp add: fps_inverse_mult fps_const_inverse)
   5.427 +  also have "fps_conv_radius \<dots> > 0" using assms
   5.428 +    by (intro fps_conv_radius_inverse_pos_aux)
   5.429 +       (auto simp: fps_conv_radius_cmult_left)
   5.430 +  finally show ?thesis .
   5.431 +qed
   5.432 +
   5.433 +end
   5.434 +
   5.435 +lemma fps_conv_radius_exp [simp]: 
   5.436 +  fixes c :: "'a :: {banach, real_normed_field}"
   5.437 +  shows "fps_conv_radius (fps_exp c) = \<infinity>"
   5.438 +  unfolding fps_conv_radius_def
   5.439 +proof (rule conv_radius_inftyI'')
   5.440 +  fix z :: 'a
   5.441 +  have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))"
   5.442 +    by (rule exp_converges)
   5.443 +  also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))"
   5.444 +    by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib)
   5.445 +  finally have "summable \<dots>" by (simp add: sums_iff)
   5.446 +  thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)"
   5.447 +    by (rule summable_norm_cancel)
   5.448 +qed
   5.449 +
   5.450 +
   5.451 +subsection \<open>Evaluating power series\<close>
   5.452 +
   5.453 +lemma eval_fps_deriv:
   5.454 +  assumes "norm z < fps_conv_radius f"
   5.455 +  shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
   5.456 +  by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
   5.457 +
   5.458 +lemma fps_nth_conv_deriv:
   5.459 +  fixes f :: "complex fps"
   5.460 +  assumes "fps_conv_radius f > 0"
   5.461 +  shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
   5.462 +  using assms
   5.463 +proof (induction n arbitrary: f)
   5.464 +  case 0
   5.465 +  thus ?case by (simp add: eval_fps_def)
   5.466 +next
   5.467 +  case (Suc n f)
   5.468 +  have "(deriv ^^ Suc n) (eval_fps f) 0 = (deriv ^^ n) (deriv (eval_fps f)) 0"
   5.469 +    unfolding funpow_Suc_right o_def ..
   5.470 +  also have "eventually (\<lambda>z::complex. z \<in> eball 0 (fps_conv_radius f)) (nhds 0)"
   5.471 +    using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
   5.472 +  hence "eventually (\<lambda>z. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)"
   5.473 +    by eventually_elim (simp add: eval_fps_deriv)
   5.474 +  hence "(deriv ^^ n) (deriv (eval_fps f)) 0 = (deriv ^^ n) (eval_fps (fps_deriv f)) 0"
   5.475 +    by (intro higher_deriv_cong_ev refl)
   5.476 +  also have "\<dots> / fact n = fps_nth (fps_deriv f) n"
   5.477 +    using Suc.prems fps_conv_radius_deriv[of f] 
   5.478 +    by (intro Suc.IH [symmetric]) auto
   5.479 +  also have "\<dots> / of_nat (Suc n) = fps_nth f (Suc n)"
   5.480 +    by (simp add: fps_deriv_def del: of_nat_Suc)
   5.481 +  finally show ?case by (simp add: divide_simps)
   5.482 +qed
   5.483 +
   5.484 +lemma eval_fps_eqD:
   5.485 +  fixes f g :: "complex fps"
   5.486 +  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
   5.487 +  assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
   5.488 +  shows   "f = g"
   5.489 +proof (rule fps_ext)
   5.490 +  fix n :: nat
   5.491 +  have "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
   5.492 +    using assms by (intro fps_nth_conv_deriv)
   5.493 +  also have "(deriv ^^ n) (eval_fps f) 0 = (deriv ^^ n) (eval_fps g) 0"
   5.494 +    by (intro higher_deriv_cong_ev refl assms)
   5.495 +  also have "\<dots> / fact n = fps_nth g n"
   5.496 +    using assms by (intro fps_nth_conv_deriv [symmetric])
   5.497 +  finally show "fps_nth f n = fps_nth g n" .
   5.498 +qed
   5.499 +
   5.500 +lemma eval_fps_const [simp]: 
   5.501 +  fixes c :: "'a :: {banach, real_normed_div_algebra}"
   5.502 +  shows "eval_fps (fps_const c) z = c"
   5.503 +proof -
   5.504 +  have "(\<lambda>n::nat. if n \<in> {0} then c else 0) sums (\<Sum>n\<in>{0::nat}. c)"
   5.505 +    by (rule sums_If_finite_set) auto
   5.506 +  also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_const c) n * z ^ n) sums (\<Sum>n\<in>{0::nat}. c)"
   5.507 +    by (intro sums_cong) auto
   5.508 +  also have "(\<Sum>n\<in>{0::nat}. c) = c" 
   5.509 +    by simp
   5.510 +  finally show ?thesis
   5.511 +    by (simp add: eval_fps_def sums_iff)
   5.512 +qed
   5.513 +
   5.514 +lemma eval_fps_0 [simp]:
   5.515 +  "eval_fps (0 :: 'a :: {banach, real_normed_div_algebra} fps) z = 0"
   5.516 +  by (simp only: fps_const_0_eq_0 [symmetric] eval_fps_const)
   5.517 +
   5.518 +lemma eval_fps_1 [simp]:
   5.519 +  "eval_fps (1 :: 'a :: {banach, real_normed_div_algebra} fps) z = 1"
   5.520 +  by (simp only: fps_const_1_eq_1 [symmetric] eval_fps_const)
   5.521 +
   5.522 +lemma eval_fps_numeral [simp]:
   5.523 +  "eval_fps (numeral n :: 'a :: {banach, real_normed_div_algebra} fps) z = numeral n"
   5.524 +  by (simp only: numeral_fps_const eval_fps_const)
   5.525 +
   5.526 +lemma eval_fps_X_power [simp]:
   5.527 +  "eval_fps (fps_X ^ m :: 'a :: {banach, real_normed_div_algebra} fps) z = z ^ m"
   5.528 +proof -
   5.529 +  have "(\<lambda>n::nat. if n \<in> {m} then z ^ n else 0 :: 'a) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
   5.530 +    by (rule sums_If_finite_set) auto
   5.531 +  also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
   5.532 +    by (intro sums_cong) (auto simp: fps_X_power_iff)
   5.533 +  also have "(\<Sum>n\<in>{m::nat}. z ^ n) = z ^ m"
   5.534 +    by simp
   5.535 +  finally show ?thesis
   5.536 +    by (simp add: eval_fps_def sums_iff)
   5.537 +qed
   5.538 +
   5.539 +lemma eval_fps_X [simp]:
   5.540 +  "eval_fps (fps_X :: 'a :: {banach, real_normed_div_algebra} fps) z = z"
   5.541 +  using eval_fps_X_power[of 1 z] by (simp only: power_one_right)
   5.542 +
   5.543 +lemma eval_fps_minus:
   5.544 +  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
   5.545 +  assumes "norm z < fps_conv_radius f"
   5.546 +  shows   "eval_fps (-f) z = -eval_fps f z"
   5.547 +  using assms unfolding eval_fps_def
   5.548 +  by (subst suminf_minus [symmetric]) (auto intro!: summable_fps)
   5.549 +
   5.550 +lemma eval_fps_add:
   5.551 +  fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
   5.552 +  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
   5.553 +  shows   "eval_fps (f + g) z = eval_fps f z + eval_fps g z"
   5.554 +  using assms unfolding eval_fps_def
   5.555 +  by (subst suminf_add) (auto simp: ring_distribs intro!: summable_fps)
   5.556 +
   5.557 +lemma eval_fps_diff:
   5.558 +  fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
   5.559 +  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
   5.560 +  shows   "eval_fps (f - g) z = eval_fps f z - eval_fps g z"
   5.561 +  using assms unfolding eval_fps_def
   5.562 +  by (subst suminf_diff) (auto simp: ring_distribs intro!: summable_fps)
   5.563 +
   5.564 +lemma eval_fps_mult:
   5.565 +  fixes f g :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
   5.566 +  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
   5.567 +  shows   "eval_fps (f * g) z = eval_fps f z * eval_fps g z"
   5.568 +proof -
   5.569 +  have "eval_fps f z * eval_fps g z = 
   5.570 +          (\<Sum>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i)))"
   5.571 +    unfolding eval_fps_def
   5.572 +  proof (subst Cauchy_product)
   5.573 +    show "summable (\<lambda>k. norm (fps_nth f k * z ^ k))" "summable (\<lambda>k. norm (fps_nth g k * z ^ k))"
   5.574 +      by (rule norm_summable_fps assms)+
   5.575 +  qed (simp_all add: algebra_simps)
   5.576 +  also have "(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) =
   5.577 +               (\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * z ^ k)"
   5.578 +    by (intro ext sum.cong refl) (simp add: power_add [symmetric])
   5.579 +  also have "suminf \<dots> = eval_fps (f * g) z"
   5.580 +    by (simp add: eval_fps_def fps_mult_nth atLeast0AtMost sum_distrib_right)
   5.581 +  finally show ?thesis ..
   5.582 +qed
   5.583 +
   5.584 +lemma eval_fps_shift:
   5.585 +  fixes f :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
   5.586 +  assumes "n \<le> subdegree f" "norm z < fps_conv_radius f"
   5.587 +  shows   "eval_fps (fps_shift n f) z = (if z = 0 then fps_nth f n else eval_fps f z / z ^ n)"
   5.588 +proof (cases "z = 0")
   5.589 +  case False
   5.590 +  have "eval_fps (fps_shift n f * fps_X ^ n) z = eval_fps (fps_shift n f) z * z ^ n"
   5.591 +    using assms by (subst eval_fps_mult) simp_all
   5.592 +  also from assms have "fps_shift n f * fps_X ^ n = f"
   5.593 +    by (simp add: fps_shift_times_fps_X_power)
   5.594 +  finally show ?thesis using False by (simp add: field_simps)
   5.595 +qed (simp_all add: eval_fps_at_0)
   5.596 +
   5.597 +lemma eval_fps_exp [simp]:
   5.598 +  fixes c :: "'a :: {banach, real_normed_field}"
   5.599 +  shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def
   5.600 +  by (simp add: eval_fps_def exp_def scaleR_conv_of_real divide_simps power_mult_distrib)
   5.601 +
   5.602 +lemma
   5.603 +  fixes f :: "complex fps" and r :: ereal
   5.604 +  assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0"
   5.605 +  shows   fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)"
   5.606 +    and   eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow> 
   5.607 +                               eval_fps (inverse f) z = inverse (eval_fps f z)"
   5.608 +proof -
   5.609 +  define R where "R = min (fps_conv_radius f) r"
   5.610 +  have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and> 
   5.611 +          (\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))"
   5.612 +  proof (cases "min r (fps_conv_radius f) > 0")
   5.613 +    case True
   5.614 +    define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0"
   5.615 +    have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))"
   5.616 +      using assms by (intro holomorphic_intros) auto
   5.617 +    from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)"
   5.618 +      unfolding f'_def by (rule conv_radius_fps_expansion)
   5.619 +    have eval_f': "eval_fps f' z = inverse (eval_fps f z)" 
   5.620 +      if "norm z < fps_conv_radius f" "norm z < r" for z
   5.621 +      using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto
   5.622 +  
   5.623 +    have "f * f' = 1"
   5.624 +    proof (rule eval_fps_eqD)
   5.625 +      from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')"
   5.626 +        by (auto simp: min_def split: if_splits)
   5.627 +      also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult)
   5.628 +      finally show "\<dots> > 0" .
   5.629 +    next
   5.630 +      from True have "R > 0" by (auto simp: R_def)
   5.631 +      hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)"
   5.632 +        by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
   5.633 +      thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)"
   5.634 +      proof eventually_elim
   5.635 +        case (elim z)
   5.636 +        hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z"
   5.637 +          using radius by (intro eval_fps_mult) 
   5.638 +                          (auto simp: R_def min_def split: if_splits intro: less_trans)
   5.639 +        also have "eval_fps f' z = inverse (eval_fps f z)"
   5.640 +          using elim by (intro eval_f') (auto simp: R_def)
   5.641 +        also from elim have "eval_fps f z \<noteq> 0"
   5.642 +          by (intro assms) (auto simp: R_def)
   5.643 +        hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z" 
   5.644 +          by simp
   5.645 +        finally show "eval_fps (f * f') z = eval_fps 1 z" .
   5.646 +      qed
   5.647 +    qed simp_all
   5.648 +    hence "f' = inverse f"
   5.649 +      by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac)
   5.650 +    with eval_f' and radius show ?thesis by simp
   5.651 +  next
   5.652 +    case False
   5.653 +    hence *: "eball 0 R = {}" 
   5.654 +      by (intro eball_empty) (auto simp: R_def min_def split: if_splits)
   5.655 +    show ?thesis
   5.656 +    proof safe
   5.657 +      from False have "min r (fps_conv_radius f) \<le> 0"
   5.658 +        by (simp add: min_def)
   5.659 +      also have "0 \<le> fps_conv_radius (inverse f)"
   5.660 +        by (simp add: fps_conv_radius_def conv_radius_nonneg)
   5.661 +      finally show "min r (fps_conv_radius f) \<le> \<dots>" .
   5.662 +    qed (unfold * [unfolded R_def], auto)
   5.663 +  qed
   5.664 +
   5.665 +  from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast
   5.666 +  from * show "eval_fps (inverse f) z = inverse (eval_fps f z)" 
   5.667 +    if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z
   5.668 +    using that by auto
   5.669 +qed
   5.670 +
   5.671 +lemma
   5.672 +  fixes f g :: "complex fps" and r :: ereal
   5.673 +  defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
   5.674 +  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
   5.675 +  assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0"
   5.676 +  shows   fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R"
   5.677 +    and   eval_fps_divide':
   5.678 +            "ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z"
   5.679 +proof -
   5.680 +  from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0" 
   5.681 +    by (auto simp: eval_fps_at_0 zero_ereal_def)
   5.682 +  have "R \<le> min r (fps_conv_radius g)"
   5.683 +    by (auto simp: R_def intro: min.coboundedI2)
   5.684 +  also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)"
   5.685 +    by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def)
   5.686 +  finally have radius: "fps_conv_radius (inverse g) \<ge> R" .
   5.687 +  have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))"
   5.688 +    by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
   5.689 +  also have "\<dots> \<le> fps_conv_radius (f * inverse g)"
   5.690 +    by (rule fps_conv_radius_mult)
   5.691 +  also have "f * inverse g = f / g"
   5.692 +    by (intro fps_divide_unit [symmetric] nz')
   5.693 +  finally show "fps_conv_radius (f / g) \<ge> R" .
   5.694 +
   5.695 +  assume z: "ereal (norm z) < R"
   5.696 +  have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z"
   5.697 +    using radius by (intro eval_fps_mult less_le_trans[OF z])
   5.698 +                    (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
   5.699 +  also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close>
   5.700 +    by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz)
   5.701 +       (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
   5.702 +  also have "f * inverse g = f / g" by fact
   5.703 +  finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps)
   5.704 +qed
   5.705 +
   5.706 +lemma
   5.707 +  fixes f g :: "complex fps" and r :: ereal
   5.708 +  defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
   5.709 +  assumes "subdegree g \<le> subdegree f"
   5.710 +  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
   5.711 +  assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0"
   5.712 +  shows   fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R"
   5.713 +    and   eval_fps_divide:
   5.714 +            "ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow>
   5.715 +               eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
   5.716 +proof -
   5.717 +  define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g"
   5.718 +  have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g"
   5.719 +    unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+
   5.720 +  have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0"
   5.721 +    using assms(2) by (simp_all add: f'_def g'_def)
   5.722 +  have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g"
   5.723 +    by (simp_all add: f'_def g'_def)
   5.724 +  have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)"
   5.725 +               "fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def)
   5.726 +  have g_nz: "g \<noteq> 0"
   5.727 +  proof -
   5.728 +    define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))"
   5.729 +    from \<open>r > 0\<close> have "z \<in> eball 0 r"
   5.730 +      by (cases r) (auto simp: z_def eball_def)
   5.731 +    moreover have "z \<noteq> 0" using \<open>r > 0\<close> 
   5.732 +      by (cases r) (auto simp: z_def)
   5.733 +    ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6))
   5.734 +    thus "g \<noteq> 0" by auto
   5.735 +  qed
   5.736 +  have fg: "f / g = f' * inverse g'"
   5.737 +    by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit)
   5.738 +
   5.739 +  have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z
   5.740 +  proof (cases "z = 0")
   5.741 +    case False
   5.742 +    with assms and z have "eval_fps g z \<noteq> 0" by auto
   5.743 +    also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g"
   5.744 +      by (subst g_eq) (auto simp: eval_fps_mult)
   5.745 +    finally show ?thesis by auto
   5.746 +  qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0)
   5.747 +
   5.748 +  have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')"
   5.749 +    by (auto simp: R_def min.coboundedI1 min.coboundedI2)
   5.750 +  also have "\<dots> \<le> fps_conv_radius (inverse g')"
   5.751 +    using g'_nz by (rule fps_conv_radius_inverse)
   5.752 +  finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" .
   5.753 +  hence "R \<le> fps_conv_radius (f' * inverse g')"
   5.754 +    by (intro order.trans[OF _ fps_conv_radius_mult])
   5.755 +       (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
   5.756 +  thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg)
   5.757 +
   5.758 +  fix z c :: complex assume z: "ereal (norm z) < R"
   5.759 +  assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)"
   5.760 +  show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
   5.761 +  proof (cases "z = 0")
   5.762 +    case False
   5.763 +    from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')"
   5.764 +      by simp
   5.765 +    with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z"
   5.766 +      unfolding fg by (subst eval_fps_mult) (auto simp: R_def)
   5.767 +    also have "eval_fps (inverse g') z = inverse (eval_fps g' z)"
   5.768 +      using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def)
   5.769 +    also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z"
   5.770 +      using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def)
   5.771 +    finally show ?thesis using False by simp
   5.772 +  qed (simp_all add: eval_fps_at_0 fg field_simps c)
   5.773 +qed
   5.774 +
   5.775 +
   5.776 +subsection \<open>Power series expansion of complex functions\<close>
   5.777 +
   5.778 +text \<open>
   5.779 +  This predicate contains the notion that the given formal power series converges
   5.780 +  in some disc of positive radius around the origin and is equal to the given complex
   5.781 +  function there.
   5.782 +
   5.783 +  This relationship is unique in the sense that no complex function can have more than
   5.784 +  one formal power series to which it expands, and if two holomorphic functions that are
   5.785 +  holomorphic on a connected open set around the origin and have the same power series
   5.786 +  expansion, they must be equal on that set.
   5.787 +
   5.788 +  More concrete statements about the radius of convergence can usually be made, but for
   5.789 +  many purposes, the statment that the series converges to the function in some neighbourhood
   5.790 +  of the origin is enough, and that can be shown almost fully automatically in most cases,
   5.791 +  as there are straightforward introduction rules to show this.
   5.792 +
   5.793 +  In particular, when one wants to relate the coefficients of the power series to the 
   5.794 +  values of the derivatives of the function at the origin, or if one wants to approximate
   5.795 +  the coefficients of the series with the singularities of the function, this predicate
   5.796 +  is enough.
   5.797 +\<close>
   5.798 +definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
   5.799 +  (infixl "has'_fps'_expansion" 60) 
   5.800 +  where "(f has_fps_expansion F) \<longleftrightarrow> 
   5.801 +            fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
   5.802 +
   5.803 +named_theorems fps_expansion_intros
   5.804 +
   5.805 +lemma fps_nth_fps_expansion:
   5.806 +  fixes f :: "complex \<Rightarrow> complex"
   5.807 +  assumes "f has_fps_expansion F"
   5.808 +  shows   "fps_nth F n = (deriv ^^ n) f 0 / fact n"
   5.809 +proof -
   5.810 +  have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n"
   5.811 +    using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def)
   5.812 +  also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0"
   5.813 +    using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def)
   5.814 +  finally show ?thesis .
   5.815 +qed
   5.816 +
   5.817 +lemma has_fps_expansion_fps_expansion [intro]:
   5.818 +  assumes "open A" "0 \<in> A" "f holomorphic_on A"
   5.819 +  shows   "f has_fps_expansion fps_expansion f 0"
   5.820 +proof -
   5.821 +  from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A"
   5.822 +    by (auto simp: open_contains_ball)
   5.823 +  have holo: "f holomorphic_on eball 0 (ereal r)" 
   5.824 +    using r(2) and assms(3) by auto
   5.825 +  from r(1) have "0 < ereal r" by simp
   5.826 +  also have "r \<le> fps_conv_radius (fps_expansion f 0)"
   5.827 +    using holo by (intro conv_radius_fps_expansion) auto
   5.828 +  finally have "\<dots> > 0" .
   5.829 +  moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)"
   5.830 +    using r(1) by (intro eventually_nhds_in_open) auto
   5.831 +  hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)"
   5.832 +    by eventually_elim (subst eval_fps_expansion'[OF holo], auto)
   5.833 +  ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
   5.834 +qed
   5.835 +
   5.836 +lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
   5.837 +  "(\<lambda>_. c) has_fps_expansion fps_const c"
   5.838 +  by (auto simp: has_fps_expansion_def)
   5.839 +
   5.840 +lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]: 
   5.841 +  "(\<lambda>_. 0) has_fps_expansion 0"
   5.842 +  by (auto simp: has_fps_expansion_def)
   5.843 +
   5.844 +lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]:
   5.845 +  "(\<lambda>_. 1) has_fps_expansion 1"
   5.846 +  by (auto simp: has_fps_expansion_def)
   5.847 +
   5.848 +lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]:
   5.849 +  "(\<lambda>_. numeral n) has_fps_expansion numeral n"
   5.850 +  by (auto simp: has_fps_expansion_def)
   5.851 +
   5.852 +lemma has_fps_expansion_fps_X_power [fps_expansion_intros]: 
   5.853 +  "(\<lambda>x. x ^ n) has_fps_expansion (fps_X ^ n)"
   5.854 +  by (auto simp: has_fps_expansion_def)
   5.855 +
   5.856 +lemma has_fps_expansion_fps_X [fps_expansion_intros]: 
   5.857 +  "(\<lambda>x. x) has_fps_expansion fps_X"
   5.858 +  by (auto simp: has_fps_expansion_def)
   5.859 +
   5.860 +lemma has_fps_expansion_cmult_left [fps_expansion_intros]:
   5.861 +  fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
   5.862 +  assumes "f has_fps_expansion F"
   5.863 +  shows   "(\<lambda>x. c * f x) has_fps_expansion fps_const c * F"
   5.864 +proof (cases "c = 0")
   5.865 +  case False
   5.866 +  from assms have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.867 +    by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
   5.868 +  moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
   5.869 +    by (auto simp: has_fps_expansion_def)
   5.870 +  ultimately have "eventually (\<lambda>z. eval_fps (fps_const c * F) z = c * f z) (nhds 0)"
   5.871 +    by eventually_elim (simp_all add: eval_fps_mult)
   5.872 +  with assms and False show ?thesis
   5.873 +    by (auto simp: has_fps_expansion_def fps_conv_radius_cmult_left)
   5.874 +qed auto
   5.875 +
   5.876 +lemma has_fps_expansion_cmult_right [fps_expansion_intros]:
   5.877 +  fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
   5.878 +  assumes "f has_fps_expansion F"
   5.879 +  shows   "(\<lambda>x. f x * c) has_fps_expansion F * fps_const c"
   5.880 +proof -
   5.881 +  have "F * fps_const c = fps_const c * F"
   5.882 +    by (intro fps_ext) (auto simp: mult.commute)
   5.883 +  with has_fps_expansion_cmult_left [OF assms] show ?thesis 
   5.884 +    by (simp add: mult.commute)
   5.885 +qed
   5.886 +
   5.887 +lemma has_fps_expansion_minus [fps_expansion_intros]:
   5.888 +  assumes "f has_fps_expansion F"
   5.889 +  shows   "(\<lambda>x. - f x) has_fps_expansion -F"
   5.890 +proof -
   5.891 +  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.892 +    by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
   5.893 +  moreover from assms have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
   5.894 +    by (auto simp: has_fps_expansion_def)
   5.895 +  ultimately have "eventually (\<lambda>x. eval_fps (-F) x = -f x) (nhds 0)"
   5.896 +    by eventually_elim (auto simp: eval_fps_minus)
   5.897 +  thus ?thesis using assms by (auto simp: has_fps_expansion_def)
   5.898 +qed
   5.899 +
   5.900 +lemma has_fps_expansion_add [fps_expansion_intros]:
   5.901 +  assumes "f has_fps_expansion F" "g has_fps_expansion G"
   5.902 +  shows   "(\<lambda>x. f x + g x) has_fps_expansion F + G"
   5.903 +proof -
   5.904 +  from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
   5.905 +    by (auto simp: has_fps_expansion_def)
   5.906 +  also have "\<dots> \<le> fps_conv_radius (F + G)"
   5.907 +    by (rule fps_conv_radius_add)
   5.908 +  finally have radius: "\<dots> > 0" .
   5.909 +
   5.910 +  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.911 +                  "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
   5.912 +    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
   5.913 +  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
   5.914 +            and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
   5.915 +    using assms by (auto simp: has_fps_expansion_def)
   5.916 +  ultimately have "eventually (\<lambda>x. eval_fps (F + G) x = f x + g x) (nhds 0)"
   5.917 +    by eventually_elim (auto simp: eval_fps_add)
   5.918 +  with radius show ?thesis by (auto simp: has_fps_expansion_def)
   5.919 +qed
   5.920 +
   5.921 +lemma has_fps_expansion_diff [fps_expansion_intros]:
   5.922 +  assumes "f has_fps_expansion F" "g has_fps_expansion G"
   5.923 +  shows   "(\<lambda>x. f x - g x) has_fps_expansion F - G"
   5.924 +  using has_fps_expansion_add[of f F "\<lambda>x. - g x" "-G"] assms 
   5.925 +  by (simp add: has_fps_expansion_minus)
   5.926 +
   5.927 +lemma has_fps_expansion_mult [fps_expansion_intros]:
   5.928 +  fixes F G :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
   5.929 +  assumes "f has_fps_expansion F" "g has_fps_expansion G"
   5.930 +  shows   "(\<lambda>x. f x * g x) has_fps_expansion F * G"
   5.931 +proof -
   5.932 +  from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
   5.933 +    by (auto simp: has_fps_expansion_def)
   5.934 +  also have "\<dots> \<le> fps_conv_radius (F * G)"
   5.935 +    by (rule fps_conv_radius_mult)
   5.936 +  finally have radius: "\<dots> > 0" .
   5.937 +
   5.938 +  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.939 +                  "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
   5.940 +    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
   5.941 +  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
   5.942 +            and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
   5.943 +    using assms by (auto simp: has_fps_expansion_def)
   5.944 +  ultimately have "eventually (\<lambda>x. eval_fps (F * G) x = f x * g x) (nhds 0)"
   5.945 +    by eventually_elim (auto simp: eval_fps_mult)
   5.946 +  with radius show ?thesis by (auto simp: has_fps_expansion_def)
   5.947 +qed
   5.948 +
   5.949 +lemma has_fps_expansion_inverse [fps_expansion_intros]:
   5.950 +  fixes F :: "'a :: {banach, real_normed_field} fps"
   5.951 +  assumes "f has_fps_expansion F"
   5.952 +  assumes "fps_nth F 0 \<noteq> 0"
   5.953 +  shows   "(\<lambda>x. inverse (f x)) has_fps_expansion inverse F"
   5.954 +proof -
   5.955 +  have radius: "fps_conv_radius (inverse F) > 0"
   5.956 +    using assms unfolding has_fps_expansion_def
   5.957 +    by (intro fps_conv_radius_inverse_pos) auto
   5.958 +  let ?R = "min (fps_conv_radius F) (fps_conv_radius (inverse F))"
   5.959 +  from assms radius
   5.960 +    have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.961 +         "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius (inverse F))) (nhds 0)"
   5.962 +    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
   5.963 +  moreover have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
   5.964 +    using assms by (auto simp: has_fps_expansion_def)
   5.965 +  ultimately have "eventually (\<lambda>z. eval_fps (inverse F) z = inverse (f z)) (nhds 0)"
   5.966 +  proof eventually_elim
   5.967 +    case (elim z)
   5.968 +    hence "eval_fps (inverse F * F) z = eval_fps (inverse F) z * f z"
   5.969 +      by (subst eval_fps_mult) auto
   5.970 +    also have "eval_fps (inverse F * F) z = 1"
   5.971 +      using assms by (simp add: inverse_mult_eq_1)
   5.972 +    finally show ?case by (auto simp: divide_simps)
   5.973 +  qed
   5.974 +  with radius show ?thesis by (auto simp: has_fps_expansion_def)
   5.975 +qed
   5.976 +
   5.977 +lemma has_fps_expansion_exp [fps_expansion_intros]:
   5.978 +  fixes c :: "'a :: {banach, real_normed_field}"
   5.979 +  shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c"
   5.980 +  by (auto simp: has_fps_expansion_def)
   5.981 +
   5.982 +lemma has_fps_expansion_exp1 [fps_expansion_intros]:
   5.983 +  "(\<lambda>x::'a :: {banach, real_normed_field}. exp x) has_fps_expansion fps_exp 1"
   5.984 +  using has_fps_expansion_exp[of 1] by simp
   5.985 +
   5.986 +lemma has_fps_expansion_exp_neg1 [fps_expansion_intros]:
   5.987 +  "(\<lambda>x::'a :: {banach, real_normed_field}. exp (-x)) has_fps_expansion fps_exp (-1)"
   5.988 +  using has_fps_expansion_exp[of "-1"] by simp
   5.989 +
   5.990 +lemma has_fps_expansion_deriv [fps_expansion_intros]:
   5.991 +  assumes "f has_fps_expansion F"
   5.992 +  shows   "deriv f has_fps_expansion fps_deriv F"
   5.993 +proof -
   5.994 +  have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
   5.995 +    using assms by (intro eventually_nhds_in_open)
   5.996 +                   (auto simp: has_fps_expansion_def zero_ereal_def)
   5.997 +  moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
   5.998 +    by (auto simp: has_fps_expansion_def)
   5.999 +  then obtain s where "open s" "0 \<in> s" and s: "\<And>w. w \<in> s \<Longrightarrow> eval_fps F w = f w"
  5.1000 +    by (auto simp: eventually_nhds)
  5.1001 +  hence "eventually (\<lambda>w. w \<in> s) (nhds 0)"
  5.1002 +    by (intro eventually_nhds_in_open) auto
  5.1003 +  ultimately have "eventually (\<lambda>z. eval_fps (fps_deriv F) z = deriv f z) (nhds 0)"
  5.1004 +  proof eventually_elim
  5.1005 +    case (elim z)
  5.1006 +    hence "eval_fps (fps_deriv F) z = deriv (eval_fps F) z"
  5.1007 +      by (simp add: eval_fps_deriv)
  5.1008 +    also have "eventually (\<lambda>w. w \<in> s) (nhds z)"
  5.1009 +      using elim and \<open>open s\<close> by (intro eventually_nhds_in_open) auto
  5.1010 +    hence "eventually (\<lambda>w. eval_fps F w = f w) (nhds z)"
  5.1011 +      by eventually_elim (simp add: s)
  5.1012 +    hence "deriv (eval_fps F) z = deriv f z"
  5.1013 +      by (intro deriv_cong_ev refl)
  5.1014 +    finally show ?case .
  5.1015 +  qed
  5.1016 +  with assms and fps_conv_radius_deriv[of F] show ?thesis
  5.1017 +    by (auto simp: has_fps_expansion_def)
  5.1018 +qed
  5.1019 +
  5.1020 +lemma fps_conv_radius_binomial:
  5.1021 +  fixes c :: "'a :: {real_normed_field,banach}"
  5.1022 +  shows "fps_conv_radius (fps_binomial c) = (if c \<in> \<nat> then \<infinity> else 1)"
  5.1023 +  unfolding fps_conv_radius_def by (simp add: conv_radius_gchoose)
  5.1024 +
  5.1025 +lemma fps_conv_radius_ln:
  5.1026 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1027 +  shows "fps_conv_radius (fps_ln c) = (if c = 0 then \<infinity> else 1)"
  5.1028 +proof (cases "c = 0")
  5.1029 +  case False
  5.1030 +  have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = 1"
  5.1031 +  proof (rule conv_radius_ratio_limit_nonzero)
  5.1032 +    show "(\<lambda>n. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) \<longlonglongrightarrow> 1"
  5.1033 +      using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc)
  5.1034 +  qed auto
  5.1035 +  also have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) =
  5.1036 +               conv_radius (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n :: 'a)"
  5.1037 +    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]])
  5.1038 +       (simp add: norm_mult norm_divide norm_power)
  5.1039 +  finally show ?thesis using False unfolding fps_ln_def
  5.1040 +    by (subst  fps_conv_radius_cmult_left) (simp_all add: fps_conv_radius_def)
  5.1041 +qed (auto simp: fps_ln_def)
  5.1042 +
  5.1043 +lemma fps_conv_radius_ln_nonzero [simp]:
  5.1044 +  assumes "c \<noteq> (0 :: 'a :: {banach,real_normed_field,field_char_0})"
  5.1045 +  shows   "fps_conv_radius (fps_ln c) = 1"
  5.1046 +  using assms by (simp add: fps_conv_radius_ln)
  5.1047 +
  5.1048 +lemma fps_conv_radius_sin [simp]:
  5.1049 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1050 +  shows "fps_conv_radius (fps_sin c) = \<infinity>"
  5.1051 +proof (cases "c = 0")
  5.1052 +  case False
  5.1053 +  have "\<infinity> = conv_radius (\<lambda>n. of_real (sin_coeff n) :: 'a)"
  5.1054 +  proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
  5.1055 +    case (1 z)
  5.1056 +    show ?case using summable_norm_sin[of z] by (simp add: norm_mult)
  5.1057 +  qed
  5.1058 +  also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (sin_coeff n) :: 'a)"
  5.1059 +    using False by (subst conv_radius_mult_power) auto
  5.1060 +  also have "\<dots> = fps_conv_radius (fps_sin c)" unfolding fps_conv_radius_def
  5.1061 +    by (rule conv_radius_cong_weak) (auto simp add: fps_sin_def sin_coeff_def)
  5.1062 +  finally show ?thesis by simp
  5.1063 +qed simp_all
  5.1064 +
  5.1065 +lemma fps_conv_radius_cos [simp]:
  5.1066 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1067 +  shows "fps_conv_radius (fps_cos c) = \<infinity>"
  5.1068 +proof (cases "c = 0")
  5.1069 +  case False
  5.1070 +  have "\<infinity> = conv_radius (\<lambda>n. of_real (cos_coeff n) :: 'a)"
  5.1071 +  proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
  5.1072 +    case (1 z)
  5.1073 +    show ?case using summable_norm_cos[of z] by (simp add: norm_mult)
  5.1074 +  qed
  5.1075 +  also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (cos_coeff n) :: 'a)"
  5.1076 +    using False by (subst conv_radius_mult_power) auto
  5.1077 +  also have "\<dots> = fps_conv_radius (fps_cos c)" unfolding fps_conv_radius_def
  5.1078 +    by (rule conv_radius_cong_weak) (auto simp add: fps_cos_def cos_coeff_def)
  5.1079 +  finally show ?thesis by simp
  5.1080 +qed simp_all
  5.1081 +
  5.1082 +lemma eval_fps_sin [simp]:
  5.1083 +  fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1084 +  shows "eval_fps (fps_sin c) z = sin (c * z)"
  5.1085 +proof -
  5.1086 +  have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges)
  5.1087 +  also have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_sin c) n * z ^ n)"
  5.1088 +    by (rule ext) (auto simp: sin_coeff_def fps_sin_def power_mult_distrib scaleR_conv_of_real)
  5.1089 +  finally show ?thesis by (simp add: sums_iff eval_fps_def)
  5.1090 +qed
  5.1091 +
  5.1092 +lemma eval_fps_cos [simp]:
  5.1093 +  fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1094 +  shows "eval_fps (fps_cos c) z = cos (c * z)"
  5.1095 +proof -
  5.1096 +  have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges)
  5.1097 +  also have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_cos c) n * z ^ n)"
  5.1098 +    by (rule ext) (auto simp: cos_coeff_def fps_cos_def power_mult_distrib scaleR_conv_of_real)
  5.1099 +  finally show ?thesis by (simp add: sums_iff eval_fps_def)
  5.1100 +qed
  5.1101 +
  5.1102 +lemma cos_eq_zero_imp_norm_ge:
  5.1103 +  assumes "cos (z :: complex) = 0"
  5.1104 +  shows   "norm z \<ge> pi / 2"
  5.1105 +proof -
  5.1106 +  from assms obtain n where "z = complex_of_real ((of_int n + 1 / 2) * pi)"
  5.1107 +    by (auto simp: cos_eq_0 algebra_simps)
  5.1108 +  also have "norm \<dots> = \<bar>real_of_int n + 1 / 2\<bar> * pi"
  5.1109 +    by (subst norm_of_real) (simp_all add: abs_mult)
  5.1110 +  also have "real_of_int n + 1 / 2 = of_int (2 * n + 1) / 2" by simp
  5.1111 +  also have "\<bar>\<dots>\<bar> = of_int \<bar>2 * n + 1\<bar> / 2" by (subst abs_divide) simp_all
  5.1112 +  also have "\<dots> * pi = of_int \<bar>2 * n + 1\<bar> * (pi / 2)" by simp
  5.1113 +  also have "\<dots> \<ge> of_int 1 * (pi / 2)"
  5.1114 +    by (intro mult_right_mono, subst of_int_le_iff) (auto simp: abs_if)
  5.1115 +  finally show ?thesis by simp
  5.1116 +qed
  5.1117 +
  5.1118 +lemma fps_conv_radius_tan:
  5.1119 +  fixes c :: complex
  5.1120 +  assumes "c \<noteq> 0"
  5.1121 +  shows   "fps_conv_radius (fps_tan c) \<ge> pi / (2 * norm c)"
  5.1122 +proof -
  5.1123 +  have "fps_conv_radius (fps_tan c) \<ge> 
  5.1124 +          Min {pi / (2 * norm c), fps_conv_radius (fps_sin c), fps_conv_radius (fps_cos c)}"
  5.1125 +    unfolding fps_tan_def
  5.1126 +  proof (rule fps_conv_radius_divide)
  5.1127 +    fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
  5.1128 +    with cos_eq_zero_imp_norm_ge[of "c*z"] assms 
  5.1129 +      show "eval_fps (fps_cos  c) z \<noteq> 0" by (auto simp: norm_mult field_simps)
  5.1130 +  qed (insert assms, auto)
  5.1131 +  thus ?thesis by (simp add: min_def)
  5.1132 +qed
  5.1133 +
  5.1134 +lemma eval_fps_tan:
  5.1135 +  fixes c :: complex
  5.1136 +  assumes "norm z < pi / (2 * norm c)"
  5.1137 +  shows   "eval_fps (fps_tan c) z = tan (c * z)"
  5.1138 +proof (cases "c = 0")
  5.1139 +  case False
  5.1140 +  show ?thesis unfolding fps_tan_def
  5.1141 +  proof (subst eval_fps_divide'[where r = "pi / (2 * norm c)"])
  5.1142 +    fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
  5.1143 +    with cos_eq_zero_imp_norm_ge[of "c*z"] assms 
  5.1144 +      show "eval_fps (fps_cos  c) z \<noteq> 0" using False by (auto simp: norm_mult field_simps)
  5.1145 +    qed (insert False assms, auto simp: field_simps tan_def)
  5.1146 +qed simp_all
  5.1147 +
  5.1148 +lemma eval_fps_binomial:
  5.1149 +  fixes c :: complex
  5.1150 +  assumes "norm z < 1"
  5.1151 +  shows   "eval_fps (fps_binomial c) z = (1 + z) powr c"
  5.1152 +  using gen_binomial_complex[OF assms] by (simp add: sums_iff eval_fps_def)
  5.1153 +
  5.1154 +lemma has_fps_expansion_binomial_complex [fps_expansion_intros]:
  5.1155 +  fixes c :: complex
  5.1156 +  shows "(\<lambda>x. (1 + x) powr c) has_fps_expansion fps_binomial c"
  5.1157 +proof -
  5.1158 +  have *: "eventually (\<lambda>z::complex. z \<in> eball 0 1) (nhds 0)"
  5.1159 +    by (intro eventually_nhds_in_open) auto
  5.1160 +  thus ?thesis
  5.1161 +    by (auto simp: has_fps_expansion_def eval_fps_binomial fps_conv_radius_binomial
  5.1162 +             intro!: eventually_mono [OF *])
  5.1163 +qed
  5.1164 +
  5.1165 +lemma has_fps_expansion_sin [fps_expansion_intros]:
  5.1166 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1167 +  shows "(\<lambda>x. sin (c * x)) has_fps_expansion fps_sin c"
  5.1168 +  by (auto simp: has_fps_expansion_def)
  5.1169 +
  5.1170 +lemma has_fps_expansion_sin' [fps_expansion_intros]:
  5.1171 +  "(\<lambda>x::'a :: {banach, real_normed_field}. sin x) has_fps_expansion fps_sin 1"
  5.1172 +  using has_fps_expansion_sin[of 1] by simp
  5.1173 +
  5.1174 +lemma has_fps_expansion_cos [fps_expansion_intros]:
  5.1175 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1176 +  shows "(\<lambda>x. cos (c * x)) has_fps_expansion fps_cos c"
  5.1177 +  by (auto simp: has_fps_expansion_def)
  5.1178 +
  5.1179 +lemma has_fps_expansion_cos' [fps_expansion_intros]:
  5.1180 +  "(\<lambda>x::'a :: {banach, real_normed_field}. cos x) has_fps_expansion fps_cos 1"
  5.1181 +  using has_fps_expansion_cos[of 1] by simp
  5.1182 +
  5.1183 +lemma has_fps_expansion_shift [fps_expansion_intros]:
  5.1184 +  fixes F :: "'a :: {banach, real_normed_field} fps"
  5.1185 +  assumes "f has_fps_expansion F" and "n \<le> subdegree F"
  5.1186 +  assumes "c = fps_nth F n"
  5.1187 +  shows   "(\<lambda>x. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)"
  5.1188 +proof -
  5.1189 +  have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
  5.1190 +    using assms by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
  5.1191 +  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
  5.1192 +    using assms by (auto simp: has_fps_expansion_def)
  5.1193 +  ultimately have "eventually (\<lambda>x. eval_fps (fps_shift n F) x = 
  5.1194 +                     (if x = 0 then c else f x / x ^ n)) (nhds 0)"
  5.1195 +    by eventually_elim (auto simp: eval_fps_shift assms)
  5.1196 +  with assms show ?thesis by (auto simp: has_fps_expansion_def)
  5.1197 +qed
  5.1198 +
  5.1199 +lemma has_fps_expansion_divide [fps_expansion_intros]:
  5.1200 +  fixes F G :: "'a :: {banach, real_normed_field} fps"
  5.1201 +  assumes "f has_fps_expansion F" and "g has_fps_expansion G" and 
  5.1202 +          "subdegree G \<le> subdegree F" "G \<noteq> 0"
  5.1203 +          "c = fps_nth F (subdegree G) / fps_nth G (subdegree G)"
  5.1204 +  shows   "(\<lambda>x. if x = 0 then c else f x / g x) has_fps_expansion (F / G)"
  5.1205 +proof -
  5.1206 +  define n where "n = subdegree G"
  5.1207 +  define F' and G' where "F' = fps_shift n F" and "G' = fps_shift n G"
  5.1208 +  have "F = F' * fps_X ^ n" "G = G' * fps_X ^ n" unfolding F'_def G'_def n_def 
  5.1209 +    by (rule fps_shift_times_fps_X_power [symmetric] le_refl | fact)+
  5.1210 +  moreover from assms have "fps_nth G' 0 \<noteq> 0"
  5.1211 +    by (simp add: G'_def n_def)
  5.1212 +  ultimately have FG: "F / G = F' * inverse G'"
  5.1213 +    by (simp add: fps_divide_unit)
  5.1214 +
  5.1215 +  have "(\<lambda>x. (if x = 0 then fps_nth F n else f x / x ^ n) * 
  5.1216 +          inverse (if x = 0 then fps_nth G n else g x / x ^ n)) has_fps_expansion F / G"
  5.1217 +    (is "?h has_fps_expansion _") unfolding FG F'_def G'_def n_def using \<open>G \<noteq> 0\<close>
  5.1218 +    by (intro has_fps_expansion_mult has_fps_expansion_inverse
  5.1219 +              has_fps_expansion_shift assms) auto
  5.1220 +  also have "?h = (\<lambda>x. if x = 0 then c else f x / g x)"
  5.1221 +    using assms(5) unfolding n_def 
  5.1222 +    by (intro ext) (auto split: if_splits simp: field_simps)
  5.1223 +  finally show ?thesis .
  5.1224 +qed
  5.1225 +
  5.1226 +lemma has_fps_expansion_divide' [fps_expansion_intros]:
  5.1227 +  fixes F G :: "'a :: {banach, real_normed_field} fps"
  5.1228 +  assumes "f has_fps_expansion F" and "g has_fps_expansion G" and "fps_nth G 0 \<noteq> 0"
  5.1229 +  shows   "(\<lambda>x. f x / g x) has_fps_expansion (F / G)"
  5.1230 +proof -
  5.1231 +  have "(\<lambda>x. if x = 0 then fps_nth F 0 / fps_nth G 0 else f x / g x) has_fps_expansion (F / G)"
  5.1232 +    (is "?h has_fps_expansion _") using assms(3) by (intro has_fps_expansion_divide assms) auto
  5.1233 +  also from assms have "fps_nth F 0 = f 0" "fps_nth G 0 = g 0"
  5.1234 +    by (auto simp: has_fps_expansion_def eval_fps_at_0 dest: eventually_nhds_x_imp_x)
  5.1235 +  hence "?h = (\<lambda>x. f x / g x)" by auto
  5.1236 +  finally show ?thesis .
  5.1237 +qed
  5.1238 +
  5.1239 +lemma has_fps_expansion_tan [fps_expansion_intros]:
  5.1240 +  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
  5.1241 +  shows "(\<lambda>x. tan (c * x)) has_fps_expansion fps_tan c"
  5.1242 +proof -
  5.1243 +  have "(\<lambda>x. sin (c * x) / cos (c * x)) has_fps_expansion fps_sin c / fps_cos c"
  5.1244 +    by (intro fps_expansion_intros) auto
  5.1245 +  thus ?thesis by (simp add: tan_def fps_tan_def)
  5.1246 +qed
  5.1247 +
  5.1248 +lemma has_fps_expansion_tan' [fps_expansion_intros]:
  5.1249 +  "tan has_fps_expansion fps_tan (1 :: 'a :: {banach, real_normed_field, field_char_0})"
  5.1250 +  using has_fps_expansion_tan[of 1] by simp
  5.1251 +
  5.1252 +lemma has_fps_expansion_imp_holomorphic:
  5.1253 +  assumes "f has_fps_expansion F"
  5.1254 +  obtains s where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
  5.1255 +proof -
  5.1256 +  from assms obtain s where s: "open s" "0 \<in> s" "\<And>z. z \<in> s \<Longrightarrow> eval_fps F z = f z"
  5.1257 +    unfolding has_fps_expansion_def eventually_nhds by blast
  5.1258 +  let ?s' = "eball 0 (fps_conv_radius F) \<inter> s"
  5.1259 +  have "eval_fps F holomorphic_on ?s'"
  5.1260 +    by (intro holomorphic_intros) auto
  5.1261 +  also have "?this \<longleftrightarrow> f holomorphic_on ?s'"
  5.1262 +    using s by (intro holomorphic_cong) auto
  5.1263 +  finally show ?thesis using s assms
  5.1264 +    by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
  5.1265 +qed
  5.1266 +
  5.1267 +lemma residue_fps_expansion_over_power_at_0:
  5.1268 +  assumes "f has_fps_expansion F"
  5.1269 +  shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
  5.1270 +proof -
  5.1271 +  from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
  5.1272 +  have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
  5.1273 +    using assms s unfolding has_fps_expansion_def
  5.1274 +    by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
  5.1275 +  also from assms have "\<dots> = fps_nth F n"
  5.1276 +    by (subst fps_nth_fps_expansion) auto
  5.1277 +  finally show ?thesis by simp
  5.1278 +qed
  5.1279 +
  5.1280 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Mon Aug 21 20:49:15 2017 +0200
     6.3 @@ -0,0 +1,570 @@
     6.4 +(*  
     6.5 +  Title:    HOL/Analysis/Infinite_Set_Sum.thy
     6.6 +  Author:   Manuel Eberl, TU München
     6.7 +
     6.8 +  A theory of sums over possible infinite sets. (Only works for absolute summability)
     6.9 +*)
    6.10 +section \<open>Sums over infinite sets\<close>
    6.11 +theory Infinite_Set_Sum
    6.12 +  imports Set_Integral
    6.13 +begin
    6.14 +
    6.15 +(* TODO Move *)
    6.16 +lemma sets_eq_countable:
    6.17 +  assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
    6.18 +  shows   "sets M = Pow A"
    6.19 +proof (intro equalityI subsetI)
    6.20 +  fix X assume "X \<in> Pow A"
    6.21 +  hence "(\<Union>x\<in>X. {x}) \<in> sets M"
    6.22 +    by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
    6.23 +  also have "(\<Union>x\<in>X. {x}) = X" by auto
    6.24 +  finally show "X \<in> sets M" .
    6.25 +next
    6.26 +  fix X assume "X \<in> sets M"
    6.27 +  from sets.sets_into_space[OF this] and assms 
    6.28 +    show "X \<in> Pow A" by simp
    6.29 +qed
    6.30 +
    6.31 +lemma measure_eqI_countable':
    6.32 +  assumes spaces: "space M = A" "space N = A" 
    6.33 +  assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
    6.34 +  assumes A: "countable A"
    6.35 +  assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
    6.36 +  shows "M = N"
    6.37 +proof (rule measure_eqI_countable)
    6.38 +  show "sets M = Pow A"
    6.39 +    by (intro sets_eq_countable assms)
    6.40 +  show "sets N = Pow A"
    6.41 +    by (intro sets_eq_countable assms)
    6.42 +qed fact+
    6.43 +
    6.44 +lemma PiE_singleton: 
    6.45 +  assumes "f \<in> extensional A"
    6.46 +  shows   "PiE A (\<lambda>x. {f x}) = {f}"
    6.47 +proof -
    6.48 +  {
    6.49 +    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
    6.50 +    hence "g x = f x" for x
    6.51 +      using assms by (cases "x \<in> A") (auto simp: extensional_def)
    6.52 +    hence "g = f" by (simp add: fun_eq_iff)
    6.53 +  }
    6.54 +  thus ?thesis using assms by (auto simp: extensional_def)
    6.55 +qed
    6.56 +
    6.57 +lemma count_space_PiM_finite:
    6.58 +  fixes B :: "'a \<Rightarrow> 'b set"
    6.59 +  assumes "finite A" "\<And>i. countable (B i)"
    6.60 +  shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
    6.61 +proof (rule measure_eqI_countable')
    6.62 +  show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
    6.63 +    by (simp add: space_PiM)
    6.64 +  show "space (count_space (PiE A B)) = PiE A B" by simp
    6.65 +next
    6.66 +  fix f assume f: "f \<in> PiE A B"
    6.67 +  hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
    6.68 +    by (intro sets_PiM_I_finite assms) auto
    6.69 +  also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
    6.70 +    by (intro PiE_singleton) (auto simp: PiE_def)
    6.71 +  finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
    6.72 +next
    6.73 +  interpret product_sigma_finite "(\<lambda>i. count_space (B i))"
    6.74 +    by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
    6.75 +  thm sigma_finite_measure_count_space
    6.76 +  fix f assume f: "f \<in> PiE A B"
    6.77 +  hence "{f} = PiE A (\<lambda>x. {f x})"
    6.78 +    by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
    6.79 +  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
    6.80 +               (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
    6.81 +    using f assms by (subst emeasure_PiM) auto
    6.82 +  also have "\<dots> = (\<Prod>i\<in>A. 1)"
    6.83 +    by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
    6.84 +  also have "\<dots> = emeasure (count_space (PiE A B)) {f}"
    6.85 +    using f by (subst emeasure_count_space_finite) auto
    6.86 +  finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} =
    6.87 +                  emeasure (count_space (Pi\<^sub>E A B)) {f}" .
    6.88 +qed (simp_all add: countable_PiE assms)
    6.89 +
    6.90 +
    6.91 +
    6.92 +definition abs_summable_on ::
    6.93 +    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
    6.94 +    (infix "abs'_summable'_on" 50)
    6.95 + where
    6.96 +   "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
    6.97 +
    6.98 +
    6.99 +definition infsetsum ::
   6.100 +    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
   6.101 + where
   6.102 +   "infsetsum f A = lebesgue_integral (count_space A) f"
   6.103 +
   6.104 +syntax (ASCII)
   6.105 +  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   6.106 +  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
   6.107 +syntax
   6.108 +  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
   6.109 +  ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
   6.110 +translations \<comment> \<open>Beware of argument permutation!\<close>
   6.111 +  "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
   6.112 +
   6.113 +syntax (ASCII)
   6.114 +  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
   6.115 +  ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
   6.116 +syntax
   6.117 +  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
   6.118 +  ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
   6.119 +translations
   6.120 +  "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
   6.121 +
   6.122 +print_translation \<open>
   6.123 +let
   6.124 +  fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   6.125 +        if x <> y then raise Match
   6.126 +        else
   6.127 +          let
   6.128 +            val x' = Syntax_Trans.mark_bound_body (x, Tx);
   6.129 +            val t' = subst_bound (x', t);
   6.130 +            val P' = subst_bound (x', P);
   6.131 +          in
   6.132 +            Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   6.133 +          end
   6.134 +    | sum_tr' _ = raise Match;
   6.135 +in [(@{const_syntax infsetsum}, K sum_tr')] end
   6.136 +\<close>
   6.137 +
   6.138 +
   6.139 +
   6.140 +
   6.141 +lemma restrict_count_space_subset:
   6.142 +  "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
   6.143 +  by (subst restrict_count_space) (simp_all add: Int_absorb2)
   6.144 +
   6.145 +lemma abs_summable_on_restrict:
   6.146 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
   6.147 +  assumes "A \<subseteq> B"
   6.148 +  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B"
   6.149 +proof -
   6.150 +  have "count_space A = restrict_space (count_space B) A"
   6.151 +    by (rule restrict_count_space_subset [symmetric]) fact+
   6.152 +  also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
   6.153 +    by (subst integrable_restrict_space) auto
   6.154 +  finally show ?thesis 
   6.155 +    unfolding abs_summable_on_def .
   6.156 +qed
   6.157 +
   6.158 +lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
   6.159 +  by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def)
   6.160 +
   6.161 +lemma abs_summable_on_altdef': 
   6.162 +  "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
   6.163 +  by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
   6.164 +
   6.165 +lemma abs_summable_on_cong [cong]:
   6.166 +  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> (f abs_summable_on A) \<longleftrightarrow> (g abs_summable_on B)"
   6.167 +  unfolding abs_summable_on_def by (intro integrable_cong) auto
   6.168 +
   6.169 +lemma abs_summable_on_cong_neutral:
   6.170 +  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
   6.171 +  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   6.172 +  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   6.173 +  shows   "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
   6.174 +  unfolding abs_summable_on_altdef using assms
   6.175 +  by (intro Bochner_Integration.integrable_cong refl)
   6.176 +     (auto simp: indicator_def split: if_splits)
   6.177 +
   6.178 +lemma abs_summable_on_restrict':
   6.179 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
   6.180 +  assumes "A \<subseteq> B"
   6.181 +  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B"
   6.182 +  by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)
   6.183 +
   6.184 +lemma abs_summable_on_nat_iff:
   6.185 +  "f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
   6.186 +proof -
   6.187 +  have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))"
   6.188 +    by (subst abs_summable_on_restrict'[of _ UNIV]) 
   6.189 +       (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
   6.190 +  also have "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> A then norm (f x) else 0)"
   6.191 +    by auto
   6.192 +  finally show ?thesis .
   6.193 +qed
   6.194 +
   6.195 +lemma abs_summable_on_nat_iff':
   6.196 +  "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
   6.197 +  by (subst abs_summable_on_nat_iff) auto
   6.198 +
   6.199 +lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
   6.200 +  unfolding abs_summable_on_def by (rule integrable_count_space)
   6.201 +
   6.202 +lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
   6.203 +  by simp
   6.204 +
   6.205 +lemma abs_summable_on_subset:
   6.206 +  assumes "f abs_summable_on B" and "A \<subseteq> B"
   6.207 +  shows   "f abs_summable_on A"
   6.208 +  unfolding abs_summable_on_altdef
   6.209 +  by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)
   6.210 +
   6.211 +lemma abs_summable_on_union [intro]:
   6.212 +  assumes "f abs_summable_on A" and "f abs_summable_on B"
   6.213 +  shows   "f abs_summable_on (A \<union> B)"
   6.214 +  using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto
   6.215 +
   6.216 +lemma abs_summable_on_reindex_bij_betw:
   6.217 +  assumes "bij_betw g A B"
   6.218 +  shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
   6.219 +proof -
   6.220 +  have *: "count_space B = distr (count_space A) (count_space B) g"
   6.221 +    by (rule distr_bij_count_space [symmetric]) fact
   6.222 +  show ?thesis unfolding abs_summable_on_def
   6.223 +    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) 
   6.224 +       (insert assms, auto simp: bij_betw_def)
   6.225 +qed
   6.226 +
   6.227 +lemma abs_summable_on_reindex:
   6.228 +  assumes "(\<lambda>x. f (g x)) abs_summable_on A"
   6.229 +  shows   "f abs_summable_on (g ` A)"
   6.230 +proof -
   6.231 +  define g' where "g' = inv_into A g"
   6.232 +  from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
   6.233 +    by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
   6.234 +  also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
   6.235 +    by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
   6.236 +  also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)"
   6.237 +    by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
   6.238 +  finally show ?thesis .
   6.239 +qed
   6.240 +
   6.241 +lemma abs_summable_reindex_iff: 
   6.242 +  "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
   6.243 +  by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
   6.244 +
   6.245 +lemma abs_summable_on_Sigma_project:
   6.246 +  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   6.247 +  assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
   6.248 +  shows   "(\<lambda>y. f (x, y)) abs_summable_on (B x)"
   6.249 +proof -
   6.250 +  from assms(2) have "f abs_summable_on (Sigma {x} B)"
   6.251 +    by (intro abs_summable_on_subset [OF assms(1)]) auto
   6.252 +  also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)"
   6.253 +    by (rule abs_summable_on_cong) auto
   6.254 +  finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
   6.255 +    by (rule abs_summable_on_reindex)
   6.256 +  also have "snd ` Sigma {x} B = B x"
   6.257 +    using assms by (auto simp: image_iff)
   6.258 +  finally show ?thesis .
   6.259 +qed
   6.260 +
   6.261 +lemma abs_summable_on_Times_swap:
   6.262 +  "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A"
   6.263 +proof -
   6.264 +  have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
   6.265 +    by (auto simp: bij_betw_def inj_on_def)
   6.266 +  show ?thesis
   6.267 +    by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
   6.268 +       (simp_all add: case_prod_unfold)
   6.269 +qed
   6.270 +
   6.271 +lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A"
   6.272 +  by (simp add: abs_summable_on_def)
   6.273 +
   6.274 +lemma abs_summable_on_uminus [intro]:
   6.275 +  "f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A"
   6.276 +  unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)
   6.277 +
   6.278 +lemma abs_summable_on_add [intro]:
   6.279 +  assumes "f abs_summable_on A" and "g abs_summable_on A"
   6.280 +  shows   "(\<lambda>x. f x + g x) abs_summable_on A"
   6.281 +  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)
   6.282 +
   6.283 +lemma abs_summable_on_diff [intro]:
   6.284 +  assumes "f abs_summable_on A" and "g abs_summable_on A"
   6.285 +  shows   "(\<lambda>x. f x - g x) abs_summable_on A"
   6.286 +  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)
   6.287 +
   6.288 +lemma abs_summable_on_scaleR_left [intro]:
   6.289 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.290 +  shows   "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A"
   6.291 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)
   6.292 +
   6.293 +lemma abs_summable_on_scaleR_right [intro]:
   6.294 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.295 +  shows   "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A"
   6.296 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)
   6.297 +
   6.298 +lemma abs_summable_on_cmult_right [intro]:
   6.299 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   6.300 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.301 +  shows   "(\<lambda>x. c * f x) abs_summable_on A"
   6.302 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)
   6.303 +
   6.304 +lemma abs_summable_on_cmult_left [intro]:
   6.305 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   6.306 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.307 +  shows   "(\<lambda>x. f x * c) abs_summable_on A"
   6.308 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
   6.309 +
   6.310 +
   6.311 +
   6.312 +lemma not_summable_infsetsum_eq:
   6.313 +  "\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0"
   6.314 +  by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)
   6.315 +
   6.316 +lemma infsetsum_altdef:
   6.317 +  "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
   6.318 +  by (subst integral_restrict_space [symmetric])
   6.319 +     (auto simp: restrict_count_space_subset infsetsum_def)
   6.320 +
   6.321 +lemma infsetsum_altdef':
   6.322 +  "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
   6.323 +  by (subst integral_restrict_space [symmetric])
   6.324 +     (auto simp: restrict_count_space_subset infsetsum_def)
   6.325 +
   6.326 +lemma infsetsum_cong [cong]:
   6.327 +  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
   6.328 +  unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
   6.329 +
   6.330 +lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0"
   6.331 +  by (simp add: infsetsum_def)
   6.332 +
   6.333 +lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
   6.334 +  by simp
   6.335 +
   6.336 +lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
   6.337 +  by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
   6.338 +
   6.339 +lemma infsetsum_nat: 
   6.340 +  assumes "f abs_summable_on A"
   6.341 +  shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
   6.342 +proof -
   6.343 +  from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
   6.344 +    unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto
   6.345 +  also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
   6.346 +    by auto
   6.347 +  finally show ?thesis .
   6.348 +qed
   6.349 +
   6.350 +lemma infsetsum_nat': 
   6.351 +  assumes "f abs_summable_on UNIV"
   6.352 +  shows   "infsetsum f UNIV = (\<Sum>n. f n)"
   6.353 +  using assms by (subst infsetsum_nat) auto
   6.354 +
   6.355 +lemma sums_infsetsum_nat:
   6.356 +  assumes "f abs_summable_on A"
   6.357 +  shows   "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A"
   6.358 +proof -
   6.359 +  from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
   6.360 +    by (simp add: abs_summable_on_nat_iff)
   6.361 +  also have "(\<lambda>n. if n \<in> A then norm (f n) else 0) = (\<lambda>n. norm (if n \<in> A then f n else 0))"
   6.362 +    by auto
   6.363 +  finally have "summable (\<lambda>n. if n \<in> A then f n else 0)"
   6.364 +    by (rule summable_norm_cancel)
   6.365 +  with assms show ?thesis
   6.366 +    by (auto simp: sums_iff infsetsum_nat)
   6.367 +qed
   6.368 +
   6.369 +lemma sums_infsetsum_nat':
   6.370 +  assumes "f abs_summable_on UNIV"
   6.371 +  shows   "f sums infsetsum f UNIV"
   6.372 +  using sums_infsetsum_nat [OF assms] by simp
   6.373 +
   6.374 +lemma infsetsum_Un_disjoint:
   6.375 +  assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}"
   6.376 +  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B"
   6.377 +  using assms unfolding infsetsum_altdef abs_summable_on_altdef
   6.378 +  by (subst set_integral_Un) auto
   6.379 +
   6.380 +lemma infsetsum_Diff:
   6.381 +  assumes "f abs_summable_on B" "A \<subseteq> B"
   6.382 +  shows   "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
   6.383 +proof -
   6.384 +  have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A"
   6.385 +    using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
   6.386 +  also from assms(2) have "(B - A) \<union> A = B"
   6.387 +    by auto
   6.388 +  ultimately show ?thesis
   6.389 +    by (simp add: algebra_simps)
   6.390 +qed
   6.391 +
   6.392 +lemma infsetsum_Un_Int:
   6.393 +  assumes "f abs_summable_on (A \<union> B)"
   6.394 +  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)"
   6.395 +proof -
   6.396 +  have "A \<union> B = A \<union> (B - A \<inter> B)"
   6.397 +    by auto
   6.398 +  also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)"
   6.399 +    by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
   6.400 +  also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)"
   6.401 +    by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
   6.402 +  finally show ?thesis 
   6.403 +    by (simp add: algebra_simps)
   6.404 +qed
   6.405 +
   6.406 +lemma infsetsum_reindex_bij_betw:
   6.407 +  assumes "bij_betw g A B"
   6.408 +  shows   "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B"
   6.409 +proof -
   6.410 +  have *: "count_space B = distr (count_space A) (count_space B) g"
   6.411 +    by (rule distr_bij_count_space [symmetric]) fact
   6.412 +  show ?thesis unfolding infsetsum_def
   6.413 +    by (subst *, subst integral_distr[of _ _ "count_space B"]) 
   6.414 +       (insert assms, auto simp: bij_betw_def)    
   6.415 +qed
   6.416 +
   6.417 +lemma infsetsum_reindex:
   6.418 +  assumes "inj_on g A"
   6.419 +  shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
   6.420 +  by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
   6.421 +
   6.422 +lemma infsetsum_cong_neutral:
   6.423 +  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
   6.424 +  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
   6.425 +  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
   6.426 +  shows   "infsetsum f A = infsetsum g B"
   6.427 +  unfolding infsetsum_altdef using assms
   6.428 +  by (intro Bochner_Integration.integral_cong refl)
   6.429 +     (auto simp: indicator_def split: if_splits)
   6.430 +
   6.431 +lemma infsetsum_Sigma:
   6.432 +  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
   6.433 +  assumes [simp]: "countable A" and "\<And>i. countable (B i)"
   6.434 +  assumes summable: "f abs_summable_on (Sigma A B)"
   6.435 +  shows   "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
   6.436 +proof -
   6.437 +  define B' where "B' = (\<Union>i\<in>A. B i)"
   6.438 +  have [simp]: "countable B'" 
   6.439 +    unfolding B'_def by (intro countable_UN assms)
   6.440 +  interpret pair_sigma_finite "count_space A" "count_space B'"
   6.441 +    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
   6.442 +
   6.443 +  have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
   6.444 +    using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
   6.445 +  also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))"
   6.446 +    by (intro Bochner_Integration.integrable_cong)
   6.447 +       (auto simp: pair_measure_countable indicator_def split: if_splits)
   6.448 +  finally have integrable: \<dots> .
   6.449 +  
   6.450 +  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
   6.451 +          (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
   6.452 +    unfolding infsetsum_def by simp
   6.453 +  also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
   6.454 +    by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl)
   6.455 +       (auto simp: B'_def)
   6.456 +  also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
   6.457 +    by (subst integral_fst [OF integrable]) auto
   6.458 +  also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
   6.459 +    by (intro Bochner_Integration.integral_cong)
   6.460 +       (auto simp: pair_measure_countable indicator_def split: if_splits)
   6.461 +  also have "\<dots> = infsetsum f (Sigma A B)"
   6.462 +    by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
   6.463 +  finally show ?thesis ..
   6.464 +qed
   6.465 +
   6.466 +lemma infsetsum_Times:
   6.467 +  fixes A :: "'a set" and B :: "'b set"
   6.468 +  assumes [simp]: "countable A" and "countable B"
   6.469 +  assumes summable: "f abs_summable_on (A \<times> B)"
   6.470 +  shows   "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A"
   6.471 +  using assms by (subst infsetsum_Sigma) auto
   6.472 +
   6.473 +lemma infsetsum_Times':
   6.474 +  fixes A :: "'a set" and B :: "'b set"
   6.475 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
   6.476 +  assumes [simp]: "countable A" and [simp]: "countable B"
   6.477 +  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)"
   6.478 +  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
   6.479 +  using assms by (subst infsetsum_Times) auto
   6.480 +
   6.481 +lemma infsetsum_swap:
   6.482 +  fixes A :: "'a set" and B :: "'b set"
   6.483 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
   6.484 +  assumes [simp]: "countable A" and [simp]: "countable B"
   6.485 +  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B"
   6.486 +  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
   6.487 +proof -
   6.488 +  from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A"
   6.489 +    by (subst abs_summable_on_Times_swap) auto
   6.490 +  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)"
   6.491 +    by (auto simp: bij_betw_def inj_on_def)
   6.492 +  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
   6.493 +    using summable by (subst infsetsum_Times) auto
   6.494 +  also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)"
   6.495 +    by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric])
   6.496 +       (simp_all add: case_prod_unfold)
   6.497 +  also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
   6.498 +    using summable' by (subst infsetsum_Times) auto
   6.499 +  finally show ?thesis .
   6.500 +qed
   6.501 +
   6.502 +lemma infsetsum_prod_PiE:
   6.503 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
   6.504 +  assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
   6.505 +  assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
   6.506 +  shows   "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
   6.507 +proof -
   6.508 +  define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
   6.509 +  from assms have [simp]: "countable (B' x)" for x
   6.510 +    by (auto simp: B'_def)
   6.511 +  then interpret product_sigma_finite "count_space \<circ> B'"
   6.512 +    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
   6.513 +  have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) =
   6.514 +          (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))"
   6.515 +    by (simp add: infsetsum_def)
   6.516 +  also have "PiE A B = PiE A B'"
   6.517 +    by (intro PiE_cong) (simp_all add: B'_def)
   6.518 +  hence "count_space (PiE A B) = count_space (PiE A B')"
   6.519 +    by simp
   6.520 +  also have "\<dots> = PiM A (count_space \<circ> B')"
   6.521 +    unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
   6.522 +  also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))"
   6.523 +    by (subst product_integral_prod) 
   6.524 +       (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
   6.525 +  also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
   6.526 +    by (intro prod.cong refl) (simp_all add: B'_def)
   6.527 +  finally show ?thesis .
   6.528 +qed
   6.529 +
   6.530 +lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A"
   6.531 +  unfolding infsetsum_def abs_summable_on_def 
   6.532 +  by (rule Bochner_Integration.integral_minus)
   6.533 +
   6.534 +lemma infsetsum_add:
   6.535 +  assumes "f abs_summable_on A" and "g abs_summable_on A"
   6.536 +  shows   "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A"
   6.537 +  using assms unfolding infsetsum_def abs_summable_on_def 
   6.538 +  by (rule Bochner_Integration.integral_add)
   6.539 +
   6.540 +lemma infsetsum_diff:
   6.541 +  assumes "f abs_summable_on A" and "g abs_summable_on A"
   6.542 +  shows   "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A"
   6.543 +  using assms unfolding infsetsum_def abs_summable_on_def 
   6.544 +  by (rule Bochner_Integration.integral_diff)
   6.545 +
   6.546 +lemma infsetsum_scaleR_left:
   6.547 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.548 +  shows   "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c"
   6.549 +  using assms unfolding infsetsum_def abs_summable_on_def 
   6.550 +  by (rule Bochner_Integration.integral_scaleR_left)
   6.551 +
   6.552 +lemma infsetsum_scaleR_right:
   6.553 +  "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A"
   6.554 +  unfolding infsetsum_def abs_summable_on_def 
   6.555 +  by (subst Bochner_Integration.integral_scaleR_right) auto
   6.556 +
   6.557 +lemma infsetsum_cmult_left:
   6.558 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   6.559 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.560 +  shows   "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c"
   6.561 +  using assms unfolding infsetsum_def abs_summable_on_def 
   6.562 +  by (rule Bochner_Integration.integral_mult_left)
   6.563 +
   6.564 +lemma infsetsum_cmult_right:
   6.565 +  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   6.566 +  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   6.567 +  shows   "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A"
   6.568 +  using assms unfolding infsetsum_def abs_summable_on_def 
   6.569 +  by (rule Bochner_Integration.integral_mult_right)
   6.570 +
   6.571 +(* TODO Generalise with bounded_linear *)
   6.572 +
   6.573 +end
     7.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 21 19:20:02 2017 +0200
     7.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 21 20:49:15 2017 +0200
     7.3 @@ -402,53 +402,53 @@
     7.4  qed 
     7.5  
     7.6  
     7.7 -subsection \<open>The eXtractor series X\<close>
     7.8 +subsection \<open>The efps_Xtractor series fps_X\<close>
     7.9  
    7.10  lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
    7.11    by (induct n) auto
    7.12  
    7.13 -definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
    7.14 -
    7.15 -lemma X_mult_nth [simp]:
    7.16 -  "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
    7.17 +definition "fps_X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
    7.18 +
    7.19 +lemma fps_X_mult_nth [simp]:
    7.20 +  "(fps_X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
    7.21  proof (cases "n = 0")
    7.22    case False
    7.23 -  have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
    7.24 +  have "(fps_X * f) $n = (\<Sum>i = 0..n. fps_X $ i * f $ (n - i))"
    7.25      by (simp add: fps_mult_nth)
    7.26    also have "\<dots> = f $ (n - 1)"
    7.27 -    using False by (simp add: X_def mult_delta_left sum.delta)
    7.28 +    using False by (simp add: fps_X_def mult_delta_left sum.delta)
    7.29    finally show ?thesis
    7.30      using False by simp
    7.31  next
    7.32    case True
    7.33    then show ?thesis
    7.34 -    by (simp add: fps_mult_nth X_def)
    7.35 +    by (simp add: fps_mult_nth fps_X_def)
    7.36  qed
    7.37  
    7.38 -lemma X_mult_right_nth[simp]:
    7.39 -  "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))"
    7.40 +lemma fps_X_mult_right_nth[simp]:
    7.41 +  "((a::'a::semiring_1 fps) * fps_X) $ n = (if n = 0 then 0 else a $ (n - 1))"
    7.42  proof -
    7.43 -  have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
    7.44 -    by (simp add: fps_times_def X_def)
    7.45 +  have "(a * fps_X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
    7.46 +    by (simp add: fps_times_def fps_X_def)
    7.47    also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
    7.48      by (intro sum.cong) auto
    7.49    also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: sum.delta)
    7.50    finally show ?thesis .
    7.51  qed
    7.52  
    7.53 -lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
    7.54 +lemma fps_mult_fps_X_commute: "fps_X * (a :: 'a :: semiring_1 fps) = a * fps_X" 
    7.55    by (simp add: fps_eq_iff)
    7.56  
    7.57 -lemma X_power_iff: "X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)"
    7.58 +lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)"
    7.59    by (induction n) (auto simp: fps_eq_iff)
    7.60  
    7.61 -lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
    7.62 -  by (simp add: X_def)
    7.63 -
    7.64 -lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
    7.65 -  by (simp add: X_power_iff)
    7.66 -
    7.67 -lemma X_power_mult_nth: "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
    7.68 +lemma fps_X_nth[simp]: "fps_X$n = (if n = 1 then 1 else 0)"
    7.69 +  by (simp add: fps_X_def)
    7.70 +
    7.71 +lemma fps_X_power_nth[simp]: "(fps_X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
    7.72 +  by (simp add: fps_X_power_iff)
    7.73 +
    7.74 +lemma fps_X_power_mult_nth: "(fps_X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
    7.75    apply (induct k arbitrary: n)
    7.76    apply simp
    7.77    unfolding power_Suc mult.assoc
    7.78 @@ -456,32 +456,32 @@
    7.79    apply auto
    7.80    done
    7.81  
    7.82 -lemma X_power_mult_right_nth:
    7.83 -    "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
    7.84 -  by (metis X_power_mult_nth mult.commute)
    7.85 -
    7.86 -
    7.87 -lemma X_neq_fps_const [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> fps_const c"
    7.88 +lemma fps_X_power_mult_right_nth:
    7.89 +    "((f :: 'a::comm_ring_1 fps) * fps_X^k) $n = (if n < k then 0 else f $ (n - k))"
    7.90 +  by (metis fps_X_power_mult_nth mult.commute)
    7.91 +
    7.92 +
    7.93 +lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> fps_const c"
    7.94  proof
    7.95 -  assume "(X::'a fps) = fps_const (c::'a)"
    7.96 -  hence "X$1 = (fps_const (c::'a))$1" by (simp only:)
    7.97 +  assume "(fps_X::'a fps) = fps_const (c::'a)"
    7.98 +  hence "fps_X$1 = (fps_const (c::'a))$1" by (simp only:)
    7.99    thus False by auto
   7.100  qed
   7.101  
   7.102 -lemma X_neq_zero [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 0"
   7.103 -  by (simp only: fps_const_0_eq_0[symmetric] X_neq_fps_const) simp
   7.104 -
   7.105 -lemma X_neq_one [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 1"
   7.106 -  by (simp only: fps_const_1_eq_1[symmetric] X_neq_fps_const) simp
   7.107 -
   7.108 -lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
   7.109 -  by (simp only: numeral_fps_const X_neq_fps_const) simp
   7.110 -
   7.111 -lemma X_pow_eq_X_pow_iff [simp]:
   7.112 -  "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n"
   7.113 +lemma fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 0"
   7.114 +  by (simp only: fps_const_0_eq_0[symmetric] fps_X_neq_fps_const) simp
   7.115 +
   7.116 +lemma fps_X_neq_one [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 1"
   7.117 +  by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp
   7.118 +
   7.119 +lemma fps_X_neq_numeral [simp]: "(fps_X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
   7.120 +  by (simp only: numeral_fps_const fps_X_neq_fps_const) simp
   7.121 +
   7.122 +lemma fps_X_pow_eq_fps_X_pow_iff [simp]:
   7.123 +  "(fps_X :: ('a :: {comm_ring_1}) fps) ^ m = fps_X ^ n \<longleftrightarrow> m = n"
   7.124  proof
   7.125 -  assume "(X :: 'a fps) ^ m = X ^ n"
   7.126 -  hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
   7.127 +  assume "(fps_X :: 'a fps) ^ m = fps_X ^ n"
   7.128 +  hence "(fps_X :: 'a fps) ^ m $ m = fps_X ^ n $ m" by (simp only:)
   7.129    thus "m = n" by (simp split: if_split_asm)
   7.130  qed simp_all
   7.131  
   7.132 @@ -553,8 +553,8 @@
   7.133  lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0"
   7.134    by (auto intro!: subdegreeI)
   7.135  
   7.136 -lemma subdegree_X [simp]: "subdegree (X :: ('a :: zero_neq_one) fps) = 1"
   7.137 -  by (auto intro!: subdegreeI simp: X_def)
   7.138 +lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1"
   7.139 +  by (auto intro!: subdegreeI simp: fps_X_def)
   7.140  
   7.141  lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
   7.142    by (cases "c = 0") (auto intro!: subdegreeI)
   7.143 @@ -705,33 +705,33 @@
   7.144  lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)"
   7.145    by (simp add: numeral_fps_const fps_shift_fps_const)
   7.146  
   7.147 -lemma fps_shift_X_power [simp]:
   7.148 -  "n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m - n) ::'a::comm_ring_1 fps)"
   7.149 +lemma fps_shift_fps_X_power [simp]:
   7.150 +  "n \<le> m \<Longrightarrow> fps_shift n (fps_X ^ m) = (fps_X ^ (m - n) ::'a::comm_ring_1 fps)"
   7.151    by (intro fps_ext) (auto simp: fps_shift_def )
   7.152  
   7.153 -lemma fps_shift_times_X_power:
   7.154 -  "n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)"
   7.155 -  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
   7.156 -
   7.157 -lemma fps_shift_times_X_power' [simp]:
   7.158 -  "fps_shift n (f * X^n) = (f :: 'a :: comm_ring_1 fps)"
   7.159 -  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
   7.160 -
   7.161 -lemma fps_shift_times_X_power'':
   7.162 -  "m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
   7.163 -  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
   7.164 +lemma fps_shift_times_fps_X_power:
   7.165 +  "n \<le> subdegree f \<Longrightarrow> fps_shift n f * fps_X ^ n = (f :: 'a :: comm_ring_1 fps)"
   7.166 +  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
   7.167 +
   7.168 +lemma fps_shift_times_fps_X_power' [simp]:
   7.169 +  "fps_shift n (f * fps_X^n) = (f :: 'a :: comm_ring_1 fps)"
   7.170 +  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
   7.171 +
   7.172 +lemma fps_shift_times_fps_X_power'':
   7.173 +  "m \<le> n \<Longrightarrow> fps_shift n (f * fps_X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
   7.174 +  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
   7.175  
   7.176  lemma fps_shift_subdegree [simp]:
   7.177    "n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n"
   7.178    by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+
   7.179  
   7.180  lemma subdegree_decompose:
   7.181 -  "f = fps_shift (subdegree f) f * X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
   7.182 -  by (rule fps_ext) (auto simp: X_power_mult_right_nth)
   7.183 +  "f = fps_shift (subdegree f) f * fps_X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
   7.184 +  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth)
   7.185  
   7.186  lemma subdegree_decompose':
   7.187 -  "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * X^n"
   7.188 -  by (rule fps_ext) (auto simp: X_power_mult_right_nth intro!: nth_less_subdegree_zero)
   7.189 +  "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * fps_X^n"
   7.190 +  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth intro!: nth_less_subdegree_zero)
   7.191  
   7.192  lemma fps_shift_fps_shift:
   7.193    "fps_shift (m + n) f = fps_shift m (fps_shift n f)"
   7.194 @@ -745,8 +745,8 @@
   7.195    assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
   7.196    shows   "fps_shift n (h*g) = h * fps_shift n g"
   7.197  proof -
   7.198 -  from assms have "g = fps_shift n g * X^n" by (rule subdegree_decompose')
   7.199 -  also have "h * ... = (h * fps_shift n g) * X^n" by simp
   7.200 +  from assms have "g = fps_shift n g * fps_X^n" by (rule subdegree_decompose')
   7.201 +  also have "h * ... = (h * fps_shift n g) * fps_X^n" by simp
   7.202    also have "fps_shift n ... = h * fps_shift n g" by simp
   7.203    finally show ?thesis .
   7.204  qed
   7.205 @@ -798,8 +798,8 @@
   7.206    by (simp add: numeral_fps_const fps_cutoff_fps_const)
   7.207  
   7.208  lemma fps_shift_cutoff:
   7.209 -  "fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f"
   7.210 -  by (simp add: fps_eq_iff X_power_mult_right_nth)
   7.211 +  "fps_shift n (f :: ('a :: comm_ring_1) fps) * fps_X^n + fps_cutoff n f = f"
   7.212 +  by (simp add: fps_eq_iff fps_X_power_mult_right_nth)
   7.213  
   7.214  
   7.215  subsection \<open>Formal Power series form a metric space\<close>
   7.216 @@ -905,11 +905,11 @@
   7.217      using kp by blast
   7.218  qed
   7.219  
   7.220 -lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
   7.221 +lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*fps_X^i) {0..m})$n =
   7.222      (if n \<le> m then a$n else 0::'a::comm_ring_1)"
   7.223    by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
   7.224  
   7.225 -lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
   7.226 +lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * fps_X^i) {0..n}) \<longlonglongrightarrow> a"
   7.227    (is "?s \<longlonglongrightarrow> a")
   7.228  proof -
   7.229    have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
   7.230 @@ -1153,12 +1153,12 @@
   7.231    "unit_factor f = fps_shift (subdegree f) f"
   7.232  
   7.233  definition fps_normalize_def [simp]:
   7.234 -  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
   7.235 +  "normalize f = (if f = 0 then 0 else fps_X ^ subdegree f)"
   7.236  
   7.237  instance proof
   7.238    fix f :: "'a fps"
   7.239    show "unit_factor f * normalize f = f"
   7.240 -    by (simp add: fps_shift_times_X_power)
   7.241 +    by (simp add: fps_shift_times_fps_X_power)
   7.242  next
   7.243    fix f g :: "'a fps"
   7.244    show "unit_factor (f * g) = unit_factor f * unit_factor g"
   7.245 @@ -1205,10 +1205,10 @@
   7.246  
   7.247    from assms nz have "f div g * g = fps_shift n (f * inverse h) * g"
   7.248      by (simp add: fps_divide_def Let_def h_def n_def)
   7.249 -  also have "... = fps_shift n (f * inverse h) * X^n * h" unfolding h_def n_def
   7.250 +  also have "... = fps_shift n (f * inverse h) * fps_X^n * h" unfolding h_def n_def
   7.251      by (subst subdegree_decompose[of g]) simp
   7.252 -  also have "fps_shift n (f * inverse h) * X^n = f * inverse h"
   7.253 -    by (rule fps_shift_times_X_power) (simp_all add: nz assms n_def)
   7.254 +  also have "fps_shift n (f * inverse h) * fps_X^n = f * inverse h"
   7.255 +    by (rule fps_shift_times_fps_X_power) (simp_all add: nz assms n_def)
   7.256    also have "... * h = f * (inverse h * h)" by simp
   7.257    also have "inverse h * h = 1" by (rule inverse_mult_eq_1) simp
   7.258    finally show ?thesis by simp
   7.259 @@ -1246,14 +1246,14 @@
   7.260  qed (simp_all add: fps_divide_def)
   7.261  
   7.262  private lemma fps_divide_cancel_aux2:
   7.263 -  "(f * X^m) div (g * X^m) = f div (g :: 'a :: field fps)"
   7.264 +  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
   7.265  proof (cases "g = 0")
   7.266    assume [simp]: "g \<noteq> 0"
   7.267 -  have "(f * X^m) div (g * X^m) =
   7.268 -          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*X^m))*X^m)"
   7.269 +  have "(f * fps_X^m) div (g * fps_X^m) =
   7.270 +          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
   7.271      by (simp add: fps_divide_def Let_def algebra_simps)
   7.272    also have "... = f div g"
   7.273 -    by (simp add: fps_shift_times_X_power'' fps_divide_def Let_def)
   7.274 +    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
   7.275    finally show ?thesis .
   7.276  qed (simp_all add: fps_divide_def)
   7.277  
   7.278 @@ -1272,11 +1272,11 @@
   7.279        with nz show ?thesis by (simp add: fps_mod_eq_zero fps_times_divide_eq)
   7.280      next
   7.281        assume "subdegree f < subdegree g"
   7.282 -      have g_decomp: "g = h * X^n" unfolding h_def n_def by (rule subdegree_decompose)
   7.283 +      have g_decomp: "g = h * fps_X^n" unfolding h_def n_def by (rule subdegree_decompose)
   7.284        have "f div g * g + f mod g =
   7.285                fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h"
   7.286          by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def)
   7.287 -      also have "... = h * (fps_shift n (f * inverse h) * X^n + fps_cutoff n (f * inverse h))"
   7.288 +      also have "... = h * (fps_shift n (f * inverse h) * fps_X^n + fps_cutoff n (f * inverse h))"
   7.289          by (subst g_decomp) (simp add: algebra_simps)
   7.290        also have "... = f * (inverse h * h)"
   7.291          by (subst fps_shift_cutoff) simp
   7.292 @@ -1292,9 +1292,9 @@
   7.293    proof -
   7.294      define m where "m = subdegree h"
   7.295      define h' where "h' = fps_shift m h"
   7.296 -    have h_decomp: "h = h' * X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
   7.297 +    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
   7.298      from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
   7.299 -    have "(h * f) div (h * g) = (h' * f * X^m) div (h' * g * X^m)"
   7.300 +    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
   7.301        by (simp add: h_decomp algebra_simps)
   7.302      also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
   7.303      finally show ?thesis .
   7.304 @@ -1306,10 +1306,10 @@
   7.305    define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
   7.306    have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
   7.307      by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add)
   7.308 -  also have "h * inverse h' = (inverse h' * h') * X^n"
   7.309 +  also have "h * inverse h' = (inverse h' * h') * fps_X^n"
   7.310      by (subst subdegree_decompose) (simp_all add: dfs)
   7.311 -  also have "... = X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
   7.312 -  also have "fps_shift n (g * X^n) = g" by simp
   7.313 +  also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
   7.314 +  also have "fps_shift n (g * fps_X^n) = g" by simp
   7.315    also have "fps_shift n (f * inverse h') = f div h"
   7.316      by (simp add: fps_divide_def Let_def dfs)
   7.317    finally show "(f + g * h) div h = g + f div h" by simp
   7.318 @@ -1354,14 +1354,14 @@
   7.319  qed (simp add: assms dvd_imp_subdegree_le)
   7.320  
   7.321  lemma fps_shift_altdef:
   7.322 -  "fps_shift n f = (f :: 'a :: field fps) div X^n"
   7.323 +  "fps_shift n f = (f :: 'a :: field fps) div fps_X^n"
   7.324    by (simp add: fps_divide_def)
   7.325    
   7.326 -lemma fps_div_X_power_nth: "((f :: 'a :: field fps) div X^n) $ k = f $ (k + n)"
   7.327 +lemma fps_div_fps_X_power_nth: "((f :: 'a :: field fps) div fps_X^n) $ k = f $ (k + n)"
   7.328    by (simp add: fps_shift_altdef [symmetric])
   7.329  
   7.330 -lemma fps_div_X_nth: "((f :: 'a :: field fps) div X) $ k = f $ Suc k"
   7.331 -  using fps_div_X_power_nth[of f 1] by simp
   7.332 +lemma fps_div_fps_X_nth: "((f :: 'a :: field fps) div fps_X) $ k = f $ Suc k"
   7.333 +  using fps_div_fps_X_power_nth[of f 1] by simp
   7.334  
   7.335  lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
   7.336    by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff)
   7.337 @@ -1419,45 +1419,45 @@
   7.338  
   7.339  lemma fps_gcd:
   7.340    assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
   7.341 -  shows   "gcd f g = X ^ min (subdegree f) (subdegree g)"
   7.342 +  shows   "gcd f g = fps_X ^ min (subdegree f) (subdegree g)"
   7.343  proof -
   7.344    let ?m = "min (subdegree f) (subdegree g)"
   7.345 -  show "gcd f g = X ^ ?m"
   7.346 +  show "gcd f g = fps_X ^ ?m"
   7.347    proof (rule sym, rule gcdI)
   7.348      fix d assume "d dvd f" "d dvd g"
   7.349 -    thus "d dvd X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff)
   7.350 +    thus "d dvd fps_X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff)
   7.351    qed (simp_all add: fps_dvd_iff)
   7.352  qed
   7.353  
   7.354  lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g =
   7.355    (if f = 0 \<and> g = 0 then 0 else
   7.356 -   if f = 0 then X ^ subdegree g else
   7.357 -   if g = 0 then X ^ subdegree f else
   7.358 -     X ^ min (subdegree f) (subdegree g))"
   7.359 +   if f = 0 then fps_X ^ subdegree g else
   7.360 +   if g = 0 then fps_X ^ subdegree f else
   7.361 +     fps_X ^ min (subdegree f) (subdegree g))"
   7.362    by (simp add: fps_gcd)
   7.363  
   7.364  lemma fps_lcm:
   7.365    assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
   7.366 -  shows   "lcm f g = X ^ max (subdegree f) (subdegree g)"
   7.367 +  shows   "lcm f g = fps_X ^ max (subdegree f) (subdegree g)"
   7.368  proof -
   7.369    let ?m = "max (subdegree f) (subdegree g)"
   7.370 -  show "lcm f g = X ^ ?m"
   7.371 +  show "lcm f g = fps_X ^ ?m"
   7.372    proof (rule sym, rule lcmI)
   7.373      fix d assume "f dvd d" "g dvd d"
   7.374 -    thus "X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff)
   7.375 +    thus "fps_X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff)
   7.376    qed (simp_all add: fps_dvd_iff)
   7.377  qed
   7.378  
   7.379  lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g =
   7.380 -  (if f = 0 \<or> g = 0 then 0 else X ^ max (subdegree f) (subdegree g))"
   7.381 +  (if f = 0 \<or> g = 0 then 0 else fps_X ^ max (subdegree f) (subdegree g))"
   7.382    by (simp add: fps_lcm)
   7.383  
   7.384  lemma fps_Gcd:
   7.385    assumes "A - {0} \<noteq> {}"
   7.386 -  shows   "Gcd A = X ^ (INF f:A-{0}. subdegree f)"
   7.387 +  shows   "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)"
   7.388  proof (rule sym, rule GcdI)
   7.389    fix f assume "f \<in> A"
   7.390 -  thus "X ^ (INF f:A - {0}. subdegree f) dvd f"
   7.391 +  thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f"
   7.392      by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower)
   7.393  next
   7.394    fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f"
   7.395 @@ -1465,25 +1465,25 @@
   7.396    with d[of f] have [simp]: "d \<noteq> 0" by auto
   7.397    from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)"
   7.398      by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric])
   7.399 -  with d assms show "d dvd X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
   7.400 +  with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
   7.401  qed simp_all
   7.402  
   7.403  lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
   7.404 -  (if A \<subseteq> {0} then 0 else X ^ (INF f:A-{0}. subdegree f))"
   7.405 +  (if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))"
   7.406    using fps_Gcd by auto
   7.407  
   7.408  lemma fps_Lcm:
   7.409    assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)"
   7.410 -  shows   "Lcm A = X ^ (SUP f:A. subdegree f)"
   7.411 +  shows   "Lcm A = fps_X ^ (SUP f:A. subdegree f)"
   7.412  proof (rule sym, rule LcmI)
   7.413    fix f assume "f \<in> A"
   7.414    moreover from assms(3) have "bdd_above (subdegree ` A)" by auto
   7.415 -  ultimately show "f dvd X ^ (SUP f:A. subdegree f)" using assms(2)
   7.416 +  ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2)
   7.417      by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper)
   7.418  next
   7.419    fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d"
   7.420    from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto
   7.421 -  show "X ^ (SUP f:A. subdegree f) dvd d"
   7.422 +  show "fps_X ^ (SUP f:A. subdegree f) dvd d"
   7.423    proof (cases "d = 0")
   7.424      assume "d \<noteq> 0"
   7.425      moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast
   7.426 @@ -1496,7 +1496,7 @@
   7.427  lemma fps_Lcm_altdef:
   7.428    "Lcm (A :: 'a :: field fps set) =
   7.429       (if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
   7.430 -      if A = {} then 1 else X ^ (SUP f:A. subdegree f))"
   7.431 +      if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))"
   7.432  proof (cases "bdd_above (subdegree`A)")
   7.433    assume unbounded: "\<not>bdd_above (subdegree`A)"
   7.434    have "Lcm A = 0"
   7.435 @@ -1568,8 +1568,8 @@
   7.436      unfolding fps_eq_iff by auto
   7.437  qed
   7.438  
   7.439 -lemma fps_deriv_X[simp]: "fps_deriv X = 1"
   7.440 -  by (simp add: fps_deriv_def X_def fps_eq_iff)
   7.441 +lemma fps_deriv_fps_X[simp]: "fps_deriv fps_X = 1"
   7.442 +  by (simp add: fps_deriv_def fps_X_def fps_eq_iff)
   7.443  
   7.444  lemma fps_deriv_neg[simp]:
   7.445    "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)"
   7.446 @@ -1878,7 +1878,7 @@
   7.447  lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f"
   7.448    by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse)
   7.449  
   7.450 -(* FIXME: The last part of this proof should go through by simp once we have a proper
   7.451 +(* FIfps_XME: The last part of this proof should go through by simp once we have a proper
   7.452     theorem collection for simplifying division on rings *)
   7.453  lemma fps_divide_deriv:
   7.454    assumes "b dvd (a :: 'a :: field fps)"
   7.455 @@ -1893,28 +1893,28 @@
   7.456    thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp)
   7.457  qed
   7.458  
   7.459 -lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
   7.460 -  by (simp add: fps_inverse_gp fps_eq_iff X_def)
   7.461 -
   7.462 -lemma fps_one_over_one_minus_X_squared:
   7.463 -  "inverse ((1 - X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
   7.464 +lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - fps_X"
   7.465 +  by (simp add: fps_inverse_gp fps_eq_iff fps_X_def)
   7.466 +
   7.467 +lemma fps_one_over_one_minus_fps_X_squared:
   7.468 +  "inverse ((1 - fps_X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
   7.469  proof -
   7.470 -  have "inverse ((1 - X)^2 :: 'a fps) = fps_deriv (inverse (1 - X))"
   7.471 +  have "inverse ((1 - fps_X)^2 :: 'a fps) = fps_deriv (inverse (1 - fps_X))"
   7.472      by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power)
   7.473 -  also have "inverse (1 - X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
   7.474 +  also have "inverse (1 - fps_X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
   7.475      by (subst fps_inverse_gp' [symmetric]) simp
   7.476    also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))"
   7.477      by (simp add: fps_deriv_def)
   7.478    finally show ?thesis .
   7.479  qed
   7.480  
   7.481 -lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
   7.482 +lemma fps_nth_deriv_fps_X[simp]: "fps_nth_deriv n fps_X = (if n = 0 then fps_X else if n=1 then 1 else 0)"
   7.483    by (cases n) simp_all
   7.484  
   7.485 -lemma fps_inverse_X_plus1: "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)"
   7.486 +lemma fps_inverse_fps_X_plus1: "inverse (1 + fps_X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)"
   7.487    (is "_ = ?r")
   7.488  proof -
   7.489 -  have eq: "(1 + X) * ?r = 1"
   7.490 +  have eq: "(1 + fps_X) * ?r = 1"
   7.491      unfolding minus_one_power_iff
   7.492      by (auto simp add: field_simps fps_eq_iff)
   7.493    show ?thesis
   7.494 @@ -1956,7 +1956,7 @@
   7.495  lemma fps_compose_nth_0 [simp]: "(f oo g) $ 0 = f $ 0"
   7.496    by (simp add: fps_compose_nth)
   7.497  
   7.498 -lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)"
   7.499 +lemma fps_compose_fps_X[simp]: "a oo fps_X = (a :: 'a::comm_ring_1 fps)"
   7.500    by (simp add: fps_ext fps_compose_def mult_delta_right sum.delta')
   7.501  
   7.502  lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a"
   7.503 @@ -1968,7 +1968,7 @@
   7.504  lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k"
   7.505    unfolding neg_numeral_fps_const by simp
   7.506  
   7.507 -lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: 'a::comm_ring_1 fps)"
   7.508 +lemma fps_X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> fps_X oo a = (a :: 'a::comm_ring_1 fps)"
   7.509    by (simp add: fps_eq_iff fps_compose_def mult_delta_left sum.delta not_le)
   7.510  
   7.511  
   7.512 @@ -1978,14 +1978,14 @@
   7.513    (* {a_{n+k}}_0^infty Corresponds to (f - sum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
   7.514  
   7.515  lemma fps_power_mult_eq_shift:
   7.516 -  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
   7.517 -    Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}"
   7.518 +  "fps_X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
   7.519 +    Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * fps_X^i) {0 .. k}"
   7.520    (is "?lhs = ?rhs")
   7.521  proof -
   7.522    have "?lhs $ n = ?rhs $ n" for n :: nat
   7.523    proof -
   7.524      have "?lhs $ n = (if n < Suc k then 0 else a n)"
   7.525 -      unfolding X_power_mult_nth by auto
   7.526 +      unfolding fps_X_power_mult_nth by auto
   7.527      also have "\<dots> = ?rhs $ n"
   7.528      proof (induct k)
   7.529        case 0
   7.530 @@ -1993,14 +1993,14 @@
   7.531          by (simp add: fps_sum_nth)
   7.532      next
   7.533        case (Suc k)
   7.534 -      have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n =
   7.535 -        (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} -
   7.536 -          fps_const (a (Suc k)) * X^ Suc k) $ n"
   7.537 +      have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. Suc k})$n =
   7.538 +        (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. k} -
   7.539 +          fps_const (a (Suc k)) * fps_X^ Suc k) $ n"
   7.540          by (simp add: field_simps)
   7.541 -      also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
   7.542 +      also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * fps_X^ Suc k)$n"
   7.543          using Suc.hyps[symmetric] unfolding fps_sub_nth by simp
   7.544        also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)"
   7.545 -        unfolding X_power_mult_right_nth
   7.546 +        unfolding fps_X_power_mult_right_nth
   7.547          apply (auto simp add: not_less fps_const_def)
   7.548          apply (rule cong[of a a, OF refl])
   7.549          apply arith
   7.550 @@ -2021,29 +2021,29 @@
   7.551    (* If f reprents {a_n} and P is a polynomial, then
   7.552          P(xD) f represents {P(n) a_n}*)
   7.553  
   7.554 -definition "XD = op * X \<circ> fps_deriv"
   7.555 -
   7.556 -lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: 'a::comm_ring_1 fps)"
   7.557 -  by (simp add: XD_def field_simps)
   7.558 -
   7.559 -lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
   7.560 -  by (simp add: XD_def field_simps)
   7.561 -
   7.562 -lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) =
   7.563 -    fps_const c * XD a + fps_const d * XD (b :: 'a::comm_ring_1 fps)"
   7.564 +definition "fps_XD = op * fps_X \<circ> fps_deriv"
   7.565 +
   7.566 +lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
   7.567 +  by (simp add: fps_XD_def field_simps)
   7.568 +
   7.569 +lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a"
   7.570 +  by (simp add: fps_XD_def field_simps)
   7.571 +
   7.572 +lemma fps_XD_linear[simp]: "fps_XD (fps_const c * a + fps_const d * b) =
   7.573 +    fps_const c * fps_XD a + fps_const d * fps_XD (b :: 'a::comm_ring_1 fps)"
   7.574    by simp
   7.575  
   7.576 -lemma XDN_linear:
   7.577 -  "(XD ^^ n) (fps_const c * a + fps_const d * b) =
   7.578 -    fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: 'a::comm_ring_1 fps)"
   7.579 +lemma fps_XDN_linear:
   7.580 +  "(fps_XD ^^ n) (fps_const c * a + fps_const d * b) =
   7.581 +    fps_const c * (fps_XD ^^ n) a + fps_const d * (fps_XD ^^ n) (b :: 'a::comm_ring_1 fps)"
   7.582    by (induct n) simp_all
   7.583  
   7.584 -lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
   7.585 +lemma fps_mult_fps_X_deriv_shift: "fps_X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
   7.586    by (simp add: fps_eq_iff)
   7.587  
   7.588 -lemma fps_mult_XD_shift:
   7.589 -  "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   7.590 -  by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def)
   7.591 +lemma fps_mult_fps_XD_shift:
   7.592 +  "(fps_XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   7.593 +  by (induct k arbitrary: a) (simp_all add: fps_XD_def fps_eq_iff field_simps del: One_nat_def)
   7.594  
   7.595  
   7.596  subsubsection \<open>Rule 3\<close>
   7.597 @@ -2051,15 +2051,15 @@
   7.598  text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
   7.599  
   7.600  
   7.601 -subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close>
   7.602 -
   7.603 -lemma fps_divide_X_minus1_sum_lemma:
   7.604 -  "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
   7.605 +subsubsection \<open>Rule 5 --- summation and "division" by (1 - fps_X)\<close>
   7.606 +
   7.607 +lemma fps_divide_fps_X_minus1_sum_lemma:
   7.608 +  "a = ((1::'a::comm_ring_1 fps) - fps_X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
   7.609  proof -
   7.610    let ?sa = "Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
   7.611 -  have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
   7.612 +  have th0: "\<And>i. (1 - (fps_X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
   7.613      by simp
   7.614 -  have "a$n = ((1 - X) * ?sa) $ n" for n
   7.615 +  have "a$n = ((1 - fps_X) * ?sa) $ n" for n
   7.616    proof (cases "n = 0")
   7.617      case True
   7.618      then show ?thesis
   7.619 @@ -2073,7 +2073,7 @@
   7.620        using False by simp_all
   7.621      have f: "finite {0}" "finite {1}" "finite {2 .. n}"
   7.622        "finite {0 .. n - 1}" "finite {n}" by simp_all
   7.623 -    have "((1 - X) * ?sa) $ n = sum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}"
   7.624 +    have "((1 - fps_X) * ?sa) $ n = sum (\<lambda>i. (1 - fps_X)$ i * ?sa $ (n - i)) {0 .. n}"
   7.625        by (simp add: fps_mult_nth)
   7.626      also have "\<dots> = a$n"
   7.627        unfolding th0
   7.628 @@ -2090,16 +2090,16 @@
   7.629      unfolding fps_eq_iff by blast
   7.630  qed
   7.631  
   7.632 -lemma fps_divide_X_minus1_sum:
   7.633 -  "a /((1::'a::field fps) - X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
   7.634 +lemma fps_divide_fps_X_minus1_sum:
   7.635 +  "a /((1::'a::field fps) - fps_X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
   7.636  proof -
   7.637 -  let ?X = "1 - (X::'a fps)"
   7.638 -  have th0: "?X $ 0 \<noteq> 0"
   7.639 +  let ?fps_X = "1 - (fps_X::'a fps)"
   7.640 +  have th0: "?fps_X $ 0 \<noteq> 0"
   7.641      by simp
   7.642 -  have "a /?X = ?X *  Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?X"
   7.643 -    using fps_divide_X_minus1_sum_lemma[of a, symmetric] th0
   7.644 +  have "a /?fps_X = ?fps_X *  Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?fps_X"
   7.645 +    using fps_divide_fps_X_minus1_sum_lemma[of a, symmetric] th0
   7.646      by (simp add: fps_divide_def mult.assoc)
   7.647 -  also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) "
   7.648 +  also have "\<dots> = (inverse ?fps_X * ?fps_X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) "
   7.649      by (simp add: ac_simps)
   7.650    finally show ?thesis
   7.651      by (simp add: inverse_mult_eq_1[OF th0])
   7.652 @@ -2495,10 +2495,10 @@
   7.653    also have "subdegree \<dots> = Suc m * subdegree g" by (rule subdegree_power)
   7.654    finally have [simp]: "subdegree f = subdegree g"
   7.655      by (subst (asm) Suc_mult_cancel1)
   7.656 -  have "fps_shift (subdegree f) f * X ^ subdegree f = f"
   7.657 +  have "fps_shift (subdegree f) f * fps_X ^ subdegree f = f"
   7.658      by (rule subdegree_decompose [symmetric])
   7.659    also have "\<dots> ^ Suc m = g ^ Suc m" by fact
   7.660 -  also have "g = fps_shift (subdegree g) g * X ^ subdegree g"
   7.661 +  also have "g = fps_shift (subdegree g) g * fps_X ^ subdegree g"
   7.662      by (rule subdegree_decompose)
   7.663    also have "subdegree f = subdegree g" by fact
   7.664    finally have "fps_shift (subdegree g) f ^ Suc m = fps_shift (subdegree g) g ^ Suc m"
   7.665 @@ -3127,17 +3127,17 @@
   7.666    then show ?thesis by (simp add: fps_eq_iff)
   7.667  qed
   7.668  
   7.669 -lemma fps_mult_X_plus_1_nth:
   7.670 -  "((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
   7.671 +lemma fps_mult_fps_X_plus_1_nth:
   7.672 +  "((1+fps_X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
   7.673  proof (cases n)
   7.674    case 0
   7.675    then show ?thesis
   7.676      by (simp add: fps_mult_nth)
   7.677  next
   7.678    case (Suc m)
   7.679 -  have "((1 + X)*a) $ n = sum (\<lambda>i. (1 + X) $ i * a $ (n - i)) {0..n}"
   7.680 +  have "((1 + fps_X)*a) $ n = sum (\<lambda>i. (1 + fps_X) $ i * a $ (n - i)) {0..n}"
   7.681      by (simp add: fps_mult_nth)
   7.682 -  also have "\<dots> = sum (\<lambda>i. (1+X)$i * a$(n-i)) {0.. 1}"
   7.683 +  also have "\<dots> = sum (\<lambda>i. (1+fps_X)$i * a$(n-i)) {0.. 1}"
   7.684      unfolding Suc by (rule sum.mono_neutral_right) auto
   7.685    also have "\<dots> = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
   7.686      by (simp add: Suc)
   7.687 @@ -3145,14 +3145,14 @@
   7.688  qed
   7.689  
   7.690  
   7.691 -subsection \<open>Finite FPS (i.e. polynomials) and X\<close>
   7.692 -
   7.693 -lemma fps_poly_sum_X:
   7.694 +subsection \<open>Finite FPS (i.e. polynomials) and fps_X\<close>
   7.695 +
   7.696 +lemma fps_poly_sum_fps_X:
   7.697    assumes "\<forall>i > n. a$i = (0::'a::comm_ring_1)"
   7.698 -  shows "a = sum (\<lambda>i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r")
   7.699 +  shows "a = sum (\<lambda>i. fps_const (a$i) * fps_X^i) {0..n}" (is "a = ?r")
   7.700  proof -
   7.701    have "a$i = ?r$i" for i
   7.702 -    unfolding fps_sum_nth fps_mult_left_const_nth X_power_nth
   7.703 +    unfolding fps_sum_nth fps_mult_left_const_nth fps_X_power_nth
   7.704      by (simp add: mult_delta_right sum.delta' assms)
   7.705    then show ?thesis
   7.706      unfolding fps_eq_iff by blast
   7.707 @@ -3163,23 +3163,23 @@
   7.708  
   7.709  fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
   7.710  where
   7.711 -  "compinv a 0 = X$0"
   7.712 +  "compinv a 0 = fps_X$0"
   7.713  | "compinv a (Suc n) =
   7.714 -    (X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
   7.715 +    (fps_X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
   7.716  
   7.717  definition "fps_inv a = Abs_fps (compinv a)"
   7.718  
   7.719  lemma fps_inv:
   7.720    assumes a0: "a$0 = 0"
   7.721      and a1: "a$1 \<noteq> 0"
   7.722 -  shows "fps_inv a oo a = X"
   7.723 +  shows "fps_inv a oo a = fps_X"
   7.724  proof -
   7.725    let ?i = "fps_inv a oo a"
   7.726 -  have "?i $n = X$n" for n
   7.727 +  have "?i $n = fps_X$n" for n
   7.728    proof (induct n rule: nat_less_induct)
   7.729      fix n
   7.730 -    assume h: "\<forall>m<n. ?i$m = X$m"
   7.731 -    show "?i $ n = X$n"
   7.732 +    assume h: "\<forall>m<n. ?i$m = fps_X$m"
   7.733 +    show "?i $ n = fps_X$n"
   7.734      proof (cases n)
   7.735        case 0
   7.736        then show ?thesis using a0
   7.737 @@ -3189,9 +3189,9 @@
   7.738        have "?i $ n = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
   7.739          by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
   7.740        also have "\<dots> = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
   7.741 -        (X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
   7.742 +        (fps_X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
   7.743          using a0 a1 Suc by (simp add: fps_inv_def)
   7.744 -      also have "\<dots> = X$n" using Suc by simp
   7.745 +      also have "\<dots> = fps_X$n" using Suc by simp
   7.746        finally show ?thesis .
   7.747      qed
   7.748    qed
   7.749 @@ -3238,7 +3238,7 @@
   7.750      by (simp add: fps_eq_iff)
   7.751  qed
   7.752  
   7.753 -lemma fps_inv_ginv: "fps_inv = fps_ginv X"
   7.754 +lemma fps_inv_ginv: "fps_inv = fps_ginv fps_X"
   7.755    apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
   7.756    apply (induct_tac n rule: nat_less_induct)
   7.757    apply auto
   7.758 @@ -3427,7 +3427,7 @@
   7.759  lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   7.760    using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
   7.761  
   7.762 -lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   7.763 +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)"
   7.764    by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta)
   7.765  
   7.766  lemma fps_inverse_compose:
   7.767 @@ -3463,16 +3463,16 @@
   7.768      (is "?one oo a = _")
   7.769  proof -
   7.770    have o0: "?one $ 0 \<noteq> 0" by simp
   7.771 -  have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp
   7.772 +  have th0: "(1 - fps_X) $ 0 \<noteq> (0::'a)" by simp
   7.773    from fps_inverse_gp[where ?'a = 'a]
   7.774 -  have "inverse ?one = 1 - X" by (simp add: fps_eq_iff)
   7.775 -  then have "inverse (inverse ?one) = inverse (1 - X)" by simp
   7.776 -  then have th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0]
   7.777 +  have "inverse ?one = 1 - fps_X" by (simp add: fps_eq_iff)
   7.778 +  then have "inverse (inverse ?one) = inverse (1 - fps_X)" by simp
   7.779 +  then have th: "?one = 1/(1 - fps_X)" unfolding fps_inverse_idempotent[OF o0]
   7.780      by (simp add: fps_divide_def)
   7.781    show ?thesis
   7.782      unfolding th
   7.783      unfolding fps_divide_compose[OF a0 th0]
   7.784 -    fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] ..
   7.785 +    fps_compose_1 fps_compose_sub_distrib fps_X_fps_compose_startby0[OF a0] ..
   7.786  qed
   7.787  
   7.788  lemma fps_const_power [simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
   7.789 @@ -3535,7 +3535,7 @@
   7.790  
   7.791  lemma fps_X_power_compose:
   7.792    assumes a0: "a$0=0"
   7.793 -  shows "X^k oo a = (a::'a::idom fps)^k"
   7.794 +  shows "fps_X^k oo a = (a::'a::idom fps)^k"
   7.795    (is "?l = ?r")
   7.796  proof (cases k)
   7.797    case 0
   7.798 @@ -3564,7 +3564,7 @@
   7.799  lemma fps_inv_right:
   7.800    assumes a0: "a$0 = 0"
   7.801      and a1: "a$1 \<noteq> 0"
   7.802 -  shows "a oo fps_inv a = X"
   7.803 +  shows "a oo fps_inv a = fps_X"
   7.804  proof -
   7.805    let ?ia = "fps_inv a"
   7.806    let ?iaa = "a oo fps_inv a"
   7.807 @@ -3572,12 +3572,12 @@
   7.808      by (simp add: fps_inv_def)
   7.809    have th1: "?iaa $ 0 = 0"
   7.810      using a0 a1 by (simp add: fps_inv_def fps_compose_nth)
   7.811 -  have th2: "X$0 = 0"
   7.812 +  have th2: "fps_X$0 = 0"
   7.813      by simp
   7.814 -  from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X"
   7.815 +  from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo fps_X"
   7.816      by simp
   7.817 -  then have "(a oo fps_inv a) oo a = X oo a"
   7.818 -    by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0])
   7.819 +  then have "(a oo fps_inv a) oo a = fps_X oo a"
   7.820 +    by (simp add: fps_compose_assoc[OF a0 th0] fps_X_fps_compose_startby0[OF a0])
   7.821    with fps_compose_inj_right[OF a0 a1] show ?thesis
   7.822      by simp
   7.823  qed
   7.824 @@ -3612,13 +3612,13 @@
   7.825      by (simp add: fps_inv_def)
   7.826    from a1 have ra1: "?r a $ 1 \<noteq> 0"
   7.827      by (simp add: fps_inv_def field_simps)
   7.828 -  have X0: "X$0 = 0"
   7.829 +  have fps_X0: "fps_X$0 = 0"
   7.830      by simp
   7.831 -  from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
   7.832 -  then have "?r (?r a) oo ?r a oo a = X oo a"
   7.833 +  from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = fps_X" .
   7.834 +  then have "?r (?r a) oo ?r a oo a = fps_X oo a"
   7.835      by simp
   7.836    then have "?r (?r a) oo (?r a oo a) = a"
   7.837 -    unfolding X_fps_compose_startby0[OF a0]
   7.838 +    unfolding fps_X_fps_compose_startby0[OF a0]
   7.839      unfolding fps_compose_assoc[OF a0 ra0, symmetric] .
   7.840    then show ?thesis
   7.841      unfolding fps_inv[OF a0 a1] by simp
   7.842 @@ -3661,13 +3661,13 @@
   7.843  lemma fps_ginv_deriv:
   7.844    assumes a0:"a$0 = (0::'a::field)"
   7.845      and a1: "a$1 \<noteq> 0"
   7.846 -  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
   7.847 +  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv fps_X a"
   7.848  proof -
   7.849    let ?ia = "fps_ginv b a"
   7.850 -  let ?iXa = "fps_ginv X a"
   7.851 +  let ?ifps_Xa = "fps_ginv fps_X a"
   7.852    let ?d = "fps_deriv"
   7.853    let ?dia = "?d ?ia"
   7.854 -  have iXa0: "?iXa $ 0 = 0"
   7.855 +  have ifps_Xa0: "?ifps_Xa $ 0 = 0"
   7.856      by (simp add: fps_ginv_def)
   7.857    have da0: "?d a $ 0 \<noteq> 0"
   7.858      using a1 by simp
   7.859 @@ -3679,21 +3679,21 @@
   7.860      by simp
   7.861    with a1 have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a"
   7.862      by (simp add: fps_divide_unit)
   7.863 -  then have "(?d ?ia oo a) oo ?iXa =  (?d b / ?d a) oo ?iXa"
   7.864 +  then have "(?d ?ia oo a) oo ?ifps_Xa =  (?d b / ?d a) oo ?ifps_Xa"
   7.865      unfolding inverse_mult_eq_1[OF da0] by simp
   7.866 -  then have "?d ?ia oo (a oo ?iXa) =  (?d b / ?d a) oo ?iXa"
   7.867 -    unfolding fps_compose_assoc[OF iXa0 a0] .
   7.868 +  then have "?d ?ia oo (a oo ?ifps_Xa) =  (?d b / ?d a) oo ?ifps_Xa"
   7.869 +    unfolding fps_compose_assoc[OF ifps_Xa0 a0] .
   7.870    then show ?thesis unfolding fps_inv_ginv[symmetric]
   7.871      unfolding fps_inv_right[OF a0 a1] by simp
   7.872  qed
   7.873  
   7.874  lemma fps_compose_linear:
   7.875 -  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
   7.876 +  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * fps_X) = Abs_fps (\<lambda>n. c^n * f $ n)"
   7.877    by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
   7.878                  if_distrib sum.delta' cong: if_cong)
   7.879                
   7.880  lemma fps_compose_uminus': 
   7.881 -  "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
   7.882 +  "fps_compose f (-fps_X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
   7.883    using fps_compose_linear[of f "-1"] 
   7.884    by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp
   7.885  
   7.886 @@ -3768,21 +3768,21 @@
   7.887    "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)"
   7.888    by (induct n) auto
   7.889  
   7.890 -lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1"
   7.891 -  by (simp add: fps_eq_iff X_fps_compose)
   7.892 +lemma fps_X_compose_fps_exp[simp]: "fps_X oo fps_exp (a::'a::field) = fps_exp a - 1"
   7.893 +  by (simp add: fps_eq_iff fps_X_fps_compose)
   7.894  
   7.895  lemma fps_inv_fps_exp_compose:
   7.896    assumes a: "a \<noteq> 0"
   7.897 -  shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X"
   7.898 -    and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X"
   7.899 +  shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X"
   7.900 +    and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X"
   7.901  proof -
   7.902    let ?b = "fps_exp a - 1"
   7.903    have b0: "?b $ 0 = 0"
   7.904      by simp
   7.905    have b1: "?b $ 1 \<noteq> 0"
   7.906      by (simp add: a)
   7.907 -  from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" .
   7.908 -  from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" .
   7.909 +  from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X" .
   7.910 +  from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X" .
   7.911  qed
   7.912  
   7.913  lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)"
   7.914 @@ -3804,11 +3804,11 @@
   7.915  qed
   7.916  
   7.917  lemma fps_exp_compose_linear [simp]: 
   7.918 -  "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)"
   7.919 +  "fps_exp (d::'a::field_char_0) oo (fps_const c * fps_X) = fps_exp (c * d)"
   7.920    by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib)
   7.921    
   7.922  lemma fps_fps_exp_compose_minus [simp]: 
   7.923 -  "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)"
   7.924 +  "fps_compose (fps_exp c) (-fps_X) = fps_exp (-c :: 'a :: field_char_0)"
   7.925    using fps_exp_compose_linear[of c "-1 :: 'a"] 
   7.926    unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp
   7.927  
   7.928 @@ -3844,14 +3844,14 @@
   7.929  
   7.930  lemma Abs_fps_if_0:
   7.931    "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) =
   7.932 -    fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
   7.933 +    fps_const v + fps_X * Abs_fps (\<lambda>n. f (Suc n))"
   7.934    by (auto simp add: fps_eq_iff)
   7.935  
   7.936  definition fps_ln :: "'a::field_char_0 \<Rightarrow> 'a fps"
   7.937    where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
   7.938  
   7.939 -lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)"
   7.940 -  unfolding fps_inverse_X_plus1
   7.941 +lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + fps_X)"
   7.942 +  unfolding fps_inverse_fps_X_plus1
   7.943    by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc)
   7.944  
   7.945  lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
   7.946 @@ -3870,13 +3870,13 @@
   7.947    have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) =
   7.948      (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)"
   7.949      by (simp add: field_simps)
   7.950 -  also have "\<dots> = fps_const a * (X + 1)"
   7.951 +  also have "\<dots> = fps_const a * (fps_X + 1)"
   7.952      apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
   7.953      apply (simp add: field_simps)
   7.954      done
   7.955 -  finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" .
   7.956 +  finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (fps_X + 1)" .
   7.957    from fps_inv_deriv[OF b0 b1, unfolded eq]
   7.958 -  have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
   7.959 +  have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (fps_X + 1)"
   7.960      using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
   7.961    then have "fps_deriv ?l = fps_deriv ?r"
   7.962      by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse)
   7.963 @@ -3891,7 +3891,7 @@
   7.964    (is "?r = ?l")
   7.965  proof-
   7.966    from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
   7.967 -  have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
   7.968 +  have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + fps_X)"
   7.969      by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add)
   7.970    also have "\<dots> = fps_deriv ?l"
   7.971      apply (simp add: fps_ln_deriv)
   7.972 @@ -3901,9 +3901,9 @@
   7.973      unfolding fps_deriv_eq_iff by simp
   7.974  qed
   7.975  
   7.976 -lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c"
   7.977 +lemma fps_X_dvd_fps_ln [simp]: "fps_X dvd fps_ln c"
   7.978  proof -
   7.979 -  have "fps_ln c = X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
   7.980 +  have "fps_ln c = fps_X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
   7.981      by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff)
   7.982    thus ?thesis by simp
   7.983  qed
   7.984 @@ -3918,11 +3918,11 @@
   7.985  
   7.986  lemma fps_binomial_ODE_unique:
   7.987    fixes c :: "'a::field_char_0"
   7.988 -  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   7.989 +  shows "fps_deriv a = (fps_const c * a) / (1 + fps_X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   7.990    (is "?lhs \<longleftrightarrow> ?rhs")
   7.991  proof
   7.992    let ?da = "fps_deriv a"
   7.993 -  let ?x1 = "(1 + X):: 'a fps"
   7.994 +  let ?x1 = "(1 + fps_X):: 'a fps"
   7.995    let ?l = "?x1 * ?da"
   7.996    let ?r = "fps_const c * a"
   7.997  
   7.998 @@ -3985,10 +3985,10 @@
   7.999  qed
  7.1000  
  7.1001  lemma fps_binomial_ODE_unique':
  7.1002 -  "(fps_deriv a = fps_const c * a / (1 + X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
  7.1003 +  "(fps_deriv a = fps_const c * a / (1 + fps_X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
  7.1004    by (subst fps_binomial_ODE_unique) auto
  7.1005  
  7.1006 -lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
  7.1007 +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + fps_X)"
  7.1008  proof -
  7.1009    let ?a = "fps_binomial c"
  7.1010    have th0: "?a = fps_const (?a$0) * ?a" by (simp)
  7.1011 @@ -4001,13 +4001,13 @@
  7.1012    let ?b = "fps_binomial"
  7.1013    let ?db = "\<lambda>x. fps_deriv (?b x)"
  7.1014    have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
  7.1015 -  also have "\<dots> = inverse (1 + X) *
  7.1016 +  also have "\<dots> = inverse (1 + fps_X) *
  7.1017        (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))"
  7.1018      unfolding fps_binomial_deriv
  7.1019      by (simp add: fps_divide_def field_simps)
  7.1020 -  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
  7.1021 +  also have "\<dots> = (fps_const (c + d)/ (1 + fps_X)) * ?P"
  7.1022      by (simp add: field_simps fps_divide_unit fps_const_add[symmetric] del: fps_const_add)
  7.1023 -  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
  7.1024 +  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + fps_X)"
  7.1025      by (simp add: fps_divide_def)
  7.1026    have "?P = fps_const (?P$0) * ?b (c + d)"
  7.1027      unfolding fps_binomial_ODE_unique[symmetric]
  7.1028 @@ -4016,35 +4016,35 @@
  7.1029    then show ?thesis by simp
  7.1030  qed
  7.1031  
  7.1032 -lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
  7.1033 +lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + fps_X)"
  7.1034    (is "?l = inverse ?r")
  7.1035  proof-
  7.1036    have th: "?r$0 \<noteq> 0" by simp
  7.1037 -  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
  7.1038 +  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + fps_X)"
  7.1039      by (simp add: fps_inverse_deriv[OF th] fps_divide_def
  7.1040        power2_eq_square mult.commute fps_const_neg[symmetric] del: fps_const_neg)
  7.1041    have eq: "inverse ?r $ 0 = 1"
  7.1042      by (simp add: fps_inverse_def)
  7.1043 -  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
  7.1044 +  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + fps_X)" "- 1"] th'] eq
  7.1045    show ?thesis by (simp add: fps_inverse_def)
  7.1046  qed
  7.1047  
  7.1048 -lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + X :: 'a :: field_char_0 fps) ^ n"
  7.1049 +lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + fps_X :: 'a :: field_char_0 fps) ^ n"
  7.1050  proof (cases "n = 0")
  7.1051    case [simp]: True
  7.1052 -  have "fps_deriv ((1 + X) ^ n :: 'a fps) = 0" by simp
  7.1053 -  also have "\<dots> = fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" by (simp add: fps_binomial_def)
  7.1054 +  have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = 0" by simp
  7.1055 +  also have "\<dots> = fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)" by (simp add: fps_binomial_def)
  7.1056    finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) simp_all
  7.1057  next
  7.1058    case False
  7.1059 -  have "fps_deriv ((1 + X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + X) ^ (n - 1)"
  7.1060 +  have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + fps_X) ^ (n - 1)"
  7.1061      by (simp add: fps_deriv_power)
  7.1062 -  also have "(1 + X :: 'a fps) $ 0 \<noteq> 0" by simp
  7.1063 -  hence "(1 + X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
  7.1064 -  with False have "(1 + X :: 'a fps) ^ (n - 1) = (1 + X) ^ n / (1 + X)"
  7.1065 +  also have "(1 + fps_X :: 'a fps) $ 0 \<noteq> 0" by simp
  7.1066 +  hence "(1 + fps_X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
  7.1067 +  with False have "(1 + fps_X :: 'a fps) ^ (n - 1) = (1 + fps_X) ^ n / (1 + fps_X)"
  7.1068      by (cases n) (simp_all )
  7.1069 -  also have "fps_const (of_nat n :: 'a) * ((1 + X) ^ n / (1 + X)) =
  7.1070 -               fps_const (of_nat n) * (1 + X) ^ n / (1 + X)"
  7.1071 +  also have "fps_const (of_nat n :: 'a) * ((1 + fps_X) ^ n / (1 + fps_X)) =
  7.1072 +               fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)"
  7.1073      by (simp add: unit_div_mult_swap)
  7.1074    finally show ?thesis
  7.1075      by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) (simp_all add: fps_power_nth)
  7.1076 @@ -4056,24 +4056,24 @@
  7.1077  lemma fps_binomial_power: "fps_binomial a ^ n = fps_binomial (of_nat n * a)"
  7.1078    by (induction n) (simp_all add: fps_binomial_add_mult ring_distribs)
  7.1079  
  7.1080 -lemma fps_binomial_1: "fps_binomial 1 = 1 + X"
  7.1081 +lemma fps_binomial_1: "fps_binomial 1 = 1 + fps_X"
  7.1082    using fps_binomial_of_nat[of 1] by simp
  7.1083  
  7.1084  lemma fps_binomial_minus_of_nat:
  7.1085 -  "fps_binomial (- of_nat n) = inverse ((1 + X :: 'a :: field_char_0 fps) ^ n)"
  7.1086 +  "fps_binomial (- of_nat n) = inverse ((1 + fps_X :: 'a :: field_char_0 fps) ^ n)"
  7.1087    by (rule sym, rule fps_inverse_unique)
  7.1088       (simp add: fps_binomial_of_nat [symmetric] fps_binomial_add_mult [symmetric])
  7.1089  
  7.1090 -lemma one_minus_const_X_power:
  7.1091 -  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * X) ^ n =
  7.1092 -     fps_compose (fps_binomial (of_nat n)) (-fps_const c * X)"
  7.1093 +lemma one_minus_const_fps_X_power:
  7.1094 +  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * fps_X) ^ n =
  7.1095 +     fps_compose (fps_binomial (of_nat n)) (-fps_const c * fps_X)"
  7.1096    by (subst fps_binomial_of_nat)
  7.1097       (simp add: fps_compose_power [symmetric] fps_compose_add_distrib fps_const_neg [symmetric] 
  7.1098             del: fps_const_neg)
  7.1099  
  7.1100 -lemma one_minus_X_const_neg_power:
  7.1101 -  "inverse ((1 - fps_const c * X) ^ n) = 
  7.1102 -       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * X)"
  7.1103 +lemma one_minus_fps_X_const_neg_power:
  7.1104 +  "inverse ((1 - fps_const c * fps_X) ^ n) = 
  7.1105 +       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * fps_X)"
  7.1106  proof (cases "c = 0")
  7.1107    case False
  7.1108    thus ?thesis
  7.1109 @@ -4082,17 +4082,17 @@
  7.1110                  fps_const_neg [symmetric] del: fps_const_neg)
  7.1111  qed simp
  7.1112  
  7.1113 -lemma X_plus_const_power:
  7.1114 -  "c \<noteq> 0 \<Longrightarrow> (X + fps_const c) ^ n =
  7.1115 -     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * X)"
  7.1116 +lemma fps_X_plus_const_power:
  7.1117 +  "c \<noteq> 0 \<Longrightarrow> (fps_X + fps_const c) ^ n =
  7.1118 +     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * fps_X)"
  7.1119    by (subst fps_binomial_of_nat)
  7.1120       (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
  7.1121                  fps_const_power [symmetric] power_mult_distrib [symmetric] 
  7.1122                  algebra_simps inverse_mult_eq_1' del: fps_const_power)
  7.1123  
  7.1124 -lemma X_plus_const_neg_power:
  7.1125 -  "c \<noteq> 0 \<Longrightarrow> inverse ((X + fps_const c) ^ n) =
  7.1126 -     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * X)"
  7.1127 +lemma fps_X_plus_const_neg_power:
  7.1128 +  "c \<noteq> 0 \<Longrightarrow> inverse ((fps_X + fps_const c) ^ n) =
  7.1129 +     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * fps_X)"
  7.1130    by (subst fps_binomial_minus_of_nat)
  7.1131       (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
  7.1132                  fps_const_power [symmetric] power_mult_distrib [symmetric] fps_inverse_compose 
  7.1133 @@ -4101,11 +4101,11 @@
  7.1134             del: fps_const_power)
  7.1135  
  7.1136  
  7.1137 -lemma one_minus_const_X_neg_power':
  7.1138 -  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * X) ^ n) =
  7.1139 +lemma one_minus_const_fps_X_neg_power':
  7.1140 +  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * fps_X) ^ n) =
  7.1141         Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
  7.1142    apply (rule fps_ext)
  7.1143 -  apply (subst one_minus_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
  7.1144 +  apply (subst one_minus_fps_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
  7.1145    apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] 
  7.1146                     gbinomial_minus binomial_gbinomial of_nat_diff)
  7.1147    done
  7.1148 @@ -4546,7 +4546,7 @@
  7.1149    by (simp add: fps_of_int [symmetric])
  7.1150  
  7.1151  lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
  7.1152 -  by (fact numeral_fps_const) (* FIXME: duplicate *)
  7.1153 +  by (fact numeral_fps_const) (* FIfps_XME: duplicate *)
  7.1154  
  7.1155  lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * c)) / fps_const 2"
  7.1156  proof -
  7.1157 @@ -4610,10 +4610,10 @@
  7.1158  lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c"
  7.1159    by (simp add: fps_eq_iff)
  7.1160  
  7.1161 -lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)"
  7.1162 +lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * fps_X)"
  7.1163  proof -
  7.1164 -  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
  7.1165 -  have th0: "(fps_const c * X) $ 0 = 0" by simp
  7.1166 +  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * fps_X)"
  7.1167 +  have th0: "(fps_const c * fps_X) $ 0 = 0" by simp
  7.1168    show ?thesis unfolding gp[OF th0, symmetric]
  7.1169      by (auto simp add: fps_eq_iff pochhammer_fact[symmetric]
  7.1170        fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong)
  7.1171 @@ -4645,26 +4645,26 @@
  7.1172    apply (simp add: algebra_simps)
  7.1173    done
  7.1174  
  7.1175 -lemma XD_nth[simp]: "XD a $ n = (if n = 0 then 0 else of_nat n * a$n)"
  7.1176 -  by (simp add: XD_def)
  7.1177 -
  7.1178 -lemma XD_0th[simp]: "XD a $ 0 = 0"
  7.1179 +lemma fps_XD_nth[simp]: "fps_XD a $ n = (if n = 0 then 0 else of_nat n * a$n)"
  7.1180 +  by (simp add: fps_XD_def)
  7.1181 +
  7.1182 +lemma fps_XD_0th[simp]: "fps_XD a $ 0 = 0"
  7.1183    by simp
  7.1184 -lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n"
  7.1185 +lemma fps_XD_Suc[simp]:" fps_XD a $ Suc n = of_nat (Suc n) * a $ Suc n"
  7.1186    by simp
  7.1187  
  7.1188 -definition "XDp c a = XD a + fps_const c * a"
  7.1189 -
  7.1190 -lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
  7.1191 -  by (simp add: XDp_def algebra_simps)
  7.1192 -
  7.1193 -lemma XDp_commute: "XDp b \<circ> XDp (c::'a::comm_ring_1) = XDp c \<circ> XDp b"
  7.1194 -  by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps)
  7.1195 -
  7.1196 -lemma XDp0 [simp]: "XDp 0 = XD"
  7.1197 +definition "fps_XDp c a = fps_XD a + fps_const c * a"
  7.1198 +
  7.1199 +lemma fps_XDp_nth[simp]: "fps_XDp c a $ n = (c + of_nat n) * a$n"
  7.1200 +  by (simp add: fps_XDp_def algebra_simps)
  7.1201 +
  7.1202 +lemma fps_XDp_commute: "fps_XDp b \<circ> fps_XDp (c::'a::comm_ring_1) = fps_XDp c \<circ> fps_XDp b"
  7.1203 +  by (auto simp add: fps_XDp_def fun_eq_iff fps_eq_iff algebra_simps)
  7.1204 +
  7.1205 +lemma fps_XDp0 [simp]: "fps_XDp 0 = fps_XD"
  7.1206    by (simp add: fun_eq_iff fps_eq_iff)
  7.1207  
  7.1208 -lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a"
  7.1209 +lemma fps_XDp_fps_integral [simp]: "fps_XDp 0 (fps_integral a c) = fps_X * a"
  7.1210    by (simp add: fps_eq_iff fps_integral_def)
  7.1211  
  7.1212  lemma fps_hypergeo_minus_nat:
  7.1213 @@ -4687,11 +4687,11 @@
  7.1214  lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
  7.1215    by (cases n) (simp_all add: pochhammer_rec)
  7.1216  
  7.1217 -lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c \<circ> r) cs (\<lambda>c. XDp c a) c0 $ n =
  7.1218 +lemma fps_XDp_foldr_nth [simp]: "foldr (\<lambda>c r. fps_XDp c \<circ> r) cs (\<lambda>c. fps_XDp c a) c0 $ n =
  7.1219      foldr (\<lambda>c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
  7.1220    by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
  7.1221  
  7.1222 -lemma genric_XDp_foldr_nth:
  7.1223 +lemma genric_fps_XDp_foldr_nth:
  7.1224    assumes f: "\<forall>n c a. f c a $ n = (of_nat n + k c) * a$n"
  7.1225    shows "foldr (\<lambda>c r. f c \<circ> r) cs (\<lambda>c. g c a) c0 $ n =
  7.1226      foldr (\<lambda>c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
  7.1227 @@ -4732,22 +4732,22 @@
  7.1228  
  7.1229  instance fps :: (comm_ring_1) complete_space
  7.1230  proof
  7.1231 -  fix X :: "nat \<Rightarrow> 'a fps"
  7.1232 -  assume "Cauchy X"
  7.1233 -  obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j"
  7.1234 +  fix fps_X :: "nat \<Rightarrow> 'a fps"
  7.1235 +  assume "Cauchy fps_X"
  7.1236 +  obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. fps_X (M i) $ j = fps_X m $ j"
  7.1237    proof -
  7.1238 -    have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" for i
  7.1239 +    have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. fps_X M $ j = fps_X m $ j" for i
  7.1240      proof -
  7.1241        have "0 < inverse ((2::real)^i)" by simp
  7.1242 -      from metric_CauchyD[OF \<open>Cauchy X\<close> this] dist_less_imp_nth_equal
  7.1243 +      from metric_CauchyD[OF \<open>Cauchy fps_X\<close> this] dist_less_imp_nth_equal
  7.1244        show ?thesis by blast
  7.1245      qed
  7.1246      then show ?thesis using that by metis
  7.1247    qed
  7.1248  
  7.1249 -  show "convergent X"
  7.1250 +  show "convergent fps_X"
  7.1251    proof (rule convergentI)
  7.1252 -    show "X \<longlonglongrightarrow> Abs_fps (\<lambda>i. X (M i) $ i)"
  7.1253 +    show "fps_X \<longlonglongrightarrow> Abs_fps (\<lambda>i. fps_X (M i) $ i)"
  7.1254        unfolding tendsto_iff
  7.1255      proof safe
  7.1256        fix e::real assume e: "0 < e"
  7.1257 @@ -4758,19 +4758,27 @@
  7.1258          by (auto simp: eventually_sequentially)
  7.1259        have "eventually (\<lambda>x. M i \<le> x) sequentially"
  7.1260          by (auto simp: eventually_sequentially)
  7.1261 -      then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially"
  7.1262 +      then show "eventually (\<lambda>x. dist (fps_X x) (Abs_fps (\<lambda>i. fps_X (M i) $ i)) < e) sequentially"
  7.1263        proof eventually_elim
  7.1264          fix x
  7.1265          assume x: "M i \<le> x"
  7.1266 -        have "X (M i) $ j = X (M j) $ j" if "j \<le> i" for j
  7.1267 +        have "fps_X (M i) $ j = fps_X (M j) $ j" if "j \<le> i" for j
  7.1268            using M that by (metis nat_le_linear)
  7.1269 -        with x have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)"
  7.1270 +        with x have "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < inverse (2 ^ i)"
  7.1271            using M by (force simp: dist_less_eq_nth_equal)
  7.1272          also note \<open>inverse (2 ^ i) < e\<close>
  7.1273 -        finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" .
  7.1274 +        finally show "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < e" .
  7.1275        qed
  7.1276      qed
  7.1277    qed
  7.1278  qed
  7.1279  
  7.1280 +(* TODO: Figure out better notation for this thing *)
  7.1281 +no_notation fps_nth (infixl "$" 75)
  7.1282 +
  7.1283 +bundle fps_notation
  7.1284 +begin
  7.1285 +notation fps_nth (infixl "$" 75)
  7.1286  end
  7.1287 +
  7.1288 +end
     8.1 --- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Aug 21 19:20:02 2017 +0200
     8.2 +++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Aug 21 20:49:15 2017 +0200
     8.3 @@ -8,6 +8,10 @@
     8.4    imports Polynomial Formal_Power_Series
     8.5  begin
     8.6  
     8.7 +context
     8.8 +  includes fps_notation
     8.9 +begin
    8.10 +
    8.11  definition fps_of_poly where
    8.12    "fps_of_poly p = Abs_fps (coeff p)"
    8.13  
    8.14 @@ -39,7 +43,7 @@
    8.15  lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n"
    8.16    by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)
    8.17  
    8.18 -lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X"
    8.19 +lemma fps_of_poly_fps_X [simp]: "fps_of_poly [:0, 1:] = fps_X"
    8.20    by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split)
    8.21  
    8.22  lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q"
    8.23 @@ -71,8 +75,8 @@
    8.24    by (induction xs) (simp_all add: fps_of_poly_mult)
    8.25  
    8.26  lemma fps_of_poly_pCons: 
    8.27 -  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X"
    8.28 -  by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
    8.29 +  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * fps_X"
    8.30 +  by (subst fps_mult_fps_X_commute [symmetric], intro fps_ext) 
    8.31       (auto simp: fps_of_poly_def coeff_pCons split: nat.split)
    8.32    
    8.33  lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)"
    8.34 @@ -81,10 +85,10 @@
    8.35  lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n"
    8.36    by (induction n) (simp_all add: fps_of_poly_mult)
    8.37    
    8.38 -lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
    8.39 +lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * fps_X ^ n"
    8.40    by (intro fps_ext) simp_all
    8.41  
    8.42 -lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
    8.43 +lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = fps_X ^ n"
    8.44    by (simp add: fps_of_poly_monom)
    8.45  
    8.46  lemma fps_of_poly_div:
    8.47 @@ -139,7 +143,7 @@
    8.48  
    8.49  
    8.50  lemmas fps_of_poly_simps =
    8.51 -  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
    8.52 +  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_fps_X
    8.53    fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
    8.54    fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
    8.55    fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
    8.56 @@ -153,7 +157,7 @@
    8.57                               fps_compose_add_distrib fps_compose_mult_distrib)
    8.58    
    8.59  lemmas reify_fps_atom =
    8.60 -  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X
    8.61 +  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_fps_X
    8.62  
    8.63  
    8.64  text \<open>
    8.65 @@ -163,7 +167,7 @@
    8.66    polynomial \<open>p\<close>.
    8.67    
    8.68    This may sound trivial, but it covers a number of annoying side conditions like 
    8.69 -  @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
    8.70 +  @{term "1 + fps_X \<noteq> 0"} that would otherwise not be solved automatically.
    8.71  \<close>
    8.72  
    8.73  ML \<open>
    8.74 @@ -208,7 +212,7 @@
    8.75      | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
    8.76          => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
    8.77               then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]})
    8.78 -    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
    8.79 +    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "fps_X"},_) $ _) => ct |> (
    8.80          rewr @{thms fps_of_poly_monom' [symmetric]}) 
    8.81      | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
    8.82          Conv.fun_conv (Conv.arg_conv reify_conv) 
    8.83 @@ -232,10 +236,10 @@
    8.84  
    8.85  simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close>
    8.86  
    8.87 -lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a"
    8.88 +lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = fps_X + fps_const a"
    8.89    by simp
    8.90  
    8.91 -lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
    8.92 +lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * fps_X"
    8.93    by simp
    8.94  
    8.95  lemma fps_of_poly_cutoff [simp]: 
    8.96 @@ -308,3 +312,5 @@
    8.97  qed (simp_all add: poly_subdegree_def prefix_length_def)
    8.98  
    8.99  end
   8.100 +
   8.101 +end