author  huffman 
Thu, 12 Mar 2009 08:57:03 0700  
changeset 30488  5c4c3a9e9102 
parent 30273  ecd6f0ca62ea 
child 30661  54858c8ad226 
child 30746  d6915b738bd9 
permissions  rwrr 
29687  1 
(* Title: Formal_Power_Series.thy 
30488  2 
ID: 
29687  3 
Author: Amine Chaieb, University of Cambridge 
4 
*) 

5 

6 
header{* A formalization of formal power series *} 

7 

8 
theory Formal_Power_Series 

9 
imports Main Fact Parity 

10 
begin 

11 

29906  12 
subsection {* The type of formal power series*} 
29687  13 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

14 
typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

15 
morphisms fps_nth Abs_fps 
29687  16 
by simp 
17 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

18 
notation fps_nth (infixl "$" 75) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

19 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

20 
lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p $ n = q $ n)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

21 
by (simp add: fps_nth_inject [symmetric] expand_fun_eq) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

22 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

23 
lemma fps_ext: "(\<And>n. p $ n = q $ n) \<Longrightarrow> p = q" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

24 
by (simp add: expand_fps_eq) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

25 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

26 
lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

27 
by (simp add: Abs_fps_inverse) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

28 

29687  29 
text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *} 
30 

31 
instantiation fps :: (zero) zero 

32 
begin 

33 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

34 
definition fps_zero_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

35 
"0 = Abs_fps (\<lambda>n. 0)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

36 

29687  37 
instance .. 
38 
end 

39 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

40 
lemma fps_zero_nth [simp]: "0 $ n = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

41 
unfolding fps_zero_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

42 

29687  43 
instantiation fps :: ("{one,zero}") one 
44 
begin 

45 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

46 
definition fps_one_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

47 
"1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

48 

29687  49 
instance .. 
50 
end 

51 

30488  52 
lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

53 
unfolding fps_one_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

54 

29687  55 
instantiation fps :: (plus) plus 
56 
begin 

57 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

58 
definition fps_plus_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

59 
"op + = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n + g $ n))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

60 

29687  61 
instance .. 
62 
end 

63 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

64 
lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

65 
unfolding fps_plus_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

66 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

67 
instantiation fps :: (minus) minus 
29687  68 
begin 
69 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

70 
definition fps_minus_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

71 
"op  = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n  g $ n))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

72 

29687  73 
instance .. 
74 
end 

75 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

76 
lemma fps_sub_nth [simp]: "(f  g) $ n = f $ n  g $ n" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

77 
unfolding fps_minus_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

78 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

79 
instantiation fps :: (uminus) uminus 
29687  80 
begin 
81 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

82 
definition fps_uminus_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

83 
"uminus = (\<lambda>f. Abs_fps (\<lambda>n.  (f $ n)))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

84 

29687  85 
instance .. 
86 
end 

87 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

88 
lemma fps_neg_nth [simp]: "( f) $ n =  (f $ n)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

89 
unfolding fps_uminus_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

90 

29687  91 
instantiation fps :: ("{comm_monoid_add, times}") times 
92 
begin 

93 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

94 
definition fps_times_def: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

95 
"op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n  i)))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

96 

29687  97 
instance .. 
98 
end 

99 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

100 
lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n  i))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

101 
unfolding fps_times_def by simp 
29687  102 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

103 
declare atLeastAtMost_iff[presburger] 
29687  104 
declare Bex_def[presburger] 
105 
declare Ball_def[presburger] 

106 

29913  107 
lemma mult_delta_left: 
108 
fixes x y :: "'a::mult_zero" 

109 
shows "(if b then x else 0) * y = (if b then x * y else 0)" 

110 
by simp 

111 

112 
lemma mult_delta_right: 

113 
fixes x y :: "'a::mult_zero" 

114 
shows "x * (if b then y else 0) = (if b then x * y else 0)" 

115 
by simp 

116 

29687  117 
lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" 
118 
by auto 

119 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" 

120 
by auto 

121 

30488  122 
subsection{* Formal power series form a commutative ring with unity, if the range of sequences 
29687  123 
they represent is a commutative ring with unity*} 
124 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

125 
instance fps :: (semigroup_add) semigroup_add 
29687  126 
proof 
127 
fix a b c :: "'a fps" show "a + b + c = a + (b + c)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

128 
by (simp add: fps_ext add_assoc) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

129 
qed 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

130 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

131 
instance fps :: (ab_semigroup_add) ab_semigroup_add 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

132 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

133 
fix a b :: "'a fps" show "a + b = b + a" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

134 
by (simp add: fps_ext add_commute) 
29687  135 
qed 
136 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

137 
lemma fps_mult_assoc_lemma: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

138 
fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

139 
shows "(\<Sum>j=0..k. \<Sum>i=0..j. f i (j  i) (n  j)) = 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

140 
(\<Sum>j=0..k. \<Sum>i=0..k  j. f j i (n  j  i))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

141 
proof (induct k) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

142 
case 0 show ?case by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

143 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

144 
case (Suc k) thus ?case 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

145 
by (simp add: Suc_diff_le setsum_addf add_assoc 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

146 
cong: strong_setsum_cong) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

147 
qed 
29687  148 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

149 
instance fps :: (semiring_0) semigroup_mult 
29687  150 
proof 
151 
fix a b c :: "'a fps" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

152 
show "(a * b) * c = a * (b * c)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

153 
proof (rule fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

154 
fix n :: nat 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

155 
have "(\<Sum>j=0..n. \<Sum>i=0..j. a$i * b$(j  i) * c$(n  j)) = 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

156 
(\<Sum>j=0..n. \<Sum>i=0..n  j. a$j * b$i * c$(n  j  i))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

157 
by (rule fps_mult_assoc_lemma) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

158 
thus "((a * b) * c) $ n = (a * (b * c)) $ n" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

159 
by (simp add: fps_mult_nth setsum_right_distrib 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

160 
setsum_left_distrib mult_assoc) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

161 
qed 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

162 
qed 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

163 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

164 
lemma fps_mult_commute_lemma: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

165 
fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

166 
shows "(\<Sum>i=0..n. f i (n  i)) = (\<Sum>i=0..n. f (n  i) i)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

167 
proof (rule setsum_reindex_cong) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

168 
show "inj_on (\<lambda>i. n  i) {0..n}" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

169 
by (rule inj_onI) simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

170 
show "{0..n} = (\<lambda>i. n  i) ` {0..n}" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

171 
by (auto, rule_tac x="n  x" in image_eqI, simp_all) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

172 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

173 
fix i assume "i \<in> {0..n}" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

174 
hence "n  (n  i) = i" by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

175 
thus "f (n  i) i = f (n  i) (n  (n  i))" by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

176 
qed 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

177 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

178 
instance fps :: (comm_semiring_0) ab_semigroup_mult 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

179 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

180 
fix a b :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

181 
show "a * b = b * a" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

182 
proof (rule fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

183 
fix n :: nat 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

184 
have "(\<Sum>i=0..n. a$i * b$(n  i)) = (\<Sum>i=0..n. a$(n  i) * b$i)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

185 
by (rule fps_mult_commute_lemma) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

186 
thus "(a * b) $ n = (b * a) $ n" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

187 
by (simp add: fps_mult_nth mult_commute) 
29687  188 
qed 
189 
qed 

190 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

191 
instance fps :: (monoid_add) monoid_add 
29687  192 
proof 
193 
fix a :: "'a fps" show "0 + a = a " 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

194 
by (simp add: fps_ext) 
29687  195 
next 
196 
fix a :: "'a fps" show "a + 0 = a " 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

197 
by (simp add: fps_ext) 
29687  198 
qed 
199 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

200 
instance fps :: (comm_monoid_add) comm_monoid_add 
29687  201 
proof 
202 
fix a :: "'a fps" show "0 + a = a " 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

203 
by (simp add: fps_ext) 
29687  204 
qed 
205 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

206 
instance fps :: (semiring_1) monoid_mult 
29687  207 
proof 
208 
fix a :: "'a fps" show "1 * a = a" 

29913  209 
by (simp add: fps_ext fps_mult_nth mult_delta_left setsum_delta) 
29687  210 
next 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

211 
fix a :: "'a fps" show "a * 1 = a" 
29913  212 
by (simp add: fps_ext fps_mult_nth mult_delta_right setsum_delta') 
29687  213 
qed 
214 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

215 
instance fps :: (cancel_semigroup_add) cancel_semigroup_add 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

216 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

217 
fix a b c :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

218 
assume "a + b = a + c" then show "b = c" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

219 
by (simp add: expand_fps_eq) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

220 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

221 
fix a b c :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

222 
assume "b + a = c + a" then show "b = c" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

223 
by (simp add: expand_fps_eq) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

224 
qed 
29687  225 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

226 
instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

227 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

228 
fix a b c :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

229 
assume "a + b = a + c" then show "b = c" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

230 
by (simp add: expand_fps_eq) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

231 
qed 
29687  232 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

233 
instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

234 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

235 
instance fps :: (group_add) group_add 
29687  236 
proof 
237 
fix a :: "'a fps" show " a + a = 0" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

238 
by (simp add: fps_ext) 
29687  239 
next 
240 
fix a b :: "'a fps" show "a  b = a +  b" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

241 
by (simp add: fps_ext diff_minus) 
29687  242 
qed 
243 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

244 
instance fps :: (ab_group_add) ab_group_add 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

245 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

246 
fix a :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

247 
show " a + a = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

248 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

249 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

250 
fix a b :: "'a fps" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

251 
show "a  b = a +  b" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

252 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

253 
qed 
29687  254 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

255 
instance fps :: (zero_neq_one) zero_neq_one 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

256 
by default (simp add: expand_fps_eq) 
29687  257 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

258 
instance fps :: (semiring_0) semiring 
29687  259 
proof 
260 
fix a b c :: "'a fps" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

261 
show "(a + b) * c = a * c + b * c" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

262 
by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf) 
29687  263 
next 
264 
fix a b c :: "'a fps" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

265 
show "a * (b + c) = a * b + a * c" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

266 
by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf) 
29687  267 
qed 
268 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

269 
instance fps :: (semiring_0) semiring_0 
29687  270 
proof 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

271 
fix a:: "'a fps" show "0 * a = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

272 
by (simp add: fps_ext fps_mult_nth) 
29687  273 
next 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

274 
fix a:: "'a fps" show "a * 0 = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

275 
by (simp add: fps_ext fps_mult_nth) 
29687  276 
qed 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

277 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

278 
instance fps :: (semiring_0_cancel) semiring_0_cancel .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

279 

29906  280 
subsection {* Selection of the nth power of the implicit variable in the infinite sum*} 
29687  281 

282 
lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

283 
by (simp add: expand_fps_eq) 
29687  284 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

285 
lemma fps_nonzero_nth_minimal: 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

286 
"f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m<n. f $ m = 0))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

287 
proof 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

288 
let ?n = "LEAST n. f $ n \<noteq> 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

289 
assume "f \<noteq> 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

290 
then have "\<exists>n. f $ n \<noteq> 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

291 
by (simp add: fps_nonzero_nth) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

292 
then have "f $ ?n \<noteq> 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

293 
by (rule LeastI_ex) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

294 
moreover have "\<forall>m<?n. f $ m = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

295 
by (auto dest: not_less_Least) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

296 
ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

297 
then show "\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m<n. f $ m = 0)" .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

298 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

299 
assume "\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m<n. f $ m = 0)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

300 
then show "f \<noteq> 0" by (auto simp add: expand_fps_eq) 
29687  301 
qed 
302 

303 
lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $ n = g $n)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

304 
by (rule expand_fps_eq) 
29687  305 

30488  306 
lemma fps_setsum_nth: "(setsum f S) $ n = setsum (\<lambda>k. (f k) $ n) S" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

307 
proof (cases "finite S") 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

308 
assume "\<not> finite S" then show ?thesis by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

309 
next 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

310 
assume "finite S" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

311 
then show ?thesis by (induct set: finite) auto 
29687  312 
qed 
313 

29906  314 
subsection{* Injection of the basic ring elements and multiplication by scalars *} 
29687  315 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

316 
definition 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

317 
"fps_const c = Abs_fps (\<lambda>n. if n = 0 then c else 0)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

318 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

319 
lemma fps_nth_fps_const [simp]: "fps_const c $ n = (if n = 0 then c else 0)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

320 
unfolding fps_const_def by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

321 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

322 
lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

323 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

324 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

325 
lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

326 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

327 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

328 
lemma fps_const_neg [simp]: " (fps_const (c::'a::ring)) = fps_const ( c)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

329 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

330 

c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

331 
lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

332 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

333 

29687  334 
lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

335 
by (simp add: fps_eq_iff fps_mult_nth setsum_0') 
29687  336 

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

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

338 
by (simp add: fps_ext) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

339 

29687  340 
lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

341 
by (simp add: fps_ext) 
29687  342 

343 
lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

344 
unfolding fps_eq_iff fps_mult_nth 
29913  345 
by (simp add: fps_const_def mult_delta_left setsum_delta) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

346 

29687  347 
lemma fps_const_mult_right: "f * fps_const (c::'a\<Colon>semiring_0) = Abs_fps (\<lambda>n. f$n * c)" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

348 
unfolding fps_eq_iff fps_mult_nth 
29913  349 
by (simp add: fps_const_def mult_delta_right setsum_delta') 
29687  350 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

351 
lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n" 
29913  352 
by (simp add: fps_mult_nth mult_delta_left setsum_delta) 
29687  353 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

354 
lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" 
29913  355 
by (simp add: fps_mult_nth mult_delta_right setsum_delta') 
29687  356 

29906  357 
subsection {* Formal power series form an integral domain*} 
29687  358 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

359 
instance fps :: (ring) ring .. 
29687  360 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

361 
instance fps :: (ring_1) ring_1 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

362 
by (intro_classes, auto simp add: diff_minus left_distrib) 
29687  363 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

364 
instance fps :: (comm_ring_1) comm_ring_1 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

365 
by (intro_classes, auto simp add: diff_minus left_distrib) 
29687  366 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

367 
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors 
29687  368 
proof 
369 
fix a b :: "'a fps" 

370 
assume a0: "a \<noteq> 0" and b0: "b \<noteq> 0" 

371 
then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0" 

372 
and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0" unfolding fps_nonzero_nth_minimal 

373 
by blast+ 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

374 
have "(a * b) $ (i+j) = (\<Sum>k=0..i+j. a$k * b$(i+jk))" 
29687  375 
by (rule fps_mult_nth) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

376 
also have "\<dots> = (a$i * b$(i+ji)) + (\<Sum>k\<in>{0..i+j}{i}. a$k * b$(i+jk))" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

377 
by (rule setsum_diff1') simp_all 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

378 
also have "(\<Sum>k\<in>{0..i+j}{i}. a$k * b$(i+jk)) = 0" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

379 
proof (rule setsum_0' [rule_format]) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

380 
fix k assume "k \<in> {0..i+j}  {i}" 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

381 
then have "k < i \<or> i+jk < j" by auto 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

382 
then show "a$k * b$(i+jk) = 0" using i j by auto 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

383 
qed 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

384 
also have "a$i * b$(i+ji) + 0 = a$i * b$j" by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

385 
also have "a$i * b$j \<noteq> 0" using i j by simp 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

386 
finally have "(a*b) $ (i+j) \<noteq> 0" . 
29687  387 
then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast 
388 
qed 

389 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

390 
instance fps :: (idom) idom .. 
29687  391 

29906  392 
subsection{* Inverses of formal power series *} 
29687  393 

394 
declare setsum_cong[fundef_cong] 

395 

396 

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

398 
begin 

399 

30488  400 
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" where 
29687  401 
"natfun_inverse f 0 = inverse (f$0)" 
30488  402 
 "natfun_inverse f n =  inverse (f$0) * setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}" 
29687  403 

30488  404 
definition fps_inverse_def: 
29687  405 
"inverse f = (if f$0 = 0 then 0 else Abs_fps (natfun_inverse f))" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

406 
definition fps_divide_def: "divide = (\<lambda>(f::'a fps) g. f * inverse g)" 
29687  407 
instance .. 
408 
end 

409 

30488  410 
lemma fps_inverse_zero[simp]: 
29687  411 
"inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

412 
by (simp add: fps_ext fps_inverse_def) 
29687  413 

414 
lemma fps_inverse_one[simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

415 
apply (auto simp add: expand_fps_eq fps_inverse_def) 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

416 
by (case_tac n, auto) 
29687  417 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

418 
instance fps :: ("{comm_monoid_add,inverse, times, uminus}") division_by_zero 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

419 
by default (rule fps_inverse_zero) 
29687  420 

421 
lemma inverse_mult_eq_1[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)" 

422 
shows "inverse f * f = 1" 

423 
proof 

424 
have c: "inverse f * f = f * inverse f" by (simp add: mult_commute) 

30488  425 
from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n" 
29687  426 
by (simp add: fps_inverse_def) 
427 
from f0 have th0: "(inverse f * f) $ 0 = 1" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

428 
by (simp add: fps_mult_nth fps_inverse_def) 
29687  429 
{fix n::nat assume np: "n >0 " 
430 
from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto 

431 
have d: "{0} \<inter> {1 .. n} = {}" by auto 

432 
have f: "finite {0::nat}" "finite {1..n}" by auto 

30488  433 
from f0 np have th0: " (inverse f$n) = 
29687  434 
(setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}) / (f$0)" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

435 
by (cases n, simp, simp add: divide_inverse fps_inverse_def) 
29687  436 
from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] 
30488  437 
have th1: "setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n} = 
438 
 (f$0) * (inverse f)$n" 

29687  439 
by (simp add: ring_simps) 
30488  440 
have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n  i))" 
29687  441 
unfolding fps_mult_nth ifn .. 
30488  442 
also have "\<dots> = f$0 * natfun_inverse f n 
29687  443 
+ (\<Sum>i = 1..n. f$i * natfun_inverse f (ni))" 
444 
unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] 

445 
by simp 

446 
also have "\<dots> = 0" unfolding th1 ifn by simp 

447 
finally have "(inverse f * f)$n = 0" unfolding c . } 

448 
with th0 show ?thesis by (simp add: fps_eq_iff) 

449 
qed 

450 

451 
lemma fps_inverse_0_iff[simp]: "(inverse f)$0 = (0::'a::division_ring) \<longleftrightarrow> f$0 = 0" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

452 
by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) 
29687  453 

454 
lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f $0 = 0" 

455 
proof 

456 
{assume "f$0 = 0" hence "inverse f = 0" by (simp add: fps_inverse_def)} 

457 
moreover 

458 
{assume h: "inverse f = 0" and c: "f $0 \<noteq> 0" 

459 
from inverse_mult_eq_1[OF c] h have False by simp} 

460 
ultimately show ?thesis by blast 

461 
qed 

462 

463 
lemma fps_inverse_idempotent[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)" 

464 
shows "inverse (inverse f) = f" 

465 
proof 

466 
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp 

30488  467 
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] 
29687  468 
have th0: "inverse f * f = inverse f * inverse (inverse f)" by (simp add: mult_ac) 
469 
then show ?thesis using f0 unfolding mult_cancel_left by simp 

470 
qed 

471 

30488  472 
lemma fps_inverse_unique: assumes f0: "f$0 \<noteq> (0::'a::field)" and fg: "f*g = 1" 
29687  473 
shows "inverse f = g" 
474 
proof 

475 
from inverse_mult_eq_1[OF f0] fg 

476 
have th0: "inverse f * f = g * f" by (simp add: mult_ac) 

477 
then show ?thesis using f0 unfolding mult_cancel_right 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

478 
by (auto simp add: expand_fps_eq) 
29687  479 
qed 
480 

30488  481 
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) 
29687  482 
= Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then  1 else 0)" 
483 
apply (rule fps_inverse_unique) 

484 
apply simp 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

485 
apply (simp add: fps_eq_iff fps_mult_nth) 
29687  486 
proof(clarsimp) 
487 
fix n::nat assume n: "n > 0" 

488 
let ?f = "\<lambda>i. if n = i then (1\<Colon>'a) else if n  i = 1 then  1 else 0" 

489 
let ?g = "\<lambda>i. if i = n then 1 else if i=n  1 then  1 else 0" 

490 
let ?h = "\<lambda>i. if i=n  1 then  1 else 0" 

30488  491 
have th1: "setsum ?f {0..n} = setsum ?g {0..n}" 
29687  492 
by (rule setsum_cong2) auto 
30488  493 
have th2: "setsum ?g {0..n  1} = setsum ?h {0..n  1}" 
29687  494 
using n apply  by (rule setsum_cong2) auto 
495 
have eq: "{0 .. n} = {0.. n  1} \<union> {n}" by auto 

30488  496 
from n have d: "{0.. n  1} \<inter> {n} = {}" by auto 
29687  497 
have f: "finite {0.. n  1}" "finite {n}" by auto 
498 
show "setsum ?f {0..n} = 0" 

30488  499 
unfolding th1 
29687  500 
apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) 
501 
unfolding th2 

502 
by(simp add: setsum_delta) 

503 
qed 

504 

29912  505 
subsection{* Formal Derivatives, and the MacLaurin theorem around 0*} 
29687  506 

507 
definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))" 

508 

509 
lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def) 

510 

511 
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" 

512 
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: ring_simps) 

513 

30488  514 
lemma fps_deriv_mult[simp]: 
29687  515 
fixes f :: "('a :: comm_ring_1) fps" 
516 
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" 

517 
proof 

518 
let ?D = "fps_deriv" 

519 
{fix n::nat 

520 
let ?Zn = "{0 ..n}" 

521 
let ?Zn1 = "{0 .. n + 1}" 

522 
let ?f = "\<lambda>i. i + 1" 

523 
have fi: "inj_on ?f {0..n}" by (simp add: inj_on_def) 

524 
have eq: "{1.. n+1} = ?f ` {0..n}" by auto 

525 
let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n  i) + 

526 
of_nat (i+1)* f $ (i+1) * g $ (n  i)" 

527 
let ?h = "\<lambda>i. of_nat i * g $ i * f $ ((n+1)  i) + 

528 
of_nat i* f $ i * g $ ((n + 1)  i)" 

529 
{fix k assume k: "k \<in> {0..n}" 

530 
have "?h (k + 1) = ?g k" using k by auto} 

531 
note th0 = this 

532 
have eq': "{0..n +1} {1 .. n+1} = {0}" by auto 

533 
have s0: "setsum (\<lambda>i. of_nat i * f $ i * g $ (n + 1  i)) ?Zn1 = setsum (\<lambda>i. of_nat (n + 1  i) * f $ (n + 1  i) * g $ i) ?Zn1" 

534 
apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1  i"]) 

535 
apply (simp add: inj_on_def Ball_def) 

536 
apply presburger 

537 
apply (rule set_ext) 

538 
apply (presburger add: image_iff) 

539 
by simp 

540 
have s1: "setsum (\<lambda>i. f $ i * g $ (n + 1  i)) ?Zn1 = setsum (\<lambda>i. f $ (n + 1  i) * g $ i) ?Zn1" 

541 
apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1  i"]) 

542 
apply (simp add: inj_on_def Ball_def) 

543 
apply presburger 

544 
apply (rule set_ext) 

545 
apply (presburger add: image_iff) 

546 
by simp 

547 
have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" by (simp only: mult_commute) 

548 
also have "\<dots> = (\<Sum>i = 0..n. ?g i)" 

549 
by (simp add: fps_mult_nth setsum_addf[symmetric]) 

550 
also have "\<dots> = setsum ?h {1..n+1}" 

551 
using th0 setsum_reindex_cong[OF fi eq, of "?g" "?h"] by auto 

552 
also have "\<dots> = setsum ?h {0..n+1}" 

553 
apply (rule setsum_mono_zero_left) 

554 
apply simp 

555 
apply (simp add: subset_eq) 

556 
unfolding eq' 

557 
by simp 

558 
also have "\<dots> = (fps_deriv (f * g)) $ n" 

559 
apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf) 

560 
unfolding s0 s1 

561 
unfolding setsum_addf[symmetric] setsum_right_distrib 

562 
apply (rule setsum_cong2) 

563 
by (auto simp add: of_nat_diff ring_simps) 

564 
finally have "(f * ?D g + ?D f * g) $ n = ?D (f*g) $ n" .} 

30488  565 
then show ?thesis unfolding fps_eq_iff by auto 
29687  566 
qed 
567 

568 
lemma fps_deriv_neg[simp]: "fps_deriv ( (f:: ('a:: comm_ring_1) fps)) =  (fps_deriv f)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

569 
by (simp add: fps_eq_iff fps_deriv_def) 
29687  570 
lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g" 
571 
using fps_deriv_linear[of 1 f 1 g] by simp 

572 

573 
lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps)  g) = fps_deriv f  fps_deriv g" 

30488  574 
unfolding diff_minus by simp 
29687  575 

576 
lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

577 
by (simp add: fps_ext fps_deriv_def fps_const_def) 
29687  578 

579 
lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f" 

580 
by simp 

581 

582 
lemma fps_deriv_0[simp]: "fps_deriv 0 = 0" 

583 
by (simp add: fps_deriv_def fps_eq_iff) 

584 

585 
lemma fps_deriv_1[simp]: "fps_deriv 1 = 0" 

586 
by (simp add: fps_deriv_def fps_eq_iff ) 

587 

588 
lemma fps_deriv_mult_const_right[simp]: "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c" 

589 
by simp 

590 

591 
lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S" 

592 
proof 

593 
{assume "\<not> finite S" hence ?thesis by simp} 

594 
moreover 

595 
{assume fS: "finite S" 

596 
have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} 

597 
ultimately show ?thesis by blast 

598 
qed 

599 

600 
lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))" 

601 
proof 

602 
{assume "f= fps_const (f$0)" hence "fps_deriv f = fps_deriv (fps_const (f$0))" by simp 

603 
hence "fps_deriv f = 0" by simp } 

604 
moreover 

605 
{assume z: "fps_deriv f = 0" 

606 
hence "\<forall>n. (fps_deriv f)$n = 0" by simp 

607 
hence "\<forall>n. f$(n+1) = 0" by (simp del: of_nat_Suc of_nat_add One_nat_def) 

608 
hence "f = fps_const (f$0)" 

609 
apply (clarsimp simp add: fps_eq_iff fps_const_def) 

610 
apply (erule_tac x="n  1" in allE) 

611 
by simp} 

612 
ultimately show ?thesis by blast 

613 
qed 

614 

30488  615 
lemma fps_deriv_eq_iff: 
29687  616 
fixes f:: "('a::{idom,semiring_char_0}) fps" 
617 
shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0  g$0) + g)" 

618 
proof 

619 
have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f  g) = 0" by simp 

620 
also have "\<dots> \<longleftrightarrow> f  g = fps_const ((fg)$0)" unfolding fps_deriv_eq_0_iff .. 

621 
finally show ?thesis by (simp add: ring_simps) 

622 
qed 

623 

624 
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)" 

625 
apply auto unfolding fps_deriv_eq_iff by blast 

30488  626 

29687  627 

628 
fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps" where 

629 
"fps_nth_deriv 0 f = f" 

630 
 "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" 

631 

632 
lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)" 

633 
by (induct n arbitrary: f, auto) 

634 

635 
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" 

636 
by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute) 

637 

638 
lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n ( (f:: ('a:: comm_ring_1) fps)) =  (fps_nth_deriv n f)" 

639 
by (induct n arbitrary: f, simp_all) 

640 

641 
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" 

642 
using fps_nth_deriv_linear[of n 1 f 1 g] by simp 

643 

644 
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" 

30488  645 
unfolding diff_minus fps_nth_deriv_add by simp 
29687  646 

647 
lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0" 

648 
by (induct n, simp_all ) 

649 

650 
lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)" 

651 
by (induct n, simp_all ) 

652 

653 
lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)" 

654 
by (cases n, simp_all) 

655 

656 
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" 

657 
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp 

658 

659 
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" 

660 
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute) 

661 

662 
lemma fps_nth_deriv_setsum: "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S" 

663 
proof 

664 
{assume "\<not> finite S" hence ?thesis by simp} 

665 
moreover 

666 
{assume fS: "finite S" 

667 
have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} 

668 
ultimately show ?thesis by blast 

669 
qed 

670 

671 
lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)" 

672 
by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult) 

673 

29906  674 
subsection {* Powers*} 
29687  675 

676 
instantiation fps :: (semiring_1) power 

677 
begin 

678 

679 
fun fps_pow :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where 

680 
"fps_pow 0 f = 1" 

681 
 "fps_pow (Suc n) f = f * fps_pow n f" 

682 

683 
definition fps_power_def: "power (f::'a fps) n = fps_pow n f" 

684 
instance .. 

685 
end 

686 

687 
instantiation fps :: (comm_ring_1) recpower 

688 
begin 

689 
instance 

690 
apply (intro_classes) 

691 
by (simp_all add: fps_power_def) 

692 
end 

693 

694 
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)" 

29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

695 
by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth) 
29687  696 

697 
lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1" 

698 
proof(induct n) 

699 
case 0 thus ?case by (simp add: fps_power_def) 

700 
next 

701 
case (Suc n) 

702 
note h = Suc.hyps[OF `a$0 = 1`] 

30488  703 
show ?case unfolding power_Suc fps_mult_nth 
29687  704 
using h `a$0 = 1` fps_power_zeroth_eq_one[OF `a$0=1`] by (simp add: ring_simps) 
705 
qed 

706 

707 
lemma startsby_one_power:"a $ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n $ 0 = 1" 

708 
by (induct n, auto simp add: fps_power_def fps_mult_nth) 

709 

710 
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0" 

711 
by (induct n, auto simp add: fps_power_def fps_mult_nth) 

712 

713 
lemma startsby_power:"a $0 = (v::'a::{comm_ring_1, recpower}) \<Longrightarrow> a^n $0 = v^n" 

714 
by (induct n, auto simp add: fps_power_def fps_mult_nth power_Suc) 

715 

716 
lemma startsby_zero_power_iff[simp]: 

717 
"a^n $0 = (0::'a::{idom, recpower}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)" 

718 
apply (rule iffI) 

719 
apply (induct n, auto simp add: power_Suc fps_mult_nth) 

720 
by (rule startsby_zero_power, simp_all) 

721 

30488  722 
lemma startsby_zero_power_prefix: 
29687  723 
assumes a0: "a $0 = (0::'a::idom)" 
724 
shows "\<forall>n < k. a ^ k $ n = 0" 

30488  725 
using a0 
29687  726 
proof(induct k rule: nat_less_induct) 
727 
fix k assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $0 = (0\<Colon>'a)" 

728 
let ?ths = "\<forall>m<k. a ^ k $ m = 0" 

729 
{assume "k = 0" then have ?ths by simp} 

730 
moreover 

731 
{fix l assume k: "k = Suc l" 

732 
{fix m assume mk: "m < k" 

30488  733 
{assume "m=0" hence "a^k $ m = 0" using startsby_zero_power[of a k] k a0 
29687  734 
by simp} 
735 
moreover 

736 
{assume m0: "m \<noteq> 0" 

737 
have "a ^k $ m = (a^l * a) $m" by (simp add: k power_Suc mult_commute) 

738 
also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m  i))" by (simp add: fps_mult_nth) 

739 
also have "\<dots> = 0" apply (rule setsum_0') 

740 
apply auto 

741 
apply (case_tac "aa = m") 

742 
using a0 

743 
apply simp 

744 
apply (rule H[rule_format]) 

30488  745 
using a0 k mk by auto 
29687  746 
finally have "a^k $ m = 0" .} 
747 
ultimately have "a^k $ m = 0" by blast} 

748 
hence ?ths by blast} 

749 
ultimately show ?ths by (cases k, auto) 

750 
qed 

751 

30488  752 
lemma startsby_zero_setsum_depends: 
29687  753 
assumes a0: "a $0 = (0::'a::idom)" and kn: "n \<ge> k" 
754 
shows "setsum (\<lambda>i. (a ^ i)$k) {0 .. n} = setsum (\<lambda>i. (a ^ i)$k) {0 .. k}" 

755 
apply (rule setsum_mono_zero_right) 

756 
using kn apply auto 

757 
apply (rule startsby_zero_power_prefix[rule_format, OF a0]) 

758 
by arith 

759 

760 
lemma startsby_zero_power_nth_same: assumes a0: "a$0 = (0::'a::{recpower, idom})" 

761 
shows "a^n $ n = (a$1) ^ n" 

762 
proof(induct n) 

763 
case 0 thus ?case by (simp add: power_0) 

764 
next 

765 
case (Suc n) 

766 
have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: ring_simps power_Suc) 

767 
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n  i)) {0.. Suc n}" by (simp add: fps_mult_nth) 

768 
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n  i)) {n .. Suc n}" 

769 
apply (rule setsum_mono_zero_right) 

770 
apply simp 

771 
apply clarsimp 

772 
apply clarsimp 

773 
apply (rule startsby_zero_power_prefix[rule_format, OF a0]) 

774 
apply arith 

775 
done 

776 
also have "\<dots> = a^n $ n * a$1" using a0 by simp 

777 
finally show ?case using Suc.hyps by (simp add: power_Suc) 

778 
qed 

779 

780 
lemma fps_inverse_power: 

781 
fixes a :: "('a::{field, recpower}) fps" 

782 
shows "inverse (a^n) = inverse a ^ n" 

783 
proof 

784 
{assume a0: "a$0 = 0" 

785 
hence eq: "inverse a = 0" by (simp add: fps_inverse_def) 

786 
{assume "n = 0" hence ?thesis by simp} 

787 
moreover 

788 
{assume n: "n > 0" 

30488  789 
from startsby_zero_power[OF a0 n] eq a0 n have ?thesis 
29687  790 
by (simp add: fps_inverse_def)} 
791 
ultimately have ?thesis by blast} 

792 
moreover 

793 
{assume a0: "a$0 \<noteq> 0" 

794 
have ?thesis 

795 
apply (rule fps_inverse_unique) 

796 
apply (simp add: a0) 

797 
unfolding power_mult_distrib[symmetric] 

798 
apply (rule ssubst[where t = "a * inverse a" and s= 1]) 

799 
apply simp_all 

800 
apply (subst mult_commute) 

801 
by (rule inverse_mult_eq_1[OF a0])} 

802 
ultimately show ?thesis by blast 

803 
qed 

804 

805 
lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n  1)" 

806 
apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add) 

807 
by (case_tac n, auto simp add: power_Suc ring_simps) 

808 

30488  809 
lemma fps_inverse_deriv: 
29687  810 
fixes a:: "('a :: field) fps" 
811 
assumes a0: "a$0 \<noteq> 0" 

812 
shows "fps_deriv (inverse a) =  fps_deriv a * inverse a ^ 2" 

813 
proof 

814 
from inverse_mult_eq_1[OF a0] 

815 
have "fps_deriv (inverse a * a) = 0" by simp 

816 
hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp 

817 
hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" by simp 

818 
with inverse_mult_eq_1[OF a0] 

819 
have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0" 

820 
unfolding power2_eq_square 

821 
apply (simp add: ring_simps) 

822 
by (simp add: mult_assoc[symmetric]) 

823 
hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a)  fps_deriv a * inverse a ^ 2 = 0  fps_deriv a * inverse a ^ 2" 

824 
by simp 

825 
then show "fps_deriv (inverse a) =  fps_deriv a * inverse a ^ 2" by (simp add: ring_simps) 

826 
qed 

827 

30488  828 
lemma fps_inverse_mult: 
29687  829 
fixes a::"('a :: field) fps" 
830 
shows "inverse (a * b) = inverse a * inverse b" 

831 
proof 

832 
{assume a0: "a$0 = 0" hence ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) 

833 
from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all 

834 
have ?thesis unfolding th by simp} 

835 
moreover 

836 
{assume b0: "b$0 = 0" hence ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) 

837 
from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all 

838 
have ?thesis unfolding th by simp} 

839 
moreover 

840 
{assume a0: "a$0 \<noteq> 0" and b0: "b$0 \<noteq> 0" 

841 
from a0 b0 have ab0:"(a*b) $ 0 \<noteq> 0" by (simp add: fps_mult_nth) 

30488  842 
from inverse_mult_eq_1[OF ab0] 
29687  843 
have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp 
844 
then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" 

845 
by (simp add: ring_simps) 

846 
then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp} 

847 
ultimately show ?thesis by blast 

848 
qed 

849 

30488  850 
lemma fps_inverse_deriv': 
29687  851 
fixes a:: "('a :: field) fps" 
852 
assumes a0: "a$0 \<noteq> 0" 

853 
shows "fps_deriv (inverse a) =  fps_deriv a / a ^ 2" 

854 
using fps_inverse_deriv[OF a0] 

855 
unfolding power2_eq_square fps_divide_def 

856 
fps_inverse_mult by simp 

857 

858 
lemma inverse_mult_eq_1': assumes f0: "f$0 \<noteq> (0::'a::field)" 

859 
shows "f * inverse f= 1" 

860 
by (metis mult_commute inverse_mult_eq_1 f0) 

861 

862 
lemma fps_divide_deriv: fixes a:: "('a :: field) fps" 

863 
assumes a0: "b$0 \<noteq> 0" 

864 
shows "fps_deriv (a / b) = (fps_deriv a * b  a * fps_deriv b) / b ^ 2" 

865 
using fps_inverse_deriv[OF a0] 

866 
by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) 

30488  867 

29906  868 
subsection{* The eXtractor series X*} 
29687  869 

870 
lemma minus_one_power_iff: "( (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else  1)" 

871 
by (induct n, auto) 

872 

873 
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)" 

874 

30488  875 
lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field))) 
29687  876 
= 1  X" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

877 
by (simp add: fps_inverse_gp fps_eq_iff X_def) 
29687  878 

879 
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n  1))" 

880 
proof 

881 
{assume n: "n \<noteq> 0" 

882 
have fN: "finite {0 .. n}" by simp 

883 
have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n  i))" by (simp add: fps_mult_nth) 

29913  884 
also have "\<dots> = f $ (n  1)" 
885 
using n by (simp add: X_def mult_delta_left setsum_delta [OF fN]) 

29687  886 
finally have ?thesis using n by simp } 
887 
moreover 

888 
{assume n: "n=0" hence ?thesis by (simp add: fps_mult_nth X_def)} 

889 
ultimately show ?thesis by blast 

890 
qed 

891 

892 
lemma X_mult_right_nth[simp]: "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n  1))" 

893 
by (metis X_mult_nth mult_commute) 

894 

895 
lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)" 

896 
proof(induct k) 

897 
case 0 thus ?case by (simp add: X_def fps_power_def fps_eq_iff) 

898 
next 

899 
case (Suc k) 

30488  900 
{fix m 
29687  901 
have "(X^Suc k) $ m = (if m = 0 then (0::'a) else (X^k) $ (m  1))" 
902 
by (simp add: power_Suc del: One_nat_def) 

903 
then have "(X^Suc k) $ m = (if m = Suc k then (1::'a) else 0)" 

904 
using Suc.hyps by (auto cong del: if_weak_cong)} 

905 
then show ?case by (simp add: fps_eq_iff) 

906 
qed 

907 

908 
lemma X_power_mult_nth: "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n  k))" 

909 
apply (induct k arbitrary: n) 

910 
apply (simp) 

30488  911 
unfolding power_Suc mult_assoc 
29687  912 
by (case_tac n, auto) 
913 

914 
lemma X_power_mult_right_nth: "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n  k))" 

915 
by (metis X_power_mult_nth mult_commute) 

916 
lemma fps_deriv_X[simp]: "fps_deriv X = 1" 

917 
by (simp add: fps_deriv_def X_def fps_eq_iff) 

918 

919 
lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" 

920 
by (cases "n", simp_all) 

921 

922 
lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def) 

923 
lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else (0::'a::comm_ring_1))" 

924 
by (simp add: X_power_iff) 

925 

926 
lemma fps_inverse_X_plus1: 

927 
"inverse (1 + X) = Abs_fps (\<lambda>n. ( (1::'a::{recpower, field})) ^ n)" (is "_ = ?r") 

928 
proof 

929 
have eq: "(1 + X) * ?r = 1" 

930 
unfolding minus_one_power_iff 

931 
apply (auto simp add: ring_simps fps_eq_iff) 

932 
by presburger+ 

933 
show ?thesis by (auto simp add: eq intro: fps_inverse_unique) 

934 
qed 

935 

30488  936 

29906  937 
subsection{* Integration *} 
29687  938 
definition "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n  1) / of_nat n))" 
939 

940 
lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a" 

941 
by (simp add: fps_integral_def fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) 

942 

943 
lemma fps_integral_linear: "fps_integral (fps_const (a::'a::{field, ring_char_0}) * 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") 

944 
proof 

945 
have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral) 

946 
moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def) 

947 
ultimately show ?thesis 

948 
unfolding fps_deriv_eq_iff by auto 

949 
qed 

30488  950 

29906  951 
subsection {* Composition of FPSs *} 
29687  952 
definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where 
953 
fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})" 

954 

955 
lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}" by (simp add: fps_compose_def) 

956 

957 
lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)" 

29913  958 
by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta') 
30488  959 

960 
lemma fps_const_compose[simp]: 

29687  961 
"fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)" 
29913  962 
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) 
29687  963 

964 
lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)" 

29913  965 
by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta 
966 
power_Suc not_le) 

29687  967 

968 

29906  969 
subsection {* Rules from Herbert Wilf's Generatingfunctionology*} 
29687  970 

29906  971 
subsubsection {* Rule 1 *} 
29687  972 
(* {a_{n+k}}_0^infty Corresponds to (f  setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*) 
973 

30488  974 
lemma fps_power_mult_eq_shift: 
29687  975 
"X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a  setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}" (is "?lhs = ?rhs") 
976 
proof 

977 
{fix n:: nat 

30488  978 
have "?lhs $ n = (if n < Suc k then 0 else a n)" 
29687  979 
unfolding X_power_mult_nth by auto 
980 
also have "\<dots> = ?rhs $ n" 

981 
proof(induct k) 

982 
case 0 thus ?case by (simp add: fps_setsum_nth power_Suc) 

983 
next 

984 
case (Suc k) 

985 
note th = Suc.hyps[symmetric] 

986 
have "(Abs_fps a  setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. Suc k})$n = (Abs_fps a  setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}  fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: ring_simps) 

987 
also have "\<dots> = (if n < Suc k then 0 else a n)  (fps_const (a (Suc k)) * X^ Suc k)$n" 

30488  988 
using th 
29687  989 
unfolding fps_sub_nth by simp 
990 
also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)" 

991 
unfolding X_power_mult_right_nth 

992 
apply (auto simp add: not_less fps_const_def) 

993 
apply (rule cong[of a a, OF refl]) 

994 
by arith 

995 
finally show ?case by simp 

996 
qed 

997 
finally have "?lhs $ n = ?rhs $ n" .} 

998 
then show ?thesis by (simp add: fps_eq_iff) 

999 
qed 

1000 

29906  1001 
subsubsection{* Rule 2*} 
29687  1002 

1003 
(* We can not reach the form of Wilf, but still near to it using rewrite rules*) 

30488  1004 
(* If f reprents {a_n} and P is a polynomial, then 
29687  1005 
P(xD) f represents {P(n) a_n}*) 
1006 

1007 
definition "XD = op * X o fps_deriv" 

1008 

1009 
lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)" 

1010 
by (simp add: XD_def ring_simps) 

1011 

1012 
lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a" 

1013 
by (simp add: XD_def ring_simps) 

1014 

1015 
lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)" 

1016 
by simp 

1017 

29689
dd086f26ee4f
removed definition of funpow , reusing that of Relation_Power
chaieb
parents:
29687
diff
changeset

1018 
lemma XDN_linear: "(XD^n) (fps_const c * a + fps_const d * b) = fps_const c * (XD^n) a + fps_const d * (XD^n) (b :: ('a::comm_ring_1) fps)" 
29687  1019 
by (induct n, simp_all) 
1020 

1021 
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff) 

1022 

29689
dd086f26ee4f
removed definition of funpow , reusing that of Relation_Power
chaieb
parents:
29687
diff
changeset

1023 
lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)" 
29687  1024 
by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def) 
1025 

29906  1026 
subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} 
1027 
subsubsection{* Rule 5  summation and "division" by (1  X)*} 

29687  1028 

1029 
lemma fps_divide_X_minus1_setsum_lemma: 

1030 
"a = ((1::('a::comm_ring_1) fps)  X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" 

1031 
proof 

1032 
let ?X = "X::('a::comm_ring_1) fps" 

1033 
let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" 

1034 
have th0: "\<And>i. (1  (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then  1 else 0)" by simp 

1035 
{fix n:: nat 

30488  1036 
{assume "n=0" hence "a$n = ((1  ?X) * ?sa) $ n" 
29687  1037 
by (simp add: fps_mult_nth)} 
1038 
moreover 

1039 
{assume n0: "n \<noteq> 0" 

1040 
then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}" 

1041 
"{0..n  1}\<union>{n} = {0..n}" 

1042 
apply (simp_all add: expand_set_eq) by presburger+ 

30488  1043 
have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" 
29687  1044 
"{0..n  1}\<inter>{n} ={}" using n0 
1045 
by (simp_all add: expand_set_eq, presburger+) 

30488  1046 
have f: "finite {0}" "finite {1}" "finite {2 .. n}" 
1047 
"finite {0 .. n  1}" "finite {n}" by simp_all 

29687  1048 
have "((1  ?X) * ?sa) $ n = setsum (\<lambda>i. (1  ?X)$ i * ?sa $ (n  i)) {0 .. n}" 
1049 
by (simp add: fps_mult_nth) 

1050 
also have "\<dots> = a$n" unfolding th0 

1051 
unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] 

1052 
unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] 

1053 
apply (simp) 

1054 
unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)] 

1055 
by simp 

1056 
finally have "a$n = ((1  ?X) * ?sa) $ n" by simp} 

1057 
ultimately have "a$n = ((1  ?X) * ?sa) $ n" by blast} 

30488  1058 
then show ?thesis 
29687  1059 
unfolding fps_eq_iff by blast 
1060 
qed 

1061 

1062 
lemma fps_divide_X_minus1_setsum: 

1063 
"a /((1::('a::field) fps)  X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" 

1064 
proof 

1065 
let ?X = "1  (X::('a::field) fps)" 

1066 
have th0: "?X $ 0 \<noteq> 0" by simp 

1067 
have "a /?X = ?X * Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) * inverse ?X" 

1068 
using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0 

1069 
by (simp add: fps_divide_def mult_assoc) 

1070 
also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) " 

1071 
by (simp add: mult_ac) 

1072 
finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) 

1073 
qed 

1074 

30488  1075 
subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary 
29687  1076 
finite product of FPS, also the relvant instance of powers of a FPS*} 
1077 

1078 
definition "natpermute n k = {l:: nat list. length l = k \<and> foldl op + 0 l = n}" 

1079 

1080 
lemma natlist_trivial_1: "natpermute n 1 = {[n]}" 

1081 
apply (auto simp add: natpermute_def) 

1082 
apply (case_tac x, auto) 

1083 
done 

1084 

30488  1085 
lemma foldl_add_start0: 
29687  1086 
"foldl op + x xs = x + foldl op + (0::nat) xs" 
1087 
apply (induct xs arbitrary: x) 

1088 
apply simp 

1089 
unfolding foldl.simps 

1090 
apply atomize 

1091 
apply (subgoal_tac "\<forall>x\<Colon>nat. foldl op + x xs = x + foldl op + (0\<Colon>nat) xs") 

1092 
apply (erule_tac x="x + a" in allE) 

1093 
apply (erule_tac x="a" in allE) 

1094 
apply simp 

1095 
apply assumption 

1096 
done 

1097 

1098 
lemma foldl_add_append: "foldl op + (x::nat) (xs@ys) = foldl op + x xs + foldl op + 0 ys" 

1099 
apply (induct ys arbitrary: x xs) 

1100 
apply auto 

1101 
apply (subst (2) foldl_add_start0) 

1102 
apply simp 

1103 
apply (subst (2) foldl_add_start0) 

1104 
by simp 

1105 

1106 
lemma foldl_add_setsum: "foldl op + (x::nat) xs = x + setsum (nth xs) {0..<length xs}" 

1107 
proof(induct xs arbitrary: x) 

1108 
case Nil thus ?case by simp 

1109 
next 

1110 
case (Cons a as x) 

1111 
have eq: "setsum (op ! (a#as)) {1..<length (a#as)} = setsum (op ! as) {0..<length as}" 

1112 
apply (rule setsum_reindex_cong [where f=Suc]) 

1113 
by (simp_all add: inj_on_def) 

1114 
have f: "finite {0}" "finite {1 ..< length (a#as)}" by simp_all 

1115 
have d: "{0} \<inter> {1..<length (a#as)} = {}" by simp 

1116 
have seq: "{0} \<union> {1..<length(a#as)} = {0 ..<length (a#as)}" by auto 

1117 
have "foldl op + x (a#as) = x + foldl op + a as " 

1118 
apply (subst foldl_add_start0) by simp 

1119 
also have "\<dots> = x + a + setsum (op ! as) {0..<length as}" unfolding Cons.hyps by simp 

1120 
also have "\<dots> = x + setsum (op ! (a#as)) {0..<length (a#as)}" 

30488  1121 
unfolding eq[symmetric] 
29687  1122 
unfolding setsum_Un_disjoint[OF f d, unfolded seq] 
1123 
by simp 

1124 
finally show ?case . 

1125 
qed 

1126 

1127 

1128 
lemma append_natpermute_less_eq: 

1129 
assumes h: "xs@ys \<in> natpermute n k" shows "foldl op + 0 xs \<le> n" and "foldl op + 0 ys \<le> n" 

1130 
proof 

1131 
{from h have "foldl op + 0 (xs@ ys) = n" by (simp add: natpermute_def) 

1132 
hence "foldl op + 0 xs + foldl op + 0 ys = n" unfolding foldl_add_append .} 

1133 
note th = this 

1134 
{from th show "foldl op + 0 xs \<le> n" by simp} 

1135 
{from th show "foldl op + 0 ys \<le> n" by simp} 

1136 
qed 

1137 

1138 
lemma natpermute_split: 

1139 
assumes mn: "h \<le> k" 

1140 
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 "?L = (\<Union>m \<in>{0..n}. ?S m)") 

1141 
proof 

30488  1142 
{fix l assume l: "l \<in> ?R" 
29687  1143 
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 
1144 
from xs have xs': "foldl op + 0 xs = m" by (simp add: natpermute_def) 

1145 
from ys have ys': "foldl op + 0 ys = n  m" by (simp add: natpermute_def) 

30488  1146 
have "l \<in> ?L" using leq xs ys h 
29687  1147 
apply simp 
1148 
apply (clarsimp simp add: natpermute_def simp del: foldl_append) 

1149 
apply (simp add: foldl_add_append[unfolded foldl_append]) 

1150 
unfolding xs' ys' 

30488  1151 
using mn xs ys 
29687  1152 
unfolding natpermute_def by simp} 
1153 
moreover 

1154 
{fix l assume l: "l \<in> natpermute n k" 

1155 
let ?xs = "take h l" 

1156 
let ?ys = "drop h l" 

1157 
let ?m = "foldl op + 0 ?xs" 

1158 
from l have ls: "foldl op + 0 (?xs @ ?ys) = n" by (simp add: natpermute_def) 

30488  1159 
have xs: "?xs \<in> natpermute ?m h" using l mn by (simp add: natpermute_def) 
29687  1160 
have ys: "?ys \<in> natpermute (n  ?m) (k  h)" using l mn ls[unfolded foldl_add_append] 
1161 
by (simp add: natpermute_def) 

1162 
from ls have m: "?m \<in> {0..n}" unfolding foldl_add_append by simp 

30488  1163 
from xs ys ls have "l \<in> ?R" 
29687  1164 
apply auto 
1165 
apply (rule bexI[where x = "?m"]) 

1166 
apply (rule exI[where x = "?xs"]) 

1167 
apply (rule exI[where x = "?ys"]) 

30488  1168 
using ls l unfolding foldl_add_append 
29687  1169 
by (auto simp add: natpermute_def)} 
1170 
ultimately show ?thesis by blast 

1171 
qed 

1172 

1173 
lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" 

1174 
by (auto simp add: natpermute_def) 

1175 
lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" 

1176 
apply (auto simp add: set_replicate_conv_if natpermute_def) 

1177 
apply (rule nth_equalityI) 

1178 
by simp_all 

1179 

1180 
lemma natpermute_finite: "finite (natpermute n k)" 

1181 
proof(induct k arbitrary: n) 

30488  1182 
case 0 thus ?case 
29687  1183 
apply (subst natpermute_split[of 0 0, simplified]) 
1184 
by (simp add: natpermute_0) 

1185 
next 

1186 
case (Suc k) 

1187 
then show ?case unfolding natpermute_split[of k "Suc k", simplified] 

1188 
apply  

1189 
apply (rule finite_UN_I) 

1190 
apply simp 

1191 
unfolding One_nat_def[symmetric] natlist_trivial_1 

1192 
apply simp 

1193 
unfolding image_Collect[symmetric] 

1194 
unfolding Collect_def mem_def 

1195 
apply (rule finite_imageI) 

1196 
apply blast 

1197 
done 

1198 
qed 

1199 

1200 
lemma natpermute_contain_maximal: 

1201 
"{xs \<in> natpermute n (k+1). n \<in> set xs} = UNION {0 .. k} (\<lambda>i. {(replicate (k+1) 0) [i:=n]})" 

1202 
(is "?A = ?B") 

1203 
proof 

1204 
{fix xs assume H: "xs \<in> natpermute n (k+1)" and n: "n \<in> set xs" 

1205 
from n obtain i where i: "i \<in> {0.. k}" "xs!i = n" using H 

30488  1206 
unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def) 
29687  1207 
have eqs: "({0..k}  {i}) \<union> {i} = {0..k}" using i by auto 
1208 
have f: "finite({0..k}  {i})" "finite {i}" by auto 

1209 
have d: "({0..k}  {i}) \<inter> {i} = {}" using i by auto 

1210 
from H have "n = setsum (nth xs) {0..k}" apply (simp add: natpermute_def) 

1211 
unfolding foldl_add_setsum by (auto simp add: atLeastLessThanSuc_atLeastAtMost) 

1212 
also have "\<dots> = n + setsum (nth xs) ({0..k}  {i})" 

1213 
unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp 

1214 
finally have zxs: "\<forall> j\<in> {0..k}  {i}. xs!j = 0" by auto 

1215 
from H have xsl: "length xs = k+1" by (simp add: natpermute_def) 

1216 
from i have i': "i < length (replicate (k+1) 0)" "i < k+1" 

1217 
unfolding length_replicate by arith+ 

1218 
have "xs = replicate (k+1) 0 [i := n]" 

1219 
apply (rule nth_equalityI) 

1220 
unfolding xsl length_list_update length_replicate 

1221 
apply simp 

1222 
apply clarify 

1223 
unfolding nth_list_update[OF i'(1)] 

1224 
using i zxs 

1225 
by (case_tac "ia=i", auto simp del: replicate.simps) 

1226 
then have "xs \<in> ?B" using i by blast} 

1227 
moreover 

1228 
{fix i assume i: "i \<in> {0..k}" 

1229 
let ?xs = "replicate (k+1) 0 [i:=n]" 

1230 
have nxs: "n \<in> set ?xs" 

1231 
apply (rule set_update_memI) using i by simp 

1232 
have xsl: "length ?xs = k+1" by (simp only: length_replicate length_list_update) 

1233 
have "foldl op + 0 ?xs = setsum (nth ?xs) {0..<k+1}" 

1234 
unfolding foldl_add_setsum add_0 length_replicate length_list_update .. 

1235 
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}" 

1236 
apply (rule setsum_cong2) by (simp del: replicate.simps) 

1237 
also have "\<dots> = n" using i by (simp add: setsum_delta) 

30488  1238 
finally 
29687  1239 
have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def 
1240 
by blast 

1241 
then have "?xs \<in> ?A" using nxs by blast} 

1242 
ultimately show ?thesis by auto 

1243 
qed 

1244 

30488  1245 
(* The general form *) 
29687  1246 
lemma fps_setprod_nth: 
1247 
fixes m :: nat and a :: "nat \<Rightarrow> ('a::comm_ring_1) fps" 

1248 
shows "(setprod a {0 .. m})$n = setsum (\<lambda>v. setprod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))" 

1249 
(is "?P m n") 

1250 
proof(induct m arbitrary: n rule: nat_less_induct) 

1251 
fix m n assume H: "\<forall>m' < m. \<forall>n. ?P m' n" 

1252 
{assume m0: "m = 0" 

1253 
hence "?P m n" apply simp 

1254 
unfolding natlist_trivial_1[where n = n, unfolded One_nat_def] by simp} 

1255 
moreover 

1256 
{fix k assume k: "m = Suc k" 

1257 
have km: "k < m" using k by arith 

1258 
have u0: "{0 .. k} \<union> {m} = {0..m}" using k apply (simp add: expand_set_eq) by presburger 

1259 
have f0: "finite {0 .. k}" "finite {m}" by auto 

1260 
have d0: "{0 .. k} \<inter> {m} = {}" using k by auto 

1261 
have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n" 

1262 
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0] by simp 

1263 
also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). \<Prod>j\<in>{0..k}. a j $ v ! j) * a m $ (n  i))" 

1264 
unfolding fps_mult_nth H[rule_format, OF km] .. 

1265 
also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)" 

1266 
apply (simp add: k) 

1267 
unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k] 

1268 
apply (subst setsum_UN_disjoint) 

30488  1269 
apply simp 
29687  1270 
apply simp 
1271 
unfolding image_Collect[symmetric] 

1272 
apply clarsimp 

1273 
apply (rule finite_imageI) 

1274 
apply (rule natpermute_finite) 

1275 
apply (clarsimp simp add: expand_set_eq) 

1276 
apply auto 

1277 
apply (rule setsum_cong2) 

1278 
unfolding setsum_left_distrib 

1279 
apply (rule sym) 

1280 
apply (rule_tac f="\<lambda>xs. xs @[n  x]" in setsum_reindex_cong) 

1281 
apply (simp add: inj_on_def) 

1282 
apply auto 

1283 
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k] 

1284 
apply (clarsimp simp add: natpermute_def nth_append) 

1285 
apply (rule_tac f="\<lambda>x. x * a (Suc k) $ (n  foldl op + 0 aa)" in cong[OF refl]) 

1286 
apply (rule setprod_cong) 

1287 
apply simp 

1288 
apply simp 

1289 
done 

1290 
finally have "?P m n" .} 

1291 
ultimately show "?P m n " by (cases m, auto) 

1292 
qed 

1293 

1294 
text{* The special form for powers *} 

1295 
lemma fps_power_nth_Suc: 

1296 
fixes m :: nat and a :: "('a::comm_ring_1) fps" 

1297 
shows "(a ^ Suc m)$n = setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))" 

1298 
proof 

1299 
have f: "finite {0 ..m}" by simp 

1300 
have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp 

1301 
show ?thesis unfolding th0 fps_setprod_nth .. 

1302 
qed 

1303 
lemma fps_power_nth: 

1304 
fixes m :: nat and a :: "('a::comm_ring_1) fps" 

1305 
shows "(a ^m)$n = (if m=0 then 1$n else setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m  1}) (natpermute n m))" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29915
diff
changeset

1306 
by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc) 
29687  1307 

30488  1308 
lemma fps_nth_power_0: 
29687  1309 
fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps" 
1310 
shows "(a ^m)$0 = (a$0) ^ m" 

1311 
proof 

1312 
{assume "m=0" hence ?thesis by simp} 

1313 
moreover 

1314 
{fix n assume m: "m = Suc n" 

1315 
have c: "m = card {0..n}" using m by simp 

1316 
have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29915
diff
changeset

1317 
apply (simp add: m fps_power_nth del: replicate.simps power_Suc) 
29687  1318 
apply (rule setprod_cong) 
1319 
by (simp_all del: replicate.simps) 

1320 
also have "\<dots> = (a$0) ^ m" 

1321 
unfolding c by (rule setprod_constant, simp) 

1322 
finally have ?thesis .} 

1323 
ultimately show ?thesis by (cases m, auto) 

1324 
qed 

1325 

30488  1326 
lemma fps_compose_inj_right: 
29687  1327 
assumes a0: "a$0 = (0::'a::{recpower,idom})" 
1328 
and a1: "a$1 \<noteq> 0" 

1329 
shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs") 

1330 
proof 

1331 
{assume ?rhs then have "?lhs" by simp} 

1332 
moreover 

1333 
{assume h: ?lhs 

30488  1334 
{fix n have "b$n = c$n" 
29687  1335 
proof(induct n rule: nat_less_induct) 
1336 
fix n assume H: "\<forall>m<n. b$m = c$m" 

1337 
{assume n0: "n=0" 

1338 
from h have "(b oo a)$n = (c oo a)$n" by simp 

1339 
hence "b$n = c$n" using n0 by (simp add: fps_compose_nth)} 

1340 
moreover 

1341 
{fix n1 assume n1: "n = Suc n1" 

1342 
have f: "finite {0 .. n1}" "finite {n}" by simp_all 

1343 
have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using n1 by auto 
