products/Sources/formale Sprachen/C/Lyx/images image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Formal_Power_Series.thy   Sprache: Unknown

(*  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
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 "$" 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 have "f $ ?n \ 0 \ (\m
    then show ?thesis ..
  qed
  show ?lhs if ?rhs
    using that by (auto simp add: expand_fps_eq)
qed

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"
proof-
  from assms(1) have "f \ 0" by auto
  moreover from assms(1) have "(LEAST i. f $ i \ 0) = d"
  proof (rule Least_equality)
    fix e assume "f $ e \ 0"
    with assms(2) have "\(e < d)" by blast
    thus "e \ d" by simp
  qed
  ultimately show ?thesis unfolding subdegree_def by simp
qed

lemma nth_subdegree_nonzero [simp,intro]: "f \ 0 \ f $ subdegree f \ 0"
proof-
  assume "f \ 0"
  hence "subdegree f = (LEAST n. f $ n \ 0)" by (simp add: subdegree_def)
  also from \<open>f \<noteq> 0\<close> have "\<exists>n. f$n \<noteq> 0" using fps_nonzero_nth by blast
  from LeastI_ex[OF this] have "f $ (LEAST n. f $ n \ 0) \ 0" .
  finally show ?thesis .
qed

lemma nth_less_subdegree_zero [dest]: "n < subdegree f \ f $ n = 0"
proof (cases "f = 0")
  assume "f \ 0" and less: "n < subdegree f"
  note less
  also from \<open>f \<noteq> 0\<close> have "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def)
  finally show "f $ n = 0" using not_less_Least by blast
qed simp_all

lemma subdegree_geI:
  assumes "f \ 0" "\i. i < n \ f$i = 0"
  shows   "subdegree f \ n"
proof (rule ccontr)
  assume "\(subdegree f \ n)"
  with assms(2) have "f $ subdegree f = 0" by simp
  moreover from assms(1) have "f $ subdegree f \ 0" by simp
  ultimately show False by contradiction
qed

lemma subdegree_greaterI:
  assumes "f \ 0" "\i. i \ n \ f$i = 0"
  shows   "subdegree f > n"
proof (rule ccontr)
  assume "\(subdegree f > n)"
  with assms(2) have "f $ subdegree f = 0" by simp
  moreover from assms(1) have "f $ subdegree f \ 0" by simp
  ultimately show False by contradiction
qed

lemma subdegree_leI:
  "f $ n \ 0 \ subdegree f \ n"
  by (rule leI) auto

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

lemma subdegree_1 [simp]: "subdegree 1 = 0"
  by  (cases "(1::'a) = 0")
      (auto intro: subdegreeI fps_ext simp: subdegree_def)

lemma subdegree_eq_0_iff: "subdegree f = 0 \ f = 0 \ f $ 0 \ 0"
proof (cases "f = 0")
  assume "f \ 0"
  thus ?thesis
    using nth_subdegree_nonzero[OF \<open>f \<noteq> 0\<close>] by (fastforce intro!: subdegreeI)
qed simp_all

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]:
  "subdegree (f-(g::('a::group_add) fps)) = subdegree (g - f)"
proof (-, cases "g-f=0")
  case True
  have "\n. (f - g) $ n = -((g - f) $ n)" by simp
  with True have "f - g = 0" by (intro fps_ext) simp
  with True show ?thesis by simp
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"
    proof-
      fix n
      from fg have "(f + g) $ n = 0" by simp
      hence "f $ n + g $ n - g $ n = - g $ n" by simp
      thus "f $ n = - g $ n" by simp      
    qed
    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-
  from assms have "f = - (- g) \ False" using expand_fps_eq by fastforce
  hence "f \ - (- g)" by fast
  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>Formal power series form a commutative ring with unity, if the range of sequences
  they represent is a commutative ring with unity\<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 ..


subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>

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

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


subsection \<open>Injection of the basic ring elements and multiplication by scalars\<close>

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

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

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

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

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

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

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

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

lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f =
    Abs_fps (\<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


subsection \<open>Formal power series form an integral domain\<close>

instance fps :: (ring) ring ..

instance fps :: (comm_ring) comm_ring ..

instance fps :: (ring_1) ring_1 ..

instance fps :: (comm_ring_1) comm_ring_1 ..

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

instance fps :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..

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

instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ..

instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..

instance fps :: (idom) idom ..

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

lemmas numeral_fps_const = fps_numeral_fps_const

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


subsection \<open>The efps_Xtractor series fps_X\<close>

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_right_mult_nth:
  assumes "k < n"
  shows   "(f * fps_cutoff n g) $ k = (f * g) $ k"
proof-
  from assms have "\i\{0..k}. fps_cutoff n g $ (k - i) = g $ (k - i)" by auto
  thus ?thesis by (simp add: fps_mult_nth)
qed

subsection \<open>Formal Power series form a metric space\<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>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>Inverses and division of formal power series\<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 x * f$0 = 1\<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 f$0 * y = 1\<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}"
  shows "fps_left_inverse 0 x = fps_const x"
  and   "fps_right_inverse 0 y = fps_const y"
  using fps_const_lr_inverse[of 0]
  by    simp_all

lemma fps_inverse_zero_conv_fps_const:
  "inverse (0::'a::{comm_monoid_add,mult_zero,uminus,inverse} fps) = fps_const (inverse 0)"
  using fps_lr_inverse_zero(2)[of "inverse (0::'a)"by (simp add: fps_inverse_def)

lemma fps_inverse_zero':
  assumes "inverse (0::'a::{comm_monoid_add,inverse,mult_zero,uminus}) = 0"
  shows   "inverse (0::'a fps) = 0"
  by      (simp add: assms fps_inverse_zero_conv_fps_const)

lemma fps_inverse_zero [simp]:
  "inverse (0::'a::division_ring fps) = 0"
  by (rule fps_inverse_zero'[OF inverse_zero])

lemma fps_lr_inverse_one:
  fixes x :: "'a::{ab_group_add,mult_zero,one}"
  and   y :: "'b::{comm_monoid_add,mult_zero,uminus,one}"
  shows "fps_left_inverse 1 x = fps_const x"
  and   "fps_right_inverse 1 y = fps_const y"
  using fps_const_lr_inverse[of 1]
  by    simp_all

lemma fps_lr_inverse_one_one:
  "fps_left_inverse 1 1 = (1::'a::{ab_group_add,mult_zero,one} fps)"
  "fps_right_inverse 1 1 = (1::'b::{comm_monoid_add,mult_zero,uminus,one} fps)"
  by (simp_all add: fps_lr_inverse_one)

lemma fps_inverse_one':
  assumes "inverse (1::'a::{comm_monoid_add,inverse,mult_zero,uminus,one}) = 1"
  shows   "inverse (1 :: 'a fps) = 1"
  using   assms fps_lr_inverse_one_one(2)
  by      (simp add: fps_inverse_def)

lemma fps_inverse_one [simp]: "inverse (1 :: 'a :: division_ring fps) = 1"
  by (rule fps_inverse_one'[OF inverse_1])

lemma fps_lr_inverse_minus:
  fixes f :: "'a::ring_1 fps"
  shows "fps_left_inverse (-f) (-x) = - fps_left_inverse f x"
  and   "fps_right_inverse (-f) (-x) = - fps_right_inverse f x"
proof-

  show "fps_left_inverse (-f) (-x) = - fps_left_inverse f x"
  proof (intro fps_ext)
    fix n show "fps_left_inverse (-f) (-x) $ n = - fps_left_inverse f x $ n"
    proof (induct n rule: nat_less_induct)
      case (1 n) thus ?case by (cases n) (simp_all add: sum_negf algebra_simps)
    qed
  qed

  show "fps_right_inverse (-f) (-x) = - fps_right_inverse f x"
  proof (intro fps_ext)
    fix n show "fps_right_inverse (-f) (-x) $ n = - fps_right_inverse f x $ n"
    proof (induct n rule: nat_less_induct)
      case (1 n) show ?case
      proof (cases n)
        case (Suc m)
        with 1 have
          "\i\{1..Suc m}. fps_right_inverse (-f) (-x) $ (Suc m - i) =
            - fps_right_inverse f x $ (Suc m - i)"
          by auto
        with Suc show ?thesis by (simp add: sum_negf algebra_simps)
      qed simp
    qed
  qed

qed

lemma fps_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: division_ring fps)"
  by (simp add: fps_inverse_def fps_lr_inverse_minus(2))

lemma fps_left_inverse:
  fixes   f :: "'a::ring_1 fps"
  assumes f0: "x * f$0 = 1"
  shows   "fps_left_inverse f x * f = 1"
proof (rule fps_ext)
  fix n show "(fps_left_inverse f x * f) $ n = 1 $ n"
    by (cases n) (simp_all add: f0 fps_mult_nth mult.assoc)
qed

lemma fps_right_inverse:
  fixes   f :: "'a::ring_1 fps"
  assumes f0: "f$0 * y = 1"
  shows   "f * fps_right_inverse f y = 1"
proof (rule fps_ext)
  fix n
  show "(f * fps_right_inverse f y) $ n = 1 $ n"
  proof (cases n)
    case (Suc k)
    moreover from Suc have "fps_right_inverse f y $ n =
            - y * sum (\<lambda>i. f$i * fps_right_inverse_constructor f y (n - i)) {1..n}"
      by simp
    hence
      "(f * fps_right_inverse f y) $ n =
        - 1 * sum (\<lambda>i. f$i * fps_right_inverse_constructor f y (n - i)) {1..n} +
        sum (\<lambda>i. f$i * (fps_right_inverse_constructor f y (n - i))) {1..n}"
      by (simp add: fps_mult_nth sum.atLeast_Suc_atMost mult.assoc f0[symmetric])
    thus "(f * fps_right_inverse f y) $ n = 1 $ n" by (simp add: Suc)
  qed (simp add: f0 fps_inverse_def)
qed

\<comment> \<open>
  It is possible in a ring for an element to have a left inverse but not a right inverse, or
  vice versa. But when an element has both, they must be the same.
\<close>
lemma fps_left_inverse_eq_fps_right_inverse:
  fixes   f :: "'a::ring_1 fps"
  assumes f0: "x * f$0 = 1" "f $ 0 * y = 1"
  \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
  shows   "fps_left_inverse f x = fps_right_inverse f y"
proof-
  from f0(2) have "f * fps_right_inverse f y = 1"
      by (simp add: fps_right_inverse)
  hence "fps_left_inverse f x * f * fps_right_inverse f y = fps_left_inverse f x"
    by (simp add: mult.assoc)
  moreover from f0(1) have
    "fps_left_inverse f x * f * fps_right_inverse f y = fps_right_inverse f y"
    by (simp add: fps_left_inverse)
  ultimately show ?thesis by simp
qed

lemma fps_left_inverse_eq_fps_right_inverse_comm:
  fixes   f :: "'a::comm_ring_1 fps"
  assumes f0: "x * f$0 = 1"
  shows   "fps_left_inverse f x = fps_right_inverse f x"
  using   assms fps_left_inverse_eq_fps_right_inverse[of x f x]
  by      (simp add: mult.commute)

lemma fps_left_inverse':
  fixes   f :: "'a::ring_1 fps"
  assumes "x * f$0 = 1" "f$0 * y = 1"
  \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
  shows   "fps_right_inverse f y * f = 1"
  using   assms fps_left_inverse_eq_fps_right_inverse[of x f y] fps_left_inverse[of x f]
  by      simp

lemma fps_right_inverse':
  fixes   f :: "'a::ring_1 fps"
  assumes "x * f$0 = 1" "f$0 * y = 1"
  \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
  shows   "f * fps_left_inverse f x = 1"
  using   assms fps_left_inverse_eq_fps_right_inverse[of x f y] fps_right_inverse[of f y]
  by      simp

lemma inverse_mult_eq_1 [intro]:
  assumes "f$0 \ (0::'a::division_ring)"
  shows   "inverse f * f = 1"
  using   fps_left_inverse'[of "inverse (f$0)"]
  by      (simp add: assms fps_inverse_def)

lemma inverse_mult_eq_1':
  assumes "f$0 \ (0::'a::division_ring)"
  shows   "f * inverse f = 1"
  using   assms fps_right_inverse
  by      (force simp: fps_inverse_def)

lemma fps_mult_left_inverse_unit_factor:
  fixes   f :: "'a::ring_1 fps"
  assumes "x * f $ subdegree f = 1"
  shows   "fps_left_inverse (unit_factor f) x * f = fps_X ^ subdegree f"
proof-
  have
    "fps_left_inverse (unit_factor f) x * f =
      fps_left_inverse (unit_factor f) x * unit_factor f * fps_X ^ subdegree f"
    using fps_unit_factor_decompose[of f] by (simp add: mult.assoc)
  with assms show ?thesis by (simp add: fps_left_inverse)
qed

lemma fps_mult_right_inverse_unit_factor:
  fixes   f :: "'a::ring_1 fps"
  assumes "f $ subdegree f * y = 1"
  shows   "f * fps_right_inverse (unit_factor f) y = fps_X ^ subdegree f"
--> --------------------

--> maximum size reached

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

[ Seitenstruktur0.58Drucken  etwas mehr zur Ethik  ]