(* Title: HOL/Computational_Algebra/Formal_Power_Series.thy
Author: Amine Chaieb, University of Cambridge
*)
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 \<Rightarrow> 'a. True}"
morphisms fps_nth Abs_fps
by simp
notation fps_nth (infixl "$" 75)
lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p $ n = q $ n)"
by (simp add: fps_nth_inject [symmetric] fun_eq_iff)
lemma fps_ext: "(\<And>n. p $ n = q $ n) \<Longrightarrow> 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 (\<lambda>n. 0)"
instance ..
end
lemma fps_zero_nth [simp]: "0 $ n = 0"
unfolding fps_zero_def by simp
instantiation fps :: ("{one, zero}") one
begin
definition fps_one_def: "1 = Abs_fps (\<lambda>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: "(+) = (\<lambda>f g. Abs_fps (\<lambda>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: "(-) = (\<lambda>f g. Abs_fps (\<lambda>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 = (\<lambda>f. Abs_fps (\<lambda>n. - (f $ n)))"
instance ..
end
lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)"
unfolding fps_uminus_def by simp
instantiation fps :: ("{comm_monoid_add, times}") times
begin
definition fps_times_def: "( * ) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
instance ..
end
lemma fps_mult_nth: "(f * g) $ n = (\<Sum>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
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 cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"
by auto
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
by auto
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
lemma fps_mult_assoc_lemma:
fixes k :: nat
and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>j=0..k. \<Sum>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) semigroup_mult
proof
fix a b c :: "'a fps"
show "(a * b) * c = a * (b * c)"
proof (rule fps_ext)
fix n :: nat
have "(\<Sum>j=0..n. \<Sum>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
lemma fps_mult_commute_lemma:
fixes n :: nat
and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>i=0..n. f i (n - i)) = (\<Sum>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) ab_semigroup_mult
proof
fix a b :: "'a fps"
show "a * b = b * a"
proof (rule fps_ext)
fix n :: nat
have "(\<Sum>i=0..n. a$i * b$(n - i)) = (\<Sum>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
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 :: (semiring_1) monoid_mult
proof
fix a :: "'a fps"
show "1 * a = a"
by (simp add: fps_ext fps_mult_nth mult_delta_left sum.delta)
show "a * 1 = a"
by (simp add: fps_ext fps_mult_nth mult_delta_right sum.delta')
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)
instance fps :: (semiring_0) semiring
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)
qed
instance fps :: (semiring_0) semiring_0
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
instance fps :: (semiring_0_cancel) semiring_0_cancel ..
instance fps :: (semiring_1) semiring_1 ..
subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)"
by (simp add: expand_fps_eq)
lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m < n. f $ m = 0))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
let ?n = "LEAST n. f $ n \<noteq> 0"
show ?rhs if ?lhs
proof -
from that have "\<exists>n. f $ n \<noteq> 0"
by (simp add: fps_nonzero_nth)
then have "f $ ?n \<noteq> 0"
by (rule LeastI_ex)
moreover have "\<forall>m<?n. f $ m = 0"
by (auto dest: not_less_Least)
ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" ..
then show ?thesis ..
qed
show ?lhs if ?rhs
using that by (auto simp add: expand_fps_eq)
qed
lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $ n = g $n)"
by (rule expand_fps_eq)
lemma fps_sum_nth: "sum f S $ n = sum (\<lambda>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 (\<lambda>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_1_eq_1 [simp]: "fps_const 1 = 1"
by (simp add: fps_ext)
lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = 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_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
by (simp add: fps_ext)
lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)"
by (simp add: fps_eq_iff fps_mult_nth sum.neutral)
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_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
unfolding fps_eq_iff fps_mult_nth
by (simp add: fps_const_def mult_delta_left sum.delta)
lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
unfolding fps_eq_iff fps_mult_nth
by (simp add: fps_const_def mult_delta_right sum.delta')
lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n"
by (simp add: fps_mult_nth mult_delta_left sum.delta)
lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c"
by (simp add: fps_mult_nth mult_delta_right sum.delta')
subsection \<open>Formal power series form an integral domain\<close>
instance fps :: (ring) ring ..
instance fps :: (ring_1) ring_1
by (intro_classes, auto simp add: distrib_right)
instance fps :: (comm_ring_1) comm_ring_1
by (intro_classes, auto simp add: distrib_right)
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
proof
fix a b :: "'a fps"
assume "a \<noteq> 0" and "b \<noteq> 0"
then obtain i j where i: "a $ i \<noteq> 0" "\<forall>k<i. a $ k = 0" and j: "b $ j \<noteq> 0" "\<forall>k<j. b $ k =0"
unfolding fps_nonzero_nth_minimal
by blast+
have "(a * b) $ (i + j) = (\<Sum>k=0..i+j. a $ k * b $ (i + j - k))"
by (rule fps_mult_nth)
also have "\<dots> = (a $ i * b $ (i + j - i)) + (\<Sum>k\<in>{0..i+j} - {i}. a $ k * b $ (i + j - k))"
by (rule sum.remove) simp_all
also have "(\<Sum>k\<in>{0..i+j}-{i}. a $ k * b $ (i + j - k)) = 0"
proof (rule sum.neutral [rule_format])
fix k assume "k \<in> {0..i+j} - {i}"
then have "k < i \<or> i+j-k < j"
by auto
then show "a $ k * b $ (i + j - k) = 0"
using i j by auto
qed
also have "a $ i * b $ (i + j - i) + 0 = a $ i * b $ j"
by simp
also have "a $ i * b $ j \<noteq> 0"
using i j by simp
finally have "(a*b) $ (i+j) \<noteq> 0" .
then show "a * b \<noteq> 0"
unfolding fps_nonzero_nth by blast
qed
instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance fps :: (idom) idom ..
lemma 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])
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 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 numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \<noteq> 0"
proof
assume "numeral f = (0 :: 'a fps)"
from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
qed
subsection \<open>The efps_Xtractor series fps_X\<close>
lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
by (induct n) auto
definition "fps_X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
lemma fps_X_mult_nth [simp]:
"(fps_X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
proof (cases "n = 0")
case False
have "(fps_X * f) $n = (\<Sum>i = 0..n. fps_X $ i * f $ (n - i))"
by (simp add: fps_mult_nth)
also have "\<dots> = f $ (n - 1)"
using False by (simp add: fps_X_def mult_delta_left sum.delta)
finally show ?thesis
using False by simp
next
case True
then show ?thesis
by (simp add: fps_mult_nth fps_X_def)
qed
lemma fps_X_mult_right_nth[simp]:
"((a::'a::semiring_1 fps) * fps_X) $ n = (if n = 0 then 0 else a $ (n - 1))"
proof -
have "(a * fps_X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))"
by (simp add: fps_times_def fps_X_def)
also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)"
by (intro sum.cong) auto
also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: sum.delta)
finally show ?thesis .
qed
lemma fps_mult_fps_X_commute: "fps_X * (a :: 'a :: semiring_1 fps) = a * fps_X"
by (simp add: fps_eq_iff)
lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (\<lambda>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::'a::comm_ring_1)"
by (simp add: fps_X_power_iff)
lemma fps_X_power_mult_nth: "(fps_X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
apply (induct k arbitrary: n)
apply simp
unfolding power_Suc mult.assoc
apply (case_tac n)
apply auto
done
lemma fps_X_power_mult_right_nth:
"((f :: 'a::comm_ring_1 fps) * fps_X^k) $n = (if n < k then 0 else f $ (n - k))"
by (metis fps_X_power_mult_nth mult.commute)
lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 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) \<noteq> 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) \<noteq> 1"
by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp
lemma fps_X_neq_numeral [simp]: "(fps_X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> 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 :: ('a :: {comm_ring_1}) fps) ^ m = fps_X ^ n \<longleftrightarrow> 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>Subdegrees\<close>
definition subdegree :: "('a::zero) fps \<Rightarrow> nat" where
"subdegree f = (if f = 0 then 0 else LEAST n. f$n \<noteq> 0)"
lemma subdegreeI:
assumes "f $ d \<noteq> 0" and "\<And>i. i < d \<Longrightarrow> f $ i = 0"
shows "subdegree f = d"
proof-
from assms(1) have "f \<noteq> 0" by auto
moreover from assms(1) have "(LEAST i. f $ i \<noteq> 0) = d"
proof (rule Least_equality)
fix e assume "f $ e \<noteq> 0"
with assms(2) have "\<not>(e < d)" by blast
thus "e \<ge> d" by simp
qed
ultimately show ?thesis unfolding subdegree_def by simp
qed
lemma nth_subdegree_nonzero [simp,intro]: "f \<noteq> 0 \<Longrightarrow> f $ subdegree f \<noteq> 0"
proof-
assume "f \<noteq> 0"
hence "subdegree f = (LEAST n. f $ n \<noteq> 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 \<noteq> 0) \<noteq> 0" .
finally show ?thesis .
qed
lemma nth_less_subdegree_zero [dest]: "n < subdegree f \<Longrightarrow> f $ n = 0"
proof (cases "f = 0")
assume "f \<noteq> 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 \<noteq> 0" "\<And>i. i < n \<Longrightarrow> f$i = 0"
shows "subdegree f \<ge> n"
proof (rule ccontr)
assume "\<not>(subdegree f \<ge> n)"
with assms(2) have "f $ subdegree f = 0" by simp
moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp
ultimately show False by contradiction
qed
lemma subdegree_greaterI:
assumes "f \<noteq> 0" "\<And>i. i \<le> n \<Longrightarrow> f$i = 0"
shows "subdegree f > n"
proof (rule ccontr)
assume "\<not>(subdegree f > n)"
with assms(2) have "f $ subdegree f = 0" by simp
moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp
ultimately show False by contradiction
qed
lemma subdegree_leI:
"f $ n \<noteq> 0 \<Longrightarrow> subdegree f \<le> n"
by (rule leI) auto
lemma subdegree_0 [simp]: "subdegree 0 = 0"
by (simp add: subdegree_def)
lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0"
by (auto intro!: subdegreeI)
lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1"
by (auto intro!: subdegreeI simp: fps_X_def)
lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
by (cases "c = 0") (auto intro!: subdegreeI)
lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0"
by (simp add: numeral_fps_const)
lemma subdegree_eq_0_iff: "subdegree f = 0 \<longleftrightarrow> f = 0 \<or> f $ 0 \<noteq> 0"
proof (cases "f = 0")
assume "f \<noteq> 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 \<noteq> 0 \<Longrightarrow> subdegree f = 0"
by (simp add: subdegree_eq_0_iff)
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 = (\<Sum>i=0..?n. f$i * g$(?n-i))"
by (simp add: fps_mult_nth)
also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?n-i) else 0)"
proof (intro sum.cong)
fix x assume x: "x \<in> {0..?n}"
hence "x = subdegree f \<or> x < subdegree f \<or> ?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 add: sum.delta)
finally show ?thesis .
qed
lemma subdegree_mult [simp]:
assumes "f \<noteq> 0" "g \<noteq> 0"
shows "subdegree ((f :: ('a :: {ring_no_zero_divisors}) fps) * g) = subdegree f + subdegree g"
proof (rule subdegreeI)
let ?n = "subdegree f + subdegree g"
have "(f * g) $ ?n = (\<Sum>i=0..?n. f$i * g$(?n-i))" by (simp add: fps_mult_nth)
also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?n-i) else 0)"
proof (intro sum.cong)
fix x assume x: "x \<in> {0..?n}"
hence "x = subdegree f \<or> x < subdegree f \<or> ?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 add: sum.delta)
also from assms have "... \<noteq> 0" by auto
finally show "(f * g) $ (subdegree f + subdegree g) \<noteq> 0" .
next
fix m assume m: "m < subdegree f + subdegree g"
have "(f * g) $ m = (\<Sum>i=0..m. f$i * g$(m-i))" by (simp add: fps_mult_nth)
also have "... = (\<Sum>i=0..m. 0)"
proof (rule sum.cong)
fix i assume "i \<in> {0..m}"
with m have "i < subdegree f \<or> m - i < subdegree g" by auto
thus "f$i * g$(m-i) = 0" by (elim disjE) auto
qed auto
finally show "(f * g) $ m = 0" by simp
qed
lemma subdegree_power [simp]:
"subdegree ((f :: ('a :: ring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
by (cases "f = 0"; induction n) simp_all
lemma subdegree_uminus [simp]:
"subdegree (-(f::('a::group_add) fps)) = subdegree f"
by (simp add: subdegree_def)
lemma subdegree_minus_commute [simp]:
"subdegree (f-(g::('a::group_add) fps)) = subdegree (g - f)"
proof -
have "f - g = -(g - f)" by simp
also have "subdegree ... = subdegree (g - f)" by (simp only: subdegree_uminus)
finally show ?thesis .
qed
lemma subdegree_add_ge:
assumes "f \<noteq> -(g :: ('a :: {group_add}) fps)"
shows "subdegree (f + g) \<ge> min (subdegree f) (subdegree g)"
proof (rule subdegree_geI)
from assms show "f + g \<noteq> 0" by (subst (asm) eq_neg_iff_add_eq_0)
next
fix i assume "i < min (subdegree f) (subdegree g)"
hence "f $ i = 0" and "g $ i = 0" by auto
thus "(f + g) $ i = 0" by force
qed
lemma subdegree_add_eq1:
assumes "f \<noteq> 0"
assumes "subdegree f < subdegree (g :: ('a :: {group_add}) fps)"
shows "subdegree (f + g) = subdegree f"
proof (rule antisym[OF subdegree_leI])
from assms show "subdegree (f + g) \<ge> subdegree f"
by (intro order.trans[OF min.boundedI subdegree_add_ge]) auto
from assms have "f $ subdegree f \<noteq> 0" "g $ subdegree f = 0" by auto
thus "(f + g) $ subdegree f \<noteq> 0" by simp
qed
lemma subdegree_add_eq2:
assumes "g \<noteq> 0"
assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)"
shows "subdegree (f + g) = subdegree g"
using subdegree_add_eq1[OF assms] by (simp add: add.commute)
lemma subdegree_diff_eq1:
assumes "f \<noteq> 0"
assumes "subdegree f < subdegree (g :: ('a :: {ab_group_add}) fps)"
shows "subdegree (f - g) = subdegree f"
using subdegree_add_eq1[of f "-g"] assms by (simp add: add.commute)
lemma subdegree_diff_eq2:
assumes "g \<noteq> 0"
assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)"
shows "subdegree (f - g) = subdegree g"
using subdegree_add_eq2[of "-g" f] assms by (simp add: add.commute)
lemma subdegree_diff_ge [simp]:
assumes "f \<noteq> (g :: ('a :: {group_add}) fps)"
shows "subdegree (f - g) \<ge> min (subdegree f) (subdegree g)"
using assms subdegree_add_ge[of f "-g"] by simp
subsection \<open>Shifting and slicing\<close>
definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
"fps_shift n f = Abs_fps (\<lambda>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_power [simp]:
"n \<le> m \<Longrightarrow> fps_shift n (fps_X ^ m) = (fps_X ^ (m - n) ::'a::comm_ring_1 fps)"
by (intro fps_ext) (auto simp: fps_shift_def )
lemma fps_shift_times_fps_X_power:
"n \<le> subdegree f \<Longrightarrow> fps_shift n f * fps_X ^ n = (f :: 'a :: comm_ring_1 fps)"
by (intro fps_ext) (auto simp: 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 :: 'a :: comm_ring_1 fps)"
by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
lemma fps_shift_times_fps_X_power'':
"m \<le> n \<Longrightarrow> fps_shift n (f * fps_X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)"
by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero)
lemma fps_shift_subdegree [simp]:
"n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n"
by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+
lemma subdegree_decompose:
"f = fps_shift (subdegree f) f * fps_X ^ subdegree (f :: ('a :: comm_ring_1) fps)"
by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth)
lemma subdegree_decompose':
"n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> 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)
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_add:
"fps_shift n (f + g) = fps_shift n f + fps_shift n g"
by (simp add: fps_eq_iff)
lemma fps_shift_mult:
assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
shows "fps_shift n (h*g) = h * fps_shift n g"
proof -
from assms have "g = fps_shift n g * fps_X^n" by (rule subdegree_decompose')
also have "h * ... = (h * fps_shift n g) * fps_X^n" by simp
also have "fps_shift n ... = h * fps_shift n g" by simp
finally show ?thesis .
qed
lemma fps_shift_mult_right:
assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)"
shows "fps_shift n (g*h) = h * fps_shift n g"
by (subst mult.commute, subst fps_shift_mult) (simp_all add: assms)
lemma nth_subdegree_zero_iff [simp]: "f $ subdegree f = 0 \<longleftrightarrow> f = 0"
by (cases "f = 0") auto
lemma fps_shift_subdegree_zero_iff [simp]:
"fps_shift (subdegree f) f = 0 \<longleftrightarrow> f = 0"
by (subst (1) nth_subdegree_zero_iff[symmetric], cases "f = 0")
(simp_all del: nth_subdegree_zero_iff)
definition "fps_cutoff n f = Abs_fps (\<lambda>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 \<longleftrightarrow> (f = 0 \<or> n \<le> subdegree f)"
proof
assume A: "fps_cutoff n f = 0"
thus "f = 0 \<or> n \<le> subdegree f"
proof (cases "f = 0")
assume "f \<noteq> 0"
with A have "n \<le> subdegree f"
by (intro subdegree_geI) (auto simp: 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 :: ('a :: comm_ring_1) fps) * fps_X^n + fps_cutoff n f = f"
by (simp add: fps_eq_iff fps_X_power_mult_right_nth)
subsection \<open>Formal Power series form a metric space\<close>
instantiation fps :: (comm_ring_1) 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 \<ge> 0"
by (simp add: dist_fps_def)
lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a"
by (simp add: dist_fps_def)
instance ..
end
instantiation fps :: (comm_ring_1) metric_space
begin
definition uniformity_fps_def [code del]:
"(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
definition open_fps_def' [code del]:
"open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
instance
proof
show th: "dist a b = 0 \<longleftrightarrow> 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 \<or> c = b" | "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast
then show "dist a b \<le> 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 \<noteq> 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 :: comm_ring_1 fps", code]
lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> 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 "\<exists>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 (\<lambda>i. fps_const(a$i)*fps_X^i) {0..m})$n =
(if n \<le> m then a$n else 0::'a::comm_ring_1)"
by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * fps_X^i) {0..n}) \<longlonglongrightarrow> a"
(is "?s \<longlonglongrightarrow> a")
proof -
have "\<exists>n0. \<forall>n \<ge> 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 \<ge> n0" for n
proof -
from that have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
by (simp add: divide_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 "\<dots> \<le> (1/2)^n0"
using nn0 by (simp add: divide_simps)
also have "\<dots> < 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 of formal power series\<close>
declare sum.cong[fundef_cong]
instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse
begin
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a"
where
"natfun_inverse f 0 = inverse (f$0)"
| "natfun_inverse f n = - inverse (f$0) * sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}"
definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))"
definition fps_divide_def:
"f div g = (if g = 0 then 0 else
let n = subdegree g; h = fps_shift n g
in fps_shift n (f * inverse h))"
instance ..
end
lemma fps_inverse_zero [simp]:
"inverse (0 :: 'a::{comm_monoid_add,inverse,times,uminus} fps) = 0"
by (simp add: fps_ext fps_inverse_def)
lemma fps_inverse_one [simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1"
apply (auto simp add: expand_fps_eq fps_inverse_def)
apply (case_tac n)
apply auto
done
lemma inverse_mult_eq_1 [intro]:
assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "inverse f * f = 1"
proof -
have c: "inverse f * f = f * inverse f"
by (simp add: mult.commute)
from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n"
by (simp add: fps_inverse_def)
from f0 have th0: "(inverse f * f) $ 0 = 1"
by (simp add: fps_mult_nth fps_inverse_def)
have "(inverse f * f)$n = 0" if np: "n > 0" for n
proof -
from np have eq: "{0..n} = {0} \<union> {1 .. n}"
by auto
have d: "{0} \<inter> {1 .. n} = {}"
by auto
from f0 np have th0: "- (inverse f $ n) =
(sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}) / (f$0)"
by (cases n) (simp_all add: divide_inverse fps_inverse_def)
from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]]
have th1: "sum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n} = - (f$0) * (inverse f)$n"
by (simp add: field_simps)
have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n - i))"
unfolding fps_mult_nth ifn ..
also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))"
by (simp add: eq)
also have "\<dots> = 0"
unfolding th1 ifn by simp
finally show ?thesis unfolding c .
qed
with th0 show ?thesis
by (simp add: fps_eq_iff)
qed
lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \<longleftrightarrow> f $ 0 = 0"
by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero)
lemma fps_inverse_nth_0 [simp]: "inverse f $ 0 = inverse (f $ 0 :: 'a :: division_ring)"
by (simp add: fps_inverse_def)
lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::division_ring) fps) \<longleftrightarrow> f $ 0 = 0"
proof
assume A: "inverse f = 0"
have "0 = inverse f $ 0" by (subst A) simp
thus "f $ 0 = 0" by simp
qed (simp add: fps_inverse_def)
lemma fps_inverse_idempotent[intro, simp]:
assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "inverse (inverse f) = f"
proof -
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
have "inverse f * f = inverse f * inverse (inverse f)"
by (simp add: ac_simps)
then show ?thesis
using f0 unfolding mult_cancel_left by simp
qed
lemma fps_inverse_unique:
assumes fg: "(f :: 'a :: field fps) * g = 1"
shows "inverse f = g"
proof -
have f0: "f $ 0 \<noteq> 0"
proof
assume "f $ 0 = 0"
hence "0 = (f * g) $ 0" by simp
also from fg have "(f * g) $ 0 = 1" by simp
finally show False by simp
qed
from inverse_mult_eq_1[OF this] fg
have th0: "inverse f * f = g * f"
by (simp add: ac_simps)
then show ?thesis
using f0
unfolding mult_cancel_right
by (auto simp add: expand_fps_eq)
qed
lemma fps_inverse_eq_0: "f$0 = 0 \<Longrightarrow> inverse (f :: 'a :: division_ring fps) = 0"
by simp
lemma sum_zero_lemma:
fixes n::nat
assumes "0 < n"
shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
proof -
let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
have th1: "sum ?f {0..n} = sum ?g {0..n}"
by (rule sum.cong) auto
have th2: "sum ?g {0..n - 1} = sum ?h {0..n - 1}"
apply (rule sum.cong)
using assms
apply auto
done
have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
by auto
from assms have d: "{0.. n - 1} \<inter> {n} = {}"
by auto
have f: "finite {0.. n - 1}" "finite {n}"
by auto
show ?thesis
unfolding th1
apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
unfolding th2
apply (simp add: sum.delta)
done
qed
lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g"
proof (cases "f$0 = 0 \<or> g$0 = 0")
assume "\<not>(f$0 = 0 \<or> g$0 = 0)"
hence [simp]: "f$0 \<noteq> 0" "g$0 \<noteq> 0" by simp_all
show ?thesis
proof (rule fps_inverse_unique)
have "f * g * (inverse f * inverse g) = (inverse f * f) * (inverse g * g)" by simp
also have "... = 1" by (subst (1 2) inverse_mult_eq_1) simp_all
finally show "f * g * (inverse f * inverse g) = 1" .
qed
next
assume A: "f$0 = 0 \<or> g$0 = 0"
hence "inverse (f * g) = 0" by simp
also from A have "... = inverse f * inverse g" by auto
finally show "inverse (f * g) = inverse f * inverse g" .
qed
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) =
Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then - 1 else 0)"
apply (rule fps_inverse_unique)
apply (simp_all add: fps_eq_iff fps_mult_nth sum_zero_lemma)
done
lemma subdegree_inverse [simp]: "subdegree (inverse (f::'a::field fps)) = 0"
proof (cases "f$0 = 0")
assume nz: "f$0 \<noteq> 0"
hence "subdegree (inverse f) + subdegree f = subdegree (inverse f * f)"
by (subst subdegree_mult) auto
also from nz have "subdegree f = 0" by (simp add: subdegree_eq_0_iff)
also from nz have "inverse f * f = 1" by (rule inverse_mult_eq_1)
finally show "subdegree (inverse f) = 0" by simp
qed (simp_all add: fps_inverse_def)
lemma fps_is_unit_iff [simp]: "(f :: 'a :: field fps) dvd 1 \<longleftrightarrow> f $ 0 \<noteq> 0"
proof
assume "f dvd 1"
then obtain g where "1 = f * g" by (elim dvdE)
from this[symmetric] have "(f*g) $ 0 = 1" by simp
thus "f $ 0 \<noteq> 0" by auto
next
assume A: "f $ 0 \<noteq> 0"
thus "f dvd 1" by (simp add: inverse_mult_eq_1[OF A, symmetric])
qed
lemma subdegree_eq_0' [simp]: "(f :: 'a :: field fps) dvd 1 \<Longrightarrow> subdegree f = 0"
by simp
lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g"
by (rule dvd_trans, subst fps_is_unit_iff) simp_all
instantiation fps :: (field) normalization_semidom
begin
definition fps_unit_factor_def [simp]:
"unit_factor f = fps_shift (subdegree f) f"
definition fps_normalize_def [simp]:
"normalize f = (if f = 0 then 0 else fps_X ^ subdegree f)"
instance proof
fix f :: "'a fps"
show "unit_factor f * normalize f = f"
by (simp add: fps_shift_times_fps_X_power)
next
fix f g :: "'a fps"
show "unit_factor (f * g) = unit_factor f * unit_factor g"
proof (cases "f = 0 \<or> g = 0")
assume "\<not>(f = 0 \<or> g = 0)"
thus "unit_factor (f * g) = unit_factor f * unit_factor g"
unfolding fps_unit_factor_def
by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
qed auto
next
fix f g :: "'a fps"
assume "g \<noteq> 0"
then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f"
by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero)
then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f"
by (simp add: fps_shift_mult_right mult.commute)
with \<open>g \<noteq> 0\<close> show "f * g / g = f"
by (simp add: fps_divide_def Let_def ac_simps)
qed (auto simp add: fps_divide_def Let_def)
end
instantiation fps :: (field) idom_modulo
begin
definition fps_mod_def:
"f mod g = (if g = 0 then f else
let n = subdegree g; h = fps_shift n g
in fps_cutoff n (f * inverse h) * h)"
lemma fps_mod_eq_zero:
assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree g"
shows "f mod g = 0"
using assms by (cases "f = 0") (auto simp: fps_cutoff_zero_iff fps_mod_def Let_def)
lemma fps_times_divide_eq:
assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree (g :: 'a fps)"
shows "f div g * g = f"
proof (cases "f = 0")
assume nz: "f \<noteq> 0"
define n where "n = subdegree g"
define h where "h = fps_shift n g"
from assms have [simp]: "h $ 0 \<noteq> 0" unfolding h_def by (simp add: n_def)
from assms nz have "f div g * g = fps_shift n (f * inverse h) * g"
by (simp add: fps_divide_def Let_def h_def n_def)
also have "... = fps_shift n (f * inverse h) * fps_X^n * h" unfolding h_def n_def
by (subst subdegree_decompose[of g]) simp
also have "fps_shift n (f * inverse h) * fps_X^n = f * inverse h"
by (rule fps_shift_times_fps_X_power) (simp_all add: nz assms n_def)
also have "... * h = f * (inverse h * h)" by simp
also have "inverse h * h = 1" by (rule inverse_mult_eq_1) simp
finally show ?thesis by simp
qed (simp_all add: fps_divide_def Let_def)
lemma
assumes "g$0 \<noteq> 0"
shows fps_divide_unit: "f div g = f * inverse g" and fps_mod_unit [simp]: "f mod g = 0"
proof -
from assms have [simp]: "subdegree g = 0" by (simp add: subdegree_eq_0_iff)
from assms show "f div g = f * inverse g"
by (auto simp: fps_divide_def Let_def subdegree_eq_0_iff)
from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto
qed
instance proof
fix f g :: "'a fps"
define n where "n = subdegree g"
define h where "h = fps_shift n g"
show "f div g * g + f mod g = f"
proof (cases "g = 0 \<or> f = 0")
assume "\<not>(g = 0 \<or> f = 0)"
hence nz [simp]: "f \<noteq> 0" "g \<noteq> 0" by simp_all
show ?thesis
proof (rule disjE[OF le_less_linear])
assume "subdegree f \<ge> subdegree g"
with nz show ?thesis by (simp add: fps_mod_eq_zero fps_times_divide_eq)
next
assume "subdegree f < subdegree g"
have g_decomp: "g = h * fps_X^n" unfolding h_def n_def by (rule subdegree_decompose)
have "f div g * g + f mod g =
fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h"
by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def)
also have "... = h * (fps_shift n (f * inverse h) * fps_X^n + fps_cutoff n (f * inverse h))"
by (subst g_decomp) (simp add: algebra_simps)
also have "... = f * (inverse h * h)"
by (subst fps_shift_cutoff) simp
also have "inverse h * h = 1" by (rule inverse_mult_eq_1) (simp add: h_def n_def)
finally show ?thesis by simp
qed
qed (auto simp: fps_mod_def fps_divide_def Let_def)
qed
end
lemma subdegree_mod:
assumes "f \<noteq> 0" "subdegree f < subdegree g"
shows "subdegree (f mod g) = subdegree f"
proof (cases "f div g * g = 0")
assume "f div g * g \<noteq> 0"
hence [simp]: "f div g \<noteq> 0" "g \<noteq> 0" by auto
from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
also from assms have "subdegree ... = subdegree f"
by (intro subdegree_diff_eq1) simp_all
finally show ?thesis .
next
assume zero: "f div g * g = 0"
from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps)
also note zero
finally show ?thesis by simp
qed
lemma fps_divide_nth_0 [simp]: "g $ 0 \<noteq> 0 \<Longrightarrow> (f div g) $ 0 = f $ 0 / (g $ 0 :: _ :: field)"
by (simp add: fps_divide_unit divide_inverse)
lemma dvd_imp_subdegree_le:
"(f :: 'a :: idom fps) dvd g \<Longrightarrow> g \<noteq> 0 \<Longrightarrow> subdegree f \<le> subdegree g"
by (auto elim: dvdE)
lemma fps_dvd_iff:
assumes "(f :: 'a :: field fps) \<noteq> 0" "g \<noteq> 0"
shows "f dvd g \<longleftrightarrow> subdegree f \<le> subdegree g"
proof
assume "subdegree f \<le> subdegree g"
with assms have "g mod f = 0"
by (simp add: fps_mod_def Let_def fps_cutoff_zero_iff)
thus "f dvd g" by (simp add: dvd_eq_mod_eq_0)
qed (simp add: assms dvd_imp_subdegree_le)
lemma fps_shift_altdef:
"fps_shift n f = (f :: 'a :: field fps) div fps_X^n"
by (simp add: fps_divide_def)
lemma fps_div_fps_X_power_nth: "((f :: 'a :: field fps) div fps_X^n) $ k = f $ (k + n)"
by (simp add: fps_shift_altdef [symmetric])
lemma fps_div_fps_X_nth: "((f :: 'a :: field fps) div fps_X) $ k = f $ Suc k"
using fps_div_fps_X_power_nth[of f 1] by simp
lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff)
lemma fps_const_divide: "fps_const (x :: _ :: field) / fps_const y = fps_const (x / y)"
by (cases "y = 0") (simp_all add: fps_divide_unit fps_const_inverse divide_inverse)
lemma inverse_fps_numeral:
"inverse (numeral n :: ('a :: field_char_0) fps) = fps_const (inverse (numeral n))"
by (intro fps_inverse_unique fps_ext) (simp_all add: fps_numeral_nth)
lemma fps_numeral_divide_divide:
"x / numeral b / numeral c = (x / numeral (b * c) :: 'a :: field fps)"
by (cases "numeral b = (0::'a)"; cases "numeral c = (0::'a)")
(simp_all add: fps_divide_unit fps_inverse_mult [symmetric] numeral_fps_const numeral_mult
del: numeral_mult [symmetric])
lemma fps_numeral_mult_divide:
"numeral b * x / numeral c = (numeral b / numeral c * x :: 'a :: field fps)"
by (cases "numeral c = (0::'a)") (simp_all add: fps_divide_unit numeral_fps_const)
lemmas fps_numeral_simps =
fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
lemma subdegree_div:
assumes "q dvd p"
shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q"
proof (cases "p = 0")
case False
from assms have "p = p div q * q" by simp
also from assms False have "subdegree \<dots> = subdegree (p div q) + subdegree q"
by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff)
finally show ?thesis by simp
qed simp_all
lemma subdegree_div_unit:
assumes "q $ 0 \<noteq> 0"
shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p"
using assms by (subst subdegree_div) simp_all
subsection \<open>Formal power series form a Euclidean ring\<close>
instantiation fps :: (field) euclidean_ring_cancel
begin
definition fps_euclidean_size_def:
"euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
context
begin
private lemma fps_divide_cancel_aux1:
assumes "h$0 \<noteq> (0 :: 'a :: field)"
shows "(h * f) div (h * g) = f div g"
proof (cases "g = 0")
assume "g \<noteq> 0"
from assms have "h \<noteq> 0" by auto
note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
have "(h * f) div (h * g) =
fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
by (simp add: fps_divide_def Let_def)
also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
(inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
qed (simp_all add: fps_divide_def)
private lemma fps_divide_cancel_aux2:
"(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
proof (cases "g = 0")
assume [simp]: "g \<noteq> 0"
have "(f * fps_X^m) div (g * fps_X^m) =
fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
by (simp add: fps_divide_def Let_def algebra_simps)
also have "... = f div g"
by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
finally show ?thesis .
qed (simp_all add: fps_divide_def)
instance proof
fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
show "euclidean_size f \<le> euclidean_size (f * g)"
by (cases "f = 0") (auto simp: fps_euclidean_size_def)
show "euclidean_size (f mod g) < euclidean_size g"
apply (cases "f = 0", simp add: fps_euclidean_size_def)
apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
done
show "(h * f) div (h * g) = f div g" if "h \<noteq> 0"
for f g h :: "'a fps"
proof -
define m where "m = subdegree h"
define h' where "h' = fps_shift m h"
have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
by (simp add: h_decomp algebra_simps)
also have "... = f div g"
by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
finally show ?thesis .
qed
show "(f + g * h) div h = g + f div h"
if "h \<noteq> 0" for f g h :: "'a fps"
proof -
define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
by (simp add: fps_divide_def Let_def dfs [symmetric] algebra_simps fps_shift_add that)
also have "h * inverse h' = (inverse h' * h') * fps_X^n"
by (subst subdegree_decompose) (simp_all add: dfs)
also have "... = fps_X^n"
by (subst inverse_mult_eq_1) (simp_all add: dfs that)
also have "fps_shift n (g * fps_X^n) = g" by simp
also have "fps_shift n (f * inverse h') = f div h"
by (simp add: fps_divide_def Let_def dfs)
finally show ?thesis by simp
qed
qed (simp_all add: fps_euclidean_size_def)
end
end
instance fps :: (field) normalization_euclidean_semiring ..
instantiation fps :: (field) euclidean_ring_gcd
begin
definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
definition fps_lcm_def: "(lcm :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.lcm"
definition fps_Gcd_def: "(Gcd :: 'a fps set \<Rightarrow> _) = Euclidean_Algorithm.Gcd"
definition fps_Lcm_def: "(Lcm :: 'a fps set \<Rightarrow> _) = Euclidean_Algorithm.Lcm"
instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
end
lemma fps_gcd:
assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
shows "gcd f g = fps_X ^ min (subdegree f) (subdegree g)"
proof -
let ?m = "min (subdegree f) (subdegree g)"
show "gcd f g = fps_X ^ ?m"
proof (rule sym, rule gcdI)
fix d assume "d dvd f" "d dvd g"
thus "d dvd fps_X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff)
qed (simp_all add: fps_dvd_iff)
qed
lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g =
(if f = 0 \<and> g = 0 then 0 else
if f = 0 then fps_X ^ subdegree g else
if g = 0 then fps_X ^ subdegree f else
fps_X ^ min (subdegree f) (subdegree g))"
by (simp add: fps_gcd)
lemma fps_lcm:
assumes [simp]: "f \<noteq> 0" "g \<noteq> 0"
shows "lcm f g = fps_X ^ max (subdegree f) (subdegree g)"
proof -
let ?m = "max (subdegree f) (subdegree g)"
show "lcm f g = fps_X ^ ?m"
proof (rule sym, rule lcmI)
fix d assume "f dvd d" "g dvd d"
thus "fps_X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff)
qed (simp_all add: fps_dvd_iff)
qed
lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g =
(if f = 0 \<or> g = 0 then 0 else fps_X ^ max (subdegree f) (subdegree g))"
by (simp add: fps_lcm)
lemma fps_Gcd:
assumes "A - {0} \<noteq> {}"
shows "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)"
proof (rule sym, rule GcdI)
fix f assume "f \<in> A"
thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f"
by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower)
next
fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f"
from assms obtain f where "f \<in> A - {0}" by auto
with d[of f] have [simp]: "d \<noteq> 0" by auto
from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)"
by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric])
with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
qed simp_all
lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
(if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))"
using fps_Gcd by auto
lemma fps_Lcm:
assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)"
shows "Lcm A = fps_X ^ (SUP f:A. subdegree f)"
proof (rule sym, rule LcmI)
fix f assume "f \<in> A"
moreover from assms(3) have "bdd_above (subdegree ` A)" by auto
ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2)
by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper)
next
fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d"
from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto
show "fps_X ^ (SUP f:A. subdegree f) dvd d"
proof (cases "d = 0")
assume "d \<noteq> 0"
moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast
ultimately have "subdegree d \<ge> (SUP f:A. subdegree f)" using assms
by (intro cSUP_least) (auto simp: fps_dvd_iff)
with \<open>d \<noteq> 0\<close> show ?thesis by (simp add: fps_dvd_iff)
qed simp_all
qed simp_all
lemma fps_Lcm_altdef:
"Lcm (A :: 'a :: field fps set) =
(if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))"
proof (cases "bdd_above (subdegree`A)")
assume unbounded: "\<not>bdd_above (subdegree`A)"
have "Lcm A = 0"
proof (rule ccontr)
assume "Lcm A \<noteq> 0"
from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
unfolding bdd_above_def by (auto simp: not_le)
moreover from f and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all
ultimately show False by simp
qed
with unbounded show ?thesis by simp
qed (simp_all add: fps_Lcm Lcm_eq_0_I)
subsection \<open>Formal Derivatives, and the MacLaurin theorem around 0\<close>
definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)"
by (simp add: fps_deriv_def)
lemma fps_0th_higher_deriv:
"(fps_deriv ^^ n) f $ 0 = (fact n * f $ n :: 'a :: {comm_ring_1, semiring_char_0})"
by (induction n arbitrary: f) (simp_all del: funpow.simps add: funpow_Suc_right algebra_simps)
lemma fps_deriv_linear[simp]:
"fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
fps_const a * fps_deriv f + fps_const b * fps_deriv g"
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
lemma fps_deriv_mult[simp]:
fixes f :: "'a::comm_ring_1 fps"
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g"
proof -
let ?D = "fps_deriv"
have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" for n
proof -
let ?Zn = "{0 ..n}"
let ?Zn1 = "{0 .. n + 1}"
let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n - i) +
of_nat (i+1)* f $ (i+1) * g $ (n - i)"
let ?h = "\<lambda>i. of_nat i * g $ i * f $ ((n+1) - i) +
of_nat i* f $ i * g $ ((n + 1) - i)"
have s0: "sum (\<lambda>i. of_nat i * f $ i * g $ (n + 1 - i)) ?Zn1 =
sum (\<lambda>i. of_nat (n + 1 - i) * f $ (n + 1 - i) * g $ i) ?Zn1"
by (rule sum.reindex_bij_witness[where i="(-) (n + 1)" and j="(-) (n + 1)"]) auto
have s1: "sum (\<lambda>i. f $ i * g $ (n + 1 - i)) ?Zn1 =
sum (\<lambda>i. f $ (n + 1 - i) * g $ i) ?Zn1"
by (rule sum.reindex_bij_witness[where i="(-) (n + 1)" and j="(-) (n + 1)"]) auto
have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n"
by (simp only: mult.commute)
also have "\<dots> = (\<Sum>i = 0..n. ?g i)"
by (simp add: fps_mult_nth sum.distrib[symmetric])
also have "\<dots> = sum ?h {0..n+1}"
by (rule sum.reindex_bij_witness_not_neutral
[where S'="{}" and T'="{0}" and j="Suc" and i="\<lambda>i. i - 1"]) auto
also have "\<dots> = (fps_deriv (f * g)) $ n"
apply (simp only: fps_deriv_nth fps_mult_nth sum.distrib)
unfolding s0 s1
unfolding sum.distrib[symmetric] sum_distrib_left
apply (rule sum.cong)
apply (auto simp add: of_nat_diff field_simps)
done
finally show ?thesis .
qed
then show ?thesis
unfolding fps_eq_iff by auto
qed
lemma fps_deriv_fps_X[simp]: "fps_deriv fps_X = 1"
by (simp add: fps_deriv_def fps_X_def fps_eq_iff)
lemma fps_deriv_neg[simp]:
"fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)"
by (simp add: fps_eq_iff fps_deriv_def)
lemma fps_deriv_add[simp]:
"fps_deriv ((f:: 'a::comm_ring_1 fps) + g) = fps_deriv f + fps_deriv g"
using fps_deriv_linear[of 1 f 1 g] by simp
lemma fps_deriv_sub[simp]:
"fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g"
using fps_deriv_add [of f "- g"] by simp
lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
by (simp add: fps_ext fps_deriv_def fps_const_def)
lemma fps_deriv_of_nat [simp]: "fps_deriv (of_nat n) = 0"
by (simp add: fps_of_nat [symmetric])
lemma fps_deriv_numeral [simp]: "fps_deriv (numeral n) = 0"
by (simp add: numeral_fps_const)
lemma fps_deriv_mult_const_left[simp]:
"fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
by simp
lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
by (simp add: fps_deriv_def fps_eq_iff)
lemma fps_deriv_1[simp]: "fps_deriv 1 = 0"
by (simp add: fps_deriv_def fps_eq_iff )
lemma fps_deriv_mult_const_right[simp]:
"fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
by simp
lemma fps_deriv_sum:
"fps_deriv (sum f S) = sum (\<lambda>i. fps_deriv (f i :: 'a::comm_ring_1 fps)) S"
proof (cases "finite S")
case False
then show ?thesis by simp
next
case True
show ?thesis by (induct rule: finite_induct [OF True]) simp_all
qed
lemma fps_deriv_eq_0_iff [simp]:
"fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
show ?lhs if ?rhs
proof -
from that have "fps_deriv f = fps_deriv (fps_const (f$0))"
by simp
then show ?thesis
by simp
qed
show ?rhs if ?lhs
proof -
from that have "\<forall>n. (fps_deriv f)$n = 0"
by simp
then have "\<forall>n. f$(n+1) = 0"
by (simp del: of_nat_Suc of_nat_add One_nat_def)
then show ?thesis
apply (clarsimp simp add: fps_eq_iff fps_const_def)
apply (erule_tac x="n - 1" in allE)
apply simp
done
qed
qed
lemma fps_deriv_eq_iff:
fixes f :: "'a::{idom,semiring_char_0} fps"
shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)"
proof -
have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0"
by simp
also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f - g) $ 0)"
unfolding fps_deriv_eq_0_iff ..
finally show ?thesis
by (simp add: field_simps)
qed
lemma fps_deriv_eq_iff_ex:
"(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)"
by (auto simp: fps_deriv_eq_iff)
fun fps_nth_deriv :: "nat \<Rightarrow> 'a::semiring_1 fps \<Rightarrow> 'a fps"
where
"fps_nth_deriv 0 f = f"
| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"
lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)"
by (induct n arbitrary: f) auto
lemma fps_nth_deriv_linear[simp]:
"fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
lemma fps_nth_deriv_neg[simp]:
"fps_nth_deriv n (- (f :: 'a::comm_ring_1 fps)) = - (fps_nth_deriv n f)"
by (induct n arbitrary: f) simp_all
lemma fps_nth_deriv_add[simp]:
"fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
using fps_nth_deriv_linear[of n 1 f 1 g] by simp
lemma fps_nth_deriv_sub[simp]:
"fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
using fps_nth_deriv_add [of n f "- g"] by simp
lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
by (induct n) simp_all
lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)"
by (induct n) simp_all
lemma fps_nth_deriv_const[simp]:
"fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
by (cases n) simp_all
lemma fps_nth_deriv_mult_const_left[simp]:
"fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp
lemma fps_nth_deriv_mult_const_right[simp]:
"fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult.commute)
lemma fps_nth_deriv_sum:
"fps_nth_deriv n (sum f S) = sum (\<lambda>i. fps_nth_deriv n (f i :: 'a::comm_ring_1 fps)) S"
proof (cases "finite S")
case True
show ?thesis by (induct rule: finite_induct [OF True]) simp_all
next
case False
then show ?thesis by simp
qed
lemma fps_deriv_maclauren_0:
"(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) $ 0 = of_nat (fact k) * f $ k"
by (induct k arbitrary: f) (auto simp add: field_simps)
subsection \<open>Powers\<close>
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)
lemma fps_power_first_eq: "(a :: 'a::comm_ring_1 fps) $ 0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
show ?case unfolding power_Suc fps_mult_nth
using Suc.hyps[OF \<open>a$0 = 1\<close>] \<open>a$0 = 1\<close> fps_power_zeroth_eq_one[OF \<open>a$0=1\<close>]
by (simp add: field_simps)
qed
lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1"
by (induct n) (auto simp add: fps_mult_nth)
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
by (induct n) (auto simp add: fps_mult_nth)
lemma startsby_power:"a $0 = (v::'a::comm_ring_1) \<Longrightarrow> a^n $0 = v^n"
by (induct n) (auto simp add: fps_mult_nth)
lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::idom) \<longleftrightarrow> n \<noteq> 0 \<and> a$0 = 0"
apply (rule iffI)
apply (induct n)
apply (auto simp add: fps_mult_nth)
apply (rule startsby_zero_power, simp_all)
done
lemma startsby_zero_power_prefix:
assumes a0: "a $ 0 = (0::'a::idom)"
shows "\<forall>n < k. a ^ k $ n = 0"
using a0
proof (induct k rule: nat_less_induct)
fix k
assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0"
show "\<forall>m<k. a ^ k $ m = 0"
proof (cases k)
case 0
then show ?thesis by simp
next
case (Suc l)
have "a^k $ m = 0" if mk: "m < k" for m
proof (cases "m = 0")
case True
then show ?thesis
using startsby_zero_power[of a k] Suc a0 by simp
next
case False
have "a ^k $ m = (a^l * a) $m"
by (simp add: Suc mult.commute)
also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))"
by (simp add: fps_mult_nth)
also have "\<dots> = 0"
apply (rule sum.neutral)
apply auto
apply (case_tac "x = m")
using a0 apply simp
apply (rule H[rule_format])
using a0 Suc mk apply auto
done
finally show ?thesis .
qed
then show ?thesis by blast
qed
qed
lemma startsby_zero_sum_depends:
assumes a0: "a $0 = (0::'a::idom)"
and kn: "n \<ge> k"
shows "sum (\<lambda>i. (a ^ i)$k) {0 .. n} = sum (\<lambda>i. (a ^ i)$k) {0 .. k}"
apply (rule sum.mono_neutral_right)
using kn
apply auto
apply (rule startsby_zero_power_prefix[rule_format, OF a0])
apply arith
done
lemma startsby_zero_power_nth_same:
assumes a0: "a$0 = (0::'a::idom)"
shows "a^n $ n = (a$1) ^ n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)"
by (simp add: field_simps)
also have "\<dots> = sum (\<lambda>i. a^n$i * a $ (Suc n - i)) {0.. Suc n}"
by (simp add: fps_mult_nth)
also have "\<dots> = sum (\<lambda>i. a^n$i * a $ (Suc n - i)) {n .. Suc n}"
apply (rule sum.mono_neutral_right)
apply simp
apply clarsimp
apply clarsimp
apply (rule startsby_zero_power_prefix[rule_format, OF a0])
apply arith
done
also have "\<dots> = a^n $ n * a$1"
using a0 by simp
finally show ?case
using Suc.hyps by simp
qed
lemma fps_inverse_power:
fixes a :: "'a::field fps"
shows "inverse (a^n) = inverse a ^ n"
by (induction n) (simp_all add: fps_inverse_mult)
lemma fps_deriv_power:
"fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)"
apply (induct n)
apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add)
apply (case_tac n)
apply (auto simp add: field_simps)
done
lemma fps_inverse_deriv:
fixes a :: "'a::field fps"
assumes a0: "a$0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
proof -
from inverse_mult_eq_1[OF a0]
have "fps_deriv (inverse a * a) = 0" by simp
then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0"
by simp
then have "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0"
by simp
with inverse_mult_eq_1[OF a0]
have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0"
unfolding power2_eq_square
apply (simp add: field_simps)
apply (simp add: mult.assoc[symmetric])
done
then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * (inverse a)\<^sup>2 =
0 - fps_deriv a * (inverse a)\<^sup>2"
by simp
then show "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
by (simp add: field_simps)
qed
lemma fps_inverse_deriv':
fixes a :: "'a::field fps"
assumes a0: "a $ 0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
using fps_inverse_deriv[OF a0] a0
by (simp add: fps_divide_unit power2_eq_square fps_inverse_mult)
lemma inverse_mult_eq_1':
assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "f * inverse f = 1"
by (metis mult.commute inverse_mult_eq_1 f0)
lemma fps_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: field fps)"
by (cases "f$0 = 0") (auto intro: fps_inverse_unique simp: inverse_mult_eq_1' fps_inverse_eq_0)
lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f"
by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse)
(* FIfps_XME: The last part of this proof should go through by simp once we have a proper
theorem collection for simplifying division on rings *)
lemma fps_divide_deriv:
assumes "b dvd (a :: 'a :: field fps)"
shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2"
proof -
have eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b div c" for a b c :: "'a :: field fps"
by (drule sym) (simp add: mult.assoc)
from assms have "a = a / b * b" by simp
also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp
finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms
by (simp add: power2_eq_square algebra_simps)
thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp)
qed
lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - fps_X"
by (simp add: fps_inverse_gp fps_eq_iff fps_X_def)
lemma fps_one_over_one_minus_fps_X_squared:
"inverse ((1 - fps_X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))"
proof -
have "inverse ((1 - fps_X)^2 :: 'a fps) = fps_deriv (inverse (1 - fps_X))"
by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power)
also have "inverse (1 - fps_X :: 'a fps) = Abs_fps (\<lambda>_. 1)"
by (subst fps_inverse_gp' [symmetric]) simp
also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))"
by (simp add: fps_deriv_def)
finally show ?thesis .
qed
lemma fps_nth_deriv_fps_X[simp]: "fps_nth_deriv n fps_X = (if n = 0 then fps_X else if n=1 then 1 else 0)"
by (cases n) simp_all
lemma fps_inverse_fps_X_plus1: "inverse (1 + fps_X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)"
(is "_ = ?r")
proof -
have eq: "(1 + fps_X) * ?r = 1"
unfolding minus_one_power_iff
by (auto simp add: field_simps fps_eq_iff)
show ?thesis
by (auto simp add: eq intro: fps_inverse_unique)
qed
subsection \<open>Integration\<close>
definition fps_integral :: "'a::field_char_0 fps \<Rightarrow> 'a \<Rightarrow> 'a fps"
where "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a"
unfolding fps_integral_def fps_deriv_def
by (simp add: fps_eq_iff del: of_nat_Suc)
lemma fps_integral_linear:
"fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) =
fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0"
(is "?l = ?r")
proof -
have "fps_deriv ?l = fps_deriv ?r"
by (simp add: fps_deriv_fps_integral)
moreover have "?l$0 = ?r$0"
by (simp add: fps_integral_def)
ultimately show ?thesis
unfolding fps_deriv_eq_iff by auto
qed
subsection \<open>Composition of FPSs\<close>
definition fps_compose :: "'a::semiring_1 fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55)
where "a oo b = Abs_fps (\<lambda>n. sum (\<lambda>i. a$i * (b^i$n)) {0..n})"
lemma fps_compose_nth: "(a oo b)$n = sum (\<lambda>i. a$i * (b^i$n)) {0..n}"
by (simp add: fps_compose_def)
lemma fps_compose_nth_0 [simp]: "(f oo g) $ 0 = f $ 0"
by (simp add: fps_compose_nth)
lemma fps_compose_fps_X[simp]: "a oo fps_X = (a :: 'a::comm_ring_1 fps)"
by (simp add: fps_ext fps_compose_def mult_delta_right sum.delta')
lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta)
lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k"
unfolding numeral_fps_const by simp
lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k"
unfolding neg_numeral_fps_const by simp
lemma fps_X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> fps_X oo a = (a :: 'a::comm_ring_1 fps)"
by (simp add: fps_eq_iff fps_compose_def mult_delta_left sum.delta not_le)
subsection \<open>Rules from Herbert Wilf's Generatingfunctionology\<close>
subsubsection \<open>Rule 1\<close>
(* {a_{n+k}}_0^infty Corresponds to (f - sum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
lemma fps_power_mult_eq_shift:
"fps_X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * fps_X^i) {0 .. k}"
(is "?lhs = ?rhs")
proof -
have "?lhs $ n = ?rhs $ n" for n :: nat
proof -
have "?lhs $ n = (if n < Suc k then 0 else a n)"
unfolding fps_X_power_mult_nth by auto
also have "\<dots> = ?rhs $ n"
proof (induct k)
case 0
then show ?case
by (simp add: fps_sum_nth)
next
case (Suc k)
have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. Suc k})$n =
(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. k} -
fps_const (a (Suc k)) * fps_X^ Suc k) $ n"
by (simp add: field_simps)
also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * fps_X^ Suc k)$n"
using Suc.hyps[symmetric] unfolding fps_sub_nth by simp
also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)"
unfolding fps_X_power_mult_right_nth
apply (auto simp add: not_less fps_const_def)
apply (rule cong[of a a, OF refl])
apply arith
done
finally show ?case
by simp
qed
finally show ?thesis .
qed
then show ?thesis
by (simp add: fps_eq_iff)
qed
subsubsection \<open>Rule 2\<close>
(* We can not reach the form of Wilf, but still near to it using rewrite rules*)
(* If f reprents {a_n} and P is a polynomial, then
P(xD) f represents {P(n) a_n}*)
definition "fps_XD = ( * ) fps_X \<circ> fps_deriv"
lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
by (simp add: fps_XD_def field_simps)
lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a"
by (simp add: fps_XD_def field_simps)
lemma fps_XD_linear[simp]: "fps_XD (fps_const c * a + fps_const d * b) =
fps_const c * fps_XD a + fps_const d * fps_XD (b :: 'a::comm_ring_1 fps)"
by simp
lemma fps_XDN_linear:
"(fps_XD ^^ n) (fps_const c * a + fps_const d * b) =
fps_const c * (fps_XD ^^ n) a + fps_const d * (fps_XD ^^ n) (b :: 'a::comm_ring_1 fps)"
by (induct n) simp_all
lemma fps_mult_fps_X_deriv_shift: "fps_X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
by (simp add: fps_eq_iff)
lemma fps_mult_fps_XD_shift:
"(fps_XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
by (induct k arbitrary: a) (simp_all add: fps_XD_def fps_eq_iff field_simps del: One_nat_def)
subsubsection \<open>Rule 3\<close>
text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
subsubsection \<open>Rule 5 --- summation and "division" by (1 - fps_X)\<close>
lemma fps_divide_fps_X_minus1_sum_lemma:
"a = ((1::'a::comm_ring_1 fps) - fps_X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
proof -
let ?sa = "Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
have th0: "\<And>i. (1 - (fps_X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
by simp
have "a$n = ((1 - fps_X) * ?sa) $ n" for n
proof (cases "n = 0")
case True
then show ?thesis
by (simp add: fps_mult_nth)
next
case False
then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1} \<union> {2..n} = {1..n}"
"{0..n - 1} \<union> {n} = {0..n}"
by (auto simp: set_eq_iff)
have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" "{0..n - 1} \<inter> {n} = {}"
using False by simp_all
have f: "finite {0}" "finite {1}" "finite {2 .. n}"
"finite {0 .. n - 1}" "finite {n}" by simp_all
have "((1 - fps_X) * ?sa) $ n = sum (\<lambda>i. (1 - fps_X)$ i * ?sa $ (n - i)) {0 .. n}"
by (simp add: fps_mult_nth)
also have "\<dots> = a$n"
unfolding th0
unfolding sum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)]
unfolding sum.union_disjoint[OF f(2) f(3) d(2)]
apply (simp)
unfolding sum.union_disjoint[OF f(4,5) d(3), unfolded u(3)]
apply simp
done
finally show ?thesis
by simp
qed
then show ?thesis
unfolding fps_eq_iff by blast
qed
lemma fps_divide_fps_X_minus1_sum:
"a /((1::'a::field fps) - fps_X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
proof -
let ?fps_X = "1 - (fps_X::'a fps)"
have th0: "?fps_X $ 0 \<noteq> 0"
by simp
have "a /?fps_X = ?fps_X * Abs_fps (\<lambda>n::nat. sum (($) a) {0..n}) * inverse ?fps_X"
using fps_divide_fps_X_minus1_sum_lemma[of a, symmetric] th0
by (simp add: fps_divide_def mult.assoc)
also have "\<dots> = (inverse ?fps_X * ?fps_X) * Abs_fps (\<lambda>n::nat. sum (($) a) {0..n}) "
by (simp add: ac_simps)
finally show ?thesis
by (simp add: inverse_mult_eq_1[OF th0])
qed
subsubsection \<open>Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
finite product of FPS, also the relvant instance of powers of a FPS\<close>
definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"
lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
apply (auto simp add: natpermute_def)
apply (case_tac x)
apply auto
done
lemma append_natpermute_less_eq:
assumes "xs @ ys \<in> natpermute n k"
shows "sum_list xs \<le> n"
and "sum_list ys \<le> n"
proof -
from assms have "sum_list (xs @ ys) = n"
by (simp add: natpermute_def)
then have "sum_list xs + sum_list ys = n"
by simp
then show "sum_list xs \<le> n" and "sum_list ys \<le> n"
by simp_all
qed
lemma natpermute_split:
assumes "h \<le> k"
shows "natpermute n k =
(\<Union>m \<in>{0..n}. {l1 @ l2 |l1 l2. l1 \<in> natpermute m h \<and> l2 \<in> natpermute (n - m) (k - h)})"
(is "?L = ?R" is "_ = (\<Union>m \<in>{0..n}. ?S m)")
proof
show "?R \<subseteq> ?L"
proof
fix l
assume l: "l \<in> ?R"
from l obtain m xs ys where h: "m \<in> {0..n}"
and xs: "xs \<in> natpermute m h"
and ys: "ys \<in> natpermute (n - m) (k - h)"
and leq: "l = xs@ys" by blast
from xs have xs': "sum_list xs = m"
by (simp add: natpermute_def)
from ys have ys': "sum_list ys = n - m"
by (simp add: natpermute_def)
show "l \<in> ?L" using leq xs ys h
apply (clarsimp simp add: natpermute_def)
unfolding xs' ys'
using assms xs ys
unfolding natpermute_def
apply simp
done
qed
show "?L \<subseteq> ?R"
proof
fix l
assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
let ?ys = "drop h l"
let ?m = "sum_list ?xs"
from l have ls: "sum_list (?xs @ ?ys) = n"
by (simp add: natpermute_def)
have xs: "?xs \<in> natpermute ?m h" using l assms
by (simp add: natpermute_def)
have l_take_drop: "sum_list l = sum_list (take h l @ drop h l)"
by simp
then have ys: "?ys \<in> natpermute (n - ?m) (k - h)"
using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
from ls have m: "?m \<in> {0..n}"
by (simp add: l_take_drop del: append_take_drop_id)
from xs ys ls show "l \<in> ?R"
apply auto
apply (rule bexI [where x = "?m"])
apply (rule exI [where x = "?xs"])
apply (rule exI [where x = "?ys"])
using ls l
apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
apply simp
done
qed
qed
lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})"
by (auto simp add: natpermute_def)
lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})"
apply (auto simp add: set_replicate_conv_if natpermute_def)
apply (rule nth_equalityI)
apply simp_all
done
lemma natpermute_finite: "finite (natpermute n k)"
proof (induct k arbitrary: n)
case 0
then show ?case
apply (subst natpermute_split[of 0 0, simplified])
apply (simp add: natpermute_0)
done
next
case (Suc k)
then show ?case unfolding natpermute_split [of k "Suc k", simplified]
apply -
apply (rule finite_UN_I)
apply simp
unfolding One_nat_def[symmetric] natlist_trivial_1
apply simp
done
qed
lemma natpermute_contain_maximal:
"{xs \<in> natpermute n (k + 1). n \<in> set xs} = (\<Union>i\<in>{0 .. k}. {(replicate (k + 1) 0) [i:=n]})"
(is "?A = ?B")
proof
show "?A \<subseteq> ?B"
proof
fix xs
assume "xs \<in> ?A"
then have H: "xs \<in> natpermute n (k + 1)" and n: "n \<in> set xs"
by blast+