Quelle Formal_Laurent_Series.thy Sprache: Isabelle

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

section \<open>A formalization of formal Laurent series\<close>

theory Formal_Laurent_Series
imports
  Polynomial_FPS
begin

subsection \<open>The type of formal Laurent series\<close>

subsubsection \<open>Type definition\<close>

typedef (overloaded) 'a fls = "{f::int \ 'a::zero. \\<^sub>\ n::nat. f (- int n) = 0}"
  morphisms fls_nth Abs_fls
proof
  show "(\x. 0) \ {f::int \ 'a::zero. \\<^sub>\ n::nat. f (- int n) = 0}"
    by simp
qed

setup_lifting type_definition_fls

unbundle fps_syntax
notation fls_nth (infixl \<open>$$\<close> 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)"
  by (simp add: fls_nth_inject[symmetric] fun_eq_iff)

lemma nth_Abs_fls [simp]: "\\<^sub>\n. f (- int n) = 0 \ Abs_fls f $$ n = f n"
by (simp add: Abs_fls_inverse[OF CollectI])

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
  shows   "Abs_fls f $$ n = f n"
proof (intro nth_Abs_fls_ex_nat_lower_bound)
  from assms obtain N::int where "\n
  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
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 thesis) \ thesis" by fast
qed

subsubsection \<open>Definition of basic Laurent series\<close>

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

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"
    by (simp add: eventually_cofinite)
  instance ..
end

lemma fls_one_nth [simp]:
  "1 $$ n = (if n = 0 then 1 else 0)"
  by (simp add: one_fls_def eventually_cofinite)

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

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

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

lemma fls_X_inv_nth [simp]:
  "fls_X_inv $$ n = (if n = -1 then 1 else 0)"
  by (simp add: fls_X_inv_def eventually_cofinite)

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

subsection \<open>Subdegrees\<close>

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 (simp add: M_def)
  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 \<open>M \<le> m\<close> 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' \<noteq> 0" "\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n' \<le> m"
    from n'(1) M have "M \ n'" by fast
    define l where "l = nat (n' - M)"
    from \<open>M \<le> n'\<close> 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"
  by (simp add: fls_subdegree_def)

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 \<open>Shifting\<close>

subsubsection \<open>Shift definition\<close>

definition fls_shift :: "int \ ('a::zero) fls \ 'a fls"
  where "fls_shift n f \ Abs_fls (\k. f $$ (k+n))"
\<comment> \<open>Since the index set is unbounded in both directions, we can shift in either direction.\<close>

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
  hence "\n
  thus "\N. \n
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"
  by (metis add_minus_cancel fls_shift_eq_iff fls_shift_fls_shift)

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

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"
  by (simp_all add: fls_X_conv_shift_1 fls_X_inv_conv_shift_1)

subsubsection \<open>Base factor\<close>

text \<open>
  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}.
\<close>

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 \<open>Conversion between formal power and Laurent series\<close>

subsubsection \<open>Converting Laurent to power series\<close>

text \<open>
  We can truncate a Laurent series at index 0 to create a power series, called the regular part.
\<close>

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

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:
  "\\<^sub>\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 (\<lambda>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")
        (simp_all add: fls_regpart_eq0_imp_nonpos_subdegree)

lemma fls_regpart_subdegree_conv:
  assumes "fls_subdegree f \ 0"
  shows   "subdegree (fls_regpart f) = nat (fls_subdegree f)"
\<comment>\<open>
  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.
\<close>
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 \<open>
  The terms below the zeroth form a polynomial in the inverse of the implied variable,
  called the principle part.
\<close>

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]
    by (simp add: fls_prpart_def)
  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"
  by (simp add: fls_prpart_eq0_iff)

lemma fls_prpart_one [simp]: "fls_prpart 1 = 0"
  by (simp add: fls_prpart_eq0_iff)

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

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 (simp add: LHS_def RHS_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 \<open>The essential data of a formal Laurant series resides from the subdegree up.\<close>

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

lemma fls_base_factor_to_fps_nth:
  "fls_base_factor_to_fps f $ n = f $$ (fls_subdegree f + int n)"
  by (simp add: algebra_simps)

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 \<open>Converting power to Laurent series\<close>

text \<open>We can extend a power series by 0s below to create a Laurent series.\<close>

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 \<open>Algebraic structures\<close>

subsubsection \<open>Addition\<close>

instantiation fls :: (monoid_add) plus
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 "\\<^sub>\n. f (- int n) = 0" "\\<^sub>\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 "\\<^sub>\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

instance fls :: (monoid_add) monoid_add
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

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

lemma fls_nth_sum: "fls_nth (\x\A. f x) n = (\x\A. fls_nth (f x) n)"
  by (induction A rule: infinite_finite_induct) auto

subsubsection \<open>Subtraction and negatives\<close>

instantiation fls :: (group_add) minus
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 "\\<^sub>\n. f (- int n) = 0" "\\<^sub>\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 "\\<^sub>\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

instantiation fls :: (group_add) uminus
begin
  lift_definition uminus_fls :: "'a fls \ 'a fls" is "\f n. - f n"
  proof-
    fix f :: "int \ 'a" assume "\\<^sub>\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 "\\<^sub>\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

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

instance fls :: (ab_group_add) ab_group_add
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]
        add_diff_cancel[of "fls_regpart_as_fls f" "fls_prpart_as_fls 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]
        add_diff_cancel[of "fls_prpart_as_fls f" "fls_regpart_as_fls f"]
  by    simp

subsubsection \<open>Multiplication\<close>

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

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 =
        (\<Sum>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 del: of_nat_diff)
    moreover have
      "(\i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i)) =
        (\<Sum>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)
    qed (simp add: 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)) =
      (\<Sum>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)
  qed (simp_all add: dfg_def algebra_simps)
  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)) =
      (\<Sum>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)
  qed (simp_all add: dfg_def algebra_simps)
  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)"
  by (simp add: fls_times_nth(1))

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) ))"
    by (simp add: fls_times_def)
  moreover have
    "a * (0::'a fls) =
      fls_shift (fls_subdegree a) (fps_to_fls ( (fls_base_factor_to_fps a)*(0::'a fps) ))"
    by (simp add: fls_times_def)
  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]
  by    (simp_all add: fls_times_def fps_one_mult)

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)
    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))
  qed (simp add: fls_times_nth_eq0)
  show "(f * fls_const x ) $$ n = f$$n * x"
  proof (cases "n)
    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 (simp add: fls_times_nth_eq0)
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_subdegree_add_eq1:
  assumes "f \ 0" "fls_subdegree f < fls_subdegree g"
  shows   "fls_subdegree (f + g) = fls_subdegree f"
proof (intro antisym)
  from assms have *: "fls_nth (f + g) (fls_subdegree f) \ 0"
    by auto
  from * show "fls_subdegree (f + g) \ fls_subdegree f"
    by (rule fls_subdegree_leI)
  from * have "f + g \ 0"
    using fls_nonzeroI by blast
  thus "fls_subdegree f \ fls_subdegree (f + g)"
    using assms(2) fls_plus_subdegree by force
qed

lemma fls_subdegree_add_eq2:
  assumes "g \ 0" "fls_subdegree g < fls_subdegree f"
  shows   "fls_subdegree (f + g) = fls_subdegree g"
proof (intro antisym)
  from assms have *: "fls_nth (f + g) (fls_subdegree g) \ 0"
    by auto
  from * show "fls_subdegree (f + g) \ fls_subdegree g"
    by (rule fls_subdegree_leI)
  from * have "f + g \ 0"
    using fls_nonzeroI by blast
  thus "fls_subdegree g \ fls_subdegree (f + g)"
    using assms(2) fls_plus_subdegree by force
qed

lemma fls_subdegree_diff_eq1:
  assumes "f \ 0" "fls_subdegree f < fls_subdegree g"
  shows   "fls_subdegree (f - g) = fls_subdegree f"
  using fls_subdegree_add_eq1[of f "-g"] assms by simp

lemma fls_subdegree_diff_eq2:
  assumes "g \ 0" "fls_subdegree g < fls_subdegree f"
  shows   "fls_subdegree (f - g) = fls_subdegree g"
  using fls_subdegree_add_eq2[of "-g" f] assms by simp

lemma nat_minus_fls_subdegree_plus_const_eq:
  "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
proof (cases "fls_subdegree F < 0")
  case True
  hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
    by (intro fls_subdegree_add_eq1) auto
  thus ?thesis
    by simp
next
  case False
  thus ?thesis
    by (auto simp: fls_subdegree_ge0I)
qed

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)"
      by (simp add: algebra_simps fls_times_def)
  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)"
      by (simp add: algebra_simps fls_times_def)
  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)"
  by    (simp add: fls_shifted_times_simps)

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"]
  by    (simp_all add: fls_shifted_times_simps)

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

lemma fls_times_base_factor_conv_shifted_times:
\<comment> \<open>Convenience form of lemma @{text "fls_times_both_shifted_simp"}.\<close>
  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)"
  by (simp add: fls_times_both_shifted_simp)

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
          )
        )
      )"
    by (simp add:
      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)"
      by (simp add: fps_mult_subdegree_ge fls_regpart_subdegree_conv[symmetric])
    with 1 assms show ?thesis by simp
  qed (simp add: 1)
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
qed (simp add: fps_times_conv_fls_times)

lemma fls_X_times_conv_shift:
  fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls"
  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:
  fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  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:
  fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls"
  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"]
    by    (simp_all add: fls_times_conv_fps_times)
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)"
    by (simp add: fls_times_both_shifted_simp)
  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"
    by (simp_all add: fls_shift_nonneg_subdegree)
  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"
    by (simp_all add: fls_shift_nonneg_subdegree)
  have
    "a * (b + c) =
      fls_shift (- (fls_subdegree a + min (fls_subdegree b) (fls_subdegree c))) (
        fls_base_factor a * (
          fls_shift (min (fls_subdegree b) (fls_subdegree c)) b +
          fls_shift (min (fls_subdegree b) (fls_subdegree c)) c
        )
      )
    "
    using fls_times_both_shifted_simp[of
            "-fls_subdegree a" "fls_base_factor a"
            "-min (fls_subdegree b) (fls_subdegree c)"
            "fls_shift (min (fls_subdegree b) (fls_subdegree c)) b +
            fls_shift (min (fls_subdegree b) (fls_subdegree c)) c"
          ]
    by    simp
  also have
    "\ =
      fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c)))
        (fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) b)
      +
      fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c)))
        (fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) c)
    "
    using bc
    by    (simp add: fls_mult_distrib_subdegree_ge_0(2) del: fls_base_factor_def)
  finally show "a * (b + c) = a * b + a * c" by (simp add: fls_times_both_shifted_simp)

qed

lemma fls_mult_commute_subdegree_ge_0:
  fixes   f g :: "'a::comm_semiring_0 fls"
  assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0"
  shows   "f * g = g * f"
  using   assms
  by      (simp add: fls_times_conv_fps_times mult.commute)

lemma fls_mult_commute_base_factor:
  fixes a b c :: "'a::comm_semiring_0 fls"
  shows "fls_base_factor a * fls_base_factor b = fls_base_factor b * fls_base_factor a"
  by    (simp add: fls_mult_commute_subdegree_ge_0 del: fls_base_factor_def)

instance fls :: (comm_semiring_0) comm_semiring_0
proof
  fix a b c :: "'a fls"
  show "a * b = b * a"
    using fls_times_conv_base_factor_times[of a b] fls_times_conv_base_factor_times[of b a]
          fls_mult_commute_base_factor[of a b]
    by    (simp add: add.commute)
qed (simp add: distrib_right)

instance fls :: (semiring_1) semiring_1
  by (standard, simp_all add: fls_mult_one)

lemma fls_of_nat: "(of_nat n :: 'a::semiring_1 fls) = fls_const (of_nat n)"
  by (induct n) (auto intro: fls_eqI)

lemma fls_of_nat_nth: "of_nat n $$ k = (if k=0 then of_nat n else 0)"
  by (simp add: fls_of_nat)

lemma fls_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: fls_of_nat)

lemma fls_subdegree_of_nat [simp]: "fls_subdegree (of_nat n) = 0"
  by (simp add: fls_of_nat)

lemma fls_shift_of_nat_nth:
  "fls_shift k (of_nat a) $$ n = (if n=-k then of_nat a else 0)"
  by (simp add: fls_of_nat fls_shift_const_nth)

lemma fls_base_factor_of_nat [simp]:
  "fls_base_factor (of_nat n :: 'a::semiring_1 fls) = (of_nat n :: 'a fls)"
  by (simp add: fls_of_nat)

lemma fls_regpart_of_nat [simp]: "fls_regpart (of_nat n) = (of_nat n :: 'a::semiring_1 fps)"
  by (simp add: fls_of_nat fps_of_nat)

lemma fls_prpart_of_nat [simp]: "fls_prpart (of_nat n) = 0"
  by (simp add: fls_prpart_eq0_iff)

lemma fls_base_factor_to_fps_of_nat:
  "fls_base_factor_to_fps (of_nat n) = (of_nat n :: 'a::semiring_1 fps)"
  by simp

lemma fps_to_fls_of_nat:
  "fps_to_fls (of_nat n) = (of_nat n :: 'a::semiring_1 fls)"
proof -
  have "fps_to_fls (of_nat n) = fps_to_fls (fps_const (of_nat n))"
    by (simp add: fps_of_nat)
  thus ?thesis by (simp add: fls_of_nat)
qed

lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
  by (metis fps_to_fls_of_nat of_nat_numeral)

lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b"
  by (induction b) (auto simp flip: fls_const_mult_const)

lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n"
  by (metis fls_of_nat of_nat_numeral)

lemma fls_mult_of_numeral_nth [simp]:
  shows "(numeral k * f) $$ n = numeral k * f $$ n"
  and   "(f * numeral k) $$ n = f $$ n * numeral k"
  by (metis fls_const_numeral fls_mult_const_nth)+

lemma fls_nth_numeral' [simp]:
  "numeral n $$ 0 = numeral n" "k \ 0 \ numeral n $$ k = 0"
  by (metis fls_const_nth fls_const_numeral)+

instance fls :: (comm_semiring_1) comm_semiring_1
  by standard simp

instance fls :: (ring) ring ..

instance fls :: (comm_ring) comm_ring ..

instance fls :: (ring_1) ring_1 ..

lemma fls_of_int_nonneg: "(of_int (int n) :: 'a::ring_1 fls) = fls_const (of_int (int n))"
  by (induct n) (auto intro: fls_eqI)

lemma fls_of_int: "(of_int i :: 'a::ring_1 fls) = fls_const (of_int i)"
proof (induct i)
  case (neg i)
  have "of_int (int (Suc i)) = fls_const (of_int (int (Suc i)) :: 'a)"
    using fls_of_int_nonneg[of "Suc i"] by simp
  hence "- of_int (int (Suc i)) = - fls_const (of_int (int (Suc i)) :: 'a)"
    by simp
  thus ?case by (simp add: fls_const_uminus[symmetric])
qed (rule fls_of_int_nonneg)

lemma fls_of_int_nth: "of_int n $$ k = (if k=0 then of_int n else 0)"
  by (simp add: fls_of_int)

lemma fls_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: fls_of_int)

lemma fls_subdegree_of_int [simp]: "fls_subdegree (of_int i) = 0"
  by (simp add: fls_of_int)

lemma fls_shift_of_int_nth:
  "fls_shift k (of_int i) $$ n = (if n=-k then of_int i else 0)"
  by (simp add: fls_of_int_nth)

lemma fls_base_factor_of_int [simp]:
  "fls_base_factor (of_int i :: 'a::ring_1 fls) = (of_int i :: 'a fls)"
  by (simp add: fls_of_int)

lemma fls_regpart_of_int [simp]:
  "fls_regpart (of_int i) = (of_int i :: 'a::ring_1 fps)"
  by (simp add: fls_of_int fps_of_int)

lemma fls_prpart_of_int [simp]: "fls_prpart (of_int n) = 0"
  by (simp add: fls_prpart_eq0_iff)

lemma fls_base_factor_to_fps_of_int:
  "fls_base_factor_to_fps (of_int i) = (of_int i :: 'a::ring_1 fps)"
  by simp

lemma fps_to_fls_of_int:
  "fps_to_fls (of_int i) = (of_int i :: 'a::ring_1 fls)"
proof -
  have "fps_to_fls (of_int i) = fps_to_fls (fps_const (of_int i))"
    by (simp add: fps_of_int)
  thus ?thesis by (simp add: fls_of_int)
qed

instance fls :: (comm_ring_1) comm_ring_1 ..

instance fls :: (semiring_no_zero_divisors) semiring_no_zero_divisors
proof
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Dauer der Verarbeitung: 0.28 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.