# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1503341355 -7200
# Node ID 4b8d1df8933b0b85cf643e579b312d839304cee1
# Parent  5c0a3f63057dc3bd8802dfbaf3b3aeea55241216
HOL-Analysis: Convergent FPS and infinite sums

diff -r 5c0a3f63057d -r 4b8d1df8933b CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Aug 21 19:20:02 2017 +0200
+++ b/CONTRIBUTORS	Mon Aug 21 20:49:15 2017 +0200
@@ -14,6 +14,11 @@
   Prover IDE improvements.
   Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
 
+* August 2017: Manuel Eberl, TUM
+  HOL-Analysis: infinite products over natural numbers,
+  infinite sums over arbitrary sets, connection between formal
+  power series and analytic complex functions
+
 * March 2017: Alasdair Armstrong, University of Sheffield and
   Simon Foster, University of York
   Fixed-point theory and Galois Connections in HOL-Algebra.
diff -r 5c0a3f63057d -r 4b8d1df8933b NEWS
--- a/NEWS	Mon Aug 21 19:20:02 2017 +0200
+++ b/NEWS	Mon Aug 21 20:49:15 2017 +0200
@@ -215,8 +215,8 @@
 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
 been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
 
-* Theory "HOL-Library.Formal_Power_Series": constants E/L/F have been
-renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
+* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
+renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
 space. INCOMPATIBILITY.
 
 * Theory "HOL-Library.FinFun" has been moved to AFP (again).
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Mon Aug 21 19:20:02 2017 +0200
+++ b/src/HOL/Analysis/Analysis.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -11,6 +11,7 @@
   Bounded_Continuous_Function
   Function_Topology
   Infinite_Products
+  Infinite_Set_Sum
   Weierstrass_Theorems
   Polytope
   Jordan_Curve
@@ -18,6 +19,7 @@
   Great_Picard
   Poly_Roots
   Conformal_Mappings
+  FPS_Convergence
   Generalised_Binomial_Theorem
   Gamma_Function
 begin
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 19:20:02 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -73,6 +73,10 @@
 lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
   by (simp add: field_differentiable_within_exp holomorphic_on_def)
 
+lemma holomorphic_on_exp' [holomorphic_intros]:
+  "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
+  using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
+
 subsection\<open>Euler and de Moivre formulas.\<close>
 
 text\<open>The sine series times @{term i}\<close>
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Analysis/FPS_Convergence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -0,0 +1,1277 @@
+(*  
+  Title:    HOL/Analysis/FPS_Convergence.thy
+  Author:   Manuel Eberl, TU München
+
+  Connection of formal power series and actual convergent power series on Banach spaces
+  (most notably the complex numbers).
+*)
+section \<open>Convergence of formal power series\<close>
+theory FPS_Convergence
+imports
+  Conformal_Mappings
+  Generalised_Binomial_Theorem
+  "HOL-Computational_Algebra.Formal_Power_Series"
+begin
+
+subsection \<open>Balls with extended real radius\<close>
+
+text \<open>
+  The following is a variant of @{const ball} that also allows an infinite radius.
+\<close>
+definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where
+  "eball z r = {z'. ereal (dist z z') < r}"
+
+lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r"
+  by (simp add: eball_def)
+
+lemma eball_ereal [simp]: "eball z (ereal r) = ball z r"
+  by auto
+
+lemma eball_inf [simp]: "eball z \<infinity> = UNIV"
+  by auto
+
+lemma eball_empty [simp]: "r \<le> 0 \<Longrightarrow> eball z r = {}"
+proof safe
+  fix x assume "r \<le> 0" "x \<in> eball z r"
+  hence "dist z x < r" by simp
+  also have "\<dots> \<le> ereal 0" using \<open>r \<le> 0\<close> by (simp add: zero_ereal_def)
+  finally show "x \<in> {}" by simp
+qed
+
+lemma eball_conv_UNION_balls:
+  "eball z r = (\<Union>r'\<in>{r'. ereal r' < r}. ball z r')"
+  by (cases r) (use dense gt_ex in force)+
+
+lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'"
+  by auto
+
+lemma ball_eball_mono: "ereal r \<le> r' \<Longrightarrow> ball z r \<le> eball z r'"
+  using eball_mono[of "ereal r" r'] by simp
+
+lemma open_eball [simp, intro]: "open (eball z r)" 
+  by (cases r) auto
+
+
+subsection \<open>Basic properties of convergent power series\<close>
+
+definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
+  "fps_conv_radius f = conv_radius (fps_nth f)"
+
+definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
+
+definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
+  "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
+
+lemma norm_summable_fps:
+  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
+  shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fps_nth f n * z ^ n))"
+  by (rule abs_summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
+
+lemma summable_fps:
+  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
+  shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
+  by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
+
+lemma sums_eval_fps:
+  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
+  assumes "norm z < fps_conv_radius f"
+  shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
+  using assms unfolding eval_fps_def fps_conv_radius_def
+  by (intro summable_sums summable_in_conv_radius) simp_all
+
+lemma
+  fixes r :: ereal
+  assumes "f holomorphic_on eball z0 r"
+  shows   conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r"
+    and   eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z"
+    and   eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)"
+proof -
+  have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
+    if "z \<in> ball z0 r'" "ereal r' < r" for z r'
+  proof -
+    from that(2) have "ereal r' \<le> r" by simp
+    from assms(1) and this have "f holomorphic_on ball z0 r'"
+      by (rule holomorphic_on_subset[OF _ ball_eball_mono])
+    from holomorphic_power_series [OF this that(1)] 
+      show ?thesis by (simp add: fps_expansion_def)
+  qed
+  hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
+    if "z \<in> eball z0 r" for z
+    using that by (subst (asm) eball_conv_UNION_balls) blast
+  show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def
+  proof (rule conv_radius_geI_ex)
+    fix r' :: real assume r': "r' > 0" "ereal r' < r"
+    thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)"
+      using *[of "z0 + of_real r'"]
+      by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm)
+  qed
+  show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z
+    using *[OF that] by (simp add: eval_fps_def sums_iff)
+  show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z
+    using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm)
+qed
+
+lemma continuous_on_eval_fps:
+  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
+  shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)"
+proof (subst continuous_on_eq_continuous_at [OF open_eball], safe)
+  fix x :: 'a assume x: "x \<in> eball 0 (fps_conv_radius f)"
+  define r where "r = (if fps_conv_radius f = \<infinity> then norm x + 1 else
+                        (norm x + real_of_ereal (fps_conv_radius f)) / 2)"
+  have r: "norm x < r \<and> ereal r < fps_conv_radius f"
+    using x by (cases "fps_conv_radius f") 
+               (auto simp: r_def eball_def split: if_splits)
+
+  have "continuous_on (cball 0 r) (\<lambda>x. \<Sum>i. fps_nth f i * (x - 0) ^ i)"
+    by (rule powser_continuous_suminf) (insert r, auto simp: fps_conv_radius_def)
+  hence "continuous_on (cball 0 r) (eval_fps f)"
+    by (simp add: eval_fps_def)
+  thus "isCont (eval_fps f) x"
+    by (rule continuous_on_interior) (use r in auto)
+qed
+
+lemma continuous_on_eval_fps' [continuous_intros]:
+  assumes "continuous_on A g"
+  assumes "g ` A \<subseteq> eball 0 (fps_conv_radius f)"
+  shows   "continuous_on A (\<lambda>x. eval_fps f (g x))"
+  using continuous_on_compose2[OF continuous_on_eval_fps assms] .
+
+lemma has_field_derivative_powser:
+  fixes z :: "'a :: {banach, real_normed_field}"
+  assumes "ereal (norm z) < conv_radius f"
+  shows   "((\<lambda>z. \<Sum>n. f n * z ^ n) has_field_derivative (\<Sum>n. diffs f n * z ^ n)) (at z within A)"
+proof -
+  define K where "K = (if conv_radius f = \<infinity> then norm z + 1 
+                         else (norm z + real_of_ereal (conv_radius f)) / 2)"
+  have K: "norm z < K \<and> ereal K < conv_radius f"
+    using assms by (cases "conv_radius f") (auto simp: K_def)
+  have "0 \<le> norm z" by simp
+  also from K have "\<dots> < K" by simp
+  finally have K_pos: "K > 0" by simp
+
+  have "summable (\<lambda>n. f n * of_real K ^ n)"
+    using K and K_pos by (intro summable_in_conv_radius) auto
+  moreover from K and K_pos have "norm z < norm (of_real K :: 'a)" by auto
+  ultimately show ?thesis
+    by (rule has_field_derivative_at_within [OF termdiffs_strong])
+qed
+
+lemma has_field_derivative_eval_fps:
+  fixes z :: "'a :: {banach, real_normed_field}"
+  assumes "norm z < fps_conv_radius f"
+  shows   "(eval_fps f has_field_derivative eval_fps (fps_deriv f) z) (at z within A)"
+proof -
+  have "(eval_fps f has_field_derivative eval_fps (Abs_fps (diffs (fps_nth f))) z) (at z within A)"
+    using assms unfolding eval_fps_def fps_nth_Abs_fps fps_conv_radius_def
+    by (intro has_field_derivative_powser) auto
+  also have "Abs_fps (diffs (fps_nth f)) = fps_deriv f"
+    by (simp add: fps_eq_iff diffs_def)
+  finally show ?thesis .
+qed
+
+lemma holomorphic_on_eval_fps [holomorphic_intros]:
+  fixes z :: "'a :: {banach, real_normed_field}"
+  assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
+  shows   "eval_fps f holomorphic_on A"
+proof (rule holomorphic_on_subset [OF _ assms])
+  show "eval_fps f holomorphic_on eball 0 (fps_conv_radius f)"
+  proof (subst holomorphic_on_open [OF open_eball], safe, goal_cases)
+    case (1 x)
+    thus ?case
+      by (intro exI[of _ "eval_fps (fps_deriv f) x"]) (auto intro: has_field_derivative_eval_fps)
+  qed
+qed
+
+lemma analytic_on_eval_fps:
+  fixes z :: "'a :: {banach, real_normed_field}"
+  assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
+  shows   "eval_fps f analytic_on A"
+proof (rule analytic_on_subset [OF _ assms])
+  show "eval_fps f analytic_on eball 0 (fps_conv_radius f)"
+    using holomorphic_on_eval_fps[of "eball 0 (fps_conv_radius f)"] 
+    by (subst analytic_on_open) auto
+qed
+
+
+subsection \<open>Lower bounds on radius of convergence\<close>
+
+lemma fps_conv_radius_deriv:
+  fixes f :: "'a :: {banach, real_normed_field} fps"
+  shows "fps_conv_radius (fps_deriv f) \<ge> fps_conv_radius f"
+  unfolding fps_conv_radius_def
+proof (rule conv_radius_geI_ex)
+  fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)"
+  define K where "K = (if conv_radius (fps_nth f) = \<infinity> then r + 1 
+                         else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)"
+  have K: "r < K \<and> ereal K < conv_radius (fps_nth f)"
+    using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def)
+  have "summable (\<lambda>n. diffs (fps_nth f) n * of_real r ^ n)"
+  proof (rule termdiff_converges)
+    fix x :: 'a assume "norm x < K"
+    hence "ereal (norm x) < ereal K" by simp
+    also have "\<dots> < conv_radius (fps_nth f)" using K by simp
+    finally show "summable (\<lambda>n. fps_nth f n * x ^ n)"
+      by (intro summable_in_conv_radius) auto
+  qed (insert K r, auto)
+  also have "\<dots> = (\<lambda>n. fps_nth (fps_deriv f) n * of_real r ^ n)"
+    by (simp add: fps_deriv_def diffs_def)
+  finally show "\<exists>z::'a. norm z = r \<and> summable (\<lambda>n. fps_nth (fps_deriv f) n * z ^ n)"
+    using r by (intro exI[of _ "of_real r"]) auto
+qed
+
+lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"
+  by (simp add: eval_fps_def)
+
+lemma fps_conv_radius_norm [simp]: 
+  "fps_conv_radius (Abs_fps (\<lambda>n. norm (fps_nth f n))) = fps_conv_radius f"
+  by (simp add: fps_conv_radius_def)
+
+lemma fps_conv_radius_const [simp]: "fps_conv_radius (fps_const c) = \<infinity>"
+proof -
+  have "fps_conv_radius (fps_const c) = conv_radius (\<lambda>_. 0 :: 'a)"
+    unfolding fps_conv_radius_def
+    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto
+  thus ?thesis by simp
+qed
+
+lemma fps_conv_radius_0 [simp]: "fps_conv_radius 0 = \<infinity>"
+  by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const)
+
+lemma fps_conv_radius_1 [simp]: "fps_conv_radius 1 = \<infinity>"
+  by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const)
+
+lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>"
+  by (simp add: numeral_fps_const)
+
+lemma fps_conv_radius_fps_X_power [simp]: "fps_conv_radius (fps_X ^ n) = \<infinity>"
+proof -
+  have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (\<lambda>_. 0 :: 'a)"
+    unfolding fps_conv_radius_def 
+    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of n]]) 
+       (auto simp: fps_X_power_iff)
+  thus ?thesis by simp
+qed
+
+lemma fps_conv_radius_fps_X [simp]: "fps_conv_radius fps_X = \<infinity>"
+  using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right)
+
+lemma fps_conv_radius_shift [simp]:
+  "fps_conv_radius (fps_shift n f) = fps_conv_radius f"
+  by (simp add: fps_conv_radius_def fps_shift_def conv_radius_shift)
+
+lemma fps_conv_radius_cmult_left:
+  "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (fps_const c * f) = fps_conv_radius f"
+  unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_left)
+
+lemma fps_conv_radius_cmult_right:
+  "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (f * fps_const c) = fps_conv_radius f"
+  unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_right)
+
+lemma fps_conv_radius_uminus [simp]:
+  "fps_conv_radius (-f) = fps_conv_radius f"
+  using fps_conv_radius_cmult_left[of "-1" f]
+  by (simp add: fps_const_neg [symmetric] del: fps_const_neg)
+
+lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
+  unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
+  by simp
+
+lemma fps_conv_radius_diff: "fps_conv_radius (f - g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
+  using fps_conv_radius_add[of f "-g"] by simp
+
+lemma fps_conv_radius_mult: "fps_conv_radius (f * g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
+  using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"]
+  by (simp add: fps_mult_nth fps_conv_radius_def atLeast0AtMost)
+
+lemma fps_conv_radius_power: "fps_conv_radius (f ^ n) \<ge> fps_conv_radius f"
+proof (induction n)
+  case (Suc n)
+  hence "fps_conv_radius f \<le> min (fps_conv_radius f) (fps_conv_radius (f ^ n))"
+    by simp
+  also have "\<dots> \<le> fps_conv_radius (f * f ^ n)" 
+    by (rule fps_conv_radius_mult)
+  finally show ?case by simp
+qed simp_all
+
+context
+begin
+
+lemma natfun_inverse_bound:
+  fixes f :: "'a :: {real_normed_field} fps"
+  assumes "fps_nth f 0 = 1" and "\<delta> > 0" 
+      and summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
+      and le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
+  shows   "norm (natfun_inverse f n) \<le> inverse (\<delta> ^ n)"
+proof (induction n rule: less_induct)
+  case (less m)
+  show ?case
+  proof (cases m)
+    case 0
+    thus ?thesis using assms by (simp add: divide_simps norm_inverse norm_divide)
+  next
+    case [simp]: (Suc n)
+    have "norm (natfun_inverse f (Suc n)) = 
+            norm (\<Sum>i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))"
+      (is "_ = norm ?S") using assms 
+      by (simp add: field_simps norm_mult norm_divide del: sum_cl_ivl_Suc)
+    also have "norm ?S \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))"
+      by (rule norm_sum)
+    also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (Suc n - i))"
+    proof (intro sum_mono, goal_cases)
+      case (1 i)
+      have "norm (fps_nth f i * natfun_inverse f (Suc n - i)) =
+              norm (fps_nth f i) * norm (natfun_inverse f (Suc n - i))"
+        by (simp add: norm_mult)
+      also have "\<dots> \<le> norm (fps_nth f i) * inverse (\<delta> ^ (Suc n - i))"
+        using 1 by (intro mult_left_mono less.IH) auto
+      also have "\<dots> = norm (fps_nth f i) / \<delta> ^ (Suc n - i)"
+        by (simp add: divide_simps)
+      finally show ?case .
+    qed
+    also have "\<dots> = (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) / \<delta> ^ Suc n"
+      by (subst sum_divide_distrib, rule sum.cong)
+         (insert \<open>\<delta> > 0\<close>, auto simp: field_simps power_diff)
+    also have "(\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) =
+                 (\<Sum>i=0..n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i))"
+      by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all
+    also have "{0..n} = {..<Suc n}" by auto
+    also have "(\<Sum>i< Suc n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i)) \<le> 
+                 (\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ (Suc n))"
+      using \<open>\<delta> > 0\<close> by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto
+    also have "\<dots> \<le> 1" by fact
+    finally show ?thesis using \<open>\<delta> > 0\<close> 
+      by (simp add: divide_right_mono divide_simps)
+  qed
+qed
+
+private lemma fps_conv_radius_inverse_pos_aux:
+  fixes f :: "'a :: {banach, real_normed_field} fps"
+  assumes "fps_nth f 0 = 1" "fps_conv_radius f > 0"
+  shows   "fps_conv_radius (inverse f) > 0"
+proof -
+  let ?R = "fps_conv_radius f"
+  define h where "h = Abs_fps (\<lambda>n. norm (fps_nth f n))"
+  have [simp]: "fps_conv_radius h = ?R" by (simp add: h_def)
+  have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)"
+    by (intro continuous_on_eval_fps)
+  hence *: "open (eval_fps h -` A \<inter> eball 0 ?R)" if "open A" for A
+    using that by (subst (asm) continuous_on_open_vimage) auto
+  have "open (eval_fps h -` {..<2} \<inter> eball 0 ?R)"
+    by (rule *) auto
+  moreover have "0 \<in> eval_fps h -` {..<2} \<inter> eball 0 ?R"
+    using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def)
+  ultimately obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "ball 0 \<epsilon> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R"
+    by (subst (asm) open_contains_ball_eq) blast+
+
+  define \<delta> where "\<delta> = real_of_ereal (min (ereal \<epsilon> / 2) (?R / 2))"
+  have \<delta>: "0 < \<delta> \<and> \<delta> < \<epsilon> \<and> ereal \<delta> < ?R"
+    using \<open>\<epsilon> > 0\<close> and assms by (cases ?R) (auto simp: \<delta>_def min_def)
+
+  have summable: "summable (\<lambda>n. norm (fps_nth f n) * \<delta> ^ n)"
+    using \<delta> by (intro summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
+  hence "(\<lambda>n. norm (fps_nth f n) * \<delta> ^ n) sums eval_fps h \<delta>"
+    by (simp add: eval_fps_def summable_sums h_def)
+  hence "(\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) sums (eval_fps h \<delta> - 1)"
+    by (subst sums_Suc_iff) (auto simp: assms)
+  moreover {
+    from \<delta> have "\<delta> \<in> ball 0 \<epsilon>" by auto
+    also have "\<dots> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" by fact
+    finally have "eval_fps h \<delta> < 2" by simp
+  }
+  ultimately have le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
+    by (simp add: sums_iff)
+  from summable have summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
+    by (subst summable_Suc_iff)
+
+  have "0 < \<delta>" using \<delta> by blast
+  also have "\<delta> = inverse (limsup (\<lambda>n. ereal (inverse \<delta>)))"
+    using \<delta> by (subst Limsup_const) auto
+  also have "\<dots> \<le> conv_radius (natfun_inverse f)"
+    unfolding conv_radius_def
+  proof (intro ereal_inverse_antimono Limsup_mono
+           eventually_mono[OF eventually_gt_at_top[of 0]])
+    fix n :: nat assume n: "n > 0"
+    have "root n (norm (natfun_inverse f n)) \<le> root n (inverse (\<delta> ^ n))"
+      using n assms \<delta> le summable 
+      by (intro real_root_le_mono natfun_inverse_bound) auto
+    also have "\<dots> = inverse \<delta>"
+      using n \<delta> by (simp add: power_inverse [symmetric] real_root_pos2)
+    finally show "ereal (inverse \<delta>) \<ge> ereal (root n (norm (natfun_inverse f n)))" 
+      by (subst ereal_less_eq)
+  next
+    have "0 = limsup (\<lambda>n. 0::ereal)" 
+      by (rule Limsup_const [symmetric]) auto
+    also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (natfun_inverse f n))))"
+      by (intro Limsup_mono) (auto simp: real_root_ge_zero)
+    finally show "0 \<le> \<dots>" by simp
+  qed
+  also have "\<dots> = fps_conv_radius (inverse f)"
+    using assms by (simp add: fps_conv_radius_def fps_inverse_def)
+  finally show ?thesis by (simp add: zero_ereal_def)
+qed
+
+lemma fps_conv_radius_inverse_pos:
+  fixes f :: "'a :: {banach, real_normed_field} fps"
+  assumes "fps_nth f 0 \<noteq> 0" and "fps_conv_radius f > 0"
+  shows   "fps_conv_radius (inverse f) > 0"
+proof -
+  let ?c = "fps_nth f 0"
+  have "fps_conv_radius (inverse f) = fps_conv_radius (fps_const ?c * inverse f)"
+    using assms by (subst fps_conv_radius_cmult_left) auto
+  also have "fps_const ?c * inverse f = inverse (fps_const (inverse ?c) * f)"
+    using assms by (simp add: fps_inverse_mult fps_const_inverse)
+  also have "fps_conv_radius \<dots> > 0" using assms
+    by (intro fps_conv_radius_inverse_pos_aux)
+       (auto simp: fps_conv_radius_cmult_left)
+  finally show ?thesis .
+qed
+
+end
+
+lemma fps_conv_radius_exp [simp]: 
+  fixes c :: "'a :: {banach, real_normed_field}"
+  shows "fps_conv_radius (fps_exp c) = \<infinity>"
+  unfolding fps_conv_radius_def
+proof (rule conv_radius_inftyI'')
+  fix z :: 'a
+  have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))"
+    by (rule exp_converges)
+  also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))"
+    by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib)
+  finally have "summable \<dots>" by (simp add: sums_iff)
+  thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)"
+    by (rule summable_norm_cancel)
+qed
+
+
+subsection \<open>Evaluating power series\<close>
+
+lemma eval_fps_deriv:
+  assumes "norm z < fps_conv_radius f"
+  shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
+  by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
+
+lemma fps_nth_conv_deriv:
+  fixes f :: "complex fps"
+  assumes "fps_conv_radius f > 0"
+  shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
+  using assms
+proof (induction n arbitrary: f)
+  case 0
+  thus ?case by (simp add: eval_fps_def)
+next
+  case (Suc n f)
+  have "(deriv ^^ Suc n) (eval_fps f) 0 = (deriv ^^ n) (deriv (eval_fps f)) 0"
+    unfolding funpow_Suc_right o_def ..
+  also have "eventually (\<lambda>z::complex. z \<in> eball 0 (fps_conv_radius f)) (nhds 0)"
+    using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
+  hence "eventually (\<lambda>z. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)"
+    by eventually_elim (simp add: eval_fps_deriv)
+  hence "(deriv ^^ n) (deriv (eval_fps f)) 0 = (deriv ^^ n) (eval_fps (fps_deriv f)) 0"
+    by (intro higher_deriv_cong_ev refl)
+  also have "\<dots> / fact n = fps_nth (fps_deriv f) n"
+    using Suc.prems fps_conv_radius_deriv[of f] 
+    by (intro Suc.IH [symmetric]) auto
+  also have "\<dots> / of_nat (Suc n) = fps_nth f (Suc n)"
+    by (simp add: fps_deriv_def del: of_nat_Suc)
+  finally show ?case by (simp add: divide_simps)
+qed
+
+lemma eval_fps_eqD:
+  fixes f g :: "complex fps"
+  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
+  assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
+  shows   "f = g"
+proof (rule fps_ext)
+  fix n :: nat
+  have "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
+    using assms by (intro fps_nth_conv_deriv)
+  also have "(deriv ^^ n) (eval_fps f) 0 = (deriv ^^ n) (eval_fps g) 0"
+    by (intro higher_deriv_cong_ev refl assms)
+  also have "\<dots> / fact n = fps_nth g n"
+    using assms by (intro fps_nth_conv_deriv [symmetric])
+  finally show "fps_nth f n = fps_nth g n" .
+qed
+
+lemma eval_fps_const [simp]: 
+  fixes c :: "'a :: {banach, real_normed_div_algebra}"
+  shows "eval_fps (fps_const c) z = c"
+proof -
+  have "(\<lambda>n::nat. if n \<in> {0} then c else 0) sums (\<Sum>n\<in>{0::nat}. c)"
+    by (rule sums_If_finite_set) auto
+  also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_const c) n * z ^ n) sums (\<Sum>n\<in>{0::nat}. c)"
+    by (intro sums_cong) auto
+  also have "(\<Sum>n\<in>{0::nat}. c) = c" 
+    by simp
+  finally show ?thesis
+    by (simp add: eval_fps_def sums_iff)
+qed
+
+lemma eval_fps_0 [simp]:
+  "eval_fps (0 :: 'a :: {banach, real_normed_div_algebra} fps) z = 0"
+  by (simp only: fps_const_0_eq_0 [symmetric] eval_fps_const)
+
+lemma eval_fps_1 [simp]:
+  "eval_fps (1 :: 'a :: {banach, real_normed_div_algebra} fps) z = 1"
+  by (simp only: fps_const_1_eq_1 [symmetric] eval_fps_const)
+
+lemma eval_fps_numeral [simp]:
+  "eval_fps (numeral n :: 'a :: {banach, real_normed_div_algebra} fps) z = numeral n"
+  by (simp only: numeral_fps_const eval_fps_const)
+
+lemma eval_fps_X_power [simp]:
+  "eval_fps (fps_X ^ m :: 'a :: {banach, real_normed_div_algebra} fps) z = z ^ m"
+proof -
+  have "(\<lambda>n::nat. if n \<in> {m} then z ^ n else 0 :: 'a) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
+    by (rule sums_If_finite_set) auto
+  also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
+    by (intro sums_cong) (auto simp: fps_X_power_iff)
+  also have "(\<Sum>n\<in>{m::nat}. z ^ n) = z ^ m"
+    by simp
+  finally show ?thesis
+    by (simp add: eval_fps_def sums_iff)
+qed
+
+lemma eval_fps_X [simp]:
+  "eval_fps (fps_X :: 'a :: {banach, real_normed_div_algebra} fps) z = z"
+  using eval_fps_X_power[of 1 z] by (simp only: power_one_right)
+
+lemma eval_fps_minus:
+  fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
+  assumes "norm z < fps_conv_radius f"
+  shows   "eval_fps (-f) z = -eval_fps f z"
+  using assms unfolding eval_fps_def
+  by (subst suminf_minus [symmetric]) (auto intro!: summable_fps)
+
+lemma eval_fps_add:
+  fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
+  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
+  shows   "eval_fps (f + g) z = eval_fps f z + eval_fps g z"
+  using assms unfolding eval_fps_def
+  by (subst suminf_add) (auto simp: ring_distribs intro!: summable_fps)
+
+lemma eval_fps_diff:
+  fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
+  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
+  shows   "eval_fps (f - g) z = eval_fps f z - eval_fps g z"
+  using assms unfolding eval_fps_def
+  by (subst suminf_diff) (auto simp: ring_distribs intro!: summable_fps)
+
+lemma eval_fps_mult:
+  fixes f g :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+  assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
+  shows   "eval_fps (f * g) z = eval_fps f z * eval_fps g z"
+proof -
+  have "eval_fps f z * eval_fps g z = 
+          (\<Sum>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i)))"
+    unfolding eval_fps_def
+  proof (subst Cauchy_product)
+    show "summable (\<lambda>k. norm (fps_nth f k * z ^ k))" "summable (\<lambda>k. norm (fps_nth g k * z ^ k))"
+      by (rule norm_summable_fps assms)+
+  qed (simp_all add: algebra_simps)
+  also have "(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) =
+               (\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * z ^ k)"
+    by (intro ext sum.cong refl) (simp add: power_add [symmetric])
+  also have "suminf \<dots> = eval_fps (f * g) z"
+    by (simp add: eval_fps_def fps_mult_nth atLeast0AtMost sum_distrib_right)
+  finally show ?thesis ..
+qed
+
+lemma eval_fps_shift:
+  fixes f :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+  assumes "n \<le> subdegree f" "norm z < fps_conv_radius f"
+  shows   "eval_fps (fps_shift n f) z = (if z = 0 then fps_nth f n else eval_fps f z / z ^ n)"
+proof (cases "z = 0")
+  case False
+  have "eval_fps (fps_shift n f * fps_X ^ n) z = eval_fps (fps_shift n f) z * z ^ n"
+    using assms by (subst eval_fps_mult) simp_all
+  also from assms have "fps_shift n f * fps_X ^ n = f"
+    by (simp add: fps_shift_times_fps_X_power)
+  finally show ?thesis using False by (simp add: field_simps)
+qed (simp_all add: eval_fps_at_0)
+
+lemma eval_fps_exp [simp]:
+  fixes c :: "'a :: {banach, real_normed_field}"
+  shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def
+  by (simp add: eval_fps_def exp_def scaleR_conv_of_real divide_simps power_mult_distrib)
+
+lemma
+  fixes f :: "complex fps" and r :: ereal
+  assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0"
+  shows   fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)"
+    and   eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow> 
+                               eval_fps (inverse f) z = inverse (eval_fps f z)"
+proof -
+  define R where "R = min (fps_conv_radius f) r"
+  have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and> 
+          (\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))"
+  proof (cases "min r (fps_conv_radius f) > 0")
+    case True
+    define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0"
+    have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))"
+      using assms by (intro holomorphic_intros) auto
+    from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)"
+      unfolding f'_def by (rule conv_radius_fps_expansion)
+    have eval_f': "eval_fps f' z = inverse (eval_fps f z)" 
+      if "norm z < fps_conv_radius f" "norm z < r" for z
+      using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto
+  
+    have "f * f' = 1"
+    proof (rule eval_fps_eqD)
+      from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')"
+        by (auto simp: min_def split: if_splits)
+      also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult)
+      finally show "\<dots> > 0" .
+    next
+      from True have "R > 0" by (auto simp: R_def)
+      hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)"
+        by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
+      thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)"
+      proof eventually_elim
+        case (elim z)
+        hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z"
+          using radius by (intro eval_fps_mult) 
+                          (auto simp: R_def min_def split: if_splits intro: less_trans)
+        also have "eval_fps f' z = inverse (eval_fps f z)"
+          using elim by (intro eval_f') (auto simp: R_def)
+        also from elim have "eval_fps f z \<noteq> 0"
+          by (intro assms) (auto simp: R_def)
+        hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z" 
+          by simp
+        finally show "eval_fps (f * f') z = eval_fps 1 z" .
+      qed
+    qed simp_all
+    hence "f' = inverse f"
+      by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac)
+    with eval_f' and radius show ?thesis by simp
+  next
+    case False
+    hence *: "eball 0 R = {}" 
+      by (intro eball_empty) (auto simp: R_def min_def split: if_splits)
+    show ?thesis
+    proof safe
+      from False have "min r (fps_conv_radius f) \<le> 0"
+        by (simp add: min_def)
+      also have "0 \<le> fps_conv_radius (inverse f)"
+        by (simp add: fps_conv_radius_def conv_radius_nonneg)
+      finally show "min r (fps_conv_radius f) \<le> \<dots>" .
+    qed (unfold * [unfolded R_def], auto)
+  qed
+
+  from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast
+  from * show "eval_fps (inverse f) z = inverse (eval_fps f z)" 
+    if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z
+    using that by auto
+qed
+
+lemma
+  fixes f g :: "complex fps" and r :: ereal
+  defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
+  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
+  assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0"
+  shows   fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R"
+    and   eval_fps_divide':
+            "ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z"
+proof -
+  from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0" 
+    by (auto simp: eval_fps_at_0 zero_ereal_def)
+  have "R \<le> min r (fps_conv_radius g)"
+    by (auto simp: R_def intro: min.coboundedI2)
+  also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)"
+    by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def)
+  finally have radius: "fps_conv_radius (inverse g) \<ge> R" .
+  have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))"
+    by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
+  also have "\<dots> \<le> fps_conv_radius (f * inverse g)"
+    by (rule fps_conv_radius_mult)
+  also have "f * inverse g = f / g"
+    by (intro fps_divide_unit [symmetric] nz')
+  finally show "fps_conv_radius (f / g) \<ge> R" .
+
+  assume z: "ereal (norm z) < R"
+  have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z"
+    using radius by (intro eval_fps_mult less_le_trans[OF z])
+                    (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
+  also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close>
+    by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz)
+       (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
+  also have "f * inverse g = f / g" by fact
+  finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps)
+qed
+
+lemma
+  fixes f g :: "complex fps" and r :: ereal
+  defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
+  assumes "subdegree g \<le> subdegree f"
+  assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
+  assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0"
+  shows   fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R"
+    and   eval_fps_divide:
+            "ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow>
+               eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
+proof -
+  define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g"
+  have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g"
+    unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+
+  have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0"
+    using assms(2) by (simp_all add: f'_def g'_def)
+  have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g"
+    by (simp_all add: f'_def g'_def)
+  have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)"
+               "fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def)
+  have g_nz: "g \<noteq> 0"
+  proof -
+    define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))"
+    from \<open>r > 0\<close> have "z \<in> eball 0 r"
+      by (cases r) (auto simp: z_def eball_def)
+    moreover have "z \<noteq> 0" using \<open>r > 0\<close> 
+      by (cases r) (auto simp: z_def)
+    ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6))
+    thus "g \<noteq> 0" by auto
+  qed
+  have fg: "f / g = f' * inverse g'"
+    by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit)
+
+  have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z
+  proof (cases "z = 0")
+    case False
+    with assms and z have "eval_fps g z \<noteq> 0" by auto
+    also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g"
+      by (subst g_eq) (auto simp: eval_fps_mult)
+    finally show ?thesis by auto
+  qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0)
+
+  have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')"
+    by (auto simp: R_def min.coboundedI1 min.coboundedI2)
+  also have "\<dots> \<le> fps_conv_radius (inverse g')"
+    using g'_nz by (rule fps_conv_radius_inverse)
+  finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" .
+  hence "R \<le> fps_conv_radius (f' * inverse g')"
+    by (intro order.trans[OF _ fps_conv_radius_mult])
+       (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
+  thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg)
+
+  fix z c :: complex assume z: "ereal (norm z) < R"
+  assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)"
+  show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
+  proof (cases "z = 0")
+    case False
+    from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')"
+      by simp
+    with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z"
+      unfolding fg by (subst eval_fps_mult) (auto simp: R_def)
+    also have "eval_fps (inverse g') z = inverse (eval_fps g' z)"
+      using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def)
+    also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z"
+      using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def)
+    finally show ?thesis using False by simp
+  qed (simp_all add: eval_fps_at_0 fg field_simps c)
+qed
+
+
+subsection \<open>Power series expansion of complex functions\<close>
+
+text \<open>
+  This predicate contains the notion that the given formal power series converges
+  in some disc of positive radius around the origin and is equal to the given complex
+  function there.
+
+  This relationship is unique in the sense that no complex function can have more than
+  one formal power series to which it expands, and if two holomorphic functions that are
+  holomorphic on a connected open set around the origin and have the same power series
+  expansion, they must be equal on that set.
+
+  More concrete statements about the radius of convergence can usually be made, but for
+  many purposes, the statment that the series converges to the function in some neighbourhood
+  of the origin is enough, and that can be shown almost fully automatically in most cases,
+  as there are straightforward introduction rules to show this.
+
+  In particular, when one wants to relate the coefficients of the power series to the 
+  values of the derivatives of the function at the origin, or if one wants to approximate
+  the coefficients of the series with the singularities of the function, this predicate
+  is enough.
+\<close>
+definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
+  (infixl "has'_fps'_expansion" 60) 
+  where "(f has_fps_expansion F) \<longleftrightarrow> 
+            fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
+
+named_theorems fps_expansion_intros
+
+lemma fps_nth_fps_expansion:
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes "f has_fps_expansion F"
+  shows   "fps_nth F n = (deriv ^^ n) f 0 / fact n"
+proof -
+  have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n"
+    using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def)
+  also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0"
+    using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def)
+  finally show ?thesis .
+qed
+
+lemma has_fps_expansion_fps_expansion [intro]:
+  assumes "open A" "0 \<in> A" "f holomorphic_on A"
+  shows   "f has_fps_expansion fps_expansion f 0"
+proof -
+  from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A"
+    by (auto simp: open_contains_ball)
+  have holo: "f holomorphic_on eball 0 (ereal r)" 
+    using r(2) and assms(3) by auto
+  from r(1) have "0 < ereal r" by simp
+  also have "r \<le> fps_conv_radius (fps_expansion f 0)"
+    using holo by (intro conv_radius_fps_expansion) auto
+  finally have "\<dots> > 0" .
+  moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)"
+    using r(1) by (intro eventually_nhds_in_open) auto
+  hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)"
+    by eventually_elim (subst eval_fps_expansion'[OF holo], auto)
+  ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
+  "(\<lambda>_. c) has_fps_expansion fps_const c"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]: 
+  "(\<lambda>_. 0) has_fps_expansion 0"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]:
+  "(\<lambda>_. 1) has_fps_expansion 1"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]:
+  "(\<lambda>_. numeral n) has_fps_expansion numeral n"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_fps_X_power [fps_expansion_intros]: 
+  "(\<lambda>x. x ^ n) has_fps_expansion (fps_X ^ n)"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_fps_X [fps_expansion_intros]: 
+  "(\<lambda>x. x) has_fps_expansion fps_X"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_cmult_left [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
+  assumes "f has_fps_expansion F"
+  shows   "(\<lambda>x. c * f x) has_fps_expansion fps_const c * F"
+proof (cases "c = 0")
+  case False
+  from assms have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+    by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
+  moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
+    by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>z. eval_fps (fps_const c * F) z = c * f z) (nhds 0)"
+    by eventually_elim (simp_all add: eval_fps_mult)
+  with assms and False show ?thesis
+    by (auto simp: has_fps_expansion_def fps_conv_radius_cmult_left)
+qed auto
+
+lemma has_fps_expansion_cmult_right [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
+  assumes "f has_fps_expansion F"
+  shows   "(\<lambda>x. f x * c) has_fps_expansion F * fps_const c"
+proof -
+  have "F * fps_const c = fps_const c * F"
+    by (intro fps_ext) (auto simp: mult.commute)
+  with has_fps_expansion_cmult_left [OF assms] show ?thesis 
+    by (simp add: mult.commute)
+qed
+
+lemma has_fps_expansion_minus [fps_expansion_intros]:
+  assumes "f has_fps_expansion F"
+  shows   "(\<lambda>x. - f x) has_fps_expansion -F"
+proof -
+  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+    by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
+  moreover from assms have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
+    by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>x. eval_fps (-F) x = -f x) (nhds 0)"
+    by eventually_elim (auto simp: eval_fps_minus)
+  thus ?thesis using assms by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_add [fps_expansion_intros]:
+  assumes "f has_fps_expansion F" "g has_fps_expansion G"
+  shows   "(\<lambda>x. f x + g x) has_fps_expansion F + G"
+proof -
+  from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
+    by (auto simp: has_fps_expansion_def)
+  also have "\<dots> \<le> fps_conv_radius (F + G)"
+    by (rule fps_conv_radius_add)
+  finally have radius: "\<dots> > 0" .
+
+  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+                  "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
+    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
+  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
+            and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
+    using assms by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>x. eval_fps (F + G) x = f x + g x) (nhds 0)"
+    by eventually_elim (auto simp: eval_fps_add)
+  with radius show ?thesis by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_diff [fps_expansion_intros]:
+  assumes "f has_fps_expansion F" "g has_fps_expansion G"
+  shows   "(\<lambda>x. f x - g x) has_fps_expansion F - G"
+  using has_fps_expansion_add[of f F "\<lambda>x. - g x" "-G"] assms 
+  by (simp add: has_fps_expansion_minus)
+
+lemma has_fps_expansion_mult [fps_expansion_intros]:
+  fixes F G :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+  assumes "f has_fps_expansion F" "g has_fps_expansion G"
+  shows   "(\<lambda>x. f x * g x) has_fps_expansion F * G"
+proof -
+  from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
+    by (auto simp: has_fps_expansion_def)
+  also have "\<dots> \<le> fps_conv_radius (F * G)"
+    by (rule fps_conv_radius_mult)
+  finally have radius: "\<dots> > 0" .
+
+  from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+                  "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
+    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
+  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
+            and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
+    using assms by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>x. eval_fps (F * G) x = f x * g x) (nhds 0)"
+    by eventually_elim (auto simp: eval_fps_mult)
+  with radius show ?thesis by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_inverse [fps_expansion_intros]:
+  fixes F :: "'a :: {banach, real_normed_field} fps"
+  assumes "f has_fps_expansion F"
+  assumes "fps_nth F 0 \<noteq> 0"
+  shows   "(\<lambda>x. inverse (f x)) has_fps_expansion inverse F"
+proof -
+  have radius: "fps_conv_radius (inverse F) > 0"
+    using assms unfolding has_fps_expansion_def
+    by (intro fps_conv_radius_inverse_pos) auto
+  let ?R = "min (fps_conv_radius F) (fps_conv_radius (inverse F))"
+  from assms radius
+    have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+         "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius (inverse F))) (nhds 0)"
+    by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
+  moreover have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
+    using assms by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>z. eval_fps (inverse F) z = inverse (f z)) (nhds 0)"
+  proof eventually_elim
+    case (elim z)
+    hence "eval_fps (inverse F * F) z = eval_fps (inverse F) z * f z"
+      by (subst eval_fps_mult) auto
+    also have "eval_fps (inverse F * F) z = 1"
+      using assms by (simp add: inverse_mult_eq_1)
+    finally show ?case by (auto simp: divide_simps)
+  qed
+  with radius show ?thesis by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_exp [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_field}"
+  shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_exp1 [fps_expansion_intros]:
+  "(\<lambda>x::'a :: {banach, real_normed_field}. exp x) has_fps_expansion fps_exp 1"
+  using has_fps_expansion_exp[of 1] by simp
+
+lemma has_fps_expansion_exp_neg1 [fps_expansion_intros]:
+  "(\<lambda>x::'a :: {banach, real_normed_field}. exp (-x)) has_fps_expansion fps_exp (-1)"
+  using has_fps_expansion_exp[of "-1"] by simp
+
+lemma has_fps_expansion_deriv [fps_expansion_intros]:
+  assumes "f has_fps_expansion F"
+  shows   "deriv f has_fps_expansion fps_deriv F"
+proof -
+  have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+    using assms by (intro eventually_nhds_in_open)
+                   (auto simp: has_fps_expansion_def zero_ereal_def)
+  moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
+    by (auto simp: has_fps_expansion_def)
+  then obtain s where "open s" "0 \<in> s" and s: "\<And>w. w \<in> s \<Longrightarrow> eval_fps F w = f w"
+    by (auto simp: eventually_nhds)
+  hence "eventually (\<lambda>w. w \<in> s) (nhds 0)"
+    by (intro eventually_nhds_in_open) auto
+  ultimately have "eventually (\<lambda>z. eval_fps (fps_deriv F) z = deriv f z) (nhds 0)"
+  proof eventually_elim
+    case (elim z)
+    hence "eval_fps (fps_deriv F) z = deriv (eval_fps F) z"
+      by (simp add: eval_fps_deriv)
+    also have "eventually (\<lambda>w. w \<in> s) (nhds z)"
+      using elim and \<open>open s\<close> by (intro eventually_nhds_in_open) auto
+    hence "eventually (\<lambda>w. eval_fps F w = f w) (nhds z)"
+      by eventually_elim (simp add: s)
+    hence "deriv (eval_fps F) z = deriv f z"
+      by (intro deriv_cong_ev refl)
+    finally show ?case .
+  qed
+  with assms and fps_conv_radius_deriv[of F] show ?thesis
+    by (auto simp: has_fps_expansion_def)
+qed
+
+lemma fps_conv_radius_binomial:
+  fixes c :: "'a :: {real_normed_field,banach}"
+  shows "fps_conv_radius (fps_binomial c) = (if c \<in> \<nat> then \<infinity> else 1)"
+  unfolding fps_conv_radius_def by (simp add: conv_radius_gchoose)
+
+lemma fps_conv_radius_ln:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "fps_conv_radius (fps_ln c) = (if c = 0 then \<infinity> else 1)"
+proof (cases "c = 0")
+  case False
+  have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = 1"
+  proof (rule conv_radius_ratio_limit_nonzero)
+    show "(\<lambda>n. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) \<longlonglongrightarrow> 1"
+      using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc)
+  qed auto
+  also have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) =
+               conv_radius (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n :: 'a)"
+    by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]])
+       (simp add: norm_mult norm_divide norm_power)
+  finally show ?thesis using False unfolding fps_ln_def
+    by (subst  fps_conv_radius_cmult_left) (simp_all add: fps_conv_radius_def)
+qed (auto simp: fps_ln_def)
+
+lemma fps_conv_radius_ln_nonzero [simp]:
+  assumes "c \<noteq> (0 :: 'a :: {banach,real_normed_field,field_char_0})"
+  shows   "fps_conv_radius (fps_ln c) = 1"
+  using assms by (simp add: fps_conv_radius_ln)
+
+lemma fps_conv_radius_sin [simp]:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "fps_conv_radius (fps_sin c) = \<infinity>"
+proof (cases "c = 0")
+  case False
+  have "\<infinity> = conv_radius (\<lambda>n. of_real (sin_coeff n) :: 'a)"
+  proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
+    case (1 z)
+    show ?case using summable_norm_sin[of z] by (simp add: norm_mult)
+  qed
+  also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (sin_coeff n) :: 'a)"
+    using False by (subst conv_radius_mult_power) auto
+  also have "\<dots> = fps_conv_radius (fps_sin c)" unfolding fps_conv_radius_def
+    by (rule conv_radius_cong_weak) (auto simp add: fps_sin_def sin_coeff_def)
+  finally show ?thesis by simp
+qed simp_all
+
+lemma fps_conv_radius_cos [simp]:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "fps_conv_radius (fps_cos c) = \<infinity>"
+proof (cases "c = 0")
+  case False
+  have "\<infinity> = conv_radius (\<lambda>n. of_real (cos_coeff n) :: 'a)"
+  proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
+    case (1 z)
+    show ?case using summable_norm_cos[of z] by (simp add: norm_mult)
+  qed
+  also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (cos_coeff n) :: 'a)"
+    using False by (subst conv_radius_mult_power) auto
+  also have "\<dots> = fps_conv_radius (fps_cos c)" unfolding fps_conv_radius_def
+    by (rule conv_radius_cong_weak) (auto simp add: fps_cos_def cos_coeff_def)
+  finally show ?thesis by simp
+qed simp_all
+
+lemma eval_fps_sin [simp]:
+  fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "eval_fps (fps_sin c) z = sin (c * z)"
+proof -
+  have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges)
+  also have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_sin c) n * z ^ n)"
+    by (rule ext) (auto simp: sin_coeff_def fps_sin_def power_mult_distrib scaleR_conv_of_real)
+  finally show ?thesis by (simp add: sums_iff eval_fps_def)
+qed
+
+lemma eval_fps_cos [simp]:
+  fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "eval_fps (fps_cos c) z = cos (c * z)"
+proof -
+  have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges)
+  also have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_cos c) n * z ^ n)"
+    by (rule ext) (auto simp: cos_coeff_def fps_cos_def power_mult_distrib scaleR_conv_of_real)
+  finally show ?thesis by (simp add: sums_iff eval_fps_def)
+qed
+
+lemma cos_eq_zero_imp_norm_ge:
+  assumes "cos (z :: complex) = 0"
+  shows   "norm z \<ge> pi / 2"
+proof -
+  from assms obtain n where "z = complex_of_real ((of_int n + 1 / 2) * pi)"
+    by (auto simp: cos_eq_0 algebra_simps)
+  also have "norm \<dots> = \<bar>real_of_int n + 1 / 2\<bar> * pi"
+    by (subst norm_of_real) (simp_all add: abs_mult)
+  also have "real_of_int n + 1 / 2 = of_int (2 * n + 1) / 2" by simp
+  also have "\<bar>\<dots>\<bar> = of_int \<bar>2 * n + 1\<bar> / 2" by (subst abs_divide) simp_all
+  also have "\<dots> * pi = of_int \<bar>2 * n + 1\<bar> * (pi / 2)" by simp
+  also have "\<dots> \<ge> of_int 1 * (pi / 2)"
+    by (intro mult_right_mono, subst of_int_le_iff) (auto simp: abs_if)
+  finally show ?thesis by simp
+qed
+
+lemma fps_conv_radius_tan:
+  fixes c :: complex
+  assumes "c \<noteq> 0"
+  shows   "fps_conv_radius (fps_tan c) \<ge> pi / (2 * norm c)"
+proof -
+  have "fps_conv_radius (fps_tan c) \<ge> 
+          Min {pi / (2 * norm c), fps_conv_radius (fps_sin c), fps_conv_radius (fps_cos c)}"
+    unfolding fps_tan_def
+  proof (rule fps_conv_radius_divide)
+    fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
+    with cos_eq_zero_imp_norm_ge[of "c*z"] assms 
+      show "eval_fps (fps_cos  c) z \<noteq> 0" by (auto simp: norm_mult field_simps)
+  qed (insert assms, auto)
+  thus ?thesis by (simp add: min_def)
+qed
+
+lemma eval_fps_tan:
+  fixes c :: complex
+  assumes "norm z < pi / (2 * norm c)"
+  shows   "eval_fps (fps_tan c) z = tan (c * z)"
+proof (cases "c = 0")
+  case False
+  show ?thesis unfolding fps_tan_def
+  proof (subst eval_fps_divide'[where r = "pi / (2 * norm c)"])
+    fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
+    with cos_eq_zero_imp_norm_ge[of "c*z"] assms 
+      show "eval_fps (fps_cos  c) z \<noteq> 0" using False by (auto simp: norm_mult field_simps)
+    qed (insert False assms, auto simp: field_simps tan_def)
+qed simp_all
+
+lemma eval_fps_binomial:
+  fixes c :: complex
+  assumes "norm z < 1"
+  shows   "eval_fps (fps_binomial c) z = (1 + z) powr c"
+  using gen_binomial_complex[OF assms] by (simp add: sums_iff eval_fps_def)
+
+lemma has_fps_expansion_binomial_complex [fps_expansion_intros]:
+  fixes c :: complex
+  shows "(\<lambda>x. (1 + x) powr c) has_fps_expansion fps_binomial c"
+proof -
+  have *: "eventually (\<lambda>z::complex. z \<in> eball 0 1) (nhds 0)"
+    by (intro eventually_nhds_in_open) auto
+  thus ?thesis
+    by (auto simp: has_fps_expansion_def eval_fps_binomial fps_conv_radius_binomial
+             intro!: eventually_mono [OF *])
+qed
+
+lemma has_fps_expansion_sin [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "(\<lambda>x. sin (c * x)) has_fps_expansion fps_sin c"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_sin' [fps_expansion_intros]:
+  "(\<lambda>x::'a :: {banach, real_normed_field}. sin x) has_fps_expansion fps_sin 1"
+  using has_fps_expansion_sin[of 1] by simp
+
+lemma has_fps_expansion_cos [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "(\<lambda>x. cos (c * x)) has_fps_expansion fps_cos c"
+  by (auto simp: has_fps_expansion_def)
+
+lemma has_fps_expansion_cos' [fps_expansion_intros]:
+  "(\<lambda>x::'a :: {banach, real_normed_field}. cos x) has_fps_expansion fps_cos 1"
+  using has_fps_expansion_cos[of 1] by simp
+
+lemma has_fps_expansion_shift [fps_expansion_intros]:
+  fixes F :: "'a :: {banach, real_normed_field} fps"
+  assumes "f has_fps_expansion F" and "n \<le> subdegree F"
+  assumes "c = fps_nth F n"
+  shows   "(\<lambda>x. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)"
+proof -
+  have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
+    using assms by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
+  moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
+    using assms by (auto simp: has_fps_expansion_def)
+  ultimately have "eventually (\<lambda>x. eval_fps (fps_shift n F) x = 
+                     (if x = 0 then c else f x / x ^ n)) (nhds 0)"
+    by eventually_elim (auto simp: eval_fps_shift assms)
+  with assms show ?thesis by (auto simp: has_fps_expansion_def)
+qed
+
+lemma has_fps_expansion_divide [fps_expansion_intros]:
+  fixes F G :: "'a :: {banach, real_normed_field} fps"
+  assumes "f has_fps_expansion F" and "g has_fps_expansion G" and 
+          "subdegree G \<le> subdegree F" "G \<noteq> 0"
+          "c = fps_nth F (subdegree G) / fps_nth G (subdegree G)"
+  shows   "(\<lambda>x. if x = 0 then c else f x / g x) has_fps_expansion (F / G)"
+proof -
+  define n where "n = subdegree G"
+  define F' and G' where "F' = fps_shift n F" and "G' = fps_shift n G"
+  have "F = F' * fps_X ^ n" "G = G' * fps_X ^ n" unfolding F'_def G'_def n_def 
+    by (rule fps_shift_times_fps_X_power [symmetric] le_refl | fact)+
+  moreover from assms have "fps_nth G' 0 \<noteq> 0"
+    by (simp add: G'_def n_def)
+  ultimately have FG: "F / G = F' * inverse G'"
+    by (simp add: fps_divide_unit)
+
+  have "(\<lambda>x. (if x = 0 then fps_nth F n else f x / x ^ n) * 
+          inverse (if x = 0 then fps_nth G n else g x / x ^ n)) has_fps_expansion F / G"
+    (is "?h has_fps_expansion _") unfolding FG F'_def G'_def n_def using \<open>G \<noteq> 0\<close>
+    by (intro has_fps_expansion_mult has_fps_expansion_inverse
+              has_fps_expansion_shift assms) auto
+  also have "?h = (\<lambda>x. if x = 0 then c else f x / g x)"
+    using assms(5) unfolding n_def 
+    by (intro ext) (auto split: if_splits simp: field_simps)
+  finally show ?thesis .
+qed
+
+lemma has_fps_expansion_divide' [fps_expansion_intros]:
+  fixes F G :: "'a :: {banach, real_normed_field} fps"
+  assumes "f has_fps_expansion F" and "g has_fps_expansion G" and "fps_nth G 0 \<noteq> 0"
+  shows   "(\<lambda>x. f x / g x) has_fps_expansion (F / G)"
+proof -
+  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)"
+    (is "?h has_fps_expansion _") using assms(3) by (intro has_fps_expansion_divide assms) auto
+  also from assms have "fps_nth F 0 = f 0" "fps_nth G 0 = g 0"
+    by (auto simp: has_fps_expansion_def eval_fps_at_0 dest: eventually_nhds_x_imp_x)
+  hence "?h = (\<lambda>x. f x / g x)" by auto
+  finally show ?thesis .
+qed
+
+lemma has_fps_expansion_tan [fps_expansion_intros]:
+  fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
+  shows "(\<lambda>x. tan (c * x)) has_fps_expansion fps_tan c"
+proof -
+  have "(\<lambda>x. sin (c * x) / cos (c * x)) has_fps_expansion fps_sin c / fps_cos c"
+    by (intro fps_expansion_intros) auto
+  thus ?thesis by (simp add: tan_def fps_tan_def)
+qed
+
+lemma has_fps_expansion_tan' [fps_expansion_intros]:
+  "tan has_fps_expansion fps_tan (1 :: 'a :: {banach, real_normed_field, field_char_0})"
+  using has_fps_expansion_tan[of 1] by simp
+
+lemma has_fps_expansion_imp_holomorphic:
+  assumes "f has_fps_expansion F"
+  obtains s where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
+proof -
+  from assms obtain s where s: "open s" "0 \<in> s" "\<And>z. z \<in> s \<Longrightarrow> eval_fps F z = f z"
+    unfolding has_fps_expansion_def eventually_nhds by blast
+  let ?s' = "eball 0 (fps_conv_radius F) \<inter> s"
+  have "eval_fps F holomorphic_on ?s'"
+    by (intro holomorphic_intros) auto
+  also have "?this \<longleftrightarrow> f holomorphic_on ?s'"
+    using s by (intro holomorphic_cong) auto
+  finally show ?thesis using s assms
+    by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
+qed
+
+lemma residue_fps_expansion_over_power_at_0:
+  assumes "f has_fps_expansion F"
+  shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
+proof -
+  from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
+  have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
+    using assms s unfolding has_fps_expansion_def
+    by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
+  also from assms have "\<dots> = fps_nth F n"
+    by (subst fps_nth_fps_expansion) auto
+  finally show ?thesis by simp
+qed
+
+end
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Analysis/Infinite_Set_Sum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -0,0 +1,570 @@
+(*  
+  Title:    HOL/Analysis/Infinite_Set_Sum.thy
+  Author:   Manuel Eberl, TU München
+
+  A theory of sums over possible infinite sets. (Only works for absolute summability)
+*)
+section \<open>Sums over infinite sets\<close>
+theory Infinite_Set_Sum
+  imports Set_Integral
+begin
+
+(* TODO Move *)
+lemma sets_eq_countable:
+  assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M"
+  shows   "sets M = Pow A"
+proof (intro equalityI subsetI)
+  fix X assume "X \<in> Pow A"
+  hence "(\<Union>x\<in>X. {x}) \<in> sets M"
+    by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3))
+  also have "(\<Union>x\<in>X. {x}) = X" by auto
+  finally show "X \<in> sets M" .
+next
+  fix X assume "X \<in> sets M"
+  from sets.sets_into_space[OF this] and assms 
+    show "X \<in> Pow A" by simp
+qed
+
+lemma measure_eqI_countable':
+  assumes spaces: "space M = A" "space N = A" 
+  assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
+  assumes A: "countable A"
+  assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
+  shows "M = N"
+proof (rule measure_eqI_countable)
+  show "sets M = Pow A"
+    by (intro sets_eq_countable assms)
+  show "sets N = Pow A"
+    by (intro sets_eq_countable assms)
+qed fact+
+
+lemma PiE_singleton: 
+  assumes "f \<in> extensional A"
+  shows   "PiE A (\<lambda>x. {f x}) = {f}"
+proof -
+  {
+    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
+    hence "g x = f x" for x
+      using assms by (cases "x \<in> A") (auto simp: extensional_def)
+    hence "g = f" by (simp add: fun_eq_iff)
+  }
+  thus ?thesis using assms by (auto simp: extensional_def)
+qed
+
+lemma count_space_PiM_finite:
+  fixes B :: "'a \<Rightarrow> 'b set"
+  assumes "finite A" "\<And>i. countable (B i)"
+  shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
+proof (rule measure_eqI_countable')
+  show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
+    by (simp add: space_PiM)
+  show "space (count_space (PiE A B)) = PiE A B" by simp
+next
+  fix f assume f: "f \<in> PiE A B"
+  hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
+    by (intro sets_PiM_I_finite assms) auto
+  also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
+    by (intro PiE_singleton) (auto simp: PiE_def)
+  finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
+next
+  interpret product_sigma_finite "(\<lambda>i. count_space (B i))"
+    by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms)
+  thm sigma_finite_measure_count_space
+  fix f assume f: "f \<in> PiE A B"
+  hence "{f} = PiE A (\<lambda>x. {f x})"
+    by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
+  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
+               (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
+    using f assms by (subst emeasure_PiM) auto
+  also have "\<dots> = (\<Prod>i\<in>A. 1)"
+    by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto)
+  also have "\<dots> = emeasure (count_space (PiE A B)) {f}"
+    using f by (subst emeasure_count_space_finite) auto
+  finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} =
+                  emeasure (count_space (Pi\<^sub>E A B)) {f}" .
+qed (simp_all add: countable_PiE assms)
+
+
+
+definition abs_summable_on ::
+    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
+    (infix "abs'_summable'_on" 50)
+ where
+   "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
+
+
+definition infsetsum ::
+    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
+ where
+   "infsetsum f A = lebesgue_integral (count_space A) f"
+
+syntax (ASCII)
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
+syntax
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
+translations \<comment> \<open>Beware of argument permutation!\<close>
+  "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
+
+syntax (ASCII)
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
+syntax
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
+translations
+  "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
+
+print_translation \<open>
+let
+  fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
+        if x <> y then raise Match
+        else
+          let
+            val x' = Syntax_Trans.mark_bound_body (x, Tx);
+            val t' = subst_bound (x', t);
+            val P' = subst_bound (x', P);
+          in
+            Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+          end
+    | sum_tr' _ = raise Match;
+in [(@{const_syntax infsetsum}, K sum_tr')] end
+\<close>
+
+
+
+
+lemma restrict_count_space_subset:
+  "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
+  by (subst restrict_count_space) (simp_all add: Int_absorb2)
+
+lemma abs_summable_on_restrict:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
+  assumes "A \<subseteq> B"
+  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B"
+proof -
+  have "count_space A = restrict_space (count_space B) A"
+    by (rule restrict_count_space_subset [symmetric]) fact+
+  also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f"
+    by (subst integrable_restrict_space) auto
+  finally show ?thesis 
+    unfolding abs_summable_on_def .
+qed
+
+lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f"
+  by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def)
+
+lemma abs_summable_on_altdef': 
+  "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f"
+  by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def)
+
+lemma abs_summable_on_cong [cong]:
+  "(\<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)"
+  unfolding abs_summable_on_def by (intro integrable_cong) auto
+
+lemma abs_summable_on_cong_neutral:
+  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
+  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
+  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
+  shows   "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B"
+  unfolding abs_summable_on_altdef using assms
+  by (intro Bochner_Integration.integrable_cong refl)
+     (auto simp: indicator_def split: if_splits)
+
+lemma abs_summable_on_restrict':
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}"
+  assumes "A \<subseteq> B"
+  shows   "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B"
+  by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto)
+
+lemma abs_summable_on_nat_iff:
+  "f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
+proof -
+  have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))"
+    by (subst abs_summable_on_restrict'[of _ UNIV]) 
+       (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
+  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)"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma abs_summable_on_nat_iff':
+  "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
+  by (subst abs_summable_on_nat_iff) auto
+
+lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
+  unfolding abs_summable_on_def by (rule integrable_count_space)
+
+lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}"
+  by simp
+
+lemma abs_summable_on_subset:
+  assumes "f abs_summable_on B" and "A \<subseteq> B"
+  shows   "f abs_summable_on A"
+  unfolding abs_summable_on_altdef
+  by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef)
+
+lemma abs_summable_on_union [intro]:
+  assumes "f abs_summable_on A" and "f abs_summable_on B"
+  shows   "f abs_summable_on (A \<union> B)"
+  using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto
+
+lemma abs_summable_on_reindex_bij_betw:
+  assumes "bij_betw g A B"
+  shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
+proof -
+  have *: "count_space B = distr (count_space A) (count_space B) g"
+    by (rule distr_bij_count_space [symmetric]) fact
+  show ?thesis unfolding abs_summable_on_def
+    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) 
+       (insert assms, auto simp: bij_betw_def)
+qed
+
+lemma abs_summable_on_reindex:
+  assumes "(\<lambda>x. f (g x)) abs_summable_on A"
+  shows   "f abs_summable_on (g ` A)"
+proof -
+  define g' where "g' = inv_into A g"
+  from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
+    by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
+  also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
+    by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
+  also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)"
+    by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f)
+  finally show ?thesis .
+qed
+
+lemma abs_summable_reindex_iff: 
+  "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
+  by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
+
+lemma abs_summable_on_Sigma_project:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+  assumes "f abs_summable_on (Sigma A B)" "x \<in> A"
+  shows   "(\<lambda>y. f (x, y)) abs_summable_on (B x)"
+proof -
+  from assms(2) have "f abs_summable_on (Sigma {x} B)"
+    by (intro abs_summable_on_subset [OF assms(1)]) auto
+  also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)"
+    by (rule abs_summable_on_cong) auto
+  finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)"
+    by (rule abs_summable_on_reindex)
+  also have "snd ` Sigma {x} B = B x"
+    using assms by (auto simp: image_iff)
+  finally show ?thesis .
+qed
+
+lemma abs_summable_on_Times_swap:
+  "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A"
+proof -
+  have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)"
+    by (auto simp: bij_betw_def inj_on_def)
+  show ?thesis
+    by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric])
+       (simp_all add: case_prod_unfold)
+qed
+
+lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A"
+  by (simp add: abs_summable_on_def)
+
+lemma abs_summable_on_uminus [intro]:
+  "f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A"
+  unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus)
+
+lemma abs_summable_on_add [intro]:
+  assumes "f abs_summable_on A" and "g abs_summable_on A"
+  shows   "(\<lambda>x. f x + g x) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add)
+
+lemma abs_summable_on_diff [intro]:
+  assumes "f abs_summable_on A" and "g abs_summable_on A"
+  shows   "(\<lambda>x. f x - g x) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff)
+
+lemma abs_summable_on_scaleR_left [intro]:
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left)
+
+lemma abs_summable_on_scaleR_right [intro]:
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right)
+
+lemma abs_summable_on_cmult_right [intro]:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "(\<lambda>x. c * f x) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right)
+
+lemma abs_summable_on_cmult_left [intro]:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "(\<lambda>x. f x * c) abs_summable_on A"
+  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left)
+
+
+
+lemma not_summable_infsetsum_eq:
+  "\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0"
+  by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq)
+
+lemma infsetsum_altdef:
+  "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f"
+  by (subst integral_restrict_space [symmetric])
+     (auto simp: restrict_count_space_subset infsetsum_def)
+
+lemma infsetsum_altdef':
+  "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f"
+  by (subst integral_restrict_space [symmetric])
+     (auto simp: restrict_count_space_subset infsetsum_def)
+
+lemma infsetsum_cong [cong]:
+  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B"
+  unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto
+
+lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0"
+  by (simp add: infsetsum_def)
+
+lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
+  by simp
+
+lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
+  by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
+
+lemma infsetsum_nat: 
+  assumes "f abs_summable_on A"
+  shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
+proof -
+  from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)"
+    unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto
+  also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma infsetsum_nat': 
+  assumes "f abs_summable_on UNIV"
+  shows   "infsetsum f UNIV = (\<Sum>n. f n)"
+  using assms by (subst infsetsum_nat) auto
+
+lemma sums_infsetsum_nat:
+  assumes "f abs_summable_on A"
+  shows   "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A"
+proof -
+  from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
+    by (simp add: abs_summable_on_nat_iff)
+  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))"
+    by auto
+  finally have "summable (\<lambda>n. if n \<in> A then f n else 0)"
+    by (rule summable_norm_cancel)
+  with assms show ?thesis
+    by (auto simp: sums_iff infsetsum_nat)
+qed
+
+lemma sums_infsetsum_nat':
+  assumes "f abs_summable_on UNIV"
+  shows   "f sums infsetsum f UNIV"
+  using sums_infsetsum_nat [OF assms] by simp
+
+lemma infsetsum_Un_disjoint:
+  assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}"
+  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B"
+  using assms unfolding infsetsum_altdef abs_summable_on_altdef
+  by (subst set_integral_Un) auto
+
+lemma infsetsum_Diff:
+  assumes "f abs_summable_on B" "A \<subseteq> B"
+  shows   "infsetsum f (B - A) = infsetsum f B - infsetsum f A"
+proof -
+  have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A"
+    using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto
+  also from assms(2) have "(B - A) \<union> A = B"
+    by auto
+  ultimately show ?thesis
+    by (simp add: algebra_simps)
+qed
+
+lemma infsetsum_Un_Int:
+  assumes "f abs_summable_on (A \<union> B)"
+  shows   "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)"
+proof -
+  have "A \<union> B = A \<union> (B - A \<inter> B)"
+    by auto
+  also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)"
+    by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
+  also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)"
+    by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
+  finally show ?thesis 
+    by (simp add: algebra_simps)
+qed
+
+lemma infsetsum_reindex_bij_betw:
+  assumes "bij_betw g A B"
+  shows   "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B"
+proof -
+  have *: "count_space B = distr (count_space A) (count_space B) g"
+    by (rule distr_bij_count_space [symmetric]) fact
+  show ?thesis unfolding infsetsum_def
+    by (subst *, subst integral_distr[of _ _ "count_space B"]) 
+       (insert assms, auto simp: bij_betw_def)    
+qed
+
+lemma infsetsum_reindex:
+  assumes "inj_on g A"
+  shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
+  by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
+
+lemma infsetsum_cong_neutral:
+  assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0"
+  assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0"
+  assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x"
+  shows   "infsetsum f A = infsetsum g B"
+  unfolding infsetsum_altdef using assms
+  by (intro Bochner_Integration.integral_cong refl)
+     (auto simp: indicator_def split: if_splits)
+
+lemma infsetsum_Sigma:
+  fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
+  assumes [simp]: "countable A" and "\<And>i. countable (B i)"
+  assumes summable: "f abs_summable_on (Sigma A B)"
+  shows   "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
+proof -
+  define B' where "B' = (\<Union>i\<in>A. B i)"
+  have [simp]: "countable B'" 
+    unfolding B'_def by (intro countable_UN assms)
+  interpret pair_sigma_finite "count_space A" "count_space B'"
+    by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
+
+  have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)"
+    using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
+  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))"
+    by (intro Bochner_Integration.integrable_cong)
+       (auto simp: pair_measure_countable indicator_def split: if_splits)
+  finally have integrable: \<dots> .
+  
+  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
+          (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
+    unfolding infsetsum_def by simp
+  also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)"
+    by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl)
+       (auto simp: B'_def)
+  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'))"
+    by (subst integral_fst [OF integrable]) auto
+  also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))"
+    by (intro Bochner_Integration.integral_cong)
+       (auto simp: pair_measure_countable indicator_def split: if_splits)
+  also have "\<dots> = infsetsum f (Sigma A B)"
+    by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def)
+  finally show ?thesis ..
+qed
+
+lemma infsetsum_Times:
+  fixes A :: "'a set" and B :: "'b set"
+  assumes [simp]: "countable A" and "countable B"
+  assumes summable: "f abs_summable_on (A \<times> B)"
+  shows   "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A"
+  using assms by (subst infsetsum_Sigma) auto
+
+lemma infsetsum_Times':
+  fixes A :: "'a set" and B :: "'b set"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
+  assumes [simp]: "countable A" and [simp]: "countable B"
+  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)"
+  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
+  using assms by (subst infsetsum_Times) auto
+
+lemma infsetsum_swap:
+  fixes A :: "'a set" and B :: "'b set"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}"
+  assumes [simp]: "countable A" and [simp]: "countable B"
+  assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B"
+  shows   "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
+proof -
+  from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A"
+    by (subst abs_summable_on_Times_swap) auto
+  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)"
+    by (auto simp: bij_betw_def inj_on_def)
+  have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)"
+    using summable by (subst infsetsum_Times) auto
+  also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)"
+    by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric])
+       (simp_all add: case_prod_unfold)
+  also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B"
+    using summable' by (subst infsetsum_Times) auto
+  finally show ?thesis .
+qed
+
+lemma infsetsum_prod_PiE:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
+  assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
+  assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
+  shows   "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
+proof -
+  define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})"
+  from assms have [simp]: "countable (B' x)" for x
+    by (auto simp: B'_def)
+  then interpret product_sigma_finite "count_space \<circ> B'"
+    unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable)
+  have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) =
+          (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))"
+    by (simp add: infsetsum_def)
+  also have "PiE A B = PiE A B'"
+    by (intro PiE_cong) (simp_all add: B'_def)
+  hence "count_space (PiE A B) = count_space (PiE A B')"
+    by simp
+  also have "\<dots> = PiM A (count_space \<circ> B')"
+    unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
+  also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))"
+    by (subst product_integral_prod) 
+       (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
+  also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
+    by (intro prod.cong refl) (simp_all add: B'_def)
+  finally show ?thesis .
+qed
+
+lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A"
+  unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_minus)
+
+lemma infsetsum_add:
+  assumes "f abs_summable_on A" and "g abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A"
+  using assms unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_add)
+
+lemma infsetsum_diff:
+  assumes "f abs_summable_on A" and "g abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A"
+  using assms unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_diff)
+
+lemma infsetsum_scaleR_left:
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c"
+  using assms unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_scaleR_left)
+
+lemma infsetsum_scaleR_right:
+  "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A"
+  unfolding infsetsum_def abs_summable_on_def 
+  by (subst Bochner_Integration.integral_scaleR_right) auto
+
+lemma infsetsum_cmult_left:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c"
+  using assms unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_mult_left)
+
+lemma infsetsum_cmult_right:
+  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
+  assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
+  shows   "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A"
+  using assms unfolding infsetsum_def abs_summable_on_def 
+  by (rule Bochner_Integration.integral_mult_right)
+
+(* TODO Generalise with bounded_linear *)
+
+end
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 21 19:20:02 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -402,53 +402,53 @@
 qed 
 
 
-subsection \<open>The eXtractor series X\<close>
+subsection \<open>The efps_Xtractor series fps_X\<close>
 
 lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
   by (induct n) auto
 
-definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
-
-lemma X_mult_nth [simp]:
-  "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
+definition "fps_X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
+
+lemma fps_X_mult_nth [simp]:
+  "(fps_X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
 proof (cases "n = 0")
   case False
-  have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
+  have "(fps_X * f) $n = (\<Sum>i = 0..n. fps_X $ i * f $ (n - i))"
     by (simp add: fps_mult_nth)
   also have "\<dots> = f $ (n - 1)"
-    using False by (simp add: X_def mult_delta_left sum.delta)
+    using False by (simp add: fps_X_def mult_delta_left sum.delta)
   finally show ?thesis
     using False by simp
 next
   case True
   then show ?thesis
-    by (simp add: fps_mult_nth X_def)
+    by (simp add: fps_mult_nth fps_X_def)
 qed
 
-lemma X_mult_right_nth[simp]:
-  "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))"
+lemma fps_X_mult_right_nth[simp]:
+  "((a::'a::semiring_1 fps) * fps_X) $ n = (if n = 0 then 0 else a $ (n - 1))"
 proof -
-  have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
-    by (simp add: fps_times_def X_def)
+  have "(a * fps_X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
+    by (simp add: fps_times_def fps_X_def)
   also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
     by (intro sum.cong) auto
   also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: sum.delta)
   finally show ?thesis .
 qed
 
-lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
+lemma fps_mult_fps_X_commute: "fps_X * (a :: 'a :: semiring_1 fps) = a * fps_X" 
   by (simp add: fps_eq_iff)
 
-lemma X_power_iff: "X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)"
+lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)"
   by (induction n) (auto simp: fps_eq_iff)
 
-lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
-  by (simp add: X_def)
-
-lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
-  by (simp add: X_power_iff)
-
-lemma X_power_mult_nth: "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
+lemma fps_X_nth[simp]: "fps_X$n = (if n = 1 then 1 else 0)"
+  by (simp add: fps_X_def)
+
+lemma fps_X_power_nth[simp]: "(fps_X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
+  by (simp add: fps_X_power_iff)
+
+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))"
   apply (induct k arbitrary: n)
   apply simp
   unfolding power_Suc mult.assoc
@@ -456,32 +456,32 @@
   apply auto
   done
 
-lemma X_power_mult_right_nth:
-    "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
-  by (metis X_power_mult_nth mult.commute)
-
-
-lemma X_neq_fps_const [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> fps_const c"
+lemma fps_X_power_mult_right_nth:
+    "((f :: 'a::comm_ring_1 fps) * fps_X^k) $n = (if n < k then 0 else f $ (n - k))"
+  by (metis fps_X_power_mult_nth mult.commute)
+
+
+lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> fps_const c"
 proof
-  assume "(X::'a fps) = fps_const (c::'a)"
-  hence "X$1 = (fps_const (c::'a))$1" by (simp only:)
+  assume "(fps_X::'a fps) = fps_const (c::'a)"
+  hence "fps_X$1 = (fps_const (c::'a))$1" by (simp only:)
   thus False by auto
 qed
 
-lemma X_neq_zero [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 0"
-  by (simp only: fps_const_0_eq_0[symmetric] X_neq_fps_const) simp
-
-lemma X_neq_one [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 1"
-  by (simp only: fps_const_1_eq_1[symmetric] X_neq_fps_const) simp
-
-lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
-  by (simp only: numeral_fps_const X_neq_fps_const) simp
-
-lemma X_pow_eq_X_pow_iff [simp]:
-  "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n"
+lemma fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 0"
+  by (simp only: fps_const_0_eq_0[symmetric] fps_X_neq_fps_const) simp
+
+lemma fps_X_neq_one [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 1"
+  by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp
+
+lemma fps_X_neq_numeral [simp]: "(fps_X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c"
+  by (simp only: numeral_fps_const fps_X_neq_fps_const) simp
+
+lemma fps_X_pow_eq_fps_X_pow_iff [simp]:
+  "(fps_X :: ('a :: {comm_ring_1}) fps) ^ m = fps_X ^ n \<longleftrightarrow> m = n"
 proof
-  assume "(X :: 'a fps) ^ m = X ^ n"
-  hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
+  assume "(fps_X :: 'a fps) ^ m = fps_X ^ n"
+  hence "(fps_X :: 'a fps) ^ m $ m = fps_X ^ n $ m" by (simp only:)
   thus "m = n" by (simp split: if_split_asm)
 qed simp_all
 
@@ -553,8 +553,8 @@
 lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0"
   by (auto intro!: subdegreeI)
 
-lemma subdegree_X [simp]: "subdegree (X :: ('a :: zero_neq_one) fps) = 1"
-  by (auto intro!: subdegreeI simp: X_def)
+lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1"
+  by (auto intro!: subdegreeI simp: fps_X_def)
 
 lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
   by (cases "c = 0") (auto intro!: subdegreeI)
@@ -705,33 +705,33 @@
 lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)"
   by (simp add: numeral_fps_const fps_shift_fps_const)
 
-lemma fps_shift_X_power [simp]:
-  "n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m - n) ::'a::comm_ring_1 fps)"
+lemma fps_shift_fps_X_power [simp]:
+  "n \<le> m \<Longrightarrow> fps_shift n (fps_X ^ m) = (fps_X ^ (m - n) ::'a::comm_ring_1 fps)"
   by (intro fps_ext) (auto simp: fps_shift_def )
 
-lemma fps_shift_times_X_power:
-  "n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)"
-  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
-
-lemma fps_shift_times_X_power' [simp]:
-  "fps_shift n (f * X^n) = (f :: 'a :: comm_ring_1 fps)"
-  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
-
-lemma fps_shift_times_X_power'':
-  "m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
-  by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero)
+lemma fps_shift_times_fps_X_power:
+  "n \<le> subdegree f \<Longrightarrow> fps_shift n f * fps_X ^ n = (f :: 'a :: comm_ring_1 fps)"
+  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
+
+lemma fps_shift_times_fps_X_power' [simp]:
+  "fps_shift n (f * fps_X^n) = (f :: 'a :: comm_ring_1 fps)"
+  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
+
+lemma fps_shift_times_fps_X_power'':
+  "m \<le> n \<Longrightarrow> fps_shift n (f * fps_X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
+  by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
 
 lemma fps_shift_subdegree [simp]:
   "n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n"
   by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+
 
 lemma subdegree_decompose:
-  "f = fps_shift (subdegree f) f * X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
-  by (rule fps_ext) (auto simp: X_power_mult_right_nth)
+  "f = fps_shift (subdegree f) f * fps_X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
+  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth)
 
 lemma subdegree_decompose':
-  "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * X^n"
-  by (rule fps_ext) (auto simp: X_power_mult_right_nth intro!: nth_less_subdegree_zero)
+  "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * fps_X^n"
+  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth intro!: nth_less_subdegree_zero)
 
 lemma fps_shift_fps_shift:
   "fps_shift (m + n) f = fps_shift m (fps_shift n f)"
@@ -745,8 +745,8 @@
   assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
   shows   "fps_shift n (h*g) = h * fps_shift n g"
 proof -
-  from assms have "g = fps_shift n g * X^n" by (rule subdegree_decompose')
-  also have "h * ... = (h * fps_shift n g) * X^n" by simp
+  from assms have "g = fps_shift n g * fps_X^n" by (rule subdegree_decompose')
+  also have "h * ... = (h * fps_shift n g) * fps_X^n" by simp
   also have "fps_shift n ... = h * fps_shift n g" by simp
   finally show ?thesis .
 qed
@@ -798,8 +798,8 @@
   by (simp add: numeral_fps_const fps_cutoff_fps_const)
 
 lemma fps_shift_cutoff:
-  "fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f"
-  by (simp add: fps_eq_iff X_power_mult_right_nth)
+  "fps_shift n (f :: ('a :: comm_ring_1) fps) * fps_X^n + fps_cutoff n f = f"
+  by (simp add: fps_eq_iff fps_X_power_mult_right_nth)
 
 
 subsection \<open>Formal Power series form a metric space\<close>
@@ -905,11 +905,11 @@
     using kp by blast
 qed
 
-lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
+lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*fps_X^i) {0..m})$n =
     (if n \<le> m then a$n else 0::'a::comm_ring_1)"
   by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
 
-lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
+lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * fps_X^i) {0..n}) \<longlonglongrightarrow> a"
   (is "?s \<longlonglongrightarrow> a")
 proof -
   have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
@@ -1153,12 +1153,12 @@
   "unit_factor f = fps_shift (subdegree f) f"
 
 definition fps_normalize_def [simp]:
-  "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
+  "normalize f = (if f = 0 then 0 else fps_X ^ subdegree f)"
 
 instance proof
   fix f :: "'a fps"
   show "unit_factor f * normalize f = f"
-    by (simp add: fps_shift_times_X_power)
+    by (simp add: fps_shift_times_fps_X_power)
 next
   fix f g :: "'a fps"
   show "unit_factor (f * g) = unit_factor f * unit_factor g"
@@ -1205,10 +1205,10 @@
 
   from assms nz have "f div g * g = fps_shift n (f * inverse h) * g"
     by (simp add: fps_divide_def Let_def h_def n_def)
-  also have "... = fps_shift n (f * inverse h) * X^n * h" unfolding h_def n_def
+  also have "... = fps_shift n (f * inverse h) * fps_X^n * h" unfolding h_def n_def
     by (subst subdegree_decompose[of g]) simp
-  also have "fps_shift n (f * inverse h) * X^n = f * inverse h"
-    by (rule fps_shift_times_X_power) (simp_all add: nz assms n_def)
+  also have "fps_shift n (f * inverse h) * fps_X^n = f * inverse h"
+    by (rule fps_shift_times_fps_X_power) (simp_all add: nz assms n_def)
   also have "... * h = f * (inverse h * h)" by simp
   also have "inverse h * h = 1" by (rule inverse_mult_eq_1) simp
   finally show ?thesis by simp
@@ -1246,14 +1246,14 @@
 qed (simp_all add: fps_divide_def)
 
 private lemma fps_divide_cancel_aux2:
-  "(f * X^m) div (g * X^m) = f div (g :: 'a :: field fps)"
+  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
 proof (cases "g = 0")
   assume [simp]: "g \<noteq> 0"
-  have "(f * X^m) div (g * X^m) =
-          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*X^m))*X^m)"
+  have "(f * fps_X^m) div (g * fps_X^m) =
+          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
     by (simp add: fps_divide_def Let_def algebra_simps)
   also have "... = f div g"
-    by (simp add: fps_shift_times_X_power'' fps_divide_def Let_def)
+    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
   finally show ?thesis .
 qed (simp_all add: fps_divide_def)
 
@@ -1272,11 +1272,11 @@
       with nz show ?thesis by (simp add: fps_mod_eq_zero fps_times_divide_eq)
     next
       assume "subdegree f < subdegree g"
-      have g_decomp: "g = h * X^n" unfolding h_def n_def by (rule subdegree_decompose)
+      have g_decomp: "g = h * fps_X^n" unfolding h_def n_def by (rule subdegree_decompose)
       have "f div g * g + f mod g =
               fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h"
         by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def)
-      also have "... = h * (fps_shift n (f * inverse h) * X^n + fps_cutoff n (f * inverse h))"
+      also have "... = h * (fps_shift n (f * inverse h) * fps_X^n + fps_cutoff n (f * inverse h))"
         by (subst g_decomp) (simp add: algebra_simps)
       also have "... = f * (inverse h * h)"
         by (subst fps_shift_cutoff) simp
@@ -1292,9 +1292,9 @@
   proof -
     define m where "m = subdegree h"
     define h' where "h' = fps_shift m h"
-    have h_decomp: "h = h' * X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
+    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
     from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
-    have "(h * f) div (h * g) = (h' * f * X^m) div (h' * g * X^m)"
+    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
       by (simp add: h_decomp algebra_simps)
     also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
     finally show ?thesis .
@@ -1306,10 +1306,10 @@
   define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
   have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
     by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add)
-  also have "h * inverse h' = (inverse h' * h') * X^n"
+  also have "h * inverse h' = (inverse h' * h') * fps_X^n"
     by (subst subdegree_decompose) (simp_all add: dfs)
-  also have "... = X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
-  also have "fps_shift n (g * X^n) = g" by simp
+  also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
+  also have "fps_shift n (g * fps_X^n) = g" by simp
   also have "fps_shift n (f * inverse h') = f div h"
     by (simp add: fps_divide_def Let_def dfs)
   finally show "(f + g * h) div h = g + f div h" by simp
@@ -1354,14 +1354,14 @@
 qed (simp add: assms dvd_imp_subdegree_le)
 
 lemma fps_shift_altdef:
-  "fps_shift n f = (f :: 'a :: field fps) div X^n"
+  "fps_shift n f = (f :: 'a :: field fps) div fps_X^n"
   by (simp add: fps_divide_def)
   
-lemma fps_div_X_power_nth: "((f :: 'a :: field fps) div X^n) $ k = f $ (k + n)"
+lemma fps_div_fps_X_power_nth: "((f :: 'a :: field fps) div fps_X^n) $ k = f $ (k + n)"
   by (simp add: fps_shift_altdef [symmetric])
 
-lemma fps_div_X_nth: "((f :: 'a :: field fps) div X) $ k = f $ Suc k"
-  using fps_div_X_power_nth[of f 1] by simp
+lemma fps_div_fps_X_nth: "((f :: 'a :: field fps) div fps_X) $ k = f $ Suc k"
+  using fps_div_fps_X_power_nth[of f 1] by simp
 
 lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
   by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff)
@@ -1419,45 +1419,45 @@
 
 lemma fps_gcd:
   assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
-  shows   "gcd f g = X ^ min (subdegree f) (subdegree g)"
+  shows   "gcd f g = fps_X ^ min (subdegree f) (subdegree g)"
 proof -
   let ?m = "min (subdegree f) (subdegree g)"
-  show "gcd f g = X ^ ?m"
+  show "gcd f g = fps_X ^ ?m"
   proof (rule sym, rule gcdI)
     fix d assume "d dvd f" "d dvd g"
-    thus "d dvd X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff)
+    thus "d dvd fps_X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff)
   qed (simp_all add: fps_dvd_iff)
 qed
 
 lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g =
   (if f = 0 \<and> g = 0 then 0 else
-   if f = 0 then X ^ subdegree g else
-   if g = 0 then X ^ subdegree f else
-     X ^ min (subdegree f) (subdegree g))"
+   if f = 0 then fps_X ^ subdegree g else
+   if g = 0 then fps_X ^ subdegree f else
+     fps_X ^ min (subdegree f) (subdegree g))"
   by (simp add: fps_gcd)
 
 lemma fps_lcm:
   assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
-  shows   "lcm f g = X ^ max (subdegree f) (subdegree g)"
+  shows   "lcm f g = fps_X ^ max (subdegree f) (subdegree g)"
 proof -
   let ?m = "max (subdegree f) (subdegree g)"
-  show "lcm f g = X ^ ?m"
+  show "lcm f g = fps_X ^ ?m"
   proof (rule sym, rule lcmI)
     fix d assume "f dvd d" "g dvd d"
-    thus "X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff)
+    thus "fps_X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff)
   qed (simp_all add: fps_dvd_iff)
 qed
 
 lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g =
-  (if f = 0 \<or> g = 0 then 0 else X ^ max (subdegree f) (subdegree g))"
+  (if f = 0 \<or> g = 0 then 0 else fps_X ^ max (subdegree f) (subdegree g))"
   by (simp add: fps_lcm)
 
 lemma fps_Gcd:
   assumes "A - {0} \<noteq> {}"
-  shows   "Gcd A = X ^ (INF f:A-{0}. subdegree f)"
+  shows   "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)"
 proof (rule sym, rule GcdI)
   fix f assume "f \<in> A"
-  thus "X ^ (INF f:A - {0}. subdegree f) dvd f"
+  thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f"
     by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower)
 next
   fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f"
@@ -1465,25 +1465,25 @@
   with d[of f] have [simp]: "d \<noteq> 0" by auto
   from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)"
     by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric])
-  with d assms show "d dvd X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
+  with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
 qed simp_all
 
 lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
-  (if A \<subseteq> {0} then 0 else X ^ (INF f:A-{0}. subdegree f))"
+  (if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))"
   using fps_Gcd by auto
 
 lemma fps_Lcm:
   assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)"
-  shows   "Lcm A = X ^ (SUP f:A. subdegree f)"
+  shows   "Lcm A = fps_X ^ (SUP f:A. subdegree f)"
 proof (rule sym, rule LcmI)
   fix f assume "f \<in> A"
   moreover from assms(3) have "bdd_above (subdegree ` A)" by auto
-  ultimately show "f dvd X ^ (SUP f:A. subdegree f)" using assms(2)
+  ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2)
     by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper)
 next
   fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d"
   from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto
-  show "X ^ (SUP f:A. subdegree f) dvd d"
+  show "fps_X ^ (SUP f:A. subdegree f) dvd d"
   proof (cases "d = 0")
     assume "d \<noteq> 0"
     moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast
@@ -1496,7 +1496,7 @@
 lemma fps_Lcm_altdef:
   "Lcm (A :: 'a :: field fps set) =
      (if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
-      if A = {} then 1 else X ^ (SUP f:A. subdegree f))"
+      if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))"
 proof (cases "bdd_above (subdegree`A)")
   assume unbounded: "\<not>bdd_above (subdegree`A)"
   have "Lcm A = 0"
@@ -1568,8 +1568,8 @@
     unfolding fps_eq_iff by auto
 qed
 
-lemma fps_deriv_X[simp]: "fps_deriv X = 1"
-  by (simp add: fps_deriv_def X_def fps_eq_iff)
+lemma fps_deriv_fps_X[simp]: "fps_deriv fps_X = 1"
+  by (simp add: fps_deriv_def fps_X_def fps_eq_iff)
 
 lemma fps_deriv_neg[simp]:
   "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)"
@@ -1878,7 +1878,7 @@
 lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f"
   by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse)
 
-(* FIXME: The last part of this proof should go through by simp once we have a proper
+(* FIfps_XME: The last part of this proof should go through by simp once we have a proper
    theorem collection for simplifying division on rings *)
 lemma fps_divide_deriv:
   assumes "b dvd (a :: 'a :: field fps)"
@@ -1893,28 +1893,28 @@
   thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp)
 qed
 
-lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
-  by (simp add: fps_inverse_gp fps_eq_iff X_def)
-
-lemma fps_one_over_one_minus_X_squared:
-  "inverse ((1 - X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
+lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - fps_X"
+  by (simp add: fps_inverse_gp fps_eq_iff fps_X_def)
+
+lemma fps_one_over_one_minus_fps_X_squared:
+  "inverse ((1 - fps_X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
 proof -
-  have "inverse ((1 - X)^2 :: 'a fps) = fps_deriv (inverse (1 - X))"
+  have "inverse ((1 - fps_X)^2 :: 'a fps) = fps_deriv (inverse (1 - fps_X))"
     by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power)
-  also have "inverse (1 - X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
+  also have "inverse (1 - fps_X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
     by (subst fps_inverse_gp' [symmetric]) simp
   also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))"
     by (simp add: fps_deriv_def)
   finally show ?thesis .
 qed
 
-lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
+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)"
   by (cases n) simp_all
 
-lemma fps_inverse_X_plus1: "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)"
+lemma fps_inverse_fps_X_plus1: "inverse (1 + fps_X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)"
   (is "_ = ?r")
 proof -
-  have eq: "(1 + X) * ?r = 1"
+  have eq: "(1 + fps_X) * ?r = 1"
     unfolding minus_one_power_iff
     by (auto simp add: field_simps fps_eq_iff)
   show ?thesis
@@ -1956,7 +1956,7 @@
 lemma fps_compose_nth_0 [simp]: "(f oo g) $ 0 = f $ 0"
   by (simp add: fps_compose_nth)
 
-lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)"
+lemma fps_compose_fps_X[simp]: "a oo fps_X = (a :: 'a::comm_ring_1 fps)"
   by (simp add: fps_ext fps_compose_def mult_delta_right sum.delta')
 
 lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a"
@@ -1968,7 +1968,7 @@
 lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k"
   unfolding neg_numeral_fps_const by simp
 
-lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: 'a::comm_ring_1 fps)"
+lemma fps_X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> fps_X oo a = (a :: 'a::comm_ring_1 fps)"
   by (simp add: fps_eq_iff fps_compose_def mult_delta_left sum.delta not_le)
 
 
@@ -1978,14 +1978,14 @@
   (* {a_{n+k}}_0^infty Corresponds to (f - sum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
 
 lemma fps_power_mult_eq_shift:
-  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
-    Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}"
+  "fps_X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
+    Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * fps_X^i) {0 .. k}"
   (is "?lhs = ?rhs")
 proof -
   have "?lhs $ n = ?rhs $ n" for n :: nat
   proof -
     have "?lhs $ n = (if n < Suc k then 0 else a n)"
-      unfolding X_power_mult_nth by auto
+      unfolding fps_X_power_mult_nth by auto
     also have "\<dots> = ?rhs $ n"
     proof (induct k)
       case 0
@@ -1993,14 +1993,14 @@
         by (simp add: fps_sum_nth)
     next
       case (Suc k)
-      have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n =
-        (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} -
-          fps_const (a (Suc k)) * X^ Suc k) $ n"
+      have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. Suc k})$n =
+        (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. k} -
+          fps_const (a (Suc k)) * fps_X^ Suc k) $ n"
         by (simp add: field_simps)
-      also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n"
+      also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * fps_X^ Suc k)$n"
         using Suc.hyps[symmetric] unfolding fps_sub_nth by simp
       also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)"
-        unfolding X_power_mult_right_nth
+        unfolding fps_X_power_mult_right_nth
         apply (auto simp add: not_less fps_const_def)
         apply (rule cong[of a a, OF refl])
         apply arith
@@ -2021,29 +2021,29 @@
   (* If f reprents {a_n} and P is a polynomial, then
         P(xD) f represents {P(n) a_n}*)
 
-definition "XD = op * X \<circ> fps_deriv"
-
-lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: 'a::comm_ring_1 fps)"
-  by (simp add: XD_def field_simps)
-
-lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
-  by (simp add: XD_def field_simps)
-
-lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) =
-    fps_const c * XD a + fps_const d * XD (b :: 'a::comm_ring_1 fps)"
+definition "fps_XD = op * fps_X \<circ> fps_deriv"
+
+lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
+  by (simp add: fps_XD_def field_simps)
+
+lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a"
+  by (simp add: fps_XD_def field_simps)
+
+lemma fps_XD_linear[simp]: "fps_XD (fps_const c * a + fps_const d * b) =
+    fps_const c * fps_XD a + fps_const d * fps_XD (b :: 'a::comm_ring_1 fps)"
   by simp
 
-lemma XDN_linear:
-  "(XD ^^ n) (fps_const c * a + fps_const d * b) =
-    fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: 'a::comm_ring_1 fps)"
+lemma fps_XDN_linear:
+  "(fps_XD ^^ n) (fps_const c * a + fps_const d * b) =
+    fps_const c * (fps_XD ^^ n) a + fps_const d * (fps_XD ^^ n) (b :: 'a::comm_ring_1 fps)"
   by (induct n) simp_all
 
-lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
+lemma fps_mult_fps_X_deriv_shift: "fps_X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
   by (simp add: fps_eq_iff)
 
-lemma fps_mult_XD_shift:
-  "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
-  by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def)
+lemma fps_mult_fps_XD_shift:
+  "(fps_XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+  by (induct k arbitrary: a) (simp_all add: fps_XD_def fps_eq_iff field_simps del: One_nat_def)
 
 
 subsubsection \<open>Rule 3\<close>
@@ -2051,15 +2051,15 @@
 text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
 
 
-subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close>
-
-lemma fps_divide_X_minus1_sum_lemma:
-  "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
+subsubsection \<open>Rule 5 --- summation and "division" by (1 - fps_X)\<close>
+
+lemma fps_divide_fps_X_minus1_sum_lemma:
+  "a = ((1::'a::comm_ring_1 fps) - fps_X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
 proof -
   let ?sa = "Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
-  have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
+  have th0: "\<And>i. (1 - (fps_X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
     by simp
-  have "a$n = ((1 - X) * ?sa) $ n" for n
+  have "a$n = ((1 - fps_X) * ?sa) $ n" for n
   proof (cases "n = 0")
     case True
     then show ?thesis
@@ -2073,7 +2073,7 @@
       using False by simp_all
     have f: "finite {0}" "finite {1}" "finite {2 .. n}"
       "finite {0 .. n - 1}" "finite {n}" by simp_all
-    have "((1 - X) * ?sa) $ n = sum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}"
+    have "((1 - fps_X) * ?sa) $ n = sum (\<lambda>i. (1 - fps_X)$ i * ?sa $ (n - i)) {0 .. n}"
       by (simp add: fps_mult_nth)
     also have "\<dots> = a$n"
       unfolding th0
@@ -2090,16 +2090,16 @@
     unfolding fps_eq_iff by blast
 qed
 
-lemma fps_divide_X_minus1_sum:
-  "a /((1::'a::field fps) - X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
+lemma fps_divide_fps_X_minus1_sum:
+  "a /((1::'a::field fps) - fps_X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
 proof -
-  let ?X = "1 - (X::'a fps)"
-  have th0: "?X $ 0 \<noteq> 0"
+  let ?fps_X = "1 - (fps_X::'a fps)"
+  have th0: "?fps_X $ 0 \<noteq> 0"
     by simp
-  have "a /?X = ?X *  Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?X"
-    using fps_divide_X_minus1_sum_lemma[of a, symmetric] th0
+  have "a /?fps_X = ?fps_X *  Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?fps_X"
+    using fps_divide_fps_X_minus1_sum_lemma[of a, symmetric] th0
     by (simp add: fps_divide_def mult.assoc)
-  also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) "
+  also have "\<dots> = (inverse ?fps_X * ?fps_X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) "
     by (simp add: ac_simps)
   finally show ?thesis
     by (simp add: inverse_mult_eq_1[OF th0])
@@ -2495,10 +2495,10 @@
   also have "subdegree \<dots> = Suc m * subdegree g" by (rule subdegree_power)
   finally have [simp]: "subdegree f = subdegree g"
     by (subst (asm) Suc_mult_cancel1)
-  have "fps_shift (subdegree f) f * X ^ subdegree f = f"
+  have "fps_shift (subdegree f) f * fps_X ^ subdegree f = f"
     by (rule subdegree_decompose [symmetric])
   also have "\<dots> ^ Suc m = g ^ Suc m" by fact
-  also have "g = fps_shift (subdegree g) g * X ^ subdegree g"
+  also have "g = fps_shift (subdegree g) g * fps_X ^ subdegree g"
     by (rule subdegree_decompose)
   also have "subdegree f = subdegree g" by fact
   finally have "fps_shift (subdegree g) f ^ Suc m = fps_shift (subdegree g) g ^ Suc m"
@@ -3127,17 +3127,17 @@
   then show ?thesis by (simp add: fps_eq_iff)
 qed
 
-lemma fps_mult_X_plus_1_nth:
-  "((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
+lemma fps_mult_fps_X_plus_1_nth:
+  "((1+fps_X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
 proof (cases n)
   case 0
   then show ?thesis
     by (simp add: fps_mult_nth)
 next
   case (Suc m)
-  have "((1 + X)*a) $ n = sum (\<lambda>i. (1 + X) $ i * a $ (n - i)) {0..n}"
+  have "((1 + fps_X)*a) $ n = sum (\<lambda>i. (1 + fps_X) $ i * a $ (n - i)) {0..n}"
     by (simp add: fps_mult_nth)
-  also have "\<dots> = sum (\<lambda>i. (1+X)$i * a$(n-i)) {0.. 1}"
+  also have "\<dots> = sum (\<lambda>i. (1+fps_X)$i * a$(n-i)) {0.. 1}"
     unfolding Suc by (rule sum.mono_neutral_right) auto
   also have "\<dots> = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
     by (simp add: Suc)
@@ -3145,14 +3145,14 @@
 qed
 
 
-subsection \<open>Finite FPS (i.e. polynomials) and X\<close>
-
-lemma fps_poly_sum_X:
+subsection \<open>Finite FPS (i.e. polynomials) and fps_X\<close>
+
+lemma fps_poly_sum_fps_X:
   assumes "\<forall>i > n. a$i = (0::'a::comm_ring_1)"
-  shows "a = sum (\<lambda>i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r")
+  shows "a = sum (\<lambda>i. fps_const (a$i) * fps_X^i) {0..n}" (is "a = ?r")
 proof -
   have "a$i = ?r$i" for i
-    unfolding fps_sum_nth fps_mult_left_const_nth X_power_nth
+    unfolding fps_sum_nth fps_mult_left_const_nth fps_X_power_nth
     by (simp add: mult_delta_right sum.delta' assms)
   then show ?thesis
     unfolding fps_eq_iff by blast
@@ -3163,23 +3163,23 @@
 
 fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
 where
-  "compinv a 0 = X$0"
+  "compinv a 0 = fps_X$0"
 | "compinv a (Suc n) =
-    (X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
+    (fps_X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
 
 definition "fps_inv a = Abs_fps (compinv a)"
 
 lemma fps_inv:
   assumes a0: "a$0 = 0"
     and a1: "a$1 \<noteq> 0"
-  shows "fps_inv a oo a = X"
+  shows "fps_inv a oo a = fps_X"
 proof -
   let ?i = "fps_inv a oo a"
-  have "?i $n = X$n" for n
+  have "?i $n = fps_X$n" for n
   proof (induct n rule: nat_less_induct)
     fix n
-    assume h: "\<forall>m<n. ?i$m = X$m"
-    show "?i $ n = X$n"
+    assume h: "\<forall>m<n. ?i$m = fps_X$m"
+    show "?i $ n = fps_X$n"
     proof (cases n)
       case 0
       then show ?thesis using a0
@@ -3189,9 +3189,9 @@
       have "?i $ n = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
         by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc)
       also have "\<dots> = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
-        (X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
+        (fps_X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
         using a0 a1 Suc by (simp add: fps_inv_def)
-      also have "\<dots> = X$n" using Suc by simp
+      also have "\<dots> = fps_X$n" using Suc by simp
       finally show ?thesis .
     qed
   qed
@@ -3238,7 +3238,7 @@
     by (simp add: fps_eq_iff)
 qed
 
-lemma fps_inv_ginv: "fps_inv = fps_ginv X"
+lemma fps_inv_ginv: "fps_inv = fps_ginv fps_X"
   apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
   apply (induct_tac n rule: nat_less_induct)
   apply auto
@@ -3427,7 +3427,7 @@
 lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
 
-lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
+lemma fps_X_fps_compose: "fps_X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta)
 
 lemma fps_inverse_compose:
@@ -3463,16 +3463,16 @@
     (is "?one oo a = _")
 proof -
   have o0: "?one $ 0 \<noteq> 0" by simp
-  have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp
+  have th0: "(1 - fps_X) $ 0 \<noteq> (0::'a)" by simp
   from fps_inverse_gp[where ?'a = 'a]
-  have "inverse ?one = 1 - X" by (simp add: fps_eq_iff)
-  then have "inverse (inverse ?one) = inverse (1 - X)" by simp
-  then have th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0]
+  have "inverse ?one = 1 - fps_X" by (simp add: fps_eq_iff)
+  then have "inverse (inverse ?one) = inverse (1 - fps_X)" by simp
+  then have th: "?one = 1/(1 - fps_X)" unfolding fps_inverse_idempotent[OF o0]
     by (simp add: fps_divide_def)
   show ?thesis
     unfolding th
     unfolding fps_divide_compose[OF a0 th0]
-    fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] ..
+    fps_compose_1 fps_compose_sub_distrib fps_X_fps_compose_startby0[OF a0] ..
 qed
 
 lemma fps_const_power [simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
@@ -3535,7 +3535,7 @@
 
 lemma fps_X_power_compose:
   assumes a0: "a$0=0"
-  shows "X^k oo a = (a::'a::idom fps)^k"
+  shows "fps_X^k oo a = (a::'a::idom fps)^k"
   (is "?l = ?r")
 proof (cases k)
   case 0
@@ -3564,7 +3564,7 @@
 lemma fps_inv_right:
   assumes a0: "a$0 = 0"
     and a1: "a$1 \<noteq> 0"
-  shows "a oo fps_inv a = X"
+  shows "a oo fps_inv a = fps_X"
 proof -
   let ?ia = "fps_inv a"
   let ?iaa = "a oo fps_inv a"
@@ -3572,12 +3572,12 @@
     by (simp add: fps_inv_def)
   have th1: "?iaa $ 0 = 0"
     using a0 a1 by (simp add: fps_inv_def fps_compose_nth)
-  have th2: "X$0 = 0"
+  have th2: "fps_X$0 = 0"
     by simp
-  from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X"
+  from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo fps_X"
     by simp
-  then have "(a oo fps_inv a) oo a = X oo a"
-    by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0])
+  then have "(a oo fps_inv a) oo a = fps_X oo a"
+    by (simp add: fps_compose_assoc[OF a0 th0] fps_X_fps_compose_startby0[OF a0])
   with fps_compose_inj_right[OF a0 a1] show ?thesis
     by simp
 qed
@@ -3612,13 +3612,13 @@
     by (simp add: fps_inv_def)
   from a1 have ra1: "?r a $ 1 \<noteq> 0"
     by (simp add: fps_inv_def field_simps)
-  have X0: "X$0 = 0"
+  have fps_X0: "fps_X$0 = 0"
     by simp
-  from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
-  then have "?r (?r a) oo ?r a oo a = X oo a"
+  from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = fps_X" .
+  then have "?r (?r a) oo ?r a oo a = fps_X oo a"
     by simp
   then have "?r (?r a) oo (?r a oo a) = a"
-    unfolding X_fps_compose_startby0[OF a0]
+    unfolding fps_X_fps_compose_startby0[OF a0]
     unfolding fps_compose_assoc[OF a0 ra0, symmetric] .
   then show ?thesis
     unfolding fps_inv[OF a0 a1] by simp
@@ -3661,13 +3661,13 @@
 lemma fps_ginv_deriv:
   assumes a0:"a$0 = (0::'a::field)"
     and a1: "a$1 \<noteq> 0"
-  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
+  shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv fps_X a"
 proof -
   let ?ia = "fps_ginv b a"
-  let ?iXa = "fps_ginv X a"
+  let ?ifps_Xa = "fps_ginv fps_X a"
   let ?d = "fps_deriv"
   let ?dia = "?d ?ia"
-  have iXa0: "?iXa $ 0 = 0"
+  have ifps_Xa0: "?ifps_Xa $ 0 = 0"
     by (simp add: fps_ginv_def)
   have da0: "?d a $ 0 \<noteq> 0"
     using a1 by simp
@@ -3679,21 +3679,21 @@
     by simp
   with a1 have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a"
     by (simp add: fps_divide_unit)
-  then have "(?d ?ia oo a) oo ?iXa =  (?d b / ?d a) oo ?iXa"
+  then have "(?d ?ia oo a) oo ?ifps_Xa =  (?d b / ?d a) oo ?ifps_Xa"
     unfolding inverse_mult_eq_1[OF da0] by simp
-  then have "?d ?ia oo (a oo ?iXa) =  (?d b / ?d a) oo ?iXa"
-    unfolding fps_compose_assoc[OF iXa0 a0] .
+  then have "?d ?ia oo (a oo ?ifps_Xa) =  (?d b / ?d a) oo ?ifps_Xa"
+    unfolding fps_compose_assoc[OF ifps_Xa0 a0] .
   then show ?thesis unfolding fps_inv_ginv[symmetric]
     unfolding fps_inv_right[OF a0 a1] by simp
 qed
 
 lemma fps_compose_linear:
-  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)"
+  "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * fps_X) = Abs_fps (\<lambda>n. c^n * f $ n)"
   by (simp add: fps_eq_iff fps_compose_def power_mult_distrib
                 if_distrib sum.delta' cong: if_cong)
               
 lemma fps_compose_uminus': 
-  "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
+  "fps_compose f (-fps_X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
   using fps_compose_linear[of f "-1"] 
   by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp
 
@@ -3768,21 +3768,21 @@
   "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)"
   by (induct n) auto
 
-lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1"
-  by (simp add: fps_eq_iff X_fps_compose)
+lemma fps_X_compose_fps_exp[simp]: "fps_X oo fps_exp (a::'a::field) = fps_exp a - 1"
+  by (simp add: fps_eq_iff fps_X_fps_compose)
 
 lemma fps_inv_fps_exp_compose:
   assumes a: "a \<noteq> 0"
-  shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X"
-    and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X"
+  shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X"
+    and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X"
 proof -
   let ?b = "fps_exp a - 1"
   have b0: "?b $ 0 = 0"
     by simp
   have b1: "?b $ 1 \<noteq> 0"
     by (simp add: a)
-  from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" .
-  from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" .
+  from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X" .
+  from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X" .
 qed
 
 lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)"
@@ -3804,11 +3804,11 @@
 qed
 
 lemma fps_exp_compose_linear [simp]: 
-  "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)"
+  "fps_exp (d::'a::field_char_0) oo (fps_const c * fps_X) = fps_exp (c * d)"
   by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib)
   
 lemma fps_fps_exp_compose_minus [simp]: 
-  "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)"
+  "fps_compose (fps_exp c) (-fps_X) = fps_exp (-c :: 'a :: field_char_0)"
   using fps_exp_compose_linear[of c "-1 :: 'a"] 
   unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp
 
@@ -3844,14 +3844,14 @@
 
 lemma Abs_fps_if_0:
   "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) =
-    fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
+    fps_const v + fps_X * Abs_fps (\<lambda>n. f (Suc n))"
   by (auto simp add: fps_eq_iff)
 
 definition fps_ln :: "'a::field_char_0 \<Rightarrow> 'a fps"
   where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
 
-lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)"
-  unfolding fps_inverse_X_plus1
+lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + fps_X)"
+  unfolding fps_inverse_fps_X_plus1
   by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc)
 
 lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
@@ -3870,13 +3870,13 @@
   have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) =
     (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)"
     by (simp add: field_simps)
-  also have "\<dots> = fps_const a * (X + 1)"
+  also have "\<dots> = fps_const a * (fps_X + 1)"
     apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
     apply (simp add: field_simps)
     done
-  finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" .
+  finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (fps_X + 1)" .
   from fps_inv_deriv[OF b0 b1, unfolded eq]
-  have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
+  have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (fps_X + 1)"
     using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
   then have "fps_deriv ?l = fps_deriv ?r"
     by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse)
@@ -3891,7 +3891,7 @@
   (is "?r = ?l")
 proof-
   from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
-  have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
+  have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + fps_X)"
     by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add)
   also have "\<dots> = fps_deriv ?l"
     apply (simp add: fps_ln_deriv)
@@ -3901,9 +3901,9 @@
     unfolding fps_deriv_eq_iff by simp
 qed
 
-lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c"
+lemma fps_X_dvd_fps_ln [simp]: "fps_X dvd fps_ln c"
 proof -
-  have "fps_ln c = X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
+  have "fps_ln c = fps_X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))"
     by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff)
   thus ?thesis by simp
 qed
@@ -3918,11 +3918,11 @@
 
 lemma fps_binomial_ODE_unique:
   fixes c :: "'a::field_char_0"
-  shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
+  shows "fps_deriv a = (fps_const c * a) / (1 + fps_X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   let ?da = "fps_deriv a"
-  let ?x1 = "(1 + X):: 'a fps"
+  let ?x1 = "(1 + fps_X):: 'a fps"
   let ?l = "?x1 * ?da"
   let ?r = "fps_const c * a"
 
@@ -3985,10 +3985,10 @@
 qed
 
 lemma fps_binomial_ODE_unique':
-  "(fps_deriv a = fps_const c * a / (1 + X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
+  "(fps_deriv a = fps_const c * a / (1 + fps_X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)"
   by (subst fps_binomial_ODE_unique) auto
 
-lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)"
+lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + fps_X)"
 proof -
   let ?a = "fps_binomial c"
   have th0: "?a = fps_const (?a$0) * ?a" by (simp)
@@ -4001,13 +4001,13 @@
   let ?b = "fps_binomial"
   let ?db = "\<lambda>x. fps_deriv (?b x)"
   have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)"  by simp
-  also have "\<dots> = inverse (1 + X) *
+  also have "\<dots> = inverse (1 + fps_X) *
       (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))"
     unfolding fps_binomial_deriv
     by (simp add: fps_divide_def field_simps)
-  also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P"
+  also have "\<dots> = (fps_const (c + d)/ (1 + fps_X)) * ?P"
     by (simp add: field_simps fps_divide_unit fps_const_add[symmetric] del: fps_const_add)
-  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)"
+  finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + fps_X)"
     by (simp add: fps_divide_def)
   have "?P = fps_const (?P$0) * ?b (c + d)"
     unfolding fps_binomial_ODE_unique[symmetric]
@@ -4016,35 +4016,35 @@
   then show ?thesis by simp
 qed
 
-lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
+lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + fps_X)"
   (is "?l = inverse ?r")
 proof-
   have th: "?r$0 \<noteq> 0" by simp
-  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)"
+  have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + fps_X)"
     by (simp add: fps_inverse_deriv[OF th] fps_divide_def
       power2_eq_square mult.commute fps_const_neg[symmetric] del: fps_const_neg)
   have eq: "inverse ?r $ 0 = 1"
     by (simp add: fps_inverse_def)
-  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq
+  from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + fps_X)" "- 1"] th'] eq
   show ?thesis by (simp add: fps_inverse_def)
 qed
 
-lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + X :: 'a :: field_char_0 fps) ^ n"
+lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + fps_X :: 'a :: field_char_0 fps) ^ n"
 proof (cases "n = 0")
   case [simp]: True
-  have "fps_deriv ((1 + X) ^ n :: 'a fps) = 0" by simp
-  also have "\<dots> = fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" by (simp add: fps_binomial_def)
+  have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = 0" by simp
+  also have "\<dots> = fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)" by (simp add: fps_binomial_def)
   finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) simp_all
 next
   case False
-  have "fps_deriv ((1 + X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + X) ^ (n - 1)"
+  have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + fps_X) ^ (n - 1)"
     by (simp add: fps_deriv_power)
-  also have "(1 + X :: 'a fps) $ 0 \<noteq> 0" by simp
-  hence "(1 + X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
-  with False have "(1 + X :: 'a fps) ^ (n - 1) = (1 + X) ^ n / (1 + X)"
+  also have "(1 + fps_X :: 'a fps) $ 0 \<noteq> 0" by simp
+  hence "(1 + fps_X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp)
+  with False have "(1 + fps_X :: 'a fps) ^ (n - 1) = (1 + fps_X) ^ n / (1 + fps_X)"
     by (cases n) (simp_all )
-  also have "fps_const (of_nat n :: 'a) * ((1 + X) ^ n / (1 + X)) =
-               fps_const (of_nat n) * (1 + X) ^ n / (1 + X)"
+  also have "fps_const (of_nat n :: 'a) * ((1 + fps_X) ^ n / (1 + fps_X)) =
+               fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)"
     by (simp add: unit_div_mult_swap)
   finally show ?thesis
     by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) (simp_all add: fps_power_nth)
@@ -4056,24 +4056,24 @@
 lemma fps_binomial_power: "fps_binomial a ^ n = fps_binomial (of_nat n * a)"
   by (induction n) (simp_all add: fps_binomial_add_mult ring_distribs)
 
-lemma fps_binomial_1: "fps_binomial 1 = 1 + X"
+lemma fps_binomial_1: "fps_binomial 1 = 1 + fps_X"
   using fps_binomial_of_nat[of 1] by simp
 
 lemma fps_binomial_minus_of_nat:
-  "fps_binomial (- of_nat n) = inverse ((1 + X :: 'a :: field_char_0 fps) ^ n)"
+  "fps_binomial (- of_nat n) = inverse ((1 + fps_X :: 'a :: field_char_0 fps) ^ n)"
   by (rule sym, rule fps_inverse_unique)
      (simp add: fps_binomial_of_nat [symmetric] fps_binomial_add_mult [symmetric])
 
-lemma one_minus_const_X_power:
-  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * X) ^ n =
-     fps_compose (fps_binomial (of_nat n)) (-fps_const c * X)"
+lemma one_minus_const_fps_X_power:
+  "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * fps_X) ^ n =
+     fps_compose (fps_binomial (of_nat n)) (-fps_const c * fps_X)"
   by (subst fps_binomial_of_nat)
      (simp add: fps_compose_power [symmetric] fps_compose_add_distrib fps_const_neg [symmetric] 
            del: fps_const_neg)
 
-lemma one_minus_X_const_neg_power:
-  "inverse ((1 - fps_const c * X) ^ n) = 
-       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * X)"
+lemma one_minus_fps_X_const_neg_power:
+  "inverse ((1 - fps_const c * fps_X) ^ n) = 
+       fps_compose (fps_binomial (-of_nat n)) (-fps_const c * fps_X)"
 proof (cases "c = 0")
   case False
   thus ?thesis
@@ -4082,17 +4082,17 @@
                 fps_const_neg [symmetric] del: fps_const_neg)
 qed simp
 
-lemma X_plus_const_power:
-  "c \<noteq> 0 \<Longrightarrow> (X + fps_const c) ^ n =
-     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * X)"
+lemma fps_X_plus_const_power:
+  "c \<noteq> 0 \<Longrightarrow> (fps_X + fps_const c) ^ n =
+     fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * fps_X)"
   by (subst fps_binomial_of_nat)
      (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
                 fps_const_power [symmetric] power_mult_distrib [symmetric] 
                 algebra_simps inverse_mult_eq_1' del: fps_const_power)
 
-lemma X_plus_const_neg_power:
-  "c \<noteq> 0 \<Longrightarrow> inverse ((X + fps_const c) ^ n) =
-     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * X)"
+lemma fps_X_plus_const_neg_power:
+  "c \<noteq> 0 \<Longrightarrow> inverse ((fps_X + fps_const c) ^ n) =
+     fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * fps_X)"
   by (subst fps_binomial_minus_of_nat)
      (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib
                 fps_const_power [symmetric] power_mult_distrib [symmetric] fps_inverse_compose 
@@ -4101,11 +4101,11 @@
            del: fps_const_power)
 
 
-lemma one_minus_const_X_neg_power':
-  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * X) ^ n) =
+lemma one_minus_const_fps_X_neg_power':
+  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * fps_X) ^ n) =
        Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
   apply (rule fps_ext)
-  apply (subst one_minus_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
+  apply (subst one_minus_fps_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
   apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] 
                    gbinomial_minus binomial_gbinomial of_nat_diff)
   done
@@ -4546,7 +4546,7 @@
   by (simp add: fps_of_int [symmetric])
 
 lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
-  by (fact numeral_fps_const) (* FIXME: duplicate *)
+  by (fact numeral_fps_const) (* FIfps_XME: duplicate *)
 
 lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * c)) / fps_const 2"
 proof -
@@ -4610,10 +4610,10 @@
 lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c"
   by (simp add: fps_eq_iff)
 
-lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)"
+lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * fps_X)"
 proof -
-  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
-  have th0: "(fps_const c * X) $ 0 = 0" by simp
+  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * fps_X)"
+  have th0: "(fps_const c * fps_X) $ 0 = 0" by simp
   show ?thesis unfolding gp[OF th0, symmetric]
     by (auto simp add: fps_eq_iff pochhammer_fact[symmetric]
       fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong)
@@ -4645,26 +4645,26 @@
   apply (simp add: algebra_simps)
   done
 
-lemma XD_nth[simp]: "XD a $ n = (if n = 0 then 0 else of_nat n * a$n)"
-  by (simp add: XD_def)
-
-lemma XD_0th[simp]: "XD a $ 0 = 0"
+lemma fps_XD_nth[simp]: "fps_XD a $ n = (if n = 0 then 0 else of_nat n * a$n)"
+  by (simp add: fps_XD_def)
+
+lemma fps_XD_0th[simp]: "fps_XD a $ 0 = 0"
   by simp
-lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n"
+lemma fps_XD_Suc[simp]:" fps_XD a $ Suc n = of_nat (Suc n) * a $ Suc n"
   by simp
 
-definition "XDp c a = XD a + fps_const c * a"
-
-lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
-  by (simp add: XDp_def algebra_simps)
-
-lemma XDp_commute: "XDp b \<circ> XDp (c::'a::comm_ring_1) = XDp c \<circ> XDp b"
-  by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps)
-
-lemma XDp0 [simp]: "XDp 0 = XD"
+definition "fps_XDp c a = fps_XD a + fps_const c * a"
+
+lemma fps_XDp_nth[simp]: "fps_XDp c a $ n = (c + of_nat n) * a$n"
+  by (simp add: fps_XDp_def algebra_simps)
+
+lemma fps_XDp_commute: "fps_XDp b \<circ> fps_XDp (c::'a::comm_ring_1) = fps_XDp c \<circ> fps_XDp b"
+  by (auto simp add: fps_XDp_def fun_eq_iff fps_eq_iff algebra_simps)
+
+lemma fps_XDp0 [simp]: "fps_XDp 0 = fps_XD"
   by (simp add: fun_eq_iff fps_eq_iff)
 
-lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a"
+lemma fps_XDp_fps_integral [simp]: "fps_XDp 0 (fps_integral a c) = fps_X * a"
   by (simp add: fps_eq_iff fps_integral_def)
 
 lemma fps_hypergeo_minus_nat:
@@ -4687,11 +4687,11 @@
 lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
   by (cases n) (simp_all add: pochhammer_rec)
 
-lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c \<circ> r) cs (\<lambda>c. XDp c a) c0 $ n =
+lemma fps_XDp_foldr_nth [simp]: "foldr (\<lambda>c r. fps_XDp c \<circ> r) cs (\<lambda>c. fps_XDp c a) c0 $ n =
     foldr (\<lambda>c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
   by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
 
-lemma genric_XDp_foldr_nth:
+lemma genric_fps_XDp_foldr_nth:
   assumes f: "\<forall>n c a. f c a $ n = (of_nat n + k c) * a$n"
   shows "foldr (\<lambda>c r. f c \<circ> r) cs (\<lambda>c. g c a) c0 $ n =
     foldr (\<lambda>c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
@@ -4732,22 +4732,22 @@
 
 instance fps :: (comm_ring_1) complete_space
 proof
-  fix X :: "nat \<Rightarrow> 'a fps"
-  assume "Cauchy X"
-  obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j"
+  fix fps_X :: "nat \<Rightarrow> 'a fps"
+  assume "Cauchy fps_X"
+  obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. fps_X (M i) $ j = fps_X m $ j"
   proof -
-    have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" for i
+    have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. fps_X M $ j = fps_X m $ j" for i
     proof -
       have "0 < inverse ((2::real)^i)" by simp
-      from metric_CauchyD[OF \<open>Cauchy X\<close> this] dist_less_imp_nth_equal
+      from metric_CauchyD[OF \<open>Cauchy fps_X\<close> this] dist_less_imp_nth_equal
       show ?thesis by blast
     qed
     then show ?thesis using that by metis
   qed
 
-  show "convergent X"
+  show "convergent fps_X"
   proof (rule convergentI)
-    show "X \<longlonglongrightarrow> Abs_fps (\<lambda>i. X (M i) $ i)"
+    show "fps_X \<longlonglongrightarrow> Abs_fps (\<lambda>i. fps_X (M i) $ i)"
       unfolding tendsto_iff
     proof safe
       fix e::real assume e: "0 < e"
@@ -4758,19 +4758,27 @@
         by (auto simp: eventually_sequentially)
       have "eventually (\<lambda>x. M i \<le> x) sequentially"
         by (auto simp: eventually_sequentially)
-      then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially"
+      then show "eventually (\<lambda>x. dist (fps_X x) (Abs_fps (\<lambda>i. fps_X (M i) $ i)) < e) sequentially"
       proof eventually_elim
         fix x
         assume x: "M i \<le> x"
-        have "X (M i) $ j = X (M j) $ j" if "j \<le> i" for j
+        have "fps_X (M i) $ j = fps_X (M j) $ j" if "j \<le> i" for j
           using M that by (metis nat_le_linear)
-        with x have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)"
+        with x have "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < inverse (2 ^ i)"
           using M by (force simp: dist_less_eq_nth_equal)
         also note \<open>inverse (2 ^ i) < e\<close>
-        finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" .
+        finally show "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < e" .
       qed
     qed
   qed
 qed
 
+(* TODO: Figure out better notation for this thing *)
+no_notation fps_nth (infixl "$" 75)
+
+bundle fps_notation
+begin
+notation fps_nth (infixl "$" 75)
 end
+
+end
diff -r 5c0a3f63057d -r 4b8d1df8933b src/HOL/Computational_Algebra/Polynomial_FPS.thy
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Aug 21 19:20:02 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Aug 21 20:49:15 2017 +0200
@@ -8,6 +8,10 @@
   imports Polynomial Formal_Power_Series
 begin
 
+context
+  includes fps_notation
+begin
+
 definition fps_of_poly where
   "fps_of_poly p = Abs_fps (coeff p)"
 
@@ -39,7 +43,7 @@
 lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n"
   by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly)
 
-lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X"
+lemma fps_of_poly_fps_X [simp]: "fps_of_poly [:0, 1:] = fps_X"
   by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split)
 
 lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q"
@@ -71,8 +75,8 @@
   by (induction xs) (simp_all add: fps_of_poly_mult)
 
 lemma fps_of_poly_pCons: 
-  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X"
-  by (subst fps_mult_X_commute [symmetric], intro fps_ext) 
+  "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * fps_X"
+  by (subst fps_mult_fps_X_commute [symmetric], intro fps_ext) 
      (auto simp: fps_of_poly_def coeff_pCons split: nat.split)
   
 lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)"
@@ -81,10 +85,10 @@
 lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n"
   by (induction n) (simp_all add: fps_of_poly_mult)
   
-lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n"
+lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * fps_X ^ n"
   by (intro fps_ext) simp_all
 
-lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n"
+lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = fps_X ^ n"
   by (simp add: fps_of_poly_monom)
 
 lemma fps_of_poly_div:
@@ -139,7 +143,7 @@
 
 
 lemmas fps_of_poly_simps =
-  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
+  fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_fps_X
   fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
   fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
   fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
@@ -153,7 +157,7 @@
                              fps_compose_add_distrib fps_compose_mult_distrib)
   
 lemmas reify_fps_atom =
-  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X
+  fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_fps_X
 
 
 text \<open>
@@ -163,7 +167,7 @@
   polynomial \<open>p\<close>.
   
   This may sound trivial, but it covers a number of annoying side conditions like 
-  @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
+  @{term "1 + fps_X \<noteq> 0"} that would otherwise not be solved automatically.
 \<close>
 
 ML \<open>
@@ -208,7 +212,7 @@
     | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _))
         => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv)
              then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]})
-    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> (
+    | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "fps_X"},_) $ _) => ct |> (
         rewr @{thms fps_of_poly_monom' [symmetric]}) 
     | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> (
         Conv.fun_conv (Conv.arg_conv reify_conv) 
@@ -232,10 +236,10 @@
 
 simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close>
 
-lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a"
+lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = fps_X + fps_const a"
   by simp
 
-lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X"
+lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * fps_X"
   by simp
 
 lemma fps_of_poly_cutoff [simp]: 
@@ -308,3 +312,5 @@
 qed (simp_all add: poly_subdegree_def prefix_length_def)
 
 end
+
+end