Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts

--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Wed Oct 11 17:02:33 2023 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Thu Oct 12 12:36:09 2023 +0100
@@ -4,42 +4,6 @@
 
 begin
 
-lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
-  by (metis fps_to_fls_of_nat of_nat_numeral)
-
-lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b"
-  by (induction b) (auto simp flip: fls_const_mult_const)
-
-lemma fls_deriv_numeral [simp]: "fls_deriv (numeral n) = 0"
-  by (metis fls_deriv_of_int of_int_numeral)
-
-lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n"
-  by (metis fls_of_nat of_nat_numeral)
-
-lemma fls_mult_of_int_nth [simp]:
-  shows "fls_nth (numeral k * f) n = numeral k * fls_nth f n"
-  and   "fls_nth (f * numeral k) n = fls_nth f n * numeral k"
-  by (metis fls_const_numeral fls_mult_const_nth)+
-
-lemma fls_nth_numeral' [simp]:
-  "fls_nth (numeral n) 0 = numeral n" "k \<noteq> 0 \<Longrightarrow> fls_nth (numeral n) k = 0"
-  by (subst fls_const_numeral [symmetric], subst fls_const_nth, simp)+
-
-lemma fls_subdegree_prod:
-  fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
-  assumes "\<And>x. x \<in> I \<Longrightarrow> F x \<noteq> 0"
-  shows   "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
-  using assms by (induction I rule: infinite_finite_induct) auto
-
-lemma fls_subdegree_prod':
-  fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
-  assumes "\<And>x. x \<in> I \<Longrightarrow> fls_subdegree (F x) \<noteq> 0"
-  shows   "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
-proof (intro fls_subdegree_prod)
-  show "F x \<noteq> 0" if "x \<in> I" for x
-    using assms[OF that] by auto
-qed
-
 instance fps :: (semiring_char_0) semiring_char_0
 proof
   show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
@@ -2187,211 +2151,6 @@
     by simp
 qed
 
-hide_const (open) fls_compose_fps
-
-definition fls_compose_fps :: "'a :: field fls \<Rightarrow> 'a fps \<Rightarrow> 'a fls" where
-  "fls_compose_fps F G =
-     fps_to_fls (fps_compose (fls_base_factor_to_fps F) G) * fps_to_fls G powi fls_subdegree F"
-
-lemma fps_compose_of_nat [simp]: "fps_compose (of_nat n :: 'a :: comm_ring_1 fps) H = of_nat n"
-  and fps_compose_of_int [simp]: "fps_compose (of_int i) H = of_int i"
-  unfolding fps_of_nat [symmetric] fps_of_int [symmetric] numeral_fps_const
-  by (rule fps_const_compose)+
-
-lemmas [simp] = fps_to_fls_of_nat fps_to_fls_of_int
-
-lemma fls_compose_fps_0 [simp]: "fls_compose_fps 0 H = 0"
-  and fls_compose_fps_1 [simp]: "fls_compose_fps 1 H = 1"
-  and fls_compose_fps_const [simp]: "fls_compose_fps (fls_const c) H = fls_const c"
-  and fls_compose_fps_of_nat [simp]: "fls_compose_fps (of_nat n) H = of_nat n"
-  and fls_compose_fps_of_int [simp]: "fls_compose_fps (of_int i) H = of_int i"
-  and fls_compose_fps_X [simp]: "fls_compose_fps fls_X F = fps_to_fls F"
-  by (simp_all add: fls_compose_fps_def)
-
-lemma fls_compose_fps_0_right:
-  "fls_compose_fps F 0 = (if fls_subdegree F \<ge> 0 then fls_const (fls_nth F 0) else 0)"
-  by (cases "fls_subdegree F = 0") (simp_all add: fls_compose_fps_def)
-
-lemma fls_compose_fps_shift:
-  assumes "H \<noteq> 0"
-  shows   "fls_compose_fps (fls_shift n F) H = fls_compose_fps F H * fps_to_fls H powi (-n)"
-proof (cases "F = 0")
-  case False
-  thus ?thesis
-    using assms by (simp add: fls_compose_fps_def power_int_diff power_int_minus field_simps)
-qed auto
-
-lemma fls_compose_fps_to_fls [simp]:
-  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
-  shows   "fls_compose_fps (fps_to_fls F) G = fps_to_fls (fps_compose F G)"
-proof (cases "F = 0")
-  case False
-  define n where "n = subdegree F"
-  define F' where "F' = fps_shift n F"
-  have [simp]: "F' \<noteq> 0" "subdegree F' = 0"
-    using False by (auto simp: F'_def n_def)
-  have F_eq: "F = F' * fps_X ^ n"
-    unfolding F'_def n_def using subdegree_decompose by blast
-  have "fls_compose_fps (fps_to_fls F) G =
-          fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F' * fls_X_intpow (int n))) oo G) * fps_to_fls (G ^ n)"
-    unfolding F_eq fls_compose_fps_def
-    by (simp add: fls_times_fps_to_fls fls_X_power_conv_shift_1 power_int_add
-                  fls_subdegree_fls_to_fps fps_to_fls_power fls_regpart_shift_conv_fps_shift
-             flip: fls_times_both_shifted_simp)
-  also have "fps_to_fls F' * fls_X_intpow (int n) = fps_to_fls F"
-    by (simp add: F_eq fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1)
-  also have "fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F)) oo G) * fps_to_fls (G ^ n) =
-             fps_to_fls ((fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n) oo G)"
-    by (simp add: fls_times_fps_to_fls flip: fps_compose_power add: fps_compose_mult_distrib)
-  also have "fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n = F"
-    by (simp add: F_eq)
-  finally show ?thesis .
-qed (auto simp: fls_compose_fps_def)
-
-lemma fls_compose_fps_mult:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (F * G) H = fls_compose_fps F H * fls_compose_fps G H"
-  using assms
-proof (cases "F * G = 0")
-  case False
-  hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
-    by auto
-  define n m where "n = fls_subdegree F" "m = fls_subdegree G"
-  define F' where "F' = fls_regpart (fls_shift n F)"
-  define G' where "G' = fls_regpart (fls_shift m G)"
-  have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-m) (fps_to_fls G')"
-    by (simp_all add: F'_def G'_def n_m_def)
-  have "fls_compose_fps (F * G) H = fls_compose_fps (fls_shift (-(n + m)) (fps_to_fls (F' * G'))) H"
-    by (simp add: fls_times_fps_to_fls F_eq G_eq fls_shifted_times_simps)
-  also have "\<dots> = fps_to_fls ((F' oo H) * (G' oo H)) * fps_to_fls H powi (m + n)"
-    by (simp add: fls_compose_fps_shift fps_compose_mult_distrib)
-  also have "\<dots> = fls_compose_fps F H * fls_compose_fps G H"
-    by (simp add: F_eq G_eq fls_compose_fps_shift fls_times_fps_to_fls power_int_add)
-  finally show ?thesis .
-qed auto
-
-lemma fls_compose_fps_power:
-  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
-  shows   "fls_compose_fps (F ^ n) G = fls_compose_fps F G ^ n"
-  by (induction n) (auto simp: fls_compose_fps_mult)
-
-lemma fls_compose_fps_add:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (F + G) H = fls_compose_fps F H + fls_compose_fps G H"
-proof (cases "F = 0 \<or> G = 0")
-  case False
-  hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
-    by auto
-  define n where "n = min (fls_subdegree F) (fls_subdegree G)"
-  define F' where "F' = fls_regpart (fls_shift n F)"
-  define G' where "G' = fls_regpart (fls_shift n G)"
-  have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-n) (fps_to_fls G')"
-    unfolding n_def by (simp_all add: F'_def G'_def n_def)
-  have "F + G = fls_shift (-n) (fps_to_fls (F' + G'))"
-    by (simp add: F_eq G_eq)
-  also have "fls_compose_fps \<dots> H = fls_compose_fps (fps_to_fls (F' + G')) H * fps_to_fls H powi n"
-    by (subst fls_compose_fps_shift) auto
-  also have "\<dots> = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n"
-    by (subst fls_compose_fps_to_fls) auto
-  also have "\<dots> = fls_compose_fps F H + fls_compose_fps G H"
-    by (simp add: F_eq G_eq fls_compose_fps_shift fps_compose_add_distrib algebra_simps)
-  finally show ?thesis .
-qed auto
-
-lemma fls_compose_fps_uminus [simp]: "fls_compose_fps (-F) H = -fls_compose_fps F H"
-  by (simp add: fls_compose_fps_def fps_compose_uminus)
-
-lemma fls_compose_fps_diff:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H"
-  using fls_compose_fps_add[of H F "-G"] by simp
-
-lemma fps_compose_eq_0_iff:
-  fixes F G :: "'a :: idom fps"
-  assumes "fps_nth G 0 = 0"
-  shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
-proof safe
-  assume *: "fps_compose F G = 0" "F \<noteq> 0"
-  have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
-    by simp
-  also have "fps_compose F G = 0"
-    by (simp add: *)
-  finally show "fps_nth F 0 = 0"
-    by simp
-  show "G = 0"
-  proof (rule ccontr)
-    assume "G \<noteq> 0"
-    hence "subdegree G > 0" using assms
-      using subdegree_eq_0_iff by blast
-    define N where "N = subdegree F * subdegree G"
-    have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
-      unfolding fps_compose_def by (simp add: N_def)
-    also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
-    proof (intro sum.mono_neutral_right ballI)
-      fix i assume i: "i \<in> {0..N} - {subdegree F}"
-      show "fps_nth F i * fps_nth (G ^ i) N = 0"
-      proof (cases i "subdegree F" rule: linorder_cases)
-        assume "i > subdegree F"
-        hence "fps_nth (G ^ i) N = 0"
-          using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
-        thus ?thesis by simp
-      qed (use i in \<open>auto simp: N_def\<close>)
-    qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
-    also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
-      by simp
-    also have "\<dots> \<noteq> 0"
-      using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
-    finally show False using * by auto
-  qed
-qed auto
-
-lemma fls_compose_fps_eq_0_iff:
-  assumes "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps F H = 0 \<longleftrightarrow> F = 0"
-  using assms fls_base_factor_to_fps_nonzero[of F]
-  by (cases "F = 0") (auto simp: fls_compose_fps_def fps_compose_eq_0_iff)
-
-lemma fls_compose_fps_inverse:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (inverse F) H = inverse (fls_compose_fps F H)"
-proof (cases "F = 0")
-  case False
-  have "fls_compose_fps (inverse F) H * fls_compose_fps F H =
-        fls_compose_fps (inverse F * F) H"
-    by (subst fls_compose_fps_mult) auto
-  also have "inverse F * F = 1"
-    using False by simp
-  finally show ?thesis
-    using False by (simp add: field_simps fls_compose_fps_eq_0_iff)
-qed auto
-
-lemma fls_compose_fps_divide:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (F / G) H = fls_compose_fps F H / fls_compose_fps G H"
-  using fls_compose_fps_mult[of H F "inverse G"] fls_compose_fps_inverse[of H G]
-  by (simp add: field_simps)
-
-lemma fls_compose_fps_powi:
-  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows   "fls_compose_fps (F powi n) H = fls_compose_fps F H powi n"
-  by (simp add: power_int_def fls_compose_fps_power fls_compose_fps_inverse)
-
-lemma fls_compose_fps_assoc:
-  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0" "H \<noteq> 0" "fps_nth H 0 = 0"
-  shows "fls_compose_fps (fls_compose_fps F G) H = fls_compose_fps F (fps_compose G H)"
-proof (cases "F = 0")
-  case [simp]: False
-  define n where "n = fls_subdegree F"
-  define F' where "F' = fls_regpart (fls_shift n F)"
-  have F_eq: "F = fls_shift (-n) (fps_to_fls F')"
-    by (simp add: F'_def n_def)
-  show ?thesis
-    by (simp add: F_eq fls_compose_fps_shift fls_compose_fps_mult fls_compose_fps_powi
-                  fps_compose_eq_0_iff fps_compose_assoc)
-qed auto
-
-lemma subdegree_pos_iff: "subdegree F > 0 \<longleftrightarrow> F \<noteq> 0 \<and> fps_nth F 0 = 0"
-  using subdegree_eq_0_iff[of F] by auto
 
 lemma has_fps_expansion_fps_to_fls:
   assumes "f has_laurent_expansion fps_to_fls F"
@@ -2404,7 +2163,6 @@
     by (auto simp: has_fps_expansion_to_laurent)
 qed
 
-
 lemma has_laurent_expansion_compose [laurent_expansion_intros]:
   fixes f g :: "complex \<Rightarrow> complex"
   assumes F: "f has_laurent_expansion F"
@@ -2455,34 +2213,6 @@
   using has_laurent_expansion_inverse[OF has_laurent_expansion_fps_X]
   by (simp add: fls_inverse_X)
 
-lemma fls_X_power_int [simp]: "fls_X powi n = (fls_X_intpow n :: 'a :: division_ring fls)"
-  by (auto simp: power_int_def fls_X_power_conv_shift_1 fls_inverse_X fls_inverse_shift
-           simp flip: fls_inverse_X_power)
-
-lemma fls_const_power_int: "fls_const (c powi n) = fls_const (c :: 'a :: division_ring) powi n"
-  by (auto simp: power_int_def fls_const_power fls_inverse_const)
-
-lemma fls_nth_fls_compose_fps_linear:
-  fixes c :: "'a :: field"
-  assumes [simp]: "c \<noteq> 0"
-  shows "fls_nth (fls_compose_fps F (fps_const c * fps_X)) n = fls_nth F n * c powi n"
-proof -
-  {
-    assume *: "n \<ge> fls_subdegree F"
-    hence "c ^ nat (n - fls_subdegree F) = c powi int (nat (n - fls_subdegree F))"
-      by (simp add: power_int_def)
-    also have "\<dots> * c powi fls_subdegree F = c powi (int (nat (n - fls_subdegree F)) + fls_subdegree F)"
-      using * by (subst power_int_add) auto
-    also have "\<dots> = c powi n"
-      using * by simp
-    finally have "c ^ nat (n - fls_subdegree F) * c powi fls_subdegree F = c powi n" .
-  }
-  thus ?thesis
-    by (simp add: fls_compose_fps_def fps_compose_linear fls_times_fps_to_fls power_int_mult_distrib
-                  fls_shifted_times_simps
-             flip: fls_const_power_int)
-qed
-
 lemma zorder_times_analytic:
   assumes "f analytic_on {z}" "g analytic_on {z}"
   assumes "eventually (\<lambda>z. f z * g z \<noteq> 0) (at z)"
@@ -2787,7 +2517,6 @@
     by (auto simp: eq_commute)
 qed
 
-
 lemma has_laurent_expansion_sin' [laurent_expansion_intros]:
   "sin has_laurent_expansion fps_to_fls (fps_sin 1)"
   using has_fps_expansion_sin' has_fps_expansion_to_laurent by blast

--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Wed Oct 11 17:02:33 2023 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Thu Oct 12 12:36:09 2023 +0100
@@ -1587,6 +1587,24 @@
   thus ?thesis by (simp add: fls_of_nat)
 qed
 
+lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
+  by (metis fps_to_fls_of_nat of_nat_numeral)
+
+lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b"
+  by (induction b) (auto simp flip: fls_const_mult_const)
+
+lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n"
+  by (metis fls_of_nat of_nat_numeral)
+
+lemma fls_mult_of_numeral_nth [simp]:
+  shows "(numeral k * f) $$ n = numeral k * f $$ n"
+  and   "(f * numeral k) $$ n = f $$ n * numeral k"
+  by (metis fls_const_numeral fls_mult_const_nth)+
+
+lemma fls_nth_numeral' [simp]:
+  "numeral n $$ 0 = numeral n" "k \<noteq> 0 \<Longrightarrow> numeral n $$ k = 0"
+  by (metis fls_const_nth fls_const_numeral)+
+
 instance fls :: (comm_semiring_1) comm_semiring_1
   by standard simp
 
@@ -1668,6 +1686,21 @@
 
 subsubsection \<open>Powers\<close>
 
+lemma fls_subdegree_prod:
+  fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
+  assumes "\<And>x. x \<in> I \<Longrightarrow> F x \<noteq> 0"
+  shows   "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
+  using assms by (induction I rule: infinite_finite_induct) auto
+
+lemma fls_subdegree_prod':
+  fixes F :: "'a \<Rightarrow> 'b :: field_char_0 fls"
+  assumes "\<And>x. x \<in> I \<Longrightarrow> fls_subdegree (F x) \<noteq> 0"
+  shows   "fls_subdegree (\<Prod>x\<in>I. F x) = (\<Sum>x\<in>I. fls_subdegree (F x))"
+proof (intro fls_subdegree_prod)
+  show "F x \<noteq> 0" if "x \<in> I" for x
+    using assms[OF that] by auto
+qed
+
 lemma fls_pow_subdegree_ge:
   "f^n \<noteq> 0 \<Longrightarrow> fls_subdegree (f^n) \<ge> n * fls_subdegree f"
 proof (induct n)
@@ -3254,15 +3287,236 @@
 subsection \<open>Composition\<close>
 
 definition fls_compose_fps :: "'a :: field fls \<Rightarrow> 'a fps \<Rightarrow> 'a fls" where
-  "fls_compose_fps f g =
-     (if f = 0 then 0
-      else if fls_subdegree f \<ge> 0 then fps_to_fls (fps_compose (fls_regpart f) g)
-      else fps_to_fls (fps_compose (fls_base_factor_to_fps f) g) /
-             fps_to_fls g ^ nat (-fls_subdegree f))"
-
-lemma fls_compose_fps_fps [simp]:
-  "fls_compose_fps (fps_to_fls f) g = fps_to_fls (fps_compose f g)"
-  by (simp add: fls_compose_fps_def fls_subdegree_fls_to_fps_gt0 fps_to_fls_eq_0_iff)
+  "fls_compose_fps F G =
+     fps_to_fls (fps_compose (fls_base_factor_to_fps F) G) * fps_to_fls G powi fls_subdegree F"
+
+lemma fps_compose_of_nat [simp]: "fps_compose (of_nat n :: 'a :: comm_ring_1 fps) H = of_nat n"
+  and fps_compose_of_int [simp]: "fps_compose (of_int i) H = of_int i"
+  unfolding fps_of_nat [symmetric] fps_of_int [symmetric] numeral_fps_const
+  by (rule fps_const_compose)+
+
+lemmas [simp] = fps_to_fls_of_nat fps_to_fls_of_int
+
+lemma fls_compose_fps_0 [simp]: "fls_compose_fps 0 H = 0"
+  and fls_compose_fps_1 [simp]: "fls_compose_fps 1 H = 1"
+  and fls_compose_fps_const [simp]: "fls_compose_fps (fls_const c) H = fls_const c"
+  and fls_compose_fps_of_nat [simp]: "fls_compose_fps (of_nat n) H = of_nat n"
+  and fls_compose_fps_of_int [simp]: "fls_compose_fps (of_int i) H = of_int i"
+  and fls_compose_fps_X [simp]: "fls_compose_fps fls_X F = fps_to_fls F"
+  by (simp_all add: fls_compose_fps_def)
+
+lemma fls_compose_fps_0_right:
+  "fls_compose_fps F 0 = (if 0 \<le> fls_subdegree F then fls_const (F $$ 0) else 0)"
+  by (cases "fls_subdegree F = 0") (simp_all add: fls_compose_fps_def)
+
+lemma fls_compose_fps_shift:
+  assumes "H \<noteq> 0"
+  shows   "fls_compose_fps (fls_shift n F) H = fls_compose_fps F H * fps_to_fls H powi (-n)"
+proof (cases "F = 0")
+  case False
+  thus ?thesis
+    using assms by (simp add: fls_compose_fps_def power_int_diff power_int_minus field_simps)
+qed auto
+
+lemma fls_compose_fps_to_fls [simp]:
+  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
+  shows   "fls_compose_fps (fps_to_fls F) G = fps_to_fls (fps_compose F G)"
+proof (cases "F = 0")
+  case False
+  define n where "n = subdegree F"
+  define F' where "F' = fps_shift n F"
+  have [simp]: "F' \<noteq> 0" "subdegree F' = 0"
+    using False by (auto simp: F'_def n_def)
+  have F_eq: "F = F' * fps_X ^ n"
+    unfolding F'_def n_def using subdegree_decompose by blast
+  have "fls_compose_fps (fps_to_fls F) G =
+          fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F' * fls_X_intpow (int n))) oo G) * fps_to_fls (G ^ n)"
+    unfolding F_eq fls_compose_fps_def
+    by (simp add: fls_times_fps_to_fls fls_X_power_conv_shift_1 power_int_add
+                  fls_subdegree_fls_to_fps fps_to_fls_power fls_regpart_shift_conv_fps_shift
+             flip: fls_times_both_shifted_simp)
+  also have "fps_to_fls F' * fls_X_intpow (int n) = fps_to_fls F"
+    by (simp add: F_eq fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1)
+  also have "fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F)) oo G) * fps_to_fls (G ^ n) =
+             fps_to_fls ((fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n) oo G)"
+    by (simp add: fls_times_fps_to_fls flip: fps_compose_power add: fps_compose_mult_distrib)
+  also have "fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n = F"
+    by (simp add: F_eq)
+  finally show ?thesis .
+qed (auto simp: fls_compose_fps_def)
+
+lemma fls_compose_fps_mult:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (F * G) H = fls_compose_fps F H * fls_compose_fps G H"
+  using assms
+proof (cases "F * G = 0")
+  case False
+  hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
+    by auto
+  define n m where "n = fls_subdegree F" "m = fls_subdegree G"
+  define F' where "F' = fls_regpart (fls_shift n F)"
+  define G' where "G' = fls_regpart (fls_shift m G)"
+  have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-m) (fps_to_fls G')"
+    by (simp_all add: F'_def G'_def n_m_def)
+  have "fls_compose_fps (F * G) H = fls_compose_fps (fls_shift (-(n + m)) (fps_to_fls (F' * G'))) H"
+    by (simp add: fls_times_fps_to_fls F_eq G_eq fls_shifted_times_simps)
+  also have "\<dots> = fps_to_fls ((F' oo H) * (G' oo H)) * fps_to_fls H powi (m + n)"
+    by (simp add: fls_compose_fps_shift fps_compose_mult_distrib)
+  also have "\<dots> = fls_compose_fps F H * fls_compose_fps G H"
+    by (simp add: F_eq G_eq fls_compose_fps_shift fls_times_fps_to_fls power_int_add)
+  finally show ?thesis .
+qed auto
+
+lemma fls_compose_fps_power:
+  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0"
+  shows   "fls_compose_fps (F ^ n) G = fls_compose_fps F G ^ n"
+  by (induction n) (auto simp: fls_compose_fps_mult)
+
+lemma fls_compose_fps_add:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (F + G) H = fls_compose_fps F H + fls_compose_fps G H"
+proof (cases "F = 0 \<or> G = 0")
+  case False
+  hence [simp]: "F \<noteq> 0" "G \<noteq> 0"
+    by auto
+  define n where "n = min (fls_subdegree F) (fls_subdegree G)"
+  define F' where "F' = fls_regpart (fls_shift n F)"
+  define G' where "G' = fls_regpart (fls_shift n G)"
+  have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-n) (fps_to_fls G')"
+    unfolding n_def by (simp_all add: F'_def G'_def n_def)
+  have "F + G = fls_shift (-n) (fps_to_fls (F' + G'))"
+    by (simp add: F_eq G_eq)
+  also have "fls_compose_fps \<dots> H = fls_compose_fps (fps_to_fls (F' + G')) H * fps_to_fls H powi n"
+    by (subst fls_compose_fps_shift) auto
+  also have "\<dots> = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n"
+    by (subst fls_compose_fps_to_fls) auto
+  also have "\<dots> = fls_compose_fps F H + fls_compose_fps G H"
+    by (simp add: F_eq G_eq fls_compose_fps_shift fps_compose_add_distrib algebra_simps)
+  finally show ?thesis .
+qed auto
+
+lemma fls_compose_fps_uminus [simp]: "fls_compose_fps (-F) H = -fls_compose_fps F H"
+  by (simp add: fls_compose_fps_def fps_compose_uminus)
+
+lemma fls_compose_fps_diff:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H"
+  using fls_compose_fps_add[of H F "-G"] by simp
+
+lemma fps_compose_eq_0_iff:
+  fixes F G :: "'a :: idom fps"
+  assumes "fps_nth G 0 = 0"
+  shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
+proof safe
+  assume *: "fps_compose F G = 0" "F \<noteq> 0"
+  have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
+    by simp
+  also have "fps_compose F G = 0"
+    by (simp add: *)
+  finally show "fps_nth F 0 = 0"
+    by simp
+  show "G = 0"
+  proof (rule ccontr)
+    assume "G \<noteq> 0"
+    hence "subdegree G > 0" using assms
+      using subdegree_eq_0_iff by blast
+    define N where "N = subdegree F * subdegree G"
+    have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
+      unfolding fps_compose_def by (simp add: N_def)
+    also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
+    proof (intro sum.mono_neutral_right ballI)
+      fix i assume i: "i \<in> {0..N} - {subdegree F}"
+      show "fps_nth F i * fps_nth (G ^ i) N = 0"
+      proof (cases i "subdegree F" rule: linorder_cases)
+        assume "i > subdegree F"
+        hence "fps_nth (G ^ i) N = 0"
+          using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
+        thus ?thesis by simp
+      qed (use i in \<open>auto simp: N_def\<close>)
+    qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
+    also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
+      by simp
+    also have "\<dots> \<noteq> 0"
+      using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
+    finally show False using * by auto
+  qed
+qed auto
+
+lemma fls_compose_fps_eq_0_iff:
+  assumes "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps F H = 0 \<longleftrightarrow> F = 0"
+  using assms fls_base_factor_to_fps_nonzero[of F]
+  by (cases "F = 0") (auto simp: fls_compose_fps_def fps_compose_eq_0_iff)
+
+lemma fls_compose_fps_inverse:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (inverse F) H = inverse (fls_compose_fps F H)"
+proof (cases "F = 0")
+  case False
+  have "fls_compose_fps (inverse F) H * fls_compose_fps F H =
+        fls_compose_fps (inverse F * F) H"
+    by (subst fls_compose_fps_mult) auto
+  also have "inverse F * F = 1"
+    using False by simp
+  finally show ?thesis
+    using False by (simp add: field_simps fls_compose_fps_eq_0_iff)
+qed auto
+
+lemma fls_compose_fps_divide:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (F / G) H = fls_compose_fps F H / fls_compose_fps G H"
+  using fls_compose_fps_mult[of H F "inverse G"] fls_compose_fps_inverse[of H G]
+  by (simp add: field_simps)
+
+lemma fls_compose_fps_powi:
+  assumes [simp]: "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows   "fls_compose_fps (F powi n) H = fls_compose_fps F H powi n"
+  by (simp add: power_int_def fls_compose_fps_power fls_compose_fps_inverse)
+
+lemma fls_compose_fps_assoc:
+  assumes [simp]: "G \<noteq> 0" "fps_nth G 0 = 0" "H \<noteq> 0" "fps_nth H 0 = 0"
+  shows "fls_compose_fps (fls_compose_fps F G) H = fls_compose_fps F (fps_compose G H)"
+proof (cases "F = 0")
+  case [simp]: False
+  define n where "n = fls_subdegree F"
+  define F' where "F' = fls_regpart (fls_shift n F)"
+  have F_eq: "F = fls_shift (-n) (fps_to_fls F')"
+    by (simp add: F'_def n_def)
+  show ?thesis
+    by (simp add: F_eq fls_compose_fps_shift fls_compose_fps_mult fls_compose_fps_powi
+                  fps_compose_eq_0_iff fps_compose_assoc)
+qed auto
+
+lemma subdegree_pos_iff: "subdegree F > 0 \<longleftrightarrow> F \<noteq> 0 \<and> fps_nth F 0 = 0"
+  using subdegree_eq_0_iff[of F] by auto
+
+lemma fls_X_power_int [simp]: "fls_X powi n = (fls_X_intpow n :: 'a :: division_ring fls)"
+  by (auto simp: power_int_def fls_X_power_conv_shift_1 fls_inverse_X fls_inverse_shift
+           simp flip: fls_inverse_X_power)
+
+lemma fls_const_power_int: "fls_const (c powi n) = fls_const (c :: 'a :: division_ring) powi n"
+  by (auto simp: power_int_def fls_const_power fls_inverse_const)
+
+lemma fls_nth_fls_compose_fps_linear:
+  fixes c :: "'a :: field"
+  assumes [simp]: "c \<noteq> 0"
+  shows "fls_compose_fps F (fps_const c * fps_X) $$ n = F $$ n * c powi n"
+proof -
+  {
+    assume *: "n \<ge> fls_subdegree F"
+    hence "c ^ nat (n - fls_subdegree F) = c powi int (nat (n - fls_subdegree F))"
+      by (simp add: power_int_def)
+    also have "\<dots> * c powi fls_subdegree F = c powi (int (nat (n - fls_subdegree F)) + fls_subdegree F)"
+      using * by (subst power_int_add) auto
+    also have "\<dots> = c powi n"
+      using * by simp
+    finally have "c ^ nat (n - fls_subdegree F) * c powi fls_subdegree F = c powi n" .
+  }
+  thus ?thesis
+    by (simp add: fls_compose_fps_def fps_compose_linear fls_times_fps_to_fls power_int_mult_distrib
+                  fls_shifted_times_simps
+             flip: fls_const_power_int)
+qed
 
 lemma fls_const_transfer [transfer_rule]:
   "rel_fun (=) (pcr_fls (=))
@@ -3295,8 +3549,8 @@
 
 lemma fls_nth_compose_power:
   assumes "d > 0"
-  shows   "fls_nth (fls_compose_power f d) n = (if int d dvd n then fls_nth f (n div int d) else 0)"
-  using assms by transfer auto
+  shows   "fls_compose_power f d $$ n = (if int d dvd n then f $$ (n div int d) else 0)"
+  by (simp add: assms fls_compose_power.rep_eq)
      
 
 lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0"
@@ -3385,8 +3639,8 @@
 qed (use assms in auto)
 
 lemma fls_nth_compose_power' [simp]:
-  "d = 0 \<or> \<not>d dvd n \<Longrightarrow> fls_nth (fls_compose_power f d) n = 0"
-  "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_nth (fls_compose_power f d) n = fls_nth f (n div d)"
+  "d = 0 \<or> \<not>d dvd n \<Longrightarrow> fls_compose_power f d $$ int n = 0"
+  "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_compose_power f d $$ int n = f $$ int (n div d)"
   by (transfer; force; fail)+
 
 subsection \<open>Formal differentiation and integration\<close>
@@ -3423,6 +3677,9 @@
 lemma fls_deriv_one[simp]: "fls_deriv 1 = 0"
   using fls_deriv_const[of 1] by simp
 
+lemma fls_deriv_numeral [simp]: "fls_deriv (numeral n) = 0"
+  by (metis fls_deriv_of_int of_int_numeral)
+
 lemma fls_deriv_subdegree':
   assumes "of_int (fls_subdegree f) * f $$ fls_subdegree f \<noteq> 0"
   shows   "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"