Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Computational_Algebra/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 257 kB

Quelle Formal_Power_Series.thy Sprache: Isabelle

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

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

theory Formal_Power_Series
imports
  Complex_Main
  Euclidean_Algorithm
  Primes
  "HOL-Library.FuncSet"
  "HOL-Library.Multiset"
begin

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

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

notation fps_nth (infixl \<open>$\<close> 75)

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

lemmas fps_eq_iff = expand_fps_eq

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

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

text \<open>Definition of the basic elements 0 and 1 and the basic operations of addition,
  negation and multiplication.\<close>

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

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

lemma fps_nonzero_nth: "f \ 0 \ (\ n. f $ n \ 0)"
  by (simp add: expand_fps_eq)

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

lemma fps_nonzeroI: "f$n \ 0 \ f \ 0"
  by auto

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemmas mult_nth_0 = fps_mult_nth_0
lemmas mult_nth_1 = fps_mult_nth_1

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

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

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

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

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

subsection \<open>Subdegrees\<close>

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

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

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

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

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

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

lemma subdegree_leI:
  "f $ n \ 0 \ subdegree f \ n"
  using linorder_not_less by blast

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

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

lemma subdegree_eq_0_iff: "subdegree f = 0 \ f = 0 \ f $ 0 \ 0"
  using nth_subdegree_nonzero subdegree_leI by fastforce

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

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

lemma fps_nonzero_subdegree_nonzeroI: "subdegree f > 0 \ f \ 0"
by auto

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

subsection \<open>Ring structure\<close>

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

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

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

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

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

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

instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..

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

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

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

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

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

instance fps :: (semiring_0_cancel) semiring_0_cancel ..

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

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

instance fps :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..

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

instance fps :: (comm_semiring_1) comm_semiring_1
  by standard simp

instance fps :: (semiring_1_cancel) semiring_1_cancel ..

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

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

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

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

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

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

lemma fps_const_eq_0_iff [simp]: "fps_const c = 0 \ c = 0"
  by (auto simp: fps_eq_iff)

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

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

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

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

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

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

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

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

lemmas fps_const_minus = fps_const_sub

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

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

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

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

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

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

instance fps :: (ring) ring ..

instance fps :: (comm_ring) comm_ring ..

instance fps :: (ring_1) ring_1 ..

instance fps :: (comm_ring_1) comm_ring_1 ..

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

instance fps :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..

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

instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ..

instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..

instance fps :: (idom) idom ..

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

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

lemma semiring_char_fps [simp]: "CHAR('a :: comm_semiring_1 fps) = CHAR('a)"
  by (rule CHAR_eqI) (auto simp flip: fps_of_nat simp: of_nat_eq_0_iff_char_dvd)

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

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

lemmas numeral_fps_const = fps_numeral_fps_const

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

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

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

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

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

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

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

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

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

instance fps :: (semiring_char_0) semiring_char_0
proof
  show "inj (of_nat :: nat \ 'a fps)"
  proof
    fix m n :: nat
    assume "of_nat m = (of_nat n :: 'a fps)"
    hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
      by (simp only: )
    thus "m = n"
      by simp
  qed
qed

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

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

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

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

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

lemma subdegree_prod:
  fixes f :: "'a \ 'b :: idom fps"
  assumes "\x. x \ A \ f x \ 0"
  shows   "subdegree (\x\A. f x) = (\x\A. subdegree (f x))"
  using assms by (induction A rule: infinite_finite_induct) auto

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

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

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

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

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

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

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

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

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

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

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

lemma fps_X_nth[simp]: "fps_X$n = (if n = 1 then 1 else 0)"
  by (simp add: fps_X_def)

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

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

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

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

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

lemma fps_mult_fps_X_plus_1_nth:
  "((1+fps_X)*a) $n = (if n = 0 then (a$n :: 'a::semiring_1) else a$n + a$(n - 1))"
proof (cases n)
  case 0
  then show ?thesis
    by (simp add: fps_mult_nth)
next
  case (Suc m)
  have "((1 + fps_X)*a) $ n = sum (\i. (1 + fps_X) $ i * a $ (n - i)) {0..n}"
    by (simp add: fps_mult_nth)
  also have "\ = sum (\i. (1+fps_X)$i * a$(n-i)) {0.. 1}"
    unfolding Suc by (rule sum.mono_neutral_right) auto
  also have "\ = (if n = 0 then a$n else a$n + a$(n - 1))"
    by (simp add: Suc)
  finally show ?thesis .
qed

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

lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ fps_const c"
proof
  assume "(fps_X::'a fps) = fps_const (c::'a)"
  hence "fps_X$1 = (fps_const (c::'a))$1" by (simp only:)
  thus False by auto
qed

lemma fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ 0"
  by (simp only: fps_const_0_eq_0[symmetric] fps_X_neq_fps_const) simp

lemma fps_X_neq_one [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ 1"
  by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp

lemma fps_X_neq_numeral [simp]: "fps_X \ numeral c"
  by (simp only: numeral_fps_const fps_X_neq_fps_const) simp

lemma fps_X_pow_eq_fps_X_pow_iff [simp]: "fps_X ^ m = fps_X ^ n \ m = n"
proof
  assume "(fps_X :: 'a fps) ^ m = fps_X ^ n"
  hence "(fps_X :: 'a fps) ^ m $ m = fps_X ^ n $ m" by (simp only:)
  thus "m = n" by (simp split: if_split_asm)
qed simp_all

subsection \<open>Shifting and slicing\<close>

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

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

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

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

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

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

lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)"
  by (simp add: numeral_fps_const fps_shift_fps_const)

lemma fps_shift_fps_X [simp]:
  "n \ 1 \ fps_shift n fps_X = (if n = 1 then 1 else 0)"
  by (intro fps_ext) (auto simp: fps_X_def)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma fps_shift_times_fps_X_power:
  "n \ subdegree f \ fps_shift n f * fps_X ^ n = f"
  by (intro fps_ext) (simp add: fps_X_power_mult_right_nth nth_less_subdegree_zero)

lemma fps_shift_times_fps_X_power' [simp]:
  "fps_shift n (f * fps_X^n) = f"
  by (intro fps_ext) (simp add: fps_X_power_mult_right_nth nth_less_subdegree_zero)

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

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

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

lemma subdegree_decompose':
  "n \ subdegree f \ f = fps_shift n f * fps_X^n"
  by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth intro!: nth_less_subdegree_zero)

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

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

lemma fps_unit_factor_nth_0: "f \ 0 \ unit_factor f $ 0 \ 0"
  by simp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma fps_cutoff_add: "fps_cutoff n (f + g :: 'a :: monoid_add fps) = fps_cutoff n f + fps_cutoff n g"
  by (auto simp: fps_eq_iff)

lemma fps_cutoff_diff: "fps_cutoff n (f - g :: 'a :: group_add fps) = fps_cutoff n f - fps_cutoff n g"
  by (auto simp: fps_eq_iff)

lemma fps_cutoff_uminus: "fps_cutoff n (-f :: 'a :: group_add fps) = -fps_cutoff n f"
  by (auto simp: fps_eq_iff)

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

lemma fps_cutoff_eq_fps_cutoff_iff:
  "fps_cutoff n f = fps_cutoff n g \ (\k
  by (subst fps_eq_iff) auto

lemma fps_conv_fps_X_power_mult_fps_shift:
  assumes "f = 0 \ subdegree f \ n"
  shows   "f = fps_X ^ n * fps_shift n f"
proof -
  have "f = fps_X ^ n * fps_shift n f + fps_cutoff n f"
    by (auto simp: fps_eq_iff fps_X_power_mult_nth)
  also have "fps_cutoff n f = 0"
    by (subst fps_cutoff_zero_iff) (use assms in auto)
  finally show ?thesis by simp
qed

subsection \<open>Metrizability\<close>

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

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

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

instance ..

end

instantiation fps :: (group_add) metric_space
begin

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

definition open_fps_def' [code del]:
  "open (U :: 'a fps set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)"

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

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

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

end

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

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

text \<open>Topology\<close>

subsection \<open>The topology of formal power series\<close>

text \<open>
  A set of formal power series is open iff for any power series $f$ in it, there exists some
  number $n$ such that all power series that agree with $f$ on the first $n$ components are
  also in it.
\<close>
lemma open_fps_iff:
  "open A \ (\F\A. \n. {G. fps_cutoff n G = fps_cutoff n F} \ A)"
proof
  assume "open A"
  show "\F\A. \n. {G. fps_cutoff n G = fps_cutoff n F} \ A"
  proof
    fix F :: "'a fps"
    assume F: "F \ A"
    with \<open>open A\<close> obtain e where e: "e > 0" "\<And>G. dist G F < e \<Longrightarrow> G \<in> A"
      by (force simp: open_fps_def)
    thm dist_fps_def
    have "filterlim (\n. (1/2)^n :: real) (nhds 0) at_top"
      by (intro LIMSEQ_realpow_zero) auto
    from order_tendstoD(2)[OF this e(1)] have "eventually (\n. 1 / 2 ^ n < e) at_top"
      by (simp add: power_divide)
    then obtain n where n: "1 / 2 ^ n < e"
      by (auto simp: eventually_sequentially)
    show "\n. {G. fps_cutoff n G = fps_cutoff n F} \ A"
    proof (rule exI[of _ n], safe)
      fix G assume *: "fps_cutoff n G = fps_cutoff n F"
      show "G \ A"
      proof (cases "G = F")
        case False
        hence "dist G F = inverse (2 ^ subdegree (G - F))"
          by (auto simp: dist_fps_def)
        also have "subdegree (G - F) \ n"
        proof (rule subdegree_geI)
          fix i assume "i < n"
          hence "fps_nth (G - F) i = fps_nth (fps_cutoff n G - fps_cutoff n F) i"
            by (auto simp: fps_eq_iff)
          also from * have "\ = 0"
            by simp
          finally show "fps_nth (G - F) i = 0" .
        qed (use False in auto)
        hence "inverse (2 ^ subdegree (G - F) :: real) \ inverse (2 ^ n)"
          by (intro le_imp_inverse_le power_increasing) auto
        also have "\ < e"
          using n by (simp add: field_simps)
        finally show "G \ A"
          using e(2)[of G] by auto
      qed (use \<open>F \<in> A\<close> in auto)
    qed
  qed
next
  assume *: "\F\A. \n. {G. fps_cutoff n G = fps_cutoff n F} \ A"
  show "open A"
    unfolding open_fps_def
  proof safe
    fix F assume F: "F \ A"
    with * obtain n where n: "\G. fps_cutoff n G = fps_cutoff n F \ G \ A"
      by blast
    show "\r>0. {G. dist G F < r} \ A"
    proof (rule exI[of _ "1 / 2 ^ n"], safe)
      fix G assume dist: "dist G F < 1 / 2 ^ n"
      show "G \ A"
      proof (cases "G = F")
        case False
        hence "dist G F = inverse (2 ^ subdegree (F - G))"
          by (simp add: dist_fps_def)
        with dist have "n < subdegree (F - G)"
          by (auto simp: field_simps)
        hence "fps_nth (F - G) i = 0" if "i \ n" for i
          using that nth_less_subdegree_zero[of i "F - G"] by simp
        hence "fps_cutoff n G = fps_cutoff n F"
          by (auto simp: fps_eq_iff fps_cutoff_def)
        thus "G \ A"
          by (rule n)
      qed (use \<open>F \<in> A\<close> in auto)
    qed auto
  qed
qed

lemma open_fps_cutoff: "open {H. fps_cutoff N H = fps_cutoff N G}"
  unfolding open_fps_iff
proof safe
  fix F assume F: "fps_cutoff N F = fps_cutoff N G"
  show "\n. {G. fps_cutoff n G = fps_cutoff n F}
             \<subseteq> {H. fps_cutoff N H = fps_cutoff N G}"
    by (rule exI[of _ N]) (use F in \<open>auto simp: fps_eq_iff\<close>)
qed

lemma eventually_fps_nth_eq_nhds_fps_strong:
  "eventually (\g. \k\n. fps_nth g k = fps_nth f k) (nhds f)"
proof -
  have "eventually (\g. g \ {g. fps_cutoff (n+1) g = fps_cutoff (n+1) f}) (nhds f)"
    by (rule eventually_nhds_in_open, rule open_fps_cutoff) auto
  thus ?thesis
    by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff)
qed

lemma eventually_fps_nth_eq_nhds_fps: "eventually (\g. fps_nth g k = fps_nth f k) (nhds f)"
  using eventually_fps_nth_eq_nhds_fps_strong[of k] by eventually_elim auto

text \<open>
  A family of formal power series $f_x$ tends to a limit series $g$ at some filter $F$
  iff for any $N\geq 0$, the set of $x$ for which $f_x$ and $G$ agree on the first $N$ coefficients
  is in $F$.

  For a sequence $(f_i)_{n\geq 0}$ this means that $f_i \longrightarrow G$ iff for any
  $N\geq 0$, $f_x$ and $G$ agree for all but finitely many $x$.
\<close>

lemma tendsto_fps_iff:
  "filterlim f (nhds (g :: 'a :: group_add fps)) F \
     (\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F)"
proof safe
  assume lim: "filterlim f (nhds (g :: 'a :: group_add fps)) F"
  show "eventually (\x. fps_nth (f x) n = fps_nth g n) F" for n
  proof -
    define S where "S = {H. fps_cutoff (n+1) H = fps_cutoff (n+1) g}"
    have S: "open S" "g \ S"
      unfolding S_def using open_fps_cutoff[of "n+1" g] by (auto simp: S_def)
    from lim and S have "eventually (\x. f x \ S) F"
      using topological_tendstoD by blast
    thus "eventually (\x. fps_nth (f x) n = fps_nth g n) F"
      by eventually_elim (auto simp: S_def fps_cutoff_eq_fps_cutoff_iff)
  qed
next
  assume *: "\n. eventually (\x. fps_nth (f x) n = fps_nth g n) F"
  show "filterlim f (nhds (g :: 'a :: group_add fps)) F"
  proof (rule topological_tendstoI)
    fix S :: "'a fps set"
    assume S: "open S" "g \ S"
    then obtain N where N: "{H. fps_cutoff N H = fps_cutoff N g} \ S"
      unfolding open_fps_iff by blast
    have "eventually (\x. \n\{..
      by (subst eventually_ball_finite_distrib) (use * in auto)
    hence "eventually (\x. f x \ {H. fps_cutoff N H = fps_cutoff N g}) F"
      by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff)
    thus "eventually (\x. f x \ S) F"
      by eventually_elim (use N in auto)
  qed
qed

lemma tendsto_fpsI:
  assumes "\n. eventually (\x. fps_nth (f x) n = fps_nth G n) F"
  shows   "filterlim f (nhds (G :: 'a :: group_add fps)) F"
  unfolding tendsto_fps_iff using assms by blast

text \<open>The infinite sums and justification of the notation in textbooks.\<close>

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

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

lemma fps_notation: "(\n. sum (\i. fps_const(a$i) * fps_X^i) {0..n}) \ a"
  (is "?s \ a")
proof -
  have "\n0. \n \ n0. dist (?s n) a < r" if "r > 0" for r
  proof -
    obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
      using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto
    show ?thesis
    proof -
      have "dist (?s n) a < r" if nn0: "n \ n0" for n
      proof -
        from that have thnn0: "(1/2)^n \ (1/2 :: real)^n0"
          by (simp add: field_split_simps)
        show ?thesis
        proof (cases "?s n = a")
          case True
          then show ?thesis
            unfolding dist_eq_0_iff[of "?s n" a, symmetric]
            using \<open>r > 0\<close> by (simp del: dist_eq_0_iff)
        next
          case False
          from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n - a)"
            by (simp add: dist_fps_def field_simps)
          from False have kn: "subdegree (?s n - a) > n"
            by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth)
          then have "dist (?s n) a < (1/2)^n"
            by (simp add: field_simps dist_fps_def)
          also have "\ \ (1/2)^n0"
            using nn0 by (simp add: field_split_simps)
          also have "\ < r"
            using n0 by simp
          finally show ?thesis .
        qed
      qed
      then show ?thesis by blast
    qed
  qed
  then show ?thesis
    unfolding lim_sequentially by blast
qed

subsection \<open>Division\<close>

declare sum.cong[fundef_cong]

fun fps_left_inverse_constructor ::
  "'a::{comm_monoid_add,times,uminus} fps \ 'a \ nat \ 'a"
where
  "fps_left_inverse_constructor f a 0 = a"
| "fps_left_inverse_constructor f a (Suc n) =
    - sum (\<lambda>i. fps_left_inverse_constructor f a i * f$(Suc n - i)) {0..n} * a"

\<comment> \<open>This will construct a left inverse for f in case that \<^prop>\<open>x * f$0 = 1\<close>\<close>
abbreviation "fps_left_inverse \ (\f x. Abs_fps (fps_left_inverse_constructor f x))"

fun fps_right_inverse_constructor ::
  "'a::{comm_monoid_add,times,uminus} fps \ 'a \ nat \ 'a"
where
  "fps_right_inverse_constructor f a 0 = a"
| "fps_right_inverse_constructor f a n =
    - a * sum (\<lambda>i. f$i * fps_right_inverse_constructor f a (n - i)) {1..n}"

\<comment> \<open>This will construct a right inverse for f in case that \<^prop>\<open>f$0 * y = 1\<close>\<close>
abbreviation "fps_right_inverse \ (\f y. Abs_fps (fps_right_inverse_constructor f y))"

instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse
begin

\<comment> \<open>For backwards compatibility.\<close>
abbreviation natfun_inverse:: "'a fps \ nat \ 'a"
  where "natfun_inverse f \ fps_right_inverse_constructor f (inverse (f$0))"

definition fps_inverse_def: "inverse f = Abs_fps (natfun_inverse f)"
\<comment> \<open>
  With scalars from a (possibly non-commutative) ring, this defines a right inverse.
  Furthermore, if scalars are of class @{class mult_zero} and satisfy
  condition @{term "inverse 0 = 0"}, then this will evaluate to zero when
  the zeroth term is zero.
\<close>

definition fps_divide_def: "f div g = fps_shift (subdegree g) (f * inverse (unit_factor g))"
\<comment> \<open>
  If scalars are of class @{class mult_zero} and satisfy condition
  @{term "inverse 0 = 0"}, then div by zero will equal zero.
\<close>

instance ..

end

lemma fps_lr_inverse_0_iff:
  "(fps_left_inverse f x) $ 0 = 0 \ x = 0"
  "(fps_right_inverse f x) $ 0 = 0 \ x = 0"
  by auto

lemma fps_inverse_0_iff': "(inverse f) $ 0 = 0 \ inverse (f $ 0) = 0"
  by (simp add: fps_inverse_def fps_lr_inverse_0_iff(2))

lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \ f $ 0 = 0"
  by (simp add: fps_inverse_0_iff')

lemma fps_lr_inverse_nth_0:
  "(fps_left_inverse f x) $ 0 = x" "(fps_right_inverse f x) $ 0 = x"
  by auto

lemma fps_inverse_nth_0 [simp]: "(inverse f) $ 0 = inverse (f $ 0)"
  by (simp add: fps_inverse_def)

lemma fps_lr_inverse_starting0:
  fixes f :: "'a::{comm_monoid_add,mult_zero,uminus} fps"
  and   g :: "'b::{ab_group_add,mult_zero} fps"
  shows "fps_left_inverse f 0 = 0"
  and   "fps_right_inverse g 0 = 0"
proof-
  show "fps_left_inverse f 0 = 0"
  proof (rule fps_ext)
    fix n show "fps_left_inverse f 0 $ n = 0 $ n"
      by (cases n) (simp_all add: fps_inverse_def)
  qed
  show "fps_right_inverse g 0 = 0"
  proof (rule fps_ext)
    fix n show "fps_right_inverse g 0 $ n = 0 $ n"
      by (cases n) (simp_all add: fps_inverse_def)
  qed
qed

lemma fps_lr_inverse_eq0_imp_starting0:
  "fps_left_inverse f x = 0 \ x = 0"
  "fps_right_inverse f x = 0 \ x = 0"
proof-
  assume A: "fps_left_inverse f x = 0"
  have "0 = fps_left_inverse f x $ 0" by (subst A) simp
  thus "x = 0" by simp
next
  assume A: "fps_right_inverse f x = 0"
  have "0 = fps_right_inverse f x $ 0" by (subst A) simp
  thus "x = 0" by simp
qed

lemma fps_lr_inverse_eq_0_iff:
  fixes x :: "'a::{comm_monoid_add,mult_zero,uminus}"
  and   y :: "'b::{ab_group_add,mult_zero}"
  shows "fps_left_inverse f x = 0 \ x = 0"
  and   "fps_right_inverse g y = 0 \ y = 0"
  using fps_lr_inverse_starting0 fps_lr_inverse_eq0_imp_starting0
  by    auto

lemma fps_inverse_eq_0_iff':
  fixes f :: "'a::{ab_group_add,inverse,mult_zero} fps"
  shows "inverse f = 0 \ inverse (f $ 0) = 0"
  by    (simp add: fps_inverse_def fps_lr_inverse_eq_0_iff(2))

lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::division_ring) fps) \ f $ 0 = 0"
  using fps_inverse_eq_0_iff'[of f] by simp

lemmas fps_inverse_eq_0' = iffD2[OF fps_inverse_eq_0_iff']
lemmas fps_inverse_eq_0  = iffD2[OF fps_inverse_eq_0_iff]

lemma fps_const_lr_inverse:
  fixes a :: "'a::{ab_group_add,mult_zero}"
  and   b :: "'b::{comm_monoid_add,mult_zero,uminus}"
  shows "fps_left_inverse (fps_const a) x = fps_const x"
  and   "fps_right_inverse (fps_const b) y = fps_const y"
proof-
  show "fps_left_inverse (fps_const a) x = fps_const x"
  proof (rule fps_ext)
    fix n show "fps_left_inverse (fps_const a) x $ n = fps_const x $ n"
      by (cases n) auto
  qed
  show "fps_right_inverse (fps_const b) y = fps_const y"
  proof (rule fps_ext)
    fix n show "fps_right_inverse (fps_const b) y $ n = fps_const y $ n"
      by (cases n) auto
  qed
qed

lemma fps_const_inverse:
  fixes     a :: "'a::{comm_monoid_add,inverse,mult_zero,uminus}"
  shows     "inverse (fps_const a) = fps_const (inverse a)"
  unfolding fps_inverse_def
  by        (simp add: fps_const_lr_inverse(2))

lemma fps_lr_inverse_zero:
  fixes x :: "'a::{ab_group_add,mult_zero}"
  and   y :: "'b::{comm_monoid_add,mult_zero,uminus}"
--> --------------------

--> maximum size reached

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

quality95%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

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.