# Theory 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
Primes
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"

lemma fps_nth_Abs_fps [simp]: "Abs_fps f \$ n = f n"

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)"

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"
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"

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

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"

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"

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]:
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

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)

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

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)

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))"
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]

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]
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

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 ‹Ring structure›

proof
fix a b c :: "'a fps"
show "a + b + c = a + (b + c)"
qed

proof
fix a b :: "'a fps"
show "a + b = b + a"
qed

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

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

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

proof
fix a b c :: "'a fps"
show "a + b - a = b"
show "a - b - c = a - (b + c)"
qed

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

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

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))"

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"
qed

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 ..

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

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"

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_eq_0_iff [simp]: "fps_const c = 0 ⟷ c = 0"
by (auto simp: fps_eq_iff)

lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1"

lemma fps_const_eq_1_iff [simp]: "fps_const c = 1 ⟷ c = 1"
by (auto simp: fps_eq_iff)

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)"

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

Abs_fps (λn. if n = 0 then c + f\$0 else f\$n)"

Abs_fps (λn. if n = 0 then f\$0 + c else f\$n)"

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

lemmas fps_const_minus = fps_const_sub

lemma fps_const_mult[simp]:
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

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

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

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

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

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 ..

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"]
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_of_nat: "fps_const (of_nat c) = of_nat c"

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 semiring_char_fps [simp]: "CHAR('a :: comm_semiring_1 fps) = CHAR('a)"
by (rule CHAR_eqI) (auto simp flip: fps_of_nat simp: of_nat_eq_0_iff_char_dvd)

instance fps :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
by (rule semiring_prime_charI) auto
instance fps :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
by standard
instance fps :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
by standard
instance fps :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
by standard

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)"

lemma fps_numeral_nth: "numeral n \$ i = (if i = 0 then numeral n else 0)"

lemma fps_numeral_nth_0 [simp]: "numeral n \$ 0 = numeral n"

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

lemma fps_nth_of_nat [simp]:
"(of_nat c) \$ n = (if n=0 then of_nat c else 0)"

lemma fps_nth_of_int [simp]:
"(of_int c) \$ n = (if n=0 then of_int c else 0)"

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"

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"

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

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]:
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

lemma fps_X_mult_right_nth [simp]:
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)"
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

lemma fps_mult_fps_X_commute:
shows "fps_X * a = a * fps_X"

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"
thus ?case by (simp add: mult.assoc)
qed simp

lemma fps_subdegree_mult_fps_X:
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
thus "subdegree (f * fps_X) = subdegree f + 1"
qed

lemma fps_mult_fps_X_nonzero:
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"
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)"

lemma fps_X_power_nth[simp]: "(fps_X^k) \$n = (if n = k then 1 else 0)"

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")

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)
thus "subdegree (f * fps_X ^ n) = subdegree f + n"
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
next
case (Suc m)
have "((1 + fps_X)*a) \$ n = sum (λi. (1 + fps_X) \$ i * a \$ (n - i)) {0..n}"
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))"
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)"

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)"

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)"

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

"fps_shift n (f + g) = fps_shift n f + fps_shift n g"

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"
with b show "fps_shift 1 (a*b) \$ n = (a * fps_shift 1 b) \$ n"
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))"
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)"]
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]
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))"
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]:
shows "fps_shift 1 (f * fps_X) = f"
by (intro fps_ext) (simp add: nth_less_subdegree_zero)

lemma fps_shift_times_fps_X'':
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)"]
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)"
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"

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)"

lemma fps_unit_factor_shift:
assumes "n ≤ subdegree f"
shows   "unit_factor (fps_shift n f) = unit_factor f"

lemma fps_unit_factor_mult_fps_X:
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"
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"]
next
case True
moreover have "f * unit_factor g = fps_shift (subdegree g) (f*g)"
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"]
next
case True
moreover have "unit_factor f * g = fps_shift (subdegree f) (f*g)"
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

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"

lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0"

lemma fps_cutoff_one: "fps_cutoff n 1 = (if n = 0 then 0 else 1)"

lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)"

lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)"

lemma fps_shift_cutoff:
"fps_shift n f * fps_X^n + fps_cutoff n f = f"

lemma fps_shift_cutoff':
"fps_X^n * fps_shift n f + fps_cutoff n f = f"

lemma fps_cutoff_left_mult_nth:
"k < n ⟹ (fps_cutoff n f * g) \$ k = (f * g) \$ k"

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 ‹Metrizability›

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"

instance ..

end

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"

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)"
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
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"
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
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 -
from that have thnn0: "(1/2)^n ≤ (1/2 :: real)^n0"
show ?thesis
proof (cases "?s n = a")
case True
then show ?thesis
unfolding dist_eq_0_iff[of "?s n" a, symmetric]
using ‹r > 0› by (simp del: dist_eq_0_iff)
next
case False
from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n - a)"
from False have kn: "subdegree (?s n - a) > n"
by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth)
then have "dist (?s n) a < (1/2)^n"
also have "… ≤ (1/2)^n0"
using nn0 by (simp add: field_split_simps)
also have "… < r"
using n0 by simp
finally show ?thesis .
qed
qed
then show ?thesis by blast
qed
qed
then show ?thesis
unfolding lim_sequentially by blast
qed

subsection ‹Division›

declare sum.cong[fundef_cong]

```