Theory HOL-Computational_Algebra.Formal_Power_Series

(*  Title:      HOL/Computational_Algebra/Formal_Power_Series.thy
    Author:     Amine Chaieb, University of Cambridge
    Author:     Jeremy Sylvestre, University of Alberta (Augustana Campus)
    Author:     Manuel Eberl, TU München
*)

section ‹A formalization of formal power series›

theory Formal_Power_Series
imports
  Complex_Main
  Euclidean_Algorithm
begin


subsection ‹The type of formal power series›

typedef 'a fps = "{f :: nat ⇒ 'a. True}"
  morphisms fps_nth Abs_fps
  by simp

notation fps_nth (infixl "$" 75)

lemma expand_fps_eq: "p = q ⟷ (∀n. p $ n = q $ n)"
  by (simp add: fps_nth_inject [symmetric] fun_eq_iff)

lemmas fps_eq_iff = expand_fps_eq

lemma fps_ext: "(⋀n. p $ n = q $ n) ⟹ p = q"
  by (simp add: expand_fps_eq)

lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n"
  by (simp add: Abs_fps_inverse)

text ‹Definition of the basic elements 0 and 1 and the basic operations of addition,
  negation and multiplication.›

instantiation fps :: (zero) zero
begin
  definition fps_zero_def: "0 = Abs_fps (λn. 0)"
  instance ..
end

lemma fps_zero_nth [simp]: "0 $ n = 0"
  unfolding fps_zero_def by simp

lemma fps_nonzero_nth: "f ≠ 0 ⟷ (∃ n. f $n ≠ 0)"
  by (simp add: expand_fps_eq)

lemma fps_nonzero_nth_minimal: "f ≠ 0 ⟷ (∃n. f $ n ≠ 0 ∧ (∀m < n. f $ m = 0))"
  (is "?lhs ⟷ ?rhs")
proof
  let ?n = "LEAST n. f $ n ≠ 0"
  show ?rhs if ?lhs
  proof -
    from that have "∃n. f $ n ≠ 0"
      by (simp add: fps_nonzero_nth)
    then have "f $ ?n ≠ 0"
      by (rule LeastI_ex)
    moreover have "∀m<?n. f $ m = 0"
      by (auto dest: not_less_Least)
    ultimately show ?thesis by metis
  qed
qed (auto simp: expand_fps_eq)

lemma fps_nonzeroI: "f$n ≠ 0 ⟹ f ≠ 0"
  by auto

instantiation fps :: ("{one, zero}") one
begin
  definition fps_one_def: "1 = Abs_fps (λn. if n = 0 then 1 else 0)"
  instance ..
end

lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)"
  unfolding fps_one_def by simp

instantiation fps :: (plus) plus
begin
  definition fps_plus_def: "(+) = (λf g. Abs_fps (λn. f $ n + g $ n))"
  instance ..
end

lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n"
  unfolding fps_plus_def by simp

instantiation fps :: (minus) minus
begin
  definition fps_minus_def: "(-) = (λf g. Abs_fps (λn. f $ n - g $ n))"
  instance ..
end

lemma fps_sub_nth [simp]: "(f - g) $ n = f $ n - g $ n"
  unfolding fps_minus_def by simp

instantiation fps :: (uminus) uminus
begin
  definition fps_uminus_def: "uminus = (λf. Abs_fps (λn. - (f $ n)))"
  instance ..
end

lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)"
  unfolding fps_uminus_def by simp

lemma fps_neg_0 [simp]: "-(0::'a::group_add fps) = 0"
  by (rule iffD2, rule fps_eq_iff, auto)

instantiation fps :: ("{comm_monoid_add, times}") times
begin
  definition fps_times_def: "(*) = (λf g. Abs_fps (λn. ∑i=0..n. f $ i * g $ (n - i)))"
  instance ..
end

lemma fps_mult_nth: "(f * g) $ n = (∑i=0..n. f$i * g$(n - i))"
  unfolding fps_times_def by simp

lemma fps_mult_nth_0 [simp]: "(f * g) $ 0 = f $ 0 * g $ 0"
  unfolding fps_times_def by simp

lemma fps_mult_nth_1: "(f * g) $ 1 = f$0 * g$1 + f$1 * g$0"
  by (simp add: fps_mult_nth)

lemma fps_mult_nth_1' [simp]: "(f * g) $ Suc 0 = f$0 * g$Suc 0 + f$Suc 0 * g$0"
  by (simp add: fps_mult_nth)

lemmas mult_nth_0 = fps_mult_nth_0
lemmas mult_nth_1 = fps_mult_nth_1

instance fps :: ("{comm_monoid_add, mult_zero}") mult_zero
proof
  fix a :: "'a fps"
  show "0 * a = 0" by (simp add: fps_ext fps_mult_nth)
  show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth)
qed

declare atLeastAtMost_iff [presburger]
declare Bex_def [presburger]
declare Ball_def [presburger]

lemma mult_delta_left:
  fixes x y :: "'a::mult_zero"
  shows "(if b then x else 0) * y = (if b then x * y else 0)"
  by simp

lemma mult_delta_right:
  fixes x y :: "'a::mult_zero"
  shows "x * (if b then y else 0) = (if b then x * y else 0)"
  by simp

lemma fps_one_mult:
  fixes f :: "'a::{comm_monoid_add, mult_zero, monoid_mult} fps"
  shows "1 * f = f"
  and   "f * 1 = f"
  by    (simp_all add: fps_ext fps_mult_nth mult_delta_left mult_delta_right)


subsection ‹Subdegrees›

definition subdegree :: "('a::zero) fps ⇒ nat" where
  "subdegree f = (if f = 0 then 0 else LEAST n. f$n ≠ 0)"

lemma subdegreeI:
  assumes "f $ d ≠ 0" and "⋀i. i < d ⟹ f $ i = 0"
  shows   "subdegree f = d"
  by (smt (verit) LeastI_ex assms fps_zero_nth linorder_cases not_less_Least subdegree_def)

lemma nth_subdegree_nonzero [simp,intro]: "f ≠ 0 ⟹ f $ subdegree f ≠ 0"
  using fps_nonzero_nth_minimal subdegreeI by blast

lemma nth_less_subdegree_zero [dest]: "n < subdegree f ⟹ f $ n = 0"
  by (metis fps_nonzero_nth_minimal fps_zero_nth subdegreeI)

lemma subdegree_geI:
  assumes "f ≠ 0" "⋀i. i < n ⟹ f$i = 0"
  shows   "subdegree f ≥ n"
  by (meson assms leI nth_subdegree_nonzero)

lemma subdegree_greaterI:
  assumes "f ≠ 0" "⋀i. i ≤ n ⟹ f$i = 0"
  shows   "subdegree f > n"
  by (meson assms leI nth_subdegree_nonzero)

lemma subdegree_leI:
  "f $ n ≠ 0 ⟹ subdegree f ≤ n"
  using linorder_not_less by blast

lemma subdegree_0 [simp]: "subdegree 0 = 0"
  by (simp add: subdegree_def)

lemma subdegree_1 [simp]: "subdegree 1 = 0"
  by (metis fps_one_nth nth_subdegree_nonzero subdegree_0)

lemma subdegree_eq_0_iff: "subdegree f = 0 ⟷ f = 0 ∨ f $ 0 ≠ 0"
  using nth_subdegree_nonzero subdegree_leI by fastforce

lemma subdegree_eq_0 [simp]: "f $ 0 ≠ 0 ⟹ subdegree f = 0"
  by (simp add: subdegree_eq_0_iff)

lemma nth_subdegree_zero_iff [simp]: "f $ subdegree f = 0 ⟷ f = 0"
  by (cases "f = 0") auto

lemma fps_nonzero_subdegree_nonzeroI: "subdegree f > 0 ⟹ f ≠ 0"
 by auto

lemma subdegree_uminus [simp]:
  "subdegree (-(f::('a::group_add) fps)) = subdegree f"
proof (cases "f=0")
  case False thus ?thesis by (force intro: subdegreeI)
qed simp

lemma subdegree_minus_commute [simp]:
  fixes f :: "'a::group_add fps"
  shows "subdegree (f-g) = subdegree (g - f)"
proof (cases "g-f=0")
  case True then show ?thesis
    by (metis fps_sub_nth nth_subdegree_nonzero right_minus_eq)
next
  case False show ?thesis
    using nth_subdegree_nonzero[OF False] by (fastforce intro: subdegreeI)
qed

lemma subdegree_add_ge':
  fixes   f g :: "'a::monoid_add fps"
  assumes "f + g ≠ 0"
  shows   "subdegree (f + g) ≥ min (subdegree f) (subdegree g)"
  using   assms
  by      (force intro: subdegree_geI)

lemma subdegree_add_ge:
  assumes "f ≠ -(g :: ('a :: group_add) fps)"
  shows   "subdegree (f + g) ≥ min (subdegree f) (subdegree g)"
proof (rule subdegree_add_ge')
  have "f + g = 0 ⟹ False"
  proof-
    assume fg: "f + g = 0"
    have "⋀n. f $ n = - g $ n"
      by (metis add_eq_0_iff equation_minus_iff fg fps_add_nth fps_neg_nth fps_zero_nth)
    with assms show False by (auto intro: fps_ext)
  qed
  thus "f + g ≠ 0" by fast
qed

lemma subdegree_add_eq1:
  assumes "f ≠ 0"
  and     "subdegree f < subdegree (g :: 'a::monoid_add fps)"
  shows   "subdegree (f + g) = subdegree f"
  using assms by(auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma subdegree_add_eq2:
  assumes "g ≠ 0"
  and     "subdegree g < subdegree (f :: 'a :: monoid_add fps)"
  shows   "subdegree (f + g) = subdegree g"
  using assms by (auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma subdegree_diff_eq1:
  assumes "f ≠ 0"
  and     "subdegree f < subdegree (g :: 'a :: group_add fps)"
  shows   "subdegree (f - g) = subdegree f"
  using assms by (auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma subdegree_diff_eq1_cancel:
  assumes "f ≠ 0"
  and     "subdegree f < subdegree (g :: 'a :: cancel_comm_monoid_add fps)"
  shows   "subdegree (f - g) = subdegree f"
  using assms by (auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma subdegree_diff_eq2:
  assumes "g ≠ 0"
  and     "subdegree g < subdegree (f :: 'a :: group_add fps)"
  shows   "subdegree (f - g) = subdegree g"
  using assms by (auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma subdegree_diff_ge [simp]:
  assumes "f ≠ (g :: 'a :: group_add fps)"
  shows   "subdegree (f - g) ≥ min (subdegree f) (subdegree g)"
proof-
  have "f ≠ - (- g)"
    using assms expand_fps_eq by fastforce
  moreover have "f + - g = f - g" by (simp add: fps_ext)
  ultimately show ?thesis
    using subdegree_add_ge[of f "-g"] by simp
qed

lemma subdegree_diff_ge':
  fixes   f g :: "'a :: comm_monoid_diff fps"
  assumes "f - g ≠ 0"
  shows   "subdegree (f - g) ≥ subdegree f"
  using assms by (auto intro: subdegree_geI simp: nth_less_subdegree_zero)

lemma nth_subdegree_mult_left [simp]:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ (subdegree f) = f $ subdegree f * g $ 0"
  by    (cases "subdegree f") (simp_all add: fps_mult_nth nth_less_subdegree_zero)

lemma nth_subdegree_mult_right [simp]:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ (subdegree g) = f $ 0 * g $ subdegree g"
  by    (cases "subdegree g") (simp_all add: fps_mult_nth nth_less_subdegree_zero sum.atLeast_Suc_atMost)

lemma nth_subdegree_mult [simp]:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ (subdegree f + subdegree g) = f $ subdegree f * g $ subdegree g"
proof-
  let ?n = "subdegree f + subdegree g"
  have "(f * g) $ ?n = (∑i=0..?n. f$i * g$(?n-i))"
    by (simp add: fps_mult_nth)
  also have "... = (∑i=0..?n. if i = subdegree f then f$i * g$(?n-i) else 0)"
  proof (intro sum.cong)
    fix x assume x: "x ∈ {0..?n}"
    hence "x = subdegree f ∨ x < subdegree f ∨ ?n - x < subdegree g" by auto
    thus "f $ x * g $ (?n - x) = (if x = subdegree f then f $ x * g $ (?n - x) else 0)"
      by (elim disjE conjE) auto
  qed auto
  also have "... = f $ subdegree f * g $ subdegree g" by simp
  finally show ?thesis .
qed

lemma fps_mult_nth_eq0:
  fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
  assumes "n < subdegree f + subdegree g"
  shows   "(f*g) $ n = 0"
proof-
  have "⋀i. i∈{0..n} ⟹ f$i * g$(n - i) = 0"
  proof-
    fix i assume i: "i∈{0..n}"
    show "f$i * g$(n - i) = 0"
    proof (cases "i < subdegree f ∨ n - i < subdegree g")
      case False with assms i show ?thesis by auto
    qed (auto simp: nth_less_subdegree_zero)
  qed
  thus "(f * g) $ n = 0" by (simp add: fps_mult_nth)
qed

lemma fps_mult_subdegree_ge:
  fixes   f g :: "'a::{comm_monoid_add,mult_zero} fps"
  assumes "f*g ≠ 0"
  shows   "subdegree (f*g) ≥ subdegree f + subdegree g"
  using   assms fps_mult_nth_eq0
  by      (intro subdegree_geI) simp

lemma subdegree_mult':
  fixes   f g :: "'a::{comm_monoid_add,mult_zero} fps"
  assumes "f $ subdegree f * g $ subdegree g ≠ 0"
  shows   "subdegree (f*g) = subdegree f + subdegree g"
proof-
  from assms have "(f * g) $ (subdegree f + subdegree g) ≠ 0" by simp
  hence "f*g ≠ 0" by fastforce
  hence "subdegree (f*g) ≥ subdegree f + subdegree g" using fps_mult_subdegree_ge by fast
  moreover from assms have "subdegree (f*g) ≤ subdegree f + subdegree g"
    by (intro subdegree_leI) simp
  ultimately show ?thesis by simp
qed

lemma subdegree_mult [simp]:
  fixes   f g :: "'a :: {semiring_no_zero_divisors} fps"
  assumes "f ≠ 0" "g ≠ 0"
  shows   "subdegree (f * g) = subdegree f + subdegree g"
  using   assms
  by      (intro subdegree_mult') simp

lemma fps_mult_nth_conv_upto_subdegree_left:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ n = (∑i=subdegree f..n. f $ i * g $ (n - i))"
proof (cases "subdegree f ≤ n")
  case True
  hence "{0..n} = {0..<subdegree f} ∪ {subdegree f..n}" by auto
  moreover have "{0..<subdegree f} ∩ {subdegree f..n} = {}" by auto
  ultimately show ?thesis
    using nth_less_subdegree_zero[of _ f]
    by    (simp add: fps_mult_nth sum.union_disjoint)
qed (simp add: fps_mult_nth nth_less_subdegree_zero)

lemma fps_mult_nth_conv_upto_subdegree_right:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ n = (∑i=0..n - subdegree g. f $ i * g $ (n - i))"
proof-
  have "{0..n} = {0..n - subdegree g} ∪ {n - subdegree g<..n}" by auto
  moreover have "{0..n - subdegree g} ∩ {n - subdegree g<..n} = {}" by auto
  moreover have "∀i∈{n - subdegree g<..n}. g $ (n - i) = 0"
    using nth_less_subdegree_zero[of _ g] by auto
  ultimately show ?thesis by (simp add: fps_mult_nth sum.union_disjoint)
qed

lemma fps_mult_nth_conv_inside_subdegrees:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "(f * g) $ n = (∑i=subdegree f..n - subdegree g. f $ i * g $ (n - i))"
proof (cases "subdegree f ≤ n - subdegree g")
  case True
  hence "{subdegree f..n} = {subdegree f..n - subdegree g} ∪ {n - subdegree g<..n}"
    by auto
  moreover have "{subdegree f..n - subdegree g} ∩ {n - subdegree g<..n} = {}" by auto
  moreover have "∀i∈{n - subdegree g<..n}. f $ i * g $ (n - i) = 0"
    using nth_less_subdegree_zero[of _ g] by auto
  ultimately show ?thesis
    using fps_mult_nth_conv_upto_subdegree_left[of f g n]
    by    (simp add: sum.union_disjoint)
next
  case False
  hence 1: "subdegree f > n - subdegree g" by simp
  show ?thesis
  proof (cases "f*g = 0")
    case False
    with 1 have "n < subdegree (f*g)" using fps_mult_subdegree_ge[of f g] by simp
    with 1 show ?thesis by auto
  qed (simp add: 1)
qed

lemma fps_mult_nth_outside_subdegrees:
  fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
  shows "n < subdegree f ⟹ (f * g) $ n = 0"
  and   "n < subdegree g ⟹ (f * g) $ n = 0"
  by    (auto simp: fps_mult_nth_conv_inside_subdegrees)


subsection ‹Formal power series form a commutative ring with unity, if the range of sequences
  they represent is a commutative ring with unity›

instance fps :: (semigroup_add) semigroup_add
proof
  fix a b c :: "'a fps"
  show "a + b + c = a + (b + c)"
    by (simp add: fps_ext add.assoc)
qed

instance fps :: (ab_semigroup_add) ab_semigroup_add
proof
  fix a b :: "'a fps"
  show "a + b = b + a"
    by (simp add: fps_ext add.commute)
qed

instance fps :: (monoid_add) monoid_add
proof
  fix a :: "'a fps"
  show "0 + a = a" by (simp add: fps_ext)
  show "a + 0 = a" by (simp add: fps_ext)
qed

instance fps :: (comm_monoid_add) comm_monoid_add
proof
  fix a :: "'a fps"
  show "0 + a = a" by (simp add: fps_ext)
qed

instance fps :: (cancel_semigroup_add) cancel_semigroup_add
proof
  fix a b c :: "'a fps"
  show "b = c" if "a + b = a + c"
    using that by (simp add: expand_fps_eq)
  show "b = c" if "b + a = c + a"
    using that by (simp add: expand_fps_eq)
qed

instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
proof
  fix a b c :: "'a fps"
  show "a + b - a = b"
    by (simp add: expand_fps_eq)
  show "a - b - c = a - (b + c)"
    by (simp add: expand_fps_eq diff_diff_eq)
qed

instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..

instance fps :: (group_add) group_add
proof
  fix a b :: "'a fps"
  show "- a + a = 0" by (simp add: fps_ext)
  show "a + - b = a - b" by (simp add: fps_ext)
qed

instance fps :: (ab_group_add) ab_group_add
proof
  fix a b :: "'a fps"
  show "- a + a = 0" by (simp add: fps_ext)
  show "a - b = a + - b" by (simp add: fps_ext)
qed

instance fps :: (zero_neq_one) zero_neq_one
  by standard (simp add: expand_fps_eq)

lemma fps_mult_assoc_lemma:
  fixes k :: nat
    and f :: "nat ⇒ nat ⇒ nat ⇒ 'a::comm_monoid_add"
  shows "(∑j=0..k. ∑i=0..j. f i (j - i) (n - j)) =
         (∑j=0..k. ∑i=0..k - j. f j i (n - j - i))"
  by (induct k) (simp_all add: Suc_diff_le sum.distrib add.assoc)

instance fps :: (semiring_0) semiring_0
proof
  fix a b c :: "'a fps"
  show "(a + b) * c = a * c + b * c"
    by (simp add: expand_fps_eq fps_mult_nth distrib_right sum.distrib)
  show "a * (b + c) = a * b + a * c"
    by (simp add: expand_fps_eq fps_mult_nth distrib_left sum.distrib)
  show "(a * b) * c = a * (b * c)"
  proof (rule fps_ext)
    fix n :: nat
    have "(∑j=0..n. ∑i=0..j. a$i * b$(j - i) * c$(n - j)) =
          (∑j=0..n. ∑i=0..n - j. a$j * b$i * c$(n - j - i))"
      by (rule fps_mult_assoc_lemma)
    then show "((a * b) * c) $ n = (a * (b * c)) $ n"
      by (simp add: fps_mult_nth sum_distrib_left sum_distrib_right mult.assoc)
  qed
qed

instance fps :: (semiring_0_cancel) semiring_0_cancel ..

lemma fps_mult_commute_lemma:
  fixes n :: nat
    and f :: "nat ⇒ nat ⇒ 'a::comm_monoid_add"
  shows "(∑i=0..n. f i (n - i)) = (∑i=0..n. f (n - i) i)"
  by (rule sum.reindex_bij_witness[where i="(-) n" and j="(-) n"]) auto

instance fps :: (comm_semiring_0) comm_semiring_0
proof
  fix a b c :: "'a fps"
  show "a * b = b * a"
  proof (rule fps_ext)
    fix n :: nat
    have "(∑i=0..n. a$i * b$(n - i)) = (∑i=0..n. a$(n - i) * b$i)"
      by (rule fps_mult_commute_lemma)
    then show "(a * b) $ n = (b * a) $ n"
      by (simp add: fps_mult_nth mult.commute)
  qed 
qed (simp add: distrib_right)

instance fps :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..

instance fps :: (semiring_1) semiring_1
proof
  fix a :: "'a fps"
  show "1 * a = a" "a * 1 = a" by (simp_all add: fps_one_mult)
qed

instance fps :: (comm_semiring_1) comm_semiring_1
  by standard simp

instance fps :: (semiring_1_cancel) semiring_1_cancel ..


subsection ‹Selection of the nth power of the implicit variable in the infinite sum›

lemma fps_square_nth: "(f^2) $ n = (∑k≤n. f $ k * f $ (n - k))"
  by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)

lemma fps_sum_nth: "sum f S $ n = sum (λk. (f k) $ n) S"
proof (cases "finite S")
  case True
  then show ?thesis by (induct set: finite) auto
next
  case False
  then show ?thesis by simp
qed


subsection ‹Injection of the basic ring elements and multiplication by scalars›

definition "fps_const c = Abs_fps (λn. if n = 0 then c else 0)"

lemma fps_nth_fps_const [simp]: "fps_const c $ n = (if n = 0 then c else 0)"
  unfolding fps_const_def by simp

lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0"
  by (simp add: fps_ext)

lemma fps_const_nonzero_eq_nonzero: "c ≠ 0 ⟹ fps_const c ≠ 0"
  using fps_nonzeroI[of "fps_const c" 0] by simp

lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1"
  by (simp add: fps_ext)

lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
  by (cases "c = 0") (auto intro!: subdegreeI)

lemma fps_const_neg [simp]: "- (fps_const (c::'a::group_add)) = fps_const (- c)"
  by (simp add: fps_ext)

lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + fps_const d = fps_const (c + d)"
  by (simp add: fps_ext)

lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f =
    Abs_fps (λn. if n = 0 then c + f$0 else f$n)"
  by (simp add: fps_ext)

lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) =
    Abs_fps (λn. if n = 0 then f$0 + c else f$n)"
  by (simp add: fps_ext)

lemma fps_const_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
  by (simp add: fps_ext)

lemmas fps_const_minus = fps_const_sub

lemma fps_const_mult[simp]:
  fixes c d :: "'a::{comm_monoid_add,mult_zero}"
  shows "fps_const c * fps_const d = fps_const (c * d)"
  by    (simp add: fps_eq_iff fps_mult_nth sum.neutral)

lemma fps_const_mult_left:
  "fps_const (c::'a::{comm_monoid_add,mult_zero}) * f = Abs_fps (λn. c * f$n)"
  unfolding fps_eq_iff fps_mult_nth
  by (simp add: fps_const_def mult_delta_left)

lemma fps_const_mult_right:
  "f * fps_const (c::'a::{comm_monoid_add,mult_zero}) = Abs_fps (λn. f$n * c)"
  unfolding fps_eq_iff fps_mult_nth
  by (simp add: fps_const_def mult_delta_right)

lemma fps_mult_left_const_nth [simp]:
  "(fps_const (c::'a::{comm_monoid_add,mult_zero}) * f)$n = c* f$n"
  by (simp add: fps_mult_nth mult_delta_left)

lemma fps_mult_right_const_nth [simp]:
  "(f * fps_const (c::'a::{comm_monoid_add,mult_zero}))$n = f$n * c"
  by (simp add: fps_mult_nth mult_delta_right)

lemma fps_const_power [simp]: "fps_const c ^ n = fps_const (c^n)"
  by (induct n) auto


subsection ‹Formal power series form an integral domain›

instance fps :: (ring) ring ..

instance fps :: (comm_ring) comm_ring ..

instance fps :: (ring_1) ring_1 ..

instance fps :: (comm_ring_1) comm_ring_1 ..

instance fps :: (semiring_no_zero_divisors) semiring_no_zero_divisors
proof
  fix a b :: "'a fps"
  assume "a ≠ 0" and "b ≠ 0"
  hence "(a * b) $ (subdegree a + subdegree b) ≠ 0" by simp
  thus "a * b ≠ 0" using fps_nonzero_nth by fast
qed

instance fps :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..

instance fps :: ("{cancel_semigroup_add,semiring_no_zero_divisors_cancel}")
  semiring_no_zero_divisors_cancel
proof
  fix a b c :: "'a fps"
  show "(a * c = b * c) = (c = 0 ∨ a = b)"
  proof
    assume ab: "a * c = b * c"
    have "c ≠ 0 ⟹ a = b"
    proof (rule fps_ext)
      fix n
      assume c: "c ≠ 0"
      show "a $ n = b $ n"
      proof (induct n rule: nat_less_induct)
        case (1 n)
        with ab c show ?case
          using fps_mult_nth_conv_upto_subdegree_right[of a c "subdegree c + n"]
                fps_mult_nth_conv_upto_subdegree_right[of b c "subdegree c + n"]
          by    (cases n) auto
      qed
    qed
    thus "c = 0 ∨ a = b" by fast
  qed auto
  show "(c * a = c * b) = (c = 0 ∨ a = b)"
  proof
    assume ab: "c * a = c * b"
    have "c ≠ 0 ⟹ a = b"
    proof (rule fps_ext)
      fix n
      assume c: "c ≠ 0"
      show "a $ n = b $ n"
      proof (induct n rule: nat_less_induct)
        case (1 n)
        moreover have "∀i∈{Suc (subdegree c)..subdegree c + n}. subdegree c + n - i < n" by auto
        ultimately show ?case
          using ab c fps_mult_nth_conv_upto_subdegree_left[of c a "subdegree c + n"]
                fps_mult_nth_conv_upto_subdegree_left[of c b "subdegree c + n"]
          by    (simp add: sum.atLeast_Suc_atMost)
      qed
    qed    
    thus "c = 0 ∨ a = b" by fast
  qed auto
qed

instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ..

instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..

instance fps :: (idom) idom ..

lemma fps_numeral_fps_const: "numeral k = fps_const (numeral k)"
  by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1 fps_const_add [symmetric])

lemmas numeral_fps_const = fps_numeral_fps_const

lemma neg_numeral_fps_const:
  "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)"
  by (simp add: numeral_fps_const)

lemma fps_numeral_nth: "numeral n $ i = (if i = 0 then numeral n else 0)"
  by (simp add: numeral_fps_const)

lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n"
  by (simp add: numeral_fps_const)

lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0"
  by (simp add: numeral_fps_const)

lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)

lemma fps_of_int: "fps_const (of_int c) = of_int c"
  by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
                             del: fps_const_minus fps_const_neg)

lemma fps_nth_of_nat [simp]:
  "(of_nat c) $ n = (if n=0 then of_nat c else 0)"
  by (simp add: fps_of_nat[symmetric])

lemma fps_nth_of_int [simp]:
  "(of_int c) $ n = (if n=0 then of_int c else 0)"
  by (simp add: fps_of_int[symmetric])

lemma fps_mult_of_nat_nth [simp]:
  shows "(of_nat k * f) $ n = of_nat k * f$n"
  and   "(f * of_nat k ) $ n = f$n * of_nat k"
  by    (simp_all add: fps_of_nat[symmetric])

lemma fps_mult_of_int_nth [simp]:
  shows "(of_int k * f) $ n = of_int k * f$n"
  and   "(f * of_int k ) $ n = f$n * of_int k"
  by    (simp_all add: fps_of_int[symmetric])

lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) ≠ 0"
proof
  assume "numeral f = (0 :: 'a fps)"
  from arg_cong[of _ _ "λF. F $ 0", OF this] show False by simp
qed 

lemma subdegree_power_ge:
  "f^n ≠ 0 ⟹ subdegree (f^n) ≥ n * subdegree f"
proof (induct n)
  case (Suc n) thus ?case using fps_mult_subdegree_ge by fastforce
qed simp

lemma fps_pow_nth_below_subdegree:
  "k < n * subdegree f ⟹ (f^n) $ k = 0"
proof (cases "f^n = 0")
  case False
  assume "k < n * subdegree f"
  with False have "k < subdegree (f^n)" using subdegree_power_ge[of f n] by simp
  thus "(f^n) $ k = 0" by auto
qed simp

lemma fps_pow_base [simp]:
  "(f ^ n) $ (n * subdegree f) = (f $ subdegree f) ^ n"
proof (induct n)
  case (Suc n)
  show ?case
  proof (cases "Suc n * subdegree f < subdegree f + subdegree (f^n)")
    case True with Suc show ?thesis
      by (auto simp: fps_mult_nth_eq0 distrib_right)
  next
    case False
    hence "∀i∈{Suc (subdegree f)..Suc n * subdegree f - subdegree (f ^ n)}.
            f ^ n $ (Suc n * subdegree f - i) = 0"
     by (auto simp: fps_pow_nth_below_subdegree)
   with False Suc show ?thesis
      using fps_mult_nth_conv_inside_subdegrees[of f "f^n" "Suc n * subdegree f"]
            sum.atLeast_Suc_atMost[of
              "subdegree f"
              "Suc n * subdegree f - subdegree (f ^ n)"
              "λi. f $ i * f ^ n $ (Suc n * subdegree f - i)"
            ]
      by    simp
  qed
qed simp

lemma subdegree_power_eqI:
  fixes f :: "'a::semiring_1 fps"
  shows "(f $ subdegree f) ^ n ≠ 0 ⟹ subdegree (f ^ n) = n * subdegree f"
proof (induct n)
  case (Suc n)
  from Suc have 1: "subdegree (f ^ n) = n * subdegree f" by fastforce
  with Suc(2) have "f $ subdegree f * f ^ n $ subdegree (f ^ n) ≠ 0" by simp
  with 1 show ?case using subdegree_mult'[of f "f^n"] by simp
qed simp

lemma subdegree_power [simp]:
  "subdegree ((f :: ('a :: semiring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
  by (cases "f = 0"; induction n) simp_all


subsection ‹The efps_Xtractor series fps_X›

lemma minus_one_power_iff: "(- (1::'a::ring_1)) ^ n = (if even n then 1 else - 1)"
  by (induct n) auto

definition "fps_X = Abs_fps (λn. if n = 1 then 1 else 0)"

lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1"
  by (auto intro!: subdegreeI simp: fps_X_def)

lemma fps_X_mult_nth [simp]:
  fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "(fps_X * f) $ n = (if n = 0 then 0 else f $ (n - 1))"
proof (cases n)
  case (Suc m)
  moreover have "(fps_X * f) $ Suc m = f $ (Suc m - 1)"
  proof (cases m)
    case 0 thus ?thesis using fps_mult_nth_1[of "fps_X" f] by (simp add: fps_X_def)
  next
    case (Suc k) thus ?thesis by (simp add: fps_mult_nth fps_X_def sum.atLeast_Suc_atMost)
  qed
  ultimately show ?thesis by simp
qed (simp add: fps_X_def)

lemma fps_X_mult_right_nth [simp]:
  fixes a :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "(a * fps_X) $ n = (if n = 0 then 0 else a $ (n - 1))"
proof (cases n)
  case (Suc m)
  moreover have "(a * fps_X) $ Suc m = a $ (Suc m - 1)"
  proof (cases m)
    case 0 thus ?thesis using fps_mult_nth_1[of a "fps_X"] by (simp add: fps_X_def)
  next
    case (Suc k)
    hence "(a * fps_X) $ Suc m = (∑i=0..k. a$i * fps_X$(Suc m - i)) + a$(Suc k)"
      by (simp add: fps_mult_nth fps_X_def)
    moreover have "∀i∈{0..k}. a$i * fps_X$(Suc m - i) = 0" by (auto simp: Suc fps_X_def)
    ultimately show ?thesis by (simp add: Suc)
  qed
  ultimately show ?thesis by simp
qed (simp add: fps_X_def)

lemma fps_mult_fps_X_commute:
  fixes a :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "fps_X * a = a * fps_X" 
  by (simp add: fps_eq_iff)

lemma fps_mult_fps_X_power_commute: "fps_X ^ k * a = a * fps_X ^ k"
proof (induct k)
  case (Suc k)
  hence "fps_X ^ Suc k * a = a * fps_X * fps_X ^ k"
    by (simp add: mult.assoc fps_mult_fps_X_commute[symmetric])
  thus ?case by (simp add: mult.assoc)
qed simp

lemma fps_subdegree_mult_fps_X:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  assumes "f ≠ 0"
  shows   "subdegree (fps_X * f) = subdegree f + 1"
  and     "subdegree (f * fps_X) = subdegree f + 1"
proof-
  show "subdegree (fps_X * f) = subdegree f + 1"
  proof (intro subdegreeI)
    fix i :: nat assume i: "i < subdegree f + 1"
    show "(fps_X * f) $ i = 0"
    proof (cases "i=0")
      case False with i show ?thesis by (simp add: nth_less_subdegree_zero)
    next
      case True thus ?thesis using fps_X_mult_nth[of f i] by simp
    qed
  qed (simp add: assms)
  thus "subdegree (f * fps_X) = subdegree f + 1"
    by (simp add: fps_mult_fps_X_commute)
qed

lemma fps_mult_fps_X_nonzero:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  assumes "f ≠ 0"
  shows   "fps_X * f ≠ 0"
  and     "f * fps_X ≠ 0"
  using   assms fps_subdegree_mult_fps_X[of f]
          fps_nonzero_subdegree_nonzeroI[of "fps_X * f"]
          fps_nonzero_subdegree_nonzeroI[of "f * fps_X"]
  by      auto

lemma fps_mult_fps_X_power_nonzero:
  assumes "f ≠ 0"
  shows   "fps_X ^ n * f ≠ 0"
  and     "f * fps_X ^ n ≠ 0"
proof -
  show "fps_X ^ n * f ≠ 0"
    by (induct n) (simp_all add: assms mult.assoc fps_mult_fps_X_nonzero(1))
  thus "f * fps_X ^ n ≠ 0"
    by (simp add: fps_mult_fps_X_power_commute)
qed

lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (λm. if m = n then 1 else 0)"
  by (induction n) (auto simp: fps_eq_iff)

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)"
  by (simp add: fps_X_power_iff)

lemma fps_X_power_subdegree: "subdegree (fps_X^n) = n"
  by (auto intro: subdegreeI)

lemma fps_X_power_mult_nth:
  "(fps_X^k * f) $ n = (if n < k then 0 else f $ (n - k))"
  by  (cases "n<k")
      (simp_all add: fps_mult_nth_conv_upto_subdegree_left fps_X_power_subdegree sum.atLeast_Suc_atMost)

lemma fps_X_power_mult_right_nth:
  "(f * fps_X^k) $ n = (if n < k then 0 else f $ (n - k))"
  using fps_mult_fps_X_power_commute[of k f] fps_X_power_mult_nth[of k f] by simp

lemma fps_subdegree_mult_fps_X_power:
  assumes "f ≠ 0"
  shows   "subdegree (fps_X ^ n * f) = subdegree f + n"
  and     "subdegree (f * fps_X ^ n) = subdegree f + n"
proof -
  from assms show "subdegree (fps_X ^ n * f) = subdegree f + n"
    by (induct n)
       (simp_all add: algebra_simps fps_subdegree_mult_fps_X(1) fps_mult_fps_X_power_nonzero(1))
  thus "subdegree (f * fps_X ^ n) = subdegree f + n"
    by (simp add: fps_mult_fps_X_power_commute)
qed

lemma fps_mult_fps_X_plus_1_nth:
  "((1+fps_X)*a) $n = (if n = 0 then (a$n :: 'a::semiring_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 + fps_X)*a) $ n = sum (λi. (1 + fps_X) $ i * a $ (n - i)) {0..n}"
    by (simp add: fps_mult_nth)
  also have "… = sum (λi. (1+fps_X)$i * a$(n-i)) {0.. 1}"
    unfolding Suc by (rule sum.mono_neutral_right) auto
  also have "… = (if n = 0 then a$n else a$n + a$(n - 1))"
    by (simp add: Suc)
  finally show ?thesis .
qed

lemma fps_mult_right_fps_X_plus_1_nth:
  fixes a :: "'a :: semiring_1 fps"
  shows "(a*(1+fps_X)) $ n = (if n = 0 then a$n else a$n + a$(n - 1))"
  using fps_mult_fps_X_plus_1_nth
  by    (simp add: distrib_left fps_mult_fps_X_commute distrib_right)

lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) ≠ fps_const c"
proof
  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 fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) ≠ 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) ≠ 1"
  by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp

lemma fps_X_neq_numeral [simp]: "fps_X ≠ 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 ^ m = fps_X ^ n ⟷ m = n"
proof
  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


subsection ‹Shifting and slicing›

definition fps_shift :: "nat ⇒ 'a fps ⇒ 'a fps" where
  "fps_shift n f = Abs_fps (λi. f $ (i + n))"

lemma fps_shift_nth [simp]: "fps_shift n f $ i = f $ (i + n)"
  by (simp add: fps_shift_def)

lemma fps_shift_0 [simp]: "fps_shift 0 f = f"
  by (intro fps_ext) (simp add: fps_shift_def)

lemma fps_shift_zero [simp]: "fps_shift n 0 = 0"
  by (intro fps_ext) (simp add: fps_shift_def)

lemma fps_shift_one: "fps_shift n 1 = (if n = 0 then 1 else 0)"
  by (intro fps_ext) (simp add: fps_shift_def)

lemma fps_shift_fps_const: "fps_shift n (fps_const c) = (if n = 0 then fps_const c else 0)"
  by (intro fps_ext) (simp add: fps_shift_def)

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_fps_X [simp]:
  "n ≥ 1 ⟹ fps_shift n fps_X = (if n = 1 then 1 else 0)"
  by (intro fps_ext) (auto simp: fps_X_def)

lemma fps_shift_fps_X_power [simp]:
  "n ≤ m ⟹ fps_shift n (fps_X ^ m) = fps_X ^ (m - n)"
 by (intro fps_ext) auto

lemma fps_shift_subdegree [simp]:
  "n ≤ subdegree f ⟹ subdegree (fps_shift n f) = subdegree f - n"
  by (cases "f=0") (auto intro: subdegreeI simp: nth_less_subdegree_zero)

lemma fps_shift_fps_shift:
  "fps_shift (m + n) f = fps_shift m (fps_shift n f)"
  by (rule fps_ext) (simp add: add_ac)

lemma fps_shift_fps_shift_reorder:
  "fps_shift m (fps_shift n f) = fps_shift n (fps_shift m f)"
  using fps_shift_fps_shift[of m n f] fps_shift_fps_shift[of n m f] by (simp add: add.commute)

lemma fps_shift_rev_shift:
  "m ≤ n ⟹ fps_shift n (Abs_fps (λk. if k<m then 0 else f $ (k-m))) = fps_shift (n-m) f"
  "m > n ⟹ fps_shift n (Abs_fps (λk. if k<m then 0 else f $ (k-m))) =
    Abs_fps (λk. if k<m-n then 0 else f $ (k-(m-n)))"
proof -
  assume "m ≤ n"
  thus "fps_shift n (Abs_fps (λk. if k<m then 0 else f $ (k-m))) = fps_shift (n-m) f"
    by (intro fps_ext) auto
next
  assume mn: "m > n"
  hence "⋀k. k ≥ m-n ⟹ k+n-m = k - (m-n)" by auto
  thus
    "fps_shift n (Abs_fps (λk. if k<m then 0 else f $ (k-m))) =
      Abs_fps (λk. if k<m-n then 0 else f $ (k-(m-n)))"
    by (intro fps_ext) auto
qed

lemma fps_shift_add:
  "fps_shift n (f + g) = fps_shift n f + fps_shift n g"
  by (simp add: fps_eq_iff)

lemma fps_shift_diff:
  "fps_shift n (f - g) = fps_shift n f - fps_shift n g"
  by (auto intro: fps_ext)

lemma fps_shift_uminus:
  "fps_shift n (-f) = - fps_shift n f"
  by (auto intro: fps_ext)

lemma fps_shift_mult:
  assumes "n ≤ subdegree (g :: 'b :: {comm_monoid_add, mult_zero} fps)"
  shows "fps_shift n (h*g) = h * fps_shift n g"
proof-
  have case1: "⋀a b::'b fps. 1 ≤ subdegree b ⟹ fps_shift 1 (a*b) = a * fps_shift 1 b"
  proof (rule fps_ext)
    fix a b :: "'b fps"
    and n :: nat
    assume b: "1 ≤ subdegree b"
    have "⋀i. i ≤ n ⟹ n + 1 - i = (n-i) + 1"
      by (simp add: algebra_simps)
    with b show "fps_shift 1 (a*b) $ n = (a * fps_shift 1 b) $ n"
      by (simp add: fps_mult_nth nth_less_subdegree_zero)
  qed
  have "n ≤ subdegree g ⟹ fps_shift n (h*g) = h * fps_shift n g"
  proof (induct n)
    case (Suc n)
    have "fps_shift (Suc n) (h*g) = fps_shift 1 (fps_shift n (h*g))"
      by (simp add: fps_shift_fps_shift[symmetric])
    also have "… = h * (fps_shift 1 (fps_shift n g))"
      using Suc case1 by force
    finally show ?case by (simp add: fps_shift_fps_shift[symmetric])
  qed simp
  with assms show ?thesis by fast
qed

lemma fps_shift_mult_right_noncomm:
  assumes "n ≤ subdegree (g :: 'b :: {comm_monoid_add, mult_zero} fps)"
  shows "fps_shift n (g*h) = fps_shift n g * h"
proof-
  have case1: "⋀a b::'b fps. 1 ≤ subdegree a ⟹ fps_shift 1 (a*b) = fps_shift 1 a * b"
  proof (rule fps_ext)
    fix a b :: "'b fps"
    and n :: nat
    assume "1 ≤ subdegree a"
    hence "fps_shift 1 (a*b) $ n = (∑i=Suc 0..Suc n. a$i * b$(n+1-i))"
      using sum.atLeast_Suc_atMost[of 0 "n+1" "λi. a$i * b$(n+1-i)"]
      by    (simp add: fps_mult_nth nth_less_subdegree_zero)
    thus "fps_shift 1 (a*b) $ n = (fps_shift 1 a * b) $ n"
      using sum.shift_bounds_cl_Suc_ivl[of "λi. a$i * b$(n+1-i)" 0 n]
      by    (simp add: fps_mult_nth)
  qed
  have "n ≤ subdegree g ⟹ fps_shift n (g*h) = fps_shift n g * h"
  proof (induct n)
    case (Suc n)
    have "fps_shift (Suc n) (g*h) = fps_shift 1 (fps_shift n (g*h))"
      by (simp add: fps_shift_fps_shift[symmetric])
    also have "… = (fps_shift 1 (fps_shift n g)) * h"
      using Suc case1 by force
    finally show ?case by (simp add: fps_shift_fps_shift[symmetric])
  qed simp
  with assms show ?thesis by fast
qed

lemma fps_shift_mult_right:
  assumes "n ≤ subdegree (g :: 'b :: comm_semiring_0 fps)"
  shows   "fps_shift n (g*h) = h * fps_shift n g"
  by      (simp add: assms fps_shift_mult_right_noncomm mult.commute)

lemma fps_shift_mult_both:
  fixes   f g :: "'a::{comm_monoid_add, mult_zero} fps"
  assumes "m ≤ subdegree f" "n ≤ subdegree g"
  shows   "fps_shift m f * fps_shift n g = fps_shift (m+n) (f*g)"
  using   assms
  by      (simp add: fps_shift_mult fps_shift_mult_right_noncomm fps_shift_fps_shift)

lemma fps_shift_subdegree_zero_iff [simp]:
  "fps_shift (subdegree f) f = 0 ⟷ f = 0"
  by (subst (1) nth_subdegree_zero_iff[symmetric], cases "f = 0")
     (simp_all del: nth_subdegree_zero_iff)

lemma fps_shift_times_fps_X:
  fixes f g :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "1 ≤ subdegree f ⟹ fps_shift 1 f * fps_X = f"
  by (intro fps_ext) (simp add: nth_less_subdegree_zero)

lemma fps_shift_times_fps_X' [simp]:
  fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "fps_shift 1 (f * fps_X) = f"
  by (intro fps_ext) (simp add: nth_less_subdegree_zero)

lemma fps_shift_times_fps_X'':
  fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fps"
  shows "1 ≤ n ⟹ fps_shift n (f * fps_X) = fps_shift (n - 1) f"
  by (intro fps_ext) (simp add: nth_less_subdegree_zero)

lemma fps_shift_times_fps_X_power:
  "n ≤ subdegree f ⟹ fps_shift n f * fps_X ^ n = f"
  by (intro fps_ext) (simp add: 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"
  by (intro fps_ext) (simp add: fps_X_power_mult_right_nth nth_less_subdegree_zero)

lemma fps_shift_times_fps_X_power'':
  "m ≤ n ⟹ fps_shift n (f * fps_X^m) = fps_shift (n - m) f"
  by (intro fps_ext) (simp add: fps_X_power_mult_right_nth nth_less_subdegree_zero)

lemma fps_shift_times_fps_X_power''':
  "m > n ⟹ fps_shift n (f * fps_X^m) = f * fps_X^(m - n)"
proof (cases "f=0")
  case False
  assume m: "m>n"
  hence "m = n + (m-n)" by auto
  with False m show ?thesis
    using power_add[of "fps_X::'a fps" n "m-n"]
          fps_shift_mult_right_noncomm[of n "f * fps_X^n" "fps_X^(m-n)"]
    by    (simp add: mult.assoc fps_subdegree_mult_fps_X_power(2))
qed simp

lemma subdegree_decompose:
  "f = fps_shift (subdegree f) f * fps_X ^ subdegree f"
  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth)

lemma subdegree_decompose':
  "n ≤ subdegree f ⟹ 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)

instantiation fps :: (zero) unit_factor
begin
definition fps_unit_factor_def [simp]:
  "unit_factor f = fps_shift (subdegree f) f"
instance ..
end

lemma fps_unit_factor_zero_iff: "unit_factor (f::'a::zero fps) = 0 ⟷ f = 0"
  by simp

lemma fps_unit_factor_nth_0: "f ≠ 0 ⟹ unit_factor f $ 0 ≠ 0"
  by simp

lemma fps_X_unit_factor: "unit_factor (fps_X :: 'a :: zero_neq_one fps) = 1"
 by (intro fps_ext) auto

lemma fps_X_power_unit_factor: "unit_factor (fps_X ^ n) = 1"
proof-
  define X :: "'a fps" where "X ≡ fps_X"
  hence "unit_factor (X^n) = fps_shift n (X^n)"
    by (simp add: fps_X_power_subdegree)
  moreover have "fps_shift n (X^n) = 1"
    by (auto intro: fps_ext simp: fps_X_power_iff X_def)
  ultimately show ?thesis by (simp add: X_def)
qed

lemma fps_unit_factor_decompose:
  "f = unit_factor f * fps_X ^ subdegree f"
  by (simp add: subdegree_decompose)

lemma fps_unit_factor_decompose':
  "f = fps_X ^ subdegree f * unit_factor f"
  using fps_unit_factor_decompose by (simp add: fps_mult_fps_X_power_commute)

lemma fps_unit_factor_uminus:
  "unit_factor (-f) = - unit_factor (f::'a::group_add fps)"
  by    (simp add: fps_shift_uminus)

lemma fps_unit_factor_shift:
  assumes "n ≤ subdegree f"
  shows   "unit_factor (fps_shift n f) = unit_factor f"
  by      (simp add: assms fps_shift_fps_shift[symmetric])

lemma fps_unit_factor_mult_fps_X:
  fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fps"
  shows "unit_factor (fps_X * f) = unit_factor f"
  and   "unit_factor (f * fps_X) = unit_factor f"
proof -
  show "unit_factor (fps_X * f) = unit_factor f"
    by (cases "f=0") (auto intro: fps_ext simp: fps_subdegree_mult_fps_X(1))
  thus "unit_factor (f * fps_X) = unit_factor f" by (simp add: fps_mult_fps_X_commute)
qed

lemma fps_unit_factor_mult_fps_X_power:
  shows "unit_factor (fps_X ^ n * f) = unit_factor f"
  and   "unit_factor (f * fps_X ^ n) = unit_factor f"
proof -
  show "unit_factor (fps_X ^ n * f) = unit_factor f"
  proof (induct n)
    case (Suc m) thus ?case
      using fps_unit_factor_mult_fps_X(1)[of "fps_X ^ m * f"] by (simp add: mult.assoc)
  qed simp
  thus "unit_factor (f * fps_X ^ n) = unit_factor f"
    by (simp add: fps_mult_fps_X_power_commute)
qed

lemma fps_unit_factor_mult_unit_factor:
  fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
  shows "unit_factor (f * unit_factor g) = unit_factor (f * g)"
  and   "unit_factor (unit_factor f * g) = unit_factor (f * g)"
proof -
  show "unit_factor (f * unit_factor g) = unit_factor (f * g)"
  proof (cases "f*g = 0")
    case False thus ?thesis
      using fps_mult_subdegree_ge[of f g] fps_unit_factor_shift[of "subdegree g" "f*g"]
      by    (simp add: fps_shift_mult)
  next
    case True
    moreover have "f * unit_factor g = fps_shift (subdegree g) (f*g)"
      by (simp add: fps_shift_mult)
    ultimately show ?thesis by simp
  qed
  show "unit_factor (unit_factor f * g) = unit_factor (f * g)"
  proof (cases "f*g = 0")
    case False thus ?thesis
      using fps_mult_subdegree_ge[of f g] fps_unit_factor_shift[of "subdegree f" "f*g"]
      by    (simp add: fps_shift_mult_right_noncomm)
  next
    case True
    moreover have "unit_factor f * g = fps_shift (subdegree f) (f*g)"
      by (simp add: fps_shift_mult_right_noncomm)
    ultimately show ?thesis by simp
  qed
qed

lemma fps_unit_factor_mult_both_unit_factor:
  fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
  shows "unit_factor (unit_factor f * unit_factor g) = unit_factor (f * g)"
  using fps_unit_factor_mult_unit_factor(1)[of "unit_factor f" g]
        fps_unit_factor_mult_unit_factor(2)[of f g]
  by    simp

lemma fps_unit_factor_mult':
  fixes   f g :: "'a::{comm_monoid_add,mult_zero} fps"
  assumes "f $ subdegree f * g $ subdegree g ≠ 0"
  shows   "unit_factor (f * g) = unit_factor f * unit_factor g"
  using   assms
  by      (simp add: subdegree_mult' fps_shift_mult_both)

lemma fps_unit_factor_mult:
  fixes f g :: "'a::semiring_no_zero_divisors fps"
  shows "unit_factor (f * g) = unit_factor f * unit_factor g"
  using fps_unit_factor_mult'[of f g]
  by    (cases "f=0 ∨ g=0") auto

definition "fps_cutoff n f = Abs_fps (λi. if i < n then f$i else 0)"

lemma fps_cutoff_nth [simp]: "fps_cutoff n f $ i = (if i < n then f$i else 0)"
  unfolding fps_cutoff_def by simp

lemma fps_cutoff_zero_iff: "fps_cutoff n f = 0 ⟷ (f = 0 ∨ n ≤ subdegree f)"
proof
  assume A: "fps_cutoff n f = 0"
  thus "f = 0 ∨ n ≤ subdegree f"
  proof (cases "f = 0")
    assume "f ≠ 0"
    with A have "n ≤ subdegree f"
      by (intro subdegree_geI) (simp_all add: fps_eq_iff split: if_split_asm)
    thus ?thesis ..
  qed simp
qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero)

lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0"
  by (simp add: fps_eq_iff)

lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0"
  by (simp add: fps_eq_iff)

lemma fps_cutoff_one: "fps_cutoff n 1 = (if n = 0 then 0 else 1)"
  by (simp add: fps_eq_iff)

lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)"
  by (simp add: fps_eq_iff)

lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)"
  by (simp add: numeral_fps_const fps_cutoff_fps_const)

lemma fps_shift_cutoff:
  "fps_shift n f * fps_X^n + fps_cutoff n f = f"
  by (simp add: fps_eq_iff fps_X_power_mult_right_nth)

lemma fps_shift_cutoff':
  "fps_X^n * fps_shift n f + fps_cutoff n f = f"
  by (simp add: fps_eq_iff fps_X_power_mult_nth)

lemma fps_cutoff_left_mult_nth:
  "k < n ⟹ (fps_cutoff n f * g) $ k = (f * g) $ k"
  by (simp add: fps_mult_nth)

lemma fps_cutoff_right_mult_nth:
  assumes "k < n"
  shows   "(f * fps_cutoff n g) $ k = (f * g) $ k"
proof-
  from assms have "∀i∈{0..k}. fps_cutoff n g $ (k - i) = g $ (k - i)" by auto
  thus ?thesis by (simp add: fps_mult_nth)
qed

subsection ‹Formal Power series form a metric space›

instantiation fps :: ("{minus,zero}") dist
begin

definition
  dist_fps_def: "dist (a :: 'a fps) b = (if a = b then 0 else inverse (2 ^ subdegree (a - b)))"

lemma dist_fps_ge0: "dist (a :: 'a fps) b ≥ 0"
  by (simp add: dist_fps_def)

instance ..

end

instantiation fps :: (group_add) metric_space
begin

definition uniformity_fps_def [code del]:
  "(uniformity :: ('a fps × 'a fps) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition open_fps_def' [code del]:
  "open (U :: 'a fps set) ⟷ (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a"
  by (simp add: dist_fps_def)

instance
proof
  show th: "dist a b = 0 ⟷ a = b" for a b :: "'a fps"
    by (simp add: dist_fps_def split: if_split_asm)
  then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp

  fix a b c :: "'a fps"
  consider "a = b" | "c = a ∨ c = b" | "a ≠ b" "a ≠ c" "b ≠ c" by blast
  then show "dist a b ≤ dist a c + dist b c"
  proof cases
    case 1
    then show ?thesis by (simp add: dist_fps_def)
  next
    case 2
    then show ?thesis
      by (cases "c = a") (simp_all add: th dist_fps_sym)
  next
    case neq: 3
    have False if "dist a b > dist a c + dist b c"
    proof -
      let ?n = "subdegree (a - b)"
      from neq have "dist a b > 0" "dist b c > 0" and "dist a c > 0" by (simp_all add: dist_fps_def)
      with that have "dist a b > dist a c" and "dist a b > dist b c" by simp_all
      with neq have "?n < subdegree (a - c)" and "?n < subdegree (b - c)"
        by (simp_all add: dist_fps_def field_simps)
      hence "(a - c) $ ?n = 0" and "(b - c) $ ?n = 0"
        by (simp_all only: nth_less_subdegree_zero)
      hence "(a - b) $ ?n = 0" by simp
      moreover from neq have "(a - b) $ ?n ≠ 0" by (intro nth_subdegree_nonzero) simp_all
      ultimately show False by contradiction
    qed
    thus ?thesis by (auto simp add: not_le[symmetric])
  qed
qed (rule open_fps_def' uniformity_fps_def)+

end

declare uniformity_Abort[where 'a="'a :: group_add fps", code]

lemma open_fps_def: "open (S :: 'a::group_add fps set) = (∀a ∈ S. ∃r. r >0 ∧ {y. dist y a < r} ⊆ S)"
  unfolding open_dist subset_eq by simp

text ‹The infinite sums and justification of the notation in textbooks.›

lemma reals_power_lt_ex:
  fixes x y :: real
  assumes xp: "x > 0"
    and y1: "y > 1"
  shows "∃k>0. (1/y)^k < x"
proof -
  have yp: "y > 0"
    using y1 by simp
  from reals_Archimedean2[of "max 0 (- log y x) + 1"]
  obtain k :: nat where k: "real k > max 0 (- log y x) + 1"
    by blast
  from k have kp: "k > 0"
    by simp
  from k have "real k > - log y x"
    by simp
  then have "ln y * real k > - ln x"
    unfolding log_def
    using ln_gt_zero_iff[OF yp] y1
    by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric])
  then have "ln y * real k + ln x > 0"
    by simp
  then have "exp (real k * ln y + ln x) > exp 0"
    by (simp add: ac_simps)
  then have "y ^ k * x > 1"
    unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
    by simp
  then have "x > (1 / y)^k" using yp
    by (simp add: field_simps)
  then show ?thesis
    using kp by blast
qed

lemma fps_sum_rep_nth: "(sum (λi. fps_const(a$i)*fps_X^i) {0..m})$n = (if n ≤ m then a$n else 0)"
  by (simp add: fps_sum_nth if_distrib cong del: if_weak_cong)

lemma fps_notation: "(λn. sum (λi. fps_const(a$i) * fps_X^i) {0..n}) ⇢ a"
  (is "?s ⇢ a")
proof -
  have "∃n0. ∀n ≥ n0. dist (?s n) a < r" if "r > 0" for r
  proof -
    obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
      using reals_power_lt_ex[OF ‹r > 0›, of 2] by auto
    show ?thesis
    proof -
      have "dist (?s n) a < r" if nn0: "n ≥ n0" for n
      proof