# Theory Formal_Laurent_Series

```(*
Title:      HOL/Computational_Algebra/Formal_Laurent_Series.thy
Author:     Jeremy Sylvestre, University of Alberta (Augustana Campus)
*)

section ‹A formalization of formal Laurent series›

theory Formal_Laurent_Series
imports
Polynomial_FPS
begin

subsection ‹The type of formal Laurent series›

subsubsection ‹Type definition›

typedef (overloaded) 'a fls = "{f::int ⇒ 'a::zero. ∀⇩∞ n::nat. f (- int n) = 0}"
morphisms fls_nth Abs_fls
proof
show "(λx. 0) ∈ {f::int ⇒ 'a::zero. ∀⇩∞ n::nat. f (- int n) = 0}"
by simp
qed

setup_lifting type_definition_fls

unbundle fps_notation
notation fls_nth (infixl "\$\$" 75)

lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]

lemma fls_eq_iff: "f = g ⟷ (∀n. f \$\$ n = g \$\$ n)"

lemma nth_Abs_fls [simp]: "∀⇩∞n. f (- int n) = 0 ⟹ Abs_fls f \$\$ n = f n"

lemmas nth_Abs_fls_finite_nonzero_neg_nth = nth_Abs_fls[OF iffD2, OF eventually_cofinite]
lemmas nth_Abs_fls_ex_nat_lower_bound = nth_Abs_fls[OF iffD2, OF MOST_nat]
lemmas nth_Abs_fls_nat_lower_bound = nth_Abs_fls_ex_nat_lower_bound[OF exI]

lemma nth_Abs_fls_ex_lower_bound:
assumes "∃N. ∀n<N. f n = 0"
shows   "Abs_fls f \$\$ n = f n"
proof (intro nth_Abs_fls_ex_nat_lower_bound)
from assms obtain N::int where "∀n<N. f n = 0" by fast
hence "∀n > (if N < 0 then nat (-N) else 0). f (-int n) = 0" by auto
thus "∃M. ∀n>M. f (- int n) = 0" by fast
qed

lemmas nth_Abs_fls_lower_bound = nth_Abs_fls_ex_lower_bound[OF exI]

lemmas MOST_fls_neg_nth_eq_0 [simp] = CollectD[OF fls_nth]
lemmas fls_finite_nonzero_neg_nth = iffD1[OF eventually_cofinite MOST_fls_neg_nth_eq_0]

lemma fls_nth_vanishes_below_natE:
fixes   f :: "'a::zero fls"
obtains N :: nat
where   "∀n>N. f\$\$(-int n) = 0"
using   iffD1[OF MOST_nat MOST_fls_neg_nth_eq_0]
by      blast

lemma fls_nth_vanishes_belowE:
fixes   f :: "'a::zero fls"
obtains N :: int
where   "∀n<N. f\$\$n = 0"
proof-
obtain K :: nat where K: "∀n>K. f\$\$(-int n) = 0" by (elim fls_nth_vanishes_below_natE)
have "∀n < -int K. f\$\$n = 0"
proof clarify
fix n assume n: "n < -int K"
define m where "m ≡ nat (-n)"
with n have "m > K" by simp
moreover from n m_def have "f\$\$n = f \$\$ (-int m)" by simp
ultimately show "f \$\$ n = 0" using K by simp
qed
thus "(⋀N. ∀n<N. f \$\$ n = 0 ⟹ thesis) ⟹ thesis" by fast
qed

subsubsection ‹Definition of basic Laurent series›

instantiation fls :: (zero) zero
begin
lift_definition zero_fls :: "'a fls" is "λ_. 0" by simp
instance ..
end

lemma fls_zero_nth [simp]: "0 \$\$ n = 0"

lemma fls_zero_eqI: "(⋀n. f\$\$n = 0) ⟹ f = 0"
by (fastforce intro: fls_eqI)

lemma fls_nonzeroI: "f\$\$n ≠ 0 ⟹ f ≠ 0"
by auto

lemma fls_nonzero_nth: "f ≠ 0 ⟷ (∃ n. f \$\$ n ≠ 0)"
using fls_zero_eqI by fastforce

lemma fls_trivial_delta_eq_zero [simp]: "b = 0 ⟹ Abs_fls (λn. if n=a then b else 0) = 0"
by (intro fls_zero_eqI) simp

lemma fls_delta_nth [simp]:
"Abs_fls (λn. if n=a then b else 0) \$\$ n = (if n=a then b else 0)"
using nth_Abs_fls_lower_bound[of a "λn. if n=a then b else 0"] by simp

instantiation fls :: ("{zero,one}") one
begin
lift_definition one_fls :: "'a fls" is "λk. if k = 0 then 1 else 0"
instance ..
end

lemma fls_one_nth [simp]:
"1 \$\$ n = (if n = 0 then 1 else 0)"

instance fls :: (zero_neq_one) zero_neq_one
proof (standard, standard)
assume "(0::'a fls) = (1::'a fls)"
hence "(0::'a fls) \$\$ 0 = (1::'a fls) \$\$ 0" by simp
thus False by simp
qed

definition fls_const :: "'a::zero ⇒ 'a fls"
where "fls_const c ≡ Abs_fls (λn. if n = 0 then c else 0)"

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

lemma fls_const_0 [simp]: "fls_const 0 = 0"
unfolding fls_const_def using fls_trivial_delta_eq_zero by fast

lemma fls_const_nonzero: "c ≠ 0 ⟹ fls_const c ≠ 0"
using fls_nonzeroI[of "fls_const c" 0] by simp

lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 ⟷ c = 0"
by (auto simp: fls_eq_iff)

lemma fls_const_1 [simp]: "fls_const 1 = 1"
unfolding fls_const_def one_fls_def ..

lemma fls_const_eq_1_iff [simp]: "fls_const c = 1 ⟷ c = 1"
by (auto simp: fls_eq_iff)

lift_definition fls_X :: "'a::{zero,one} fls"
is "λn. if n = 1 then 1 else 0"
by simp

lemma fls_X_nth [simp]:
"fls_X \$\$ n = (if n = 1 then 1 else 0)"

lemma fls_X_nonzero [simp]: "(fls_X :: 'a :: zero_neq_one fls) ≠ 0"
by (intro fls_nonzeroI) simp

lift_definition fls_X_inv :: "'a::{zero,one} fls"
is "λn. if n = -1 then 1 else 0"

lemma fls_X_inv_nth [simp]:
"fls_X_inv \$\$ n = (if n = -1 then 1 else 0)"

lemma fls_X_inv_nonzero [simp]: "(fls_X_inv :: 'a :: zero_neq_one fls) ≠ 0"
by (intro fls_nonzeroI) simp

subsection ‹Subdegrees›

lemma unique_fls_subdegree:
assumes "f ≠ 0"
shows   "∃!n. f\$\$n ≠ 0 ∧ (∀m. f\$\$m ≠ 0 ⟶ n ≤ m)"
proof-
obtain N::nat where N: "∀n>N. f\$\$(-int n) = 0" by (elim fls_nth_vanishes_below_natE)
define M where "M ≡ -int N"
have M: "⋀m. f\$\$m ≠ 0 ⟹ M ≤ m"
proof-
fix m assume m: "f\$\$m ≠ 0"
show "M ≤ m"
proof (cases "m<0")
case True with m N M_def show ?thesis
using allE[OF N, of "nat (-m)" False] by force
qed
have "¬ (∀k::nat. f\$\$(M + int k) = 0)"
proof
assume above0: "∀k::nat. f\$\$(M + int k) = 0"
have "f=0"
proof (rule fls_zero_eqI)
fix n show "f\$\$n = 0"
proof (cases "M ≤ n")
case True
define k where "k = nat (n - M)"
from True have "n = M + int k" by (simp add: k_def)
with above0 show ?thesis by simp
next
case False with M show ?thesis by auto
qed
qed
with assms show False by fast
qed
hence ex_k: "∃k::nat. f\$\$(M + int k) ≠ 0" by fast
define k where "k ≡ (LEAST k::nat. f\$\$(M + int k) ≠ 0)"
define n where "n ≡ M + int k"
from k_def n_def have fn: "f\$\$n ≠ 0" using LeastI_ex[OF ex_k] by simp
moreover have "∀m. f\$\$m ≠ 0 ⟶ n ≤ m"
proof (clarify)
fix m assume m: "f\$\$m ≠ 0"
with M have "M ≤ m" by fast
define l where "l = nat (m - M)"
from ‹M ≤ m› have l: "m = M + int l" by (simp add: l_def)
with n_def m k_def l show "n ≤ m"
using Least_le[of "λk. f\$\$(M + int k) ≠ 0" l] by auto
qed
moreover have "⋀n'. f\$\$n' ≠ 0 ⟹ (∀m. f\$\$m ≠ 0 ⟶ n' ≤ m) ⟹ n' = n"
proof-
fix n' :: int
assume n': "f\$\$n' ≠ 0" "∀m. f\$\$m ≠ 0 ⟶ n' ≤ m"
from n'(1) M have "M ≤ n'" by fast
define l where "l = nat (n' - M)"
from ‹M ≤ n'› have l: "n' = M + int l" by (simp add: l_def)
with n_def k_def n' fn show "n' = n"
using Least_le[of "λk. f\$\$(M + int k) ≠ 0" l] by force
qed
ultimately show ?thesis
using ex1I[of "λn. f\$\$n ≠ 0 ∧ (∀m. f\$\$m ≠ 0 ⟶ n ≤ m)" n] by blast
qed

definition fls_subdegree :: "('a::zero) fls ⇒ int"
where "fls_subdegree f ≡ (if f = 0 then 0 else LEAST n::int. f\$\$n ≠ 0)"

lemma fls_zero_subdegree [simp]: "fls_subdegree 0 = 0"

lemma nth_fls_subdegree_nonzero [simp]: "f ≠ 0 ⟹ f \$\$ fls_subdegree f ≠ 0"
using Least1I[OF unique_fls_subdegree] by (simp add: fls_subdegree_def)

lemma nth_fls_subdegree_zero_iff: "(f \$\$ fls_subdegree f = 0) ⟷ (f = 0)"
using nth_fls_subdegree_nonzero by auto

lemma fls_subdegree_leI: "f \$\$ n ≠ 0 ⟹ fls_subdegree f ≤ n"
using Least1_le[OF unique_fls_subdegree]
by    (auto simp: fls_subdegree_def)

lemma fls_subdegree_leI': "f \$\$ n ≠ 0 ⟹ n ≤ m ⟹ fls_subdegree f ≤ m"
using fls_subdegree_leI by fastforce

lemma fls_eq0_below_subdegree [simp]: "n < fls_subdegree f ⟹ f \$\$ n = 0"
using fls_subdegree_leI by fastforce

lemma fls_subdegree_geI: "f ≠ 0 ⟹ (⋀k. k < n ⟹ f \$\$ k = 0) ⟹ n ≤ fls_subdegree f"
using nth_fls_subdegree_nonzero by force

lemma fls_subdegree_ge0I: "(⋀k. k < 0 ⟹ f \$\$ k = 0) ⟹ 0 ≤ fls_subdegree f"
using fls_subdegree_geI[of f 0] by (cases "f=0") auto

lemma fls_subdegree_greaterI:
assumes "f ≠ 0" "⋀k. k ≤ n ⟹ f \$\$ k = 0"
shows   "n < fls_subdegree f"
using   assms(1) assms(2)[of "fls_subdegree f"] nth_fls_subdegree_nonzero[of f]
by      force

lemma fls_subdegree_eqI: "f \$\$ n ≠ 0 ⟹ (⋀k. k < n ⟹ f \$\$ k = 0) ⟹ fls_subdegree f = n"
using fls_subdegree_leI fls_subdegree_geI[of f]
by    fastforce

lemma fls_delta_subdegree [simp]:
"b ≠ 0 ⟹ fls_subdegree (Abs_fls (λn. if n=a then b else 0)) = a"
by (intro fls_subdegree_eqI) simp_all

lemma fls_delta0_subdegree: "fls_subdegree (Abs_fls (λn. if n=0 then a else 0)) = 0"
by (cases "a=0") simp_all

lemma fls_one_subdegree [simp]: "fls_subdegree 1 = 0"
by (auto intro: fls_delta0_subdegree simp: one_fls_def)

lemma fls_const_subdegree [simp]: "fls_subdegree (fls_const c) = 0"
by (cases "c=0") (auto intro: fls_subdegree_eqI)

lemma fls_X_subdegree [simp]: "fls_subdegree (fls_X::'a::{zero_neq_one} fls) = 1"
by (intro fls_subdegree_eqI) simp_all

lemma fls_X_inv_subdegree [simp]: "fls_subdegree (fls_X_inv::'a::{zero_neq_one} fls) = -1"
by (intro fls_subdegree_eqI) simp_all

lemma fls_eq_above_subdegreeI:
assumes "N ≤ fls_subdegree f" "N ≤ fls_subdegree g" "∀k≥N. f \$\$ k = g \$\$ k"
shows   "f = g"
proof (rule fls_eqI)
fix n from assms show "f \$\$ n = g \$\$ n" by (cases "n < N") auto
qed

subsection ‹Shifting›

subsubsection ‹Shift definition›

definition fls_shift :: "int ⇒ ('a::zero) fls ⇒ 'a fls"
where "fls_shift n f ≡ Abs_fls (λk. f \$\$ (k+n))"
― ‹Since the index set is unbounded in both directions, we can shift in either direction.›

lemma fls_shift_nth [simp]: "fls_shift m f \$\$ n = f \$\$ (n+m)"
unfolding fls_shift_def
proof (rule nth_Abs_fls_ex_lower_bound)
obtain K::int where K: "∀n<K. f\$\$n = 0" by (elim fls_nth_vanishes_belowE)
hence "∀n<K-m. f\$\$(n+m) = 0" by auto
thus "∃N. ∀n<N. f \$\$ (n + m) = 0" by fast
qed

lemma fls_shift_eq_iff: "(fls_shift m f = fls_shift m g) ⟷ (f = g)"
proof (rule iffI, rule fls_eqI)
fix k
assume 1: "fls_shift m f = fls_shift m g"
have "f \$\$ k = fls_shift m g \$\$ (k - m)" by (simp add: 1[symmetric])
thus "f \$\$ k = g \$\$ k" by simp
qed (intro fls_eqI, simp)

lemma fls_shift_0 [simp]: "fls_shift 0 f = f"
by (intro fls_eqI) simp

lemma fls_shift_subdegree [simp]:
"f ≠ 0 ⟹ fls_subdegree (fls_shift n f) = fls_subdegree f - n"
by (intro fls_subdegree_eqI) simp_all

lemma fls_shift_fls_shift [simp]: "fls_shift m (fls_shift k f) = fls_shift (k+m) f"
by (intro fls_eqI) (simp add: algebra_simps)

lemma fls_shift_fls_shift_reorder:
"fls_shift m (fls_shift k f) = fls_shift k (fls_shift m f)"
using fls_shift_fls_shift[of m k f] fls_shift_fls_shift[of k m f] by (simp add: add.commute)

lemma fls_shift_zero [simp]: "fls_shift m 0 = 0"
by (intro fls_zero_eqI) simp

lemma fls_shift_eq0_iff: "fls_shift m f = 0 ⟷ f = 0"
using fls_shift_eq_iff[of m f 0] by simp

lemma fls_shift_eq_1_iff: "fls_shift n f = 1 ⟷ f = fls_shift (-n) 1"

lemma fls_shift_nonneg_subdegree: "m ≤ fls_subdegree f ⟹ fls_subdegree (fls_shift m f) ≥ 0"
by (cases "f=0") (auto intro: fls_subdegree_geI)

lemma fls_shift_delta:
"fls_shift m (Abs_fls (λn. if n=a then b else 0)) = Abs_fls (λn. if n=a-m then b else 0)"
by (intro fls_eqI) simp

lemma fls_shift_const:
"fls_shift m (fls_const c) = Abs_fls (λn. if n=-m then c else 0)"
by (intro fls_eqI) simp

lemma fls_shift_const_nth:
"fls_shift m (fls_const c) \$\$ n = (if n=-m then c else 0)"

lemma fls_X_conv_shift_1: "fls_X = fls_shift (-1) 1"
by (intro fls_eqI) simp

lemma fls_X_shift_to_one [simp]: "fls_shift 1 fls_X = 1"
using fls_shift_fls_shift[of "-1" 1 1] by (simp add: fls_X_conv_shift_1)

lemma fls_X_inv_conv_shift_1: "fls_X_inv = fls_shift 1 1"
by (intro fls_eqI) simp

lemma fls_X_inv_shift_to_one [simp]: "fls_shift (-1) fls_X_inv = 1"
using fls_shift_fls_shift[of 1 "-1" 1] by (simp add: fls_X_inv_conv_shift_1)

lemma fls_X_fls_X_inv_conv:
"fls_X = fls_shift (-2) fls_X_inv" "fls_X_inv = fls_shift 2 fls_X"

subsubsection ‹Base factor›

text ‹
Similarly to the @{const unit_factor} for formal power series, we can decompose a formal Laurent
series as a power of the implied variable times a series of subdegree 0.
(See lemma @{text "fls_base_factor_X_power_decompose"}.)
But we will call this something other @{const unit_factor}
because it will not satisfy assumption @{text "is_unit_unit_factor"} of
@{class semidom_divide_unit_factor}.
›

definition fls_base_factor :: "('a::zero) fls ⇒ 'a fls"
where fls_base_factor_def[simp]: "fls_base_factor f = fls_shift (fls_subdegree f) f"

lemma fls_base_factor_nth: "fls_base_factor f \$\$ n = f \$\$ (n + fls_subdegree f)"
by simp

lemma fls_base_factor_nonzero [simp]: "f ≠ 0 ⟹ fls_base_factor f ≠ 0"
using fls_nonzeroI[of "fls_base_factor f" 0] by simp

lemma fls_base_factor_subdegree [simp]: "fls_subdegree (fls_base_factor f) = 0"
by (cases "f=0") auto

lemma fls_base_factor_base [simp]:
"fls_base_factor f \$\$ fls_subdegree (fls_base_factor f) = f \$\$ fls_subdegree f"
using fls_base_factor_subdegree[of f] by simp

lemma fls_conv_base_factor_shift_subdegree:
"f = fls_shift (-fls_subdegree f) (fls_base_factor f)"
by simp

lemma fls_base_factor_idem:
"fls_base_factor (fls_base_factor (f::'a::zero fls)) = fls_base_factor f"
using fls_base_factor_subdegree[of f] by simp

lemma fls_base_factor_zero: "fls_base_factor (0::'a::zero fls) = 0"
by simp

lemma fls_base_factor_zero_iff: "fls_base_factor (f::'a::zero fls) = 0 ⟷ f = 0"
proof
have "fls_shift (-fls_subdegree f) (fls_shift (fls_subdegree f) f) = f" by simp
thus "fls_base_factor f = 0 ⟹ f=0" by simp
qed simp

lemma fls_base_factor_nth_0: "f ≠ 0 ⟹ fls_base_factor f \$\$ 0 ≠ 0"
by simp

lemma fls_base_factor_one: "fls_base_factor (1::'a::{zero,one} fls) = 1"
by simp

lemma fls_base_factor_const: "fls_base_factor (fls_const c) = fls_const c"
by simp

lemma fls_base_factor_delta:
"fls_base_factor (Abs_fls (λn. if n=a then c else 0)) = fls_const c"
by  (cases "c=0") (auto intro: fls_eqI)

lemma fls_base_factor_X: "fls_base_factor (fls_X::'a::{zero_neq_one} fls) = 1"
by simp

lemma fls_base_factor_X_inv: "fls_base_factor (fls_X_inv::'a::{zero_neq_one} fls) = 1"
by simp

lemma fls_base_factor_shift [simp]: "fls_base_factor (fls_shift n f) = fls_base_factor f"
by (cases "f=0") simp_all

subsection ‹Conversion between formal power and Laurent series›

subsubsection ‹Converting Laurent to power series›

text ‹
We can truncate a Laurent series at index 0 to create a power series, called the regular part.
›

lift_definition fls_regpart :: "('a::zero) fls ⇒ 'a fps"
is "λf. Abs_fps (λn. f (int n))"
.

lemma fls_regpart_nth [simp]: "fls_regpart f \$ n = f \$\$ (int n)"

lemma fls_regpart_zero [simp]: "fls_regpart 0 = 0"
by (intro fps_ext) simp

lemma fls_regpart_one [simp]: "fls_regpart 1 = 1"
by (intro fps_ext) simp

lemma fls_regpart_Abs_fls:
"∀⇩∞n. F (- int n) = 0 ⟹ fls_regpart (Abs_fls F) = Abs_fps (λn. F (int n))"
by (intro fps_ext) auto

lemma fls_regpart_delta:
"fls_regpart (Abs_fls (λn. if n=a then b else 0)) =
(if a < 0 then 0 else Abs_fps (λn. if n=nat a then b else 0))"
by (rule fps_ext, auto)

lemma fls_regpart_const [simp]: "fls_regpart (fls_const c) = fps_const c"
by (intro fps_ext) simp

lemma fls_regpart_fls_X [simp]: "fls_regpart fls_X = fps_X"
by (intro fps_ext) simp

lemma fls_regpart_fls_X_inv [simp]: "fls_regpart fls_X_inv = 0"
by (intro fps_ext) simp

lemma fls_regpart_eq0_imp_nonpos_subdegree:
assumes "fls_regpart f = 0"
shows   "fls_subdegree f ≤ 0"
proof (cases "f=0")
case False
have "fls_subdegree f ≥ 0 ⟹ f \$\$ fls_subdegree f = 0"
proof-
assume "fls_subdegree f ≥ 0"
hence "f \$\$ (fls_subdegree f) = (fls_regpart f) \$ (nat (fls_subdegree f))" by simp
with assms show "f \$\$ (fls_subdegree f) = 0" by simp
qed
with False show ?thesis by fastforce
qed simp

lemma fls_subdegree_lt_fls_regpart_subdegree:
"fls_subdegree f ≤ int (subdegree (fls_regpart f))"
using fls_subdegree_leI nth_subdegree_nonzero[of "fls_regpart f"]
by    (cases "(fls_regpart f) = 0")

lemma fls_regpart_subdegree_conv:
assumes "fls_subdegree f ≥ 0"
shows   "subdegree (fls_regpart f) = nat (fls_subdegree f)"
―‹
This is the best we can do since if the subdegree is negative, we might still have the bad luck
that the term at index 0 is equal to 0.
›
proof (cases "f=0")
case False with assms show ?thesis by (intro subdegreeI) simp_all
qed simp

lemma fls_eq_conv_fps_eqI:
assumes "0 ≤ fls_subdegree f" "0 ≤ fls_subdegree g" "fls_regpart f = fls_regpart g"
shows   "f = g"
proof (rule fls_eq_above_subdegreeI, rule assms(1), rule assms(2), clarify)
fix k::int assume "0 ≤ k"
with assms(3) show "f \$\$ k = g \$\$ k"
using fls_regpart_nth[of f "nat k"] fls_regpart_nth[of g] by simp
qed

lemma fls_regpart_shift_conv_fps_shift:
"m ≥ 0 ⟹ fls_regpart (fls_shift m f) = fps_shift (nat m) (fls_regpart f)"
by (intro fps_ext) simp_all

lemma fps_shift_fls_regpart_conv_fls_shift:
"fps_shift m (fls_regpart f) = fls_regpart (fls_shift m f)"
by (intro fps_ext) simp_all

lemma fps_unit_factor_fls_regpart:
"fls_subdegree f ≥ 0 ⟹ unit_factor (fls_regpart f) = fls_regpart (fls_base_factor f)"
by (auto intro: fps_ext simp: fls_regpart_subdegree_conv)

text ‹
The terms below the zeroth form a polynomial in the inverse of the implied variable,
called the principle part.
›

lift_definition fls_prpart :: "('a::zero) fls ⇒ 'a poly"
is "λf. Abs_poly (λn. if n = 0 then 0 else f (- int n))"
.

lemma fls_prpart_coeff [simp]: "coeff (fls_prpart f) n = (if n = 0 then 0 else f \$\$ (- int n))"
proof-
have "{x. (if x = 0 then 0 else f \$\$ - int x) ≠ 0} ⊆ {x. f \$\$ - int x ≠ 0}"
by auto
hence "finite {x. (if x = 0 then 0 else f \$\$ - int x) ≠ 0}"
using fls_finite_nonzero_neg_nth[of f] by (simp add: rev_finite_subset)
hence "coeff (fls_prpart f) = (λn. if n = 0 then 0 else f \$\$ (- int n))"
using Abs_poly_inverse[OF CollectI, OF iffD2, OF eventually_cofinite]
thus ?thesis by simp
qed

lemma fls_prpart_eq0_iff: "(fls_prpart f = 0) ⟷ (fls_subdegree f ≥ 0)"
proof
assume 1: "fls_prpart f = 0"
show "fls_subdegree f ≥ 0"
proof (intro fls_subdegree_ge0I)
fix k::int assume "k < 0"
with 1 show "f \$\$ k = 0" using fls_prpart_coeff[of f "nat (-k)"] by simp
qed
qed (intro poly_eqI, simp)

lemma fls_prpart0 [simp]: "fls_prpart 0 = 0"

lemma fls_prpart_one [simp]: "fls_prpart 1 = 0"

lemma fls_prpart_delta:
"fls_prpart (Abs_fls (λn. if n=a then b else 0)) =
(if a<0 then Poly (replicate (nat (-a)) 0 @ [b]) else 0)"
by (intro poly_eqI) (auto simp: nth_default_def nth_append)

lemma fls_prpart_const [simp]: "fls_prpart (fls_const c) = 0"

lemma fls_prpart_X [simp]: "fls_prpart fls_X = 0"
by (intro poly_eqI) simp

lemma fls_prpart_X_inv: "fls_prpart fls_X_inv = [:0,1:]"
proof (intro poly_eqI)
fix n show "coeff (fls_prpart fls_X_inv) n = coeff [:0,1:] n"
proof (cases n)
case (Suc i) thus ?thesis by (cases i) simp_all
qed simp
qed

lemma degree_fls_prpart [simp]:
"degree (fls_prpart f) = nat (-fls_subdegree f)"
proof (cases "f=0")
case False show ?thesis unfolding degree_def
proof (intro Least_equality)
fix N assume N: "∀i>N. coeff (fls_prpart f) i = 0"
have "∀i < -int N. f \$\$ i = 0"
proof clarify
fix i assume i: "i < -int N"
hence "nat (-i) > N" by simp
with N i show "f \$\$ i = 0" using fls_prpart_coeff[of f "nat (-i)"] by auto
qed
with False have "fls_subdegree f ≥ -int N" using fls_subdegree_geI by auto
thus "nat (- fls_subdegree f) ≤ N" by simp
qed auto
qed simp

lemma fls_prpart_shift:
assumes "m ≤ 0"
shows   "fls_prpart (fls_shift m f) = pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))"
proof (intro poly_eqI)
fix n
define LHS RHS
where "LHS ≡ fls_prpart (fls_shift m f)"
and   "RHS ≡ pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))"
show "coeff LHS n = coeff RHS n"
proof (cases n)
case (Suc k)
from assms have 1: "-int (Suc k + nat (-m)) = -int (Suc k) + m" by simp
have "coeff RHS n = f \$\$ (-int (Suc k) + m)"
using arg_cong[OF 1, of "(\$\$) f"] by (simp add: Suc RHS_def coeff_poly_shift)
with Suc show ?thesis by (simp add: LHS_def)
qed

lemma fls_prpart_base_factor: "fls_prpart (fls_base_factor f) = 0"
using fls_base_factor_subdegree[of f] by (simp add: fls_prpart_eq0_iff)

text ‹The essential data of a formal Laurant series resides from the subdegree up.›

abbreviation fls_base_factor_to_fps :: "('a::zero) fls ⇒ 'a fps"
where "fls_base_factor_to_fps f ≡ fls_regpart (fls_base_factor f)"

lemma fls_base_factor_to_fps_conv_fps_shift:
assumes "fls_subdegree f ≥ 0"
shows   "fls_base_factor_to_fps f = fps_shift (nat (fls_subdegree f)) (fls_regpart f)"

lemma fls_base_factor_to_fps_nth:
"fls_base_factor_to_fps f \$ n = f \$\$ (fls_subdegree f + int n)"

lemma fls_base_factor_to_fps_base: "f ≠ 0 ⟹ fls_base_factor_to_fps f \$ 0 ≠ 0"
by simp

lemma fls_base_factor_to_fps_nonzero: "f ≠ 0 ⟹ fls_base_factor_to_fps f ≠ 0"
using fps_nonzeroI[of "fls_base_factor_to_fps f" 0] fls_base_factor_to_fps_base by simp

lemma fls_base_factor_to_fps_subdegree [simp]: "subdegree (fls_base_factor_to_fps f) = 0"
by (cases "f=0") auto

lemma fls_base_factor_to_fps_trivial:
"fls_subdegree f = 0 ⟹ fls_base_factor_to_fps f = fls_regpart f"
by simp

lemma fls_base_factor_to_fps_zero: "fls_base_factor_to_fps 0 = 0"
by simp

lemma fls_base_factor_to_fps_one: "fls_base_factor_to_fps 1 = 1"
by simp

lemma fls_base_factor_to_fps_delta:
"fls_base_factor_to_fps (Abs_fls (λn. if n=a then c else 0)) = fps_const c"
using fls_base_factor_delta[of a c] by simp

lemma fls_base_factor_to_fps_const:
"fls_base_factor_to_fps (fls_const c) = fps_const c"
by simp

lemma fls_base_factor_to_fps_X:
"fls_base_factor_to_fps (fls_X::'a::{zero_neq_one} fls) = 1"
by simp

lemma fls_base_factor_to_fps_X_inv:
"fls_base_factor_to_fps (fls_X_inv::'a::{zero_neq_one} fls) = 1"
by simp

lemma fls_base_factor_to_fps_shift:
"fls_base_factor_to_fps (fls_shift m f) = fls_base_factor_to_fps f"
using fls_base_factor_shift[of m f] by simp

lemma fls_base_factor_to_fps_base_factor:
"fls_base_factor_to_fps (fls_base_factor f) = fls_base_factor_to_fps f"
using fls_base_factor_to_fps_shift by simp

lemma fps_unit_factor_fls_base_factor:
"unit_factor (fls_base_factor_to_fps f) = fls_base_factor_to_fps f"
using fls_base_factor_to_fps_subdegree[of f] by simp

subsubsection ‹Converting power to Laurent series›

text ‹We can extend a power series by 0s below to create a Laurent series.›

definition fps_to_fls :: "('a::zero) fps ⇒ 'a fls"
where "fps_to_fls f ≡ Abs_fls (λk::int. if k<0 then 0 else f \$ (nat k))"

lemma fps_to_fls_nth [simp]:
"(fps_to_fls f) \$\$ n = (if n < 0 then 0 else f\$(nat n))"
using     nth_Abs_fls_lower_bound[of 0 "(λk::int. if k<0 then 0 else f \$ (nat k))"]
unfolding fps_to_fls_def
by        simp

lemma fps_to_fls_eq_imp_fps_eq:
assumes "fps_to_fls f = fps_to_fls g"
shows   "f = g"
proof (intro fps_ext)
fix n
have "f \$ n = fps_to_fls g \$\$ int n" by (simp add: assms[symmetric])
thus "f \$ n = g \$ n" by simp
qed

lemma fps_to_fls_eq_iff [simp]: "fps_to_fls f = fps_to_fls g ⟷ f = g"
using fps_to_fls_eq_imp_fps_eq by blast

lemma fps_zero_to_fls [simp]: "fps_to_fls 0 = 0"
by (intro fls_zero_eqI) simp

lemma fps_to_fls_nonzeroI: "f ≠ 0 ⟹ fps_to_fls f ≠ 0"
using fps_to_fls_eq_imp_fps_eq[of f 0] by auto

lemma fps_one_to_fls [simp]: "fps_to_fls 1 = 1"
by (intro fls_eqI) simp

lemma fps_to_fls_Abs_fps:
"fps_to_fls (Abs_fps F) = Abs_fls (λn. if n<0 then 0 else F (nat n))"
using nth_Abs_fls_lower_bound[of 0 "(λn::int. if n<0 then 0 else F (nat n))"]
by    (intro fls_eqI) simp

lemma fps_delta_to_fls:
"fps_to_fls (Abs_fps (λn. if n=a then b else 0)) = Abs_fls (λn. if n=int a then b else 0)"
using fls_eqI[of _ "Abs_fls (λn. if n=int a then b else 0)"] by force

lemma fps_const_to_fls [simp]: "fps_to_fls (fps_const c) = fls_const c"
by (intro fls_eqI) simp

lemma fps_X_to_fls [simp]: "fps_to_fls fps_X = fls_X"
by (fastforce intro: fls_eqI)

lemma fps_to_fls_eq_0_iff [simp]: "(fps_to_fls f = 0) ⟷ (f=0)"
using fps_to_fls_nonzeroI by auto

lemma fps_to_fls_eq_1_iff [simp]: "fps_to_fls f = 1 ⟷ f = 1"
using fps_to_fls_eq_iff by fastforce

lemma fls_subdegree_fls_to_fps_gt0: "fls_subdegree (fps_to_fls f) ≥ 0"
proof (cases "f=0")
case False show ?thesis
proof (rule fls_subdegree_geI, rule fls_nonzeroI)
from False show "fps_to_fls f \$\$ int (subdegree f) ≠ 0"
by simp
qed simp
qed simp

lemma fls_subdegree_fls_to_fps: "fls_subdegree (fps_to_fls f) = int (subdegree f)"
proof (cases "f=0")
case False
have "subdegree f = nat (fls_subdegree (fps_to_fls f))"
proof (rule subdegreeI)
from False show "f \$ (nat (fls_subdegree (fps_to_fls f))) ≠ 0"
using fls_subdegree_fls_to_fps_gt0[of f] nth_fls_subdegree_nonzero[of "fps_to_fls f"]
fps_to_fls_nonzeroI[of f]
by    simp
next
fix k assume k: "k < nat (fls_subdegree (fps_to_fls f))"
thus "f \$ k = 0"
using fls_eq0_below_subdegree[of "int k" "fps_to_fls f"] by simp
qed
thus ?thesis by (simp add: fls_subdegree_fls_to_fps_gt0)
qed simp

lemma fps_shift_to_fls [simp]:
"n ≤ subdegree f ⟹ fps_to_fls (fps_shift n f) = fls_shift (int n) (fps_to_fls f)"
by (auto intro: fls_eqI simp: nat_add_distrib nth_less_subdegree_zero)

lemma fls_base_factor_fps_to_fls: "fls_base_factor (fps_to_fls f) = fps_to_fls (unit_factor f)"
using nth_less_subdegree_zero[of _ f]
by    (auto intro: fls_eqI simp: fls_subdegree_fls_to_fps nat_add_distrib)

lemma fls_regpart_to_fls_trivial [simp]:
"fls_subdegree f ≥ 0 ⟹ fps_to_fls (fls_regpart f) = f"
by (intro fls_eqI) simp

lemma fls_regpart_fps_trivial [simp]: "fls_regpart (fps_to_fls f) = f"
by (intro fps_ext) simp

lemma fps_to_fls_base_factor_to_fps:
"fps_to_fls (fls_base_factor_to_fps f) = fls_base_factor f"
by (intro fls_eqI) simp

lemma fls_conv_base_factor_to_fps_shift_subdegree:
"f = fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f))"
using fps_to_fls_base_factor_to_fps[of f] fps_to_fls_base_factor_to_fps[of f] by simp

lemma fls_base_factor_to_fps_to_fls:
"fls_base_factor_to_fps (fps_to_fls f) = unit_factor f"
using fls_base_factor_fps_to_fls[of f] fls_regpart_fps_trivial[of "unit_factor f"]
by    simp

lemma fls_as_fps:
fixes f :: "'a :: zero fls" and n :: int
assumes n: "n ≥ -fls_subdegree f"
obtains f' where "f = fls_shift n (fps_to_fls f')"
proof -
have "fls_subdegree (fls_shift (- n) f) ≥ 0"
by (rule fls_shift_nonneg_subdegree) (use n in simp)
hence "f = fls_shift n (fps_to_fls (fls_regpart (fls_shift (-n) f)))"
by (subst fls_regpart_to_fls_trivial) simp_all
thus ?thesis
by (rule that)
qed

lemma fls_as_fps':
fixes f :: "'a :: zero fls" and n :: int
assumes n: "n ≥ -fls_subdegree f"
shows "∃f'. f = fls_shift n (fps_to_fls f')"
using fls_as_fps[OF assms] by metis

abbreviation
"fls_regpart_as_fls f ≡ fps_to_fls (fls_regpart f)"
abbreviation
"fls_prpart_as_fls f ≡
fls_shift (-fls_subdegree f) (fps_to_fls (fps_of_poly (reflect_poly (fls_prpart f))))"

lemma fls_regpart_as_fls_nth:
"fls_regpart_as_fls f \$\$ n = (if n < 0 then 0 else f \$\$ n)"
by simp

lemma fls_regpart_idem:
"fls_regpart (fls_regpart_as_fls f) = fls_regpart f"
by simp

lemma fls_prpart_as_fls_nth:
"fls_prpart_as_fls f \$\$ n = (if n < 0 then f \$\$ n else 0)"
proof (cases "n < fls_subdegree f" "n < 0" rule: case_split[case_product case_split])
case False_True
hence "nat (-fls_subdegree f) - nat (n - fls_subdegree f) = nat (-n)" by auto
with False_True show ?thesis
using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto
next
case False_False thus ?thesis
using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto
qed simp_all

lemma fls_prpart_idem [simp]: "fls_prpart (fls_prpart_as_fls f) = fls_prpart f"
using fls_prpart_as_fls_nth[of f] by (intro poly_eqI) simp

lemma fls_regpart_prpart: "fls_regpart (fls_prpart_as_fls f) = 0"
using fls_prpart_as_fls_nth[of f] by (intro fps_ext) simp

lemma fls_prpart_regpart: "fls_prpart (fls_regpart_as_fls f) = 0"
by (intro poly_eqI) simp

subsection ‹Algebraic structures›

begin
lift_definition plus_fls :: "'a fls ⇒ 'a fls ⇒ 'a fls" is "λf g n. f n + g n"
proof-
fix f f' :: "int ⇒ 'a"
assume "∀⇩∞n. f (- int n) = 0" "∀⇩∞n. f' (- int n) = 0"
from this obtain N N' where "∀n>N. f (-int n) = 0" "∀n>N'. f' (-int n) = 0"
by (auto simp: MOST_nat)
hence "∀n > max N N'. f (-int n) + f' (-int n) = 0" by auto
hence "∃K. ∀n>K. f (-int n) + f' (-int n) = 0" by fast
thus "∀⇩∞n. f (- int n) + f' (-int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end

lemma fls_plus_nth [simp]: "(f + g) \$\$ n = f \$\$ n + g \$\$ n"
by transfer simp

lemma fls_plus_const: "fls_const x + fls_const y = fls_const (x+y)"
by (intro fls_eqI) simp

lemma fls_plus_subdegree:
"f + g ≠ 0 ⟹ fls_subdegree (f + g) ≥ min (fls_subdegree f) (fls_subdegree g)"
by (auto intro: fls_subdegree_geI)

lemma fls_shift_plus [simp]:
"fls_shift m (f + g) = (fls_shift m f) + (fls_shift m g)"
by (intro fls_eqI) simp

lemma fls_regpart_plus [simp]: "fls_regpart (f + g) = fls_regpart f + fls_regpart g"
by (intro fps_ext) simp

lemma fls_prpart_plus [simp] : "fls_prpart (f + g) = fls_prpart f + fls_prpart g"
by (intro poly_eqI) simp

lemma fls_decompose_reg_pr_parts:
fixes   f :: "'a :: monoid_add fls"
defines "R  ≡ fls_regpart_as_fls f"
and     "P  ≡ fls_prpart_as_fls f"
shows   "f = P + R"
and     "f = R + P"
using   fls_prpart_as_fls_nth[of f]
by      (auto intro: fls_eqI simp add: assms)

lemma fps_to_fls_plus [simp]: "fps_to_fls (f + g) = fps_to_fls f + fps_to_fls g"
by (intro fls_eqI) simp

proof
fix a b c :: "'a fls"
show "a + b + c = a + (b + c)" by transfer (simp add: add.assoc)
show "0 + a = a" by transfer simp
show "a + 0 = a" by transfer simp
qed

by (standard, transfer, auto simp: add.commute)

subsubsection ‹Subtraction and negatives›

begin
lift_definition minus_fls :: "'a fls ⇒ 'a fls ⇒ 'a fls" is "λf g n. f n - g n"
proof-
fix f f' :: "int ⇒ 'a"
assume "∀⇩∞n. f (- int n) = 0" "∀⇩∞n. f' (- int n) = 0"
from this obtain N N' where "∀n>N. f (-int n) = 0" "∀n>N'. f' (-int n) = 0"
by (auto simp: MOST_nat)
hence "∀n > max N N'. f (-int n) - f' (-int n) = 0" by auto
hence "∃K. ∀n>K. f (-int n) - f' (-int n) = 0" by fast
thus "∀⇩∞n. f (- int n) - f' (-int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end

lemma fls_minus_nth [simp]: "(f - g) \$\$ n = f \$\$ n - g \$\$ n"
by transfer simp

lemma fls_minus_const: "fls_const x - fls_const y = fls_const (x-y)"
by (intro fls_eqI) simp

lemma fls_subdegree_minus:
"f - g ≠ 0 ⟹ fls_subdegree (f - g) ≥ min (fls_subdegree f) (fls_subdegree g)"
by (intro fls_subdegree_geI) simp_all

lemma fls_shift_minus [simp]: "fls_shift m (f - g) = (fls_shift m f) - (fls_shift m g)"
by (auto intro: fls_eqI)

lemma fls_regpart_minus [simp]: "fls_regpart (f - g) = fls_regpart f - fls_regpart g"
by (intro fps_ext) simp

lemma fls_prpart_minus [simp] : "fls_prpart (f - g) = fls_prpart f - fls_prpart g"
by (intro poly_eqI) simp

lemma fps_to_fls_minus [simp]: "fps_to_fls (f - g) = fps_to_fls f - fps_to_fls g"
by (intro fls_eqI) simp

begin
lift_definition uminus_fls :: "'a fls ⇒ 'a fls" is "λf n. - f n"
proof-
fix f :: "int ⇒ 'a" assume "∀⇩∞n. f (- int n) = 0"
from this obtain N where "∀n>N. f (-int n) = 0"
by (auto simp: MOST_nat)
hence "∀n>N. - f (-int n) = 0" by auto
hence "∃K. ∀n>K. - f (-int n) = 0" by fast
thus "∀⇩∞n. - f (- int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end

lemma fls_uminus_nth [simp]: "(-f) \$\$ n = - (f \$\$ n)"
by transfer simp

lemma fls_const_uminus[simp]: "fls_const (-x) = -fls_const x"
by (intro fls_eqI) simp

lemma fls_shift_uminus [simp]: "fls_shift m (- f) = - (fls_shift m f)"
by (auto intro: fls_eqI)

lemma fls_regpart_uminus [simp]: "fls_regpart (- f) = - fls_regpart f"
by (intro fps_ext) simp

lemma fls_prpart_uminus [simp] : "fls_prpart (- f) = - fls_prpart f"
by (intro poly_eqI) simp

lemma fps_to_fls_uminus [simp]: "fps_to_fls (- f) = - fps_to_fls f"
by (intro fls_eqI) simp

proof
fix a b :: "'a fls"
show "- a + a = 0" by transfer simp
show "a + - b = a - b" by transfer simp
qed

proof
fix a b :: "'a fls"
show "- a + a = 0" by transfer simp
show "a - b = a + - b" by transfer simp
qed

lemma fls_uminus_subdegree [simp]: "fls_subdegree (-f) = fls_subdegree f"
by (cases "f=0") (auto intro: fls_subdegree_eqI)

lemma fls_subdegree_minus_sym: "fls_subdegree (g - f) = fls_subdegree (f - g)"
using fls_uminus_subdegree[of "g-f"] by (simp add: algebra_simps)

lemma fls_regpart_sub_prpart: "fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f"
using fls_decompose_reg_pr_parts(2)[of f]
by    simp

lemma fls_prpart_sub_regpart: "fls_prpart (f - fls_regpart_as_fls f) = fls_prpart f"
using fls_decompose_reg_pr_parts(1)[of f]
by    simp

subsubsection ‹Multiplication›

instantiation fls :: ("{comm_monoid_add, times}") times
begin
definition fls_times_def:
"(*) = (λf g.
fls_shift
(- (fls_subdegree f + fls_subdegree g))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))
)"
instance ..
end

lemma fls_times_nth_eq0: "n < fls_subdegree f + fls_subdegree g ⟹ (f * g) \$\$ n = 0"

lemma fls_times_nth:
fixes   f df g dg
defines "df ≡ fls_subdegree f" and "dg ≡ fls_subdegree g"
shows   "(f * g) \$\$ n = (∑i=df + dg..n. f \$\$ (i - dg) * g \$\$ (dg + n - i))"
and     "(f * g) \$\$ n = (∑i=df..n - dg. f \$\$ i * g \$\$ (n - i))"
and     "(f * g) \$\$ n = (∑i=dg..n - df. f \$\$ (df + i - dg) * g \$\$ (dg + n - df - i))"
and     "(f * g) \$\$ n = (∑i=0..n - (df + dg). f \$\$ (df + i) * g \$\$ (n - df - i))"
proof-

define dfg where "dfg ≡ df + dg"

show 4: "(f * g) \$\$ n = (∑i=0..n - dfg. f \$\$ (df + i) * g \$\$ (n - df - i))"
proof (cases "n < dfg")
case False
from False assms have
"(f * g) \$\$ n =
(∑i = 0..nat (n - dfg). f \$\$ (df + int i) * g \$\$ (dg + int (nat (n - dfg) - i)))"
using fps_mult_nth[of "fls_base_factor_to_fps f" "fls_base_factor_to_fps g"]
fls_base_factor_to_fps_nth[of f]
fls_base_factor_to_fps_nth[of g]
by    (simp add: dfg_def fls_times_def algebra_simps)
moreover from False have index:
"⋀i. i ∈ {0..nat (n - dfg)} ⟹ dg + int (nat (n - dfg) - i) = n - df - int i"
by (auto simp: dfg_def)
ultimately have
"(f * g) \$\$ n = (∑i=0..nat (n - dfg). f \$\$ (df + int i) * g \$\$ (n - df - int i))"
by simp
moreover have
"(∑i=0..nat (n - dfg). f \$\$ (df + int i) *  g \$\$ (n - df - int i)) =
(∑i=0..n - dfg. f \$\$ (df + i) *  g \$\$ (n - df - i))"
proof (intro sum.reindex_cong)
show "inj_on nat {0..n - dfg}" by standard auto
show "{0..nat (n - dfg)} = nat ` {0..n - dfg}"
proof
show "{0..nat (n - dfg)} ⊆ nat ` {0..n - dfg}"
proof
fix i assume "i ∈ {0..nat (n - dfg)}"
hence i: "i ≥ 0" "i ≤ nat (n - dfg)" by auto
with False have "int i ≥ 0" "int i ≤ n - dfg" by auto
hence "int i ∈ {0..n - dfg}" by simp
moreover from i(1) have "i = nat (int i)" by simp
ultimately show "i ∈ nat ` {0..n - dfg}" by fast
qed
qed (auto simp: False)
ultimately show "(f * g) \$\$ n = (∑i=0..n - dfg. f \$\$ (df + i) *  g \$\$ (n - df - i))"
by simp
qed (simp add: fls_times_nth_eq0 assms dfg_def)

have
"(∑i=dfg..n. f \$\$ (i - dg) *  g \$\$ (dg + n - i)) =
(∑i=0..n - dfg. f \$\$ (df + i) *  g \$\$ (n - df - i))"
proof (intro sum.reindex_cong)
define T where "T ≡ λi. i + dfg"
show "inj_on T {0..n - dfg}" by standard (simp add: T_def)
with 4 show 1: "(f * g) \$\$ n = (∑i=dfg..n. f \$\$ (i - dg) *  g \$\$ (dg + n - i))"
by simp

have
"(∑i=dfg..n. f \$\$ (i - dg) *  g \$\$ (dg + n - i)) = (∑i=df..n - dg. f \$\$ i *  g \$\$ (n - i))"
proof (intro sum.reindex_cong)
define T where "T ≡ λi. i + dg"
show "inj_on T {df..n - dg}" by standard (simp add: T_def)
qed (auto simp: dfg_def)
with 1 show "(f * g) \$\$ n = (∑i=df..n - dg. f \$\$ i *  g \$\$ (n - i))"
by simp

have
"(∑i=dfg..n. f \$\$ (i - dg) *  g \$\$ (dg + n - i)) =
(∑i=dg..n - df. f \$\$ (df + i - dg) *  g \$\$ (dg + n - df - i))"
proof (intro sum.reindex_cong)
define T where "T ≡ λi. i + df"
show "inj_on T {dg..n - df}" by standard (simp add: T_def)
with 1 show "(f * g) \$\$ n = (∑i=dg..n - df. f \$\$ (df + i - dg) *  g \$\$ (dg + n - df - i))"
by simp

qed

lemma fls_times_base [simp]:
"(f * g) \$\$ (fls_subdegree f + fls_subdegree g) =
(f \$\$ fls_subdegree f) * (g \$\$ fls_subdegree g)"

instance fls :: ("{comm_monoid_add, mult_zero}") mult_zero
proof
fix a :: "'a fls"
have
"(0::'a fls) * a =
fls_shift (fls_subdegree a) (fps_to_fls ( (0::'a fps)*(fls_base_factor_to_fps a) ))"
moreover have
"a * (0::'a fls) =
fls_shift (fls_subdegree a) (fps_to_fls ( (fls_base_factor_to_fps a)*(0::'a fps) ))"
ultimately show "0 * a = (0::'a fls)" "a * 0 = (0::'a fls)"
by auto
qed

lemma fls_mult_one:
fixes f :: "'a::{comm_monoid_add, mult_zero, monoid_mult} fls"
shows "1 * f = f"
and   "f * 1 = f"
using fls_conv_base_factor_to_fps_shift_subdegree[of f]

lemma fls_mult_const_nth [simp]:
fixes f :: "'a::{comm_monoid_add, mult_zero} fls"
shows "(fls_const x * f) \$\$ n = x * f\$\$n"
and   "(f * fls_const x ) \$\$ n = f\$\$n * x"
proof-
show "(fls_const x * f) \$\$ n = x * f\$\$n"
proof (cases "n<fls_subdegree f")
case False
hence "{fls_subdegree f..n} = insert (fls_subdegree f) {fls_subdegree f+1..n}" by auto
thus ?thesis by (simp add: fls_times_nth(1))
show "(f * fls_const x ) \$\$ n = f\$\$n * x"
proof (cases "n<fls_subdegree f")
case False
hence "{fls_subdegree f..n} = insert n {fls_subdegree f..n-1}" by auto
thus ?thesis by (simp add: fls_times_nth(1))
qed

lemma fls_const_mult_const[simp]:
fixes x y :: "'a::{comm_monoid_add, mult_zero}"
shows "fls_const x * fls_const y = fls_const (x*y)"
by    (intro fls_eqI) simp

lemma fls_mult_subdegree_ge:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f*g ≠ 0"
shows   "fls_subdegree (f*g) ≥ fls_subdegree f + fls_subdegree g"
by      (auto intro: fls_subdegree_geI simp: assms fls_times_nth_eq0)

lemma fls_mult_subdegree_ge_0:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f ≥ 0" "fls_subdegree g ≥ 0"
shows   "fls_subdegree (f*g) ≥ 0"
using   assms fls_mult_subdegree_ge[of f g]
by      fastforce

lemma fls_mult_nonzero_base_subdegree_eq:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f \$\$ (fls_subdegree f) * g \$\$ (fls_subdegree g) ≠ 0"
shows   "fls_subdegree (f*g) = fls_subdegree f + fls_subdegree g"
proof-
from assms have "fls_subdegree (f*g) ≥ fls_subdegree f + fls_subdegree g"
using fls_nonzeroI[of "f*g" "fls_subdegree f + fls_subdegree g"]
fls_mult_subdegree_ge[of f g]
by    simp
moreover from assms have "fls_subdegree (f*g) ≤ fls_subdegree f + fls_subdegree g"
by (intro fls_subdegree_leI) simp
ultimately show ?thesis by simp
qed

lemma fls_subdegree_mult [simp]:
fixes   f g :: "'a::semiring_no_zero_divisors fls"
assumes "f ≠ 0" "g ≠ 0"
shows   "fls_subdegree (f * g) = fls_subdegree f + fls_subdegree g"
using   assms
by      (auto intro: fls_subdegree_eqI simp: fls_times_nth_eq0)

lemma fls_shifted_times_simps:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "f * (fls_shift n g) = fls_shift n (f*g)" "(fls_shift n f) * g = fls_shift n (f*g)"
proof-

show "f * (fls_shift n g) = fls_shift n (f*g)"
proof (cases "g=0")
case False
hence
"f * (fls_shift n g) =
fls_shift (- (fls_subdegree f + (fls_subdegree g - n)))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))"
unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift)
thus "f * (fls_shift n g) = fls_shift n (f*g)"
qed auto

show "(fls_shift n f)*g = fls_shift n (f*g)"
proof (cases "f=0")
case False
hence
"(fls_shift n f)*g =
fls_shift (- ((fls_subdegree f - n) + fls_subdegree g))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))"
unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift)
thus "(fls_shift n f) * g = fls_shift n (f*g)"
qed auto

qed

lemma fls_shifted_times_transfer:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "fls_shift n f * g = f * fls_shift n g"
using fls_shifted_times_simps(1)[of f n g] fls_shifted_times_simps(2)[of n f g]
by    simp

lemma fls_times_both_shifted_simp:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "(fls_shift m f) * (fls_shift n g) = fls_shift (m+n) (f*g)"

lemma fls_base_factor_mult_base_factor:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "fls_base_factor (f * fls_base_factor g) = fls_base_factor (f * g)"
and   "fls_base_factor (fls_base_factor f * g) = fls_base_factor (f * g)"
using fls_base_factor_shift[of "fls_subdegree g" "f*g"]
fls_base_factor_shift[of "fls_subdegree f" "f*g"]

lemma fls_base_factor_mult_both_base_factor:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
shows "fls_base_factor (fls_base_factor f * fls_base_factor g) = fls_base_factor (f * g)"
using fls_base_factor_mult_base_factor(1)[of "fls_base_factor f" g]
fls_base_factor_mult_base_factor(2)[of f g]
by    simp

lemma fls_base_factor_mult:
fixes f g :: "'a::semiring_no_zero_divisors fls"
shows "fls_base_factor (f * g) = fls_base_factor f * fls_base_factor g"
by    (cases "f≠0 ∧ g≠0")
(auto simp: fls_times_both_shifted_simp)

lemma fls_times_conv_base_factor_times:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows
"f * g =
fls_shift (-(fls_subdegree f + fls_subdegree g)) (fls_base_factor f * fls_base_factor g)"

lemma fls_times_base_factor_conv_shifted_times:
― ‹Convenience form of lemma @{text "fls_times_both_shifted_simp"}.›
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows
"fls_base_factor f * fls_base_factor g = fls_shift (fls_subdegree f + fls_subdegree g) (f * g)"

lemma fls_times_conv_regpart:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f ≥ 0" "fls_subdegree g ≥ 0"
shows "fls_regpart (f * g) = fls_regpart f * fls_regpart g"
proof-
from assms have 1:
"f * g =
fls_shift (- (fls_subdegree f + fls_subdegree g)) (
fps_to_fls (
fps_shift (nat (fls_subdegree f) + nat (fls_subdegree g)) (
fls_regpart f * fls_regpart g
)
)
)"
fls_times_def fls_base_factor_to_fps_conv_fps_shift[symmetric]
fls_regpart_subdegree_conv fps_shift_mult_both[symmetric]
)
show ?thesis
proof (cases "fls_regpart f * fls_regpart g = 0")
case False
with assms have
"subdegree (fls_regpart f * fls_regpart g) ≥
nat (fls_subdegree f) + nat (fls_subdegree g)"
with 1 assms show ?thesis by simp
qed

lemma fls_base_factor_to_fps_mult_conv_unit_factor:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
shows
"fls_base_factor_to_fps (f * g) =
unit_factor (fls_base_factor_to_fps f * fls_base_factor_to_fps g)"
using fls_base_factor_mult_both_base_factor[of f g]
fps_unit_factor_fls_regpart[of "fls_base_factor f * fls_base_factor g"]
fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g]
fls_mult_subdegree_ge_0[of "fls_base_factor f" "fls_base_factor g"]
fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"]
by    simp

lemma fls_base_factor_to_fps_mult':
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "(f \$\$ fls_subdegree f) * (g \$\$ fls_subdegree g) ≠ 0"
shows   "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g"
using   assms fls_mult_nonzero_base_subdegree_eq[of f g]
fls_times_base_factor_conv_shifted_times[of f g]
fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"]
fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g]
by      fastforce

lemma fls_base_factor_to_fps_mult:
fixes f g :: "'a::semiring_no_zero_divisors fls"
shows "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g"
using fls_base_factor_to_fps_mult'[of f g]
by    (cases "f=0 ∨ g=0") auto

lemma fls_times_conv_fps_times:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f ≥ 0" "fls_subdegree g ≥ 0"
shows   "f * g = fps_to_fls (fls_regpart f * fls_regpart g)"
using   assms fls_mult_subdegree_ge[of f g]
by      (cases "f * g = 0") (simp_all add: fls_times_conv_regpart[symmetric])

lemma fps_times_conv_fls_times:
fixes   f g :: "'a::{comm_monoid_add,mult_zero} fps"
shows   "f * g = fls_regpart (fps_to_fls f * fps_to_fls g)"
using   fls_subdegree_fls_to_fps_gt0 fls_times_conv_regpart[symmetric]
by      fastforce

lemma fls_times_fps_to_fls:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
shows "fps_to_fls (f * g) = fps_to_fls f * fps_to_fls g"
proof (intro fls_eq_conv_fps_eqI, rule fls_subdegree_fls_to_fps_gt0)
show "fls_subdegree (fps_to_fls f * fps_to_fls g) ≥ 0"
proof (cases "fps_to_fls f * fps_to_fls g = 0")
case False thus ?thesis
using fls_mult_subdegree_ge fls_subdegree_fls_to_fps_gt0[of f]
fls_subdegree_fls_to_fps_gt0[of g]
by    fastforce
qed simp

lemma fls_X_times_conv_shift:
shows "fls_X * f = fls_shift (-1) f" "f * fls_X = fls_shift (-1) f"
by    (simp_all add: fls_X_conv_shift_1 fls_mult_one fls_shifted_times_simps)

lemmas fls_X_times_comm = trans_sym[OF fls_X_times_conv_shift]

lemma fls_subdegree_mult_fls_X:
assumes "f ≠ 0"
shows   "fls_subdegree (fls_X * f) = fls_subdegree f + 1"
and     "fls_subdegree (f * fls_X) = fls_subdegree f + 1"
by      (auto simp: fls_X_times_conv_shift assms)

lemma fls_mult_fls_X_nonzero:
assumes "f ≠ 0"
shows   "fls_X * f ≠ 0"
and     "f * fls_X ≠ 0"
by      (auto simp: fls_X_times_conv_shift fls_shift_eq0_iff assms)

lemma fls_base_factor_mult_fls_X:
shows "fls_base_factor (fls_X * f) = fls_base_factor f"
and   "fls_base_factor (f * fls_X) = fls_base_factor f"
using fls_base_factor_shift[of "-1" f]
by    (auto simp: fls_X_times_conv_shift)

lemma fls_X_inv_times_conv_shift:
shows "fls_X_inv * f = fls_shift 1 f" "f * fls_X_inv = fls_shift 1 f"
by    (simp_all add: fls_X_inv_conv_shift_1 fls_mult_one fls_shifted_times_simps)

lemmas fls_X_inv_times_comm = trans_sym[OF fls_X_inv_times_conv_shift]

lemma fls_subdegree_mult_fls_X_inv:
assumes "f ≠ 0"
shows   "fls_subdegree (fls_X_inv * f) = fls_subdegree f - 1"
and     "fls_subdegree (f * fls_X_inv) = fls_subdegree f - 1"
by      (auto simp: fls_X_inv_times_conv_shift assms)

lemma fls_mult_fls_X_inv_nonzero:
assumes "f ≠ 0"
shows   "fls_X_inv * f ≠ 0"
and     "f * fls_X_inv ≠ 0"
by      (auto simp: fls_X_inv_times_conv_shift fls_shift_eq0_iff assms)

lemma fls_base_factor_mult_fls_X_inv:
shows "fls_base_factor (fls_X_inv * f) = fls_base_factor f"
and   "fls_base_factor (f * fls_X_inv) = fls_base_factor f"
using fls_base_factor_shift[of 1 f]
by    (auto simp: fls_X_inv_times_conv_shift)

lemma fls_mult_assoc_subdegree_ge_0:
fixes   f g h :: "'a::semiring_0 fls"
assumes "fls_subdegree f ≥ 0" "fls_subdegree g ≥ 0" "fls_subdegree h ≥ 0"
shows   "f * g * h = f * (g * h)"
using   assms
by      (simp add: fls_times_conv_fps_times fls_subdegree_fls_to_fps_gt0 mult.assoc)

lemma fls_mult_assoc_base_factor:
fixes a b c :: "'a::semiring_0 fls"
shows
"fls_base_factor a * fls_base_factor b * fls_base_factor c =
fls_base_factor a * (fls_base_factor b * fls_base_factor c)"
by    (simp add: fls_mult_assoc_subdegree_ge_0 del: fls_base_factor_def)

lemma fls_mult_distrib_subdegree_ge_0:
fixes   f g h :: "'a::semiring_0 fls"
assumes "fls_subdegree f ≥ 0" "fls_subdegree g ≥ 0" "fls_subdegree h ≥ 0"
shows   "(f + g) * h = f * h + g * h"
and     "h * (f + g) = h * f + h * g"
proof-
have "fls_subdegree (f+g) ≥ 0"
proof (cases "f+g = 0")
case False
with assms(1,2) show ?thesis
using fls_plus_subdegree by fastforce
qed simp
with assms show "(f + g) * h = f * h + g * h" "h * (f + g) = h * f + h * g"
using distrib_right[of "fls_regpart f"] distrib_left[of "fls_regpart h"]
qed

lemma fls_mult_distrib_base_factor:
fixes a b c :: "'a::semiring_0 fls"
shows
"fls_base_factor a * (fls_base_factor b + fls_base_factor c) =
fls_base_factor a * fls_base_factor b + fls_base_factor a * fls_base_factor c"
by    (simp add: fls_mult_distrib_subdegree_ge_0 del: fls_base_factor_def)

instance fls :: (semiring_0) semiring_0
proof

fix a b c :: "'a fls"
have
"a * b * c =
fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c))
(fls_base_factor a * fls_base_factor b * fls_base_factor c)"
moreover have
"a * (b * c) =
fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c))
(fls_base_factor a * fls_base_factor b * fls_base_factor c)"
using fls_mult_assoc_base_factor[of a b c] by (simp add: fls_times_both_shifted_simp)
ultimately show "a * b * c = a * (b * c)" by simp

have ab:
"fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) a) ≥ 0"
"fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) b) ≥ 0"
have
"(a + b) * c =
fls_shift (- (min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c)) (
(
fls_shift (min (fls_subdegree a) (fls_subdegree b)) a +
fls_shift (min (fls_subdegree a) (fls_subdegree b)) b
) * fls_base_factor c)"
using fls_times_both_shifted_simp[of
"-min (fls_subdegree a) (fls_subdegree b)"
"fls_shift (min (fls_subdegree a) (fls_subdegree b)) a +
fls_shift (min (fls_subdegree a) (fls_subdegree b)) b"
"-fls_subdegree c" "fls_base_factor c"
]
by    simp
also have
"… =
fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c))
(fls_shift (min (fls_subdegree a) (fls_subdegree b)) a * fls_base_factor c)
+
fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c))
(fls_shift (min (fls_subdegree a) (fls_subdegree b)) b * fls_base_factor c)"
using ab
by    (simp add: fls_mult_distrib_subdegree_ge_0(1) del: fls_base_factor_def)
finally show "(a + b) * c = a * c + b * c" by (simp add: fls_times_both_shifted_simp)

have bc:
"fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) b) ≥ 0"
"fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) c) ≥ 0"