(* 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
--> --------------------
¤ Dauer der Verarbeitung: 0.66 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
