author  wenzelm 
Wed, 07 Aug 2013 21:16:20 +0200  
changeset 52902  7196e1ce1cd8 
parent 52891  b8dede3a4f1d 
child 52903  6c89225ddeba 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Formal_Power_Series.thy 
29687  2 
Author: Amine Chaieb, University of Cambridge 
3 
*) 

4 

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

6 

7 
theory Formal_Power_Series 

51542  8 
imports Binomial 
29687  9 
begin 
10 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

11 

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

49834  14 
typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}" 
29911
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)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

21 
by (simp add: fps_nth_inject [symmetric] fun_eq_iff) 
29911
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 

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

29687  31 

36409  32 
instantiation fps :: (zero) zero 
29687  33 
begin 
34 

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

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

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

37 

29687  38 
instance .. 
39 
end 

40 

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

41 
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

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

43 

36409  44 
instantiation fps :: ("{one, zero}") one 
29687  45 
begin 
46 

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

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

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

49 

29687  50 
instance .. 
51 
end 

52 

30488  53 
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

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

55 

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

58 

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

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

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

61 

29687  62 
instance .. 
63 
end 

64 

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

65 
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

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

67 

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

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

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

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

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

73 

29687  74 
instance .. 
75 
end 

76 

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

77 
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

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

79 

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

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

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

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

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

85 

29687  86 
instance .. 
87 
end 

88 

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

89 
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

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

91 

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

94 

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

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

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

97 

29687  98 
instance .. 
99 
end 

100 

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

101 
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

102 
unfolding fps_times_def by simp 
29687  103 

52891  104 
declare atLeastAtMost_iff [presburger] 
105 
declare Bex_def [presburger] 

106 
declare Ball_def [presburger] 

29687  107 

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

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

111 
by simp 

112 

113 
lemma mult_delta_right: 

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

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

116 
by simp 

117 

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

52891  120 

29687  121 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" 
122 
by auto 

123 

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

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

127 
instance fps :: (semigroup_add) semigroup_add 
29687  128 
proof 
52891  129 
fix a b c :: "'a fps" 
130 
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

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

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

133 

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

134 
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

135 
proof 
52891  136 
fix a b :: "'a fps" 
137 
show "a + b = b + a" 

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

138 
by (simp add: fps_ext add_commute) 
29687  139 
qed 
140 

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

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

142 
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

143 
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

144 
(\<Sum>j=0..k. \<Sum>i=0..k  j. f j i (n  j  i))" 
52902  145 
by (induct k) (simp_all add: Suc_diff_le setsum_addf add_assoc) 
29687  146 

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

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

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

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

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

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

153 
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

154 
(\<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

155 
by (rule fps_mult_assoc_lemma) 
52891  156 
then show "((a * b) * c) $ n = (a * (b * c)) $ n" 
157 
by (simp add: fps_mult_nth setsum_right_distrib setsum_left_distrib mult_assoc) 

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

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

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

160 

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

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

162 
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

163 
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

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

165 
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

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

167 
show "{0..n} = (\<lambda>i. n  i) ` {0..n}" 
52902  168 
apply auto 
169 
apply (rule_tac x = "n  x" in image_eqI) 

170 
apply simp_all 

171 
done 

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

172 
next 
52891  173 
fix i 
174 
assume "i \<in> {0..n}" 

175 
then have "n  (n  i) = i" by simp 

176 
then show "f (n  i) i = f (n  i) (n  (n  i))" by simp 

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

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

178 

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

179 
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

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

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

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

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

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

185 
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

186 
by (rule fps_mult_commute_lemma) 
52891  187 
then show "(a * b) $ n = (b * a) $ n" 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

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

191 

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

192 
instance fps :: (monoid_add) monoid_add 
29687  193 
proof 
52891  194 
fix a :: "'a fps" 
195 
show "0 + a = a" by (simp add: fps_ext) 

196 
show "a + 0 = a" by (simp add: fps_ext) 

29687  197 
qed 
198 

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

199 
instance fps :: (comm_monoid_add) comm_monoid_add 
29687  200 
proof 
52891  201 
fix a :: "'a fps" 
202 
show "0 + a = a" by (simp add: fps_ext) 

29687  203 
qed 
204 

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

205 
instance fps :: (semiring_1) monoid_mult 
29687  206 
proof 
52891  207 
fix a :: "'a fps" 
52902  208 
show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum_delta) 
209 
show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum_delta') 

29687  210 
qed 
211 

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

212 
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

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

214 
fix a b c :: "'a fps" 
52891  215 
{ assume "a + b = a + c" then show "b = c" by (simp add: expand_fps_eq) } 
216 
{ assume "b + a = c + a" then show "b = c" by (simp add: expand_fps_eq) } 

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

217 
qed 
29687  218 

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

219 
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

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

221 
fix a b c :: "'a fps" 
52891  222 
assume "a + b = a + c" 
223 
then show "b = c" by (simp add: expand_fps_eq) 

29911
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_comm_monoid_add) cancel_comm_monoid_add .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

227 

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

228 
instance fps :: (group_add) group_add 
29687  229 
proof 
52891  230 
fix a b :: "'a fps" 
231 
show " a + a = 0" by (simp add: fps_ext) 

232 
show "a  b = a +  b" by (simp add: fps_ext diff_minus) 

29687  233 
qed 
234 

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

235 
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

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

237 
fix a b :: "'a fps" 
52891  238 
show " a + a = 0" by (simp add: fps_ext) 
239 
show "a  b = a +  b" by (simp add: fps_ext) 

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

240 
qed 
29687  241 

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

242 
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

243 
by default (simp add: expand_fps_eq) 
29687  244 

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

245 
instance fps :: (semiring_0) semiring 
29687  246 
proof 
247 
fix a b c :: "'a fps" 

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

248 
show "(a + b) * c = a * c + b * c" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

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

250 
show "a * (b + c) = a * b + a * c" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

251 
by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum_addf) 
29687  252 
qed 
253 

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

254 
instance fps :: (semiring_0) semiring_0 
29687  255 
proof 
52891  256 
fix a:: "'a fps" 
257 
show "0 * a = 0" by (simp add: fps_ext fps_mult_nth) 

258 
show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth) 

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

260 

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

261 
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

262 

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

265 
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

266 
by (simp add: expand_fps_eq) 
29687  267 

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

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

270 
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

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

272 
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

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

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

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

276 
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

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

278 
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

279 
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

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

281 
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

282 
then show "f \<noteq> 0" by (auto simp add: expand_fps_eq) 
29687  283 
qed 
284 

285 
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

286 
by (rule expand_fps_eq) 
29687  287 

52891  288 
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

289 
proof (cases "finite S") 
52891  290 
case True 
291 
then show ?thesis by (induct set: finite) auto 

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

292 
next 
52891  293 
case False 
294 
then show ?thesis by simp 

29687  295 
qed 
296 

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

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

300 

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

301 
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

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

303 

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

304 
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

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

306 

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

307 
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

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

309 

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

310 
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

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

312 

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

313 
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

314 
by (simp add: fps_ext) 
52891  315 

31369
8b460fd12100
Reverses idempotent; radical of E; generalized logarithm;
chaieb
parents:
31199
diff
changeset

316 
lemma fps_const_sub [simp]: "fps_const (c::'a\<Colon>group_add)  fps_const d = fps_const (c  d)" 
8b460fd12100
Reverses idempotent; radical of E; generalized logarithm;
chaieb
parents:
31199
diff
changeset

317 
by (simp add: fps_ext) 
52891  318 

29687  319 
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

320 
by (simp add: fps_eq_iff fps_mult_nth setsum_0') 
29687  321 

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

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

325 

48757  326 
lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = 
327 
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

328 
by (simp add: fps_ext) 
29687  329 

330 
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

331 
unfolding fps_eq_iff fps_mult_nth 
29913  332 
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

333 

29687  334 
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

335 
unfolding fps_eq_iff fps_mult_nth 
29913  336 
by (simp add: fps_const_def mult_delta_right setsum_delta') 
29687  337 

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

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

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

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

29906  344 
subsection {* Formal power series form an integral domain*} 
29687  345 

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

346 
instance fps :: (ring) ring .. 
29687  347 

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

348 
instance fps :: (ring_1) ring_1 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

349 
by (intro_classes, auto simp add: diff_minus distrib_right) 
29687  350 

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

351 
instance fps :: (comm_ring_1) comm_ring_1 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49834
diff
changeset

352 
by (intro_classes, auto simp add: diff_minus distrib_right) 
29687  353 

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

354 
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors 
29687  355 
proof 
356 
fix a b :: "'a fps" 

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

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

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

360 
by blast+ 

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

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

363 
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

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

365 
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

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

367 
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

368 
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

369 
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

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

371 
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

372 
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

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

376 

36311
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

377 
instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. 
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

378 

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

379 
instance fps :: (idom) idom .. 
29687  380 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

381 
lemma numeral_fps_const: "numeral k = fps_const (numeral k)" 
48757  382 
by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

383 
fps_const_add [symmetric]) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

384 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

385 
lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

386 
by (simp only: neg_numeral_def numeral_fps_const fps_const_neg) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46757
diff
changeset

387 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

388 
subsection{* The eXtractor series X*} 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

389 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

390 
lemma minus_one_power_iff: "( (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else  1)" 
48757  391 
by (induct n) auto 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

392 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

393 
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

394 
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n  1))" 
52902  395 
proof  
396 
{ 

397 
assume n: "n \<noteq> 0" 

398 
have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n  i))" 

399 
by (simp add: fps_mult_nth) 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

400 
also have "\<dots> = f $ (n  1)" 
46757  401 
using n by (simp add: X_def mult_delta_left setsum_delta) 
52902  402 
finally have ?thesis using n by simp 
403 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

404 
moreover 
52902  405 
{ 
406 
assume n: "n=0" 

407 
hence ?thesis by (simp add: fps_mult_nth X_def) 

408 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

409 
ultimately show ?thesis by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

410 
qed 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

411 

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

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

414 
by (metis X_mult_nth mult_commute) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

415 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

416 
lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)" 
52902  417 
proof (induct k) 
418 
case 0 

419 
thus ?case by (simp add: X_def fps_eq_iff) 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

420 
next 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

421 
case (Suc k) 
52891  422 
{ 
423 
fix m 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

424 
have "(X^Suc k) $ m = (if m = 0 then (0::'a) else (X^k) $ (m  1))" 
52891  425 
by (simp del: One_nat_def) 
426 
then have "(X^Suc k) $ m = (if m = Suc k then (1::'a) else 0)" 

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

428 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

429 
then show ?case by (simp add: fps_eq_iff) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

430 
qed 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

431 

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

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

434 
apply (induct k arbitrary: n) 
52891  435 
apply simp 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

436 
unfolding power_Suc mult_assoc 
48757  437 
apply (case_tac n) 
438 
apply auto 

439 
done 

440 

441 
lemma X_power_mult_right_nth: 

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

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

443 
by (metis X_power_mult_nth mult_commute) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

444 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

445 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

446 
subsection{* Formal Power series form a metric space *} 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

447 

52902  448 
definition (in dist) "ball x r = {y. dist y x < r}" 
48757  449 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

450 
instantiation fps :: (comm_ring_1) dist 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

451 
begin 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

452 

52891  453 
definition 
454 
dist_fps_def: "dist (a::'a fps) b = 

455 
(if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

456 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

457 
lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

458 
by (simp add: dist_fps_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

459 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

460 
lemma dist_fps_sym: "dist (a::'a fps) b = dist b a" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

461 
apply (auto simp add: dist_fps_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

462 
apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"]) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

463 
apply (rule ext) 
48757  464 
apply auto 
465 
done 

466 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

467 
instance .. 
48757  468 

30746  469 
end 
470 

52902  471 
lemma fps_nonzero_least_unique: 
472 
assumes a0: "a \<noteq> 0" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

473 
shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> 0) n" 
52891  474 
proof  
475 
from fps_nonzero_nth_minimal [of a] a0 

476 
obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast 

477 
then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n" 

478 
by (auto simp add: leastP_def setge_def not_le [symmetric]) 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

479 
moreover 
52891  480 
{ 
481 
fix m 

482 
assume "leastP (\<lambda>n. a $ n \<noteq> 0) m" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

483 
then have "m = n" using ln 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

484 
apply (auto simp add: leastP_def setge_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

485 
apply (erule allE[where x=n]) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

486 
apply (erule allE[where x=m]) 
52891  487 
apply simp 
488 
done 

489 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

490 
ultimately show ?thesis by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

491 
qed 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

492 

48757  493 
lemma fps_eq_least_unique: 
494 
assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

495 
shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n" 
48757  496 
using fps_nonzero_least_unique[of "a  b"] ab 
497 
by auto 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

498 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

499 
instantiation fps :: (comm_ring_1) metric_space 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

500 
begin 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

501 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

502 
definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

503 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

504 
instance 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

505 
proof 
52891  506 
fix S :: "'a fps set" 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

507 
show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

508 
by (auto simp add: open_fps_def ball_def subset_eq) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

509 
next 
48757  510 
{ 
511 
fix a b :: "'a fps" 

512 
{ 

52891  513 
assume "a = b" 
514 
then have "\<not> (\<exists>n. a $ n \<noteq> b $ n)" by simp 

48757  515 
then have "dist a b = 0" by (simp add: dist_fps_def) 
516 
} 

517 
moreover 

518 
{ 

519 
assume d: "dist a b = 0" 

52891  520 
then have "\<forall>n. a$n = b$n" 
48757  521 
by  (rule ccontr, simp add: dist_fps_def) 
522 
then have "a = b" by (simp add: fps_eq_iff) 

523 
} 

524 
ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast 

525 
} 

526 
note th = this 

527 
from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

528 
fix a b c :: "'a fps" 
48757  529 
{ 
52891  530 
assume "a = b" 
531 
then have "dist a b = 0" unfolding th . 

532 
then have "dist a b \<le> dist a c + dist b c" 

533 
using dist_fps_ge0 [of a c] dist_fps_ge0 [of b c] by simp 

48757  534 
} 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

535 
moreover 
48757  536 
{ 
52891  537 
assume "c = a \<or> c = b" 
48757  538 
then have "dist a b \<le> dist a c + dist b c" 
52891  539 
by (cases "c = a") (simp_all add: th dist_fps_sym) 
48757  540 
} 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

541 
moreover 
52891  542 
{ 
543 
assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

544 
let ?P = "\<lambda>a b n. a$n \<noteq> b$n" 
52891  545 
from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac] 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

546 
fps_eq_least_unique[OF bc] 
52891  547 
obtain nab nac nbc where nab: "leastP (?P a b) nab" 
548 
and nac: "leastP (?P a c) nac" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

549 
and nbc: "leastP (?P b c) nbc" by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

550 
from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

551 
by (auto simp add: leastP_def setge_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

552 
from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

553 
by (auto simp add: leastP_def setge_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

554 
from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

555 
by (auto simp add: leastP_def setge_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

556 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

557 
have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

558 
by (simp add: fps_eq_iff) 
52891  559 
from ab ac bc nab nac nbc 
560 
have dab: "dist a b = inverse (2 ^ nab)" 

561 
and dac: "dist a c = inverse (2 ^ nac)" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

562 
and dbc: "dist b c = inverse (2 ^ nbc)" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

563 
unfolding th0 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

564 
apply (simp_all add: dist_fps_def) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

565 
apply (erule the1_equality[OF fps_eq_least_unique[OF ab]]) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

566 
apply (erule the1_equality[OF fps_eq_least_unique[OF ac]]) 
52891  567 
apply (erule the1_equality[OF fps_eq_least_unique[OF bc]]) 
568 
done 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

569 
from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

570 
unfolding th by simp_all 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

571 
from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" 
52891  572 
using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

573 
by auto 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

574 
have th1: "\<And>n. (2::real)^n >0" by auto 
52891  575 
{ 
576 
assume h: "dist a b > dist a c + dist b c" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

577 
then have gt: "dist a b > dist a c" "dist a b > dist b c" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

578 
using pos by auto 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

579 
from gt have gtn: "nab < nbc" "nab < nac" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

580 
unfolding dab dbc dac by (auto simp add: th1) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

581 
from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)] 
52891  582 
have "a $ nab = b $ nab" by simp 
583 
with nab'(2) have False by simp 

584 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

585 
then have "dist a b \<le> dist a c + dist b c" 
52891  586 
by (auto simp add: not_le[symmetric]) 
587 
} 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

588 
ultimately show "dist a b \<le> dist a c + dist b c" by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

589 
qed 
52891  590 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

591 
end 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

592 

0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

593 
text{* The infinite sums and justification of the notation in textbooks*} 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

594 

52891  595 
lemma reals_power_lt_ex: 
596 
assumes xp: "x > 0" and y1: "(y::real) > 1" 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

597 
shows "\<exists>k>0. (1/y)^k < x" 
52891  598 
proof  
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

599 
have yp: "y > 0" using y1 by simp 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

600 
from reals_Archimedean2[of "max 0 ( log y x) + 1"] 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

601 
obtain k::nat where k: "real k > max 0 ( log y x) + 1" by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

602 
from k have kp: "k > 0" by simp 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

603 
from k have "real k >  log y x" by simp 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

604 
then have "ln y * real k >  ln x" unfolding log_def 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

605 
using ln_gt_zero_iff[OF yp] y1 
36350  606 
by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric]) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

607 
then have "ln y * real k + ln x > 0" by simp 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

608 
then have "exp (real k * ln y + ln x) > exp 0" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

609 
by (simp add: mult_ac) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

610 
then have "y ^ k * x > 1" 
52891  611 
unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp] 
612 
by simp 

613 
then have "x > (1 / y)^k" using yp 

36350  614 
by (simp add: field_simps nonzero_power_divide) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

615 
then show ?thesis using kp by blast 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

616 
qed 
52891  617 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

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

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

620 
lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else (0::'a::comm_ring_1))" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

621 
by (simp add: X_power_iff) 
52891  622 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

623 

48757  624 
lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a$i)*X^i) {0..m})$n = 
625 
(if n \<le> m then a$n else (0::'a::comm_ring_1))" 

52891  626 
apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong) 
48757  627 
apply (simp add: setsum_delta') 
628 
done 

52891  629 

52902  630 
lemma fps_notation: "(%n. setsum (%i. fps_const(a$i) * X^i) {0..n}) > a" 
631 
(is "?s > a") 

52891  632 
proof  
633 
{ 

634 
fix r:: real 

635 
assume rp: "r > 0" 

636 
have th0: "(2::real) > 1" by simp 

637 
from reals_power_lt_ex[OF rp th0] 

638 
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast 

639 
{ 

640 
fix n::nat 

641 
assume nn0: "n \<ge> n0" 

642 
then have thnn0: "(1/2)^n <= (1/2 :: real)^n0" 

643 
by (auto intro: power_decreasing) 

644 
{ 

645 
assume "?s n = a" 

646 
then have "dist (?s n) a < r" 

647 
unfolding dist_eq_0_iff[of "?s n" a, symmetric] 

648 
using rp by (simp del: dist_eq_0_iff) 

649 
} 

650 
moreover 

651 
{ 

652 
assume neq: "?s n \<noteq> a" 

653 
from fps_eq_least_unique[OF neq] 

654 
obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast 

655 
have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)" 

656 
by (simp add: fps_eq_iff) 

657 
from neq have dth: "dist (?s n) a = (1/2)^k" 

658 
unfolding th0 dist_fps_def 

659 
unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k] 

660 
by (auto simp add: inverse_eq_divide power_divide) 

661 

662 
from k have kn: "k > n" 

663 
by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm) 

664 
then have "dist (?s n) a < (1/2)^n" unfolding dth 

665 
by (auto intro: power_strict_decreasing) 

666 
also have "\<dots> <= (1/2)^n0" using nn0 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

667 
by (auto intro: power_decreasing) 
52891  668 
also have "\<dots> < r" using n0 by simp 
669 
finally have "dist (?s n) a < r" . 

670 
} 

671 
ultimately have "dist (?s n) a < r" by blast 

672 
} 

673 
then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r " by blast 

674 
} 

675 
then show ?thesis unfolding LIMSEQ_def by blast 

676 
qed 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

677 

29906  678 
subsection{* Inverses of formal power series *} 
29687  679 

680 
declare setsum_cong[fundef_cong] 

681 

36311
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

682 
instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse 
29687  683 
begin 
684 

52891  685 
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" 
686 
where 

29687  687 
"natfun_inverse f 0 = inverse (f$0)" 
30488  688 
 "natfun_inverse f n =  inverse (f$0) * setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}" 
29687  689 

52891  690 
definition 
691 
fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" 

692 

693 
definition 

694 
fps_divide_def: "divide = (\<lambda>(f::'a fps) g. f * inverse g)" 

36311
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

695 

29687  696 
instance .. 
36311
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

697 

29687  698 
end 
699 

52891  700 
lemma fps_inverse_zero [simp]: 
29687  701 
"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

702 
by (simp add: fps_ext fps_inverse_def) 
29687  703 

52891  704 
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

705 
apply (auto simp add: expand_fps_eq fps_inverse_def) 
52891  706 
apply (case_tac n) 
707 
apply auto 

708 
done 

709 

710 
lemma inverse_mult_eq_1 [intro]: 

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

29687  712 
shows "inverse f * f = 1" 
52891  713 
proof  
29687  714 
have c: "inverse f * f = f * inverse f" by (simp add: mult_commute) 
30488  715 
from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n" 
29687  716 
by (simp add: fps_inverse_def) 
717 
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

718 
by (simp add: fps_mult_nth fps_inverse_def) 
52891  719 
{ 
720 
fix n :: nat 

721 
assume np: "n > 0" 

29687  722 
from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto 
723 
have d: "{0} \<inter> {1 .. n} = {}" by auto 

52891  724 
from f0 np have th0: " (inverse f $ n) = 
29687  725 
(setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}) / (f$0)" 
52891  726 
by (cases n) (simp_all add: divide_inverse fps_inverse_def) 
29687  727 
from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] 
52891  728 
have th1: "setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n} =  (f$0) * (inverse f)$n" 
36350  729 
by (simp add: field_simps) 
30488  730 
have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n  i))" 
29687  731 
unfolding fps_mult_nth ifn .. 
52891  732 
also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (ni))" 
46757  733 
by (simp add: eq) 
29687  734 
also have "\<dots> = 0" unfolding th1 ifn by simp 
52891  735 
finally have "(inverse f * f)$n = 0" unfolding c . 
736 
} 

29687  737 
with th0 show ?thesis by (simp add: fps_eq_iff) 
738 
qed 

739 

740 
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

741 
by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) 
29687  742 

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

52891  744 
proof  
745 
{ 

746 
assume "f$0 = 0" 

747 
then have "inverse f = 0" by (simp add: fps_inverse_def) 

748 
} 

29687  749 
moreover 
52891  750 
{ 
751 
assume h: "inverse f = 0" and c: "f $0 \<noteq> 0" 

752 
from inverse_mult_eq_1[OF c] h have False by simp 

753 
} 

29687  754 
ultimately show ?thesis by blast 
755 
qed 

756 

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

29687  759 
shows "inverse (inverse f) = f" 
52891  760 
proof  
29687  761 
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp 
30488  762 
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] 
52891  763 
have "inverse f * f = inverse f * inverse (inverse f)" 
764 
by (simp add: mult_ac) 

29687  765 
then show ?thesis using f0 unfolding mult_cancel_left by simp 
766 
qed 

767 

48757  768 
lemma fps_inverse_unique: 
52902  769 
assumes f0: "f$0 \<noteq> (0::'a::field)" 
770 
and fg: "f*g = 1" 

29687  771 
shows "inverse f = g" 
52891  772 
proof  
29687  773 
from inverse_mult_eq_1[OF f0] fg 
774 
have th0: "inverse f * f = g * f" by (simp add: mult_ac) 

775 
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

776 
by (auto simp add: expand_fps_eq) 
29687  777 
qed 
778 

30488  779 
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) 
52902  780 
= Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then  1 else 0)" 
29687  781 
apply (rule fps_inverse_unique) 
782 
apply simp 

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

783 
apply (simp add: fps_eq_iff fps_mult_nth) 
52891  784 
proof clarsimp 
785 
fix n :: nat 

786 
assume n: "n > 0" 

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

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

30488  790 
have th1: "setsum ?f {0..n} = setsum ?g {0..n}" 
29687  791 
by (rule setsum_cong2) auto 
30488  792 
have th2: "setsum ?g {0..n  1} = setsum ?h {0..n  1}" 
29687  793 
using n apply  by (rule setsum_cong2) auto 
794 
have eq: "{0 .. n} = {0.. n  1} \<union> {n}" by auto 

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

30488  798 
unfolding th1 
29687  799 
apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) 
800 
unfolding th2 

52891  801 
apply (simp add: setsum_delta) 
802 
done 

29687  803 
qed 
804 

29912  805 
subsection{* Formal Derivatives, and the MacLaurin theorem around 0*} 
29687  806 

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

808 

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

811 

812 
lemma fps_deriv_linear[simp]: 

813 
"fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = 

814 
fps_const a * fps_deriv f + fps_const b * fps_deriv g" 

36350  815 
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) 
29687  816 

30488  817 
lemma fps_deriv_mult[simp]: 
29687  818 
fixes f :: "('a :: comm_ring_1) fps" 
819 
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" 

52891  820 
proof  
29687  821 
let ?D = "fps_deriv" 
52891  822 
{ fix n::nat 
29687  823 
let ?Zn = "{0 ..n}" 
824 
let ?Zn1 = "{0 .. n + 1}" 

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

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

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

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

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

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

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

52891  832 
{ 
833 
fix k 

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

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

836 
} 

29687  837 
note th0 = this 
838 
have eq': "{0..n +1} {1 .. n+1} = {0}" by auto 

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

29687  841 
apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1  i"]) 
842 
apply (simp add: inj_on_def Ball_def) 

843 
apply presburger 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

844 
apply (rule set_eqI) 
29687  845 
apply (presburger add: image_iff) 
52891  846 
apply simp 
847 
done 

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

849 
setsum (\<lambda>i. f $ (n + 1  i) * g $ i) ?Zn1" 

29687  850 
apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1  i"]) 
851 
apply (simp add: inj_on_def Ball_def) 

852 
apply presburger 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

853 
apply (rule set_eqI) 
29687  854 
apply (presburger add: image_iff) 
52891  855 
apply simp 
856 
done 

857 
have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" 

858 
by (simp only: mult_commute) 

29687  859 
also have "\<dots> = (\<Sum>i = 0..n. ?g i)" 
860 
by (simp add: fps_mult_nth setsum_addf[symmetric]) 

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

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

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

864 
apply (rule setsum_mono_zero_left) 

865 
apply simp 

866 
apply (simp add: subset_eq) 

867 
unfolding eq' 

52891  868 
apply simp 
869 
done 

29687  870 
also have "\<dots> = (fps_deriv (f * g)) $ n" 
871 
apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf) 

872 
unfolding s0 s1 

873 
unfolding setsum_addf[symmetric] setsum_right_distrib 

874 
apply (rule setsum_cong2) 

52891  875 
apply (auto simp add: of_nat_diff field_simps) 
876 
done 

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

878 
} 

30488  879 
then show ?thesis unfolding fps_eq_iff by auto 
29687  880 
qed 
881 

31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

882 
lemma fps_deriv_X[simp]: "fps_deriv X = 1" 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

883 
by (simp add: fps_deriv_def X_def fps_eq_iff) 
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

884 

29687  885 
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

886 
by (simp add: fps_eq_iff fps_deriv_def) 
52891  887 

29687  888 
lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g" 
889 
using fps_deriv_linear[of 1 f 1 g] by simp 

890 

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

30488  892 
unfolding diff_minus by simp 
29687  893 

894 
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

895 
by (simp add: fps_ext fps_deriv_def fps_const_def) 
29687  896 

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

29687  899 
by simp 
900 

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

902 
by (simp add: fps_deriv_def fps_eq_iff) 

903 

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

905 
by (simp add: fps_deriv_def fps_eq_iff ) 

906 

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

29687  909 
by simp 
910 

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

52902  913 
proof  
52891  914 
{ 
915 
assume "\<not> finite S" 

916 
then have ?thesis by simp 

917 
} 

29687  918 
moreover 
48757  919 
{ 
920 
assume fS: "finite S" 

52891  921 
have ?thesis by (induct rule: finite_induct [OF fS]) simp_all 
48757  922 
} 
29687  923 
ultimately show ?thesis by blast 
924 
qed 

925 

52902  926 
lemma fps_deriv_eq_0_iff [simp]: 
48757  927 
"fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))" 
52902  928 
proof  
52891  929 
{ 
930 
assume "f = fps_const (f$0)" 

931 
then have "fps_deriv f = fps_deriv (fps_const (f$0))" by simp 

932 
then have "fps_deriv f = 0" by simp 

933 
} 

29687  934 
moreover 
52891  935 
{ 
936 
assume z: "fps_deriv f = 0" 

937 
then have "\<forall>n. (fps_deriv f)$n = 0" by simp 

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

939 
then have "f = fps_const (f$0)" 

29687  940 
apply (clarsimp simp add: fps_eq_iff fps_const_def) 
941 
apply (erule_tac x="n  1" in allE) 

52891  942 
apply simp 
943 
done 

944 
} 

29687  945 
ultimately show ?thesis by blast 
946 
qed 

947 

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

52891  951 
proof  
29687  952 
have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f  g) = 0" by simp 
953 
also have "\<dots> \<longleftrightarrow> f  g = fps_const ((fg)$0)" unfolding fps_deriv_eq_0_iff .. 

36350  954 
finally show ?thesis by (simp add: field_simps) 
29687  955 
qed 
956 

48757  957 
lemma fps_deriv_eq_iff_ex: 
958 
"(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)" 

52891  959 
apply auto 
960 
unfolding fps_deriv_eq_iff 

48757  961 
apply blast 
962 
done 

963 

964 

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

966 
where 

29687  967 
"fps_nth_deriv 0 f = f" 
968 
 "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" 

969 

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

48757  971 
by (induct n arbitrary: f) auto 
972 

973 
lemma fps_nth_deriv_linear[simp]: 

974 
"fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = 

975 
fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g" 

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

977 

978 
lemma fps_nth_deriv_neg[simp]: 

979 
"fps_nth_deriv n ( (f:: ('a:: comm_ring_1) fps)) =  (fps_nth_deriv n f)" 

980 
by (induct n arbitrary: f) simp_all 

981 

982 
lemma fps_nth_deriv_add[simp]: 

983 
"fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g" 

29687  984 
using fps_nth_deriv_linear[of n 1 f 1 g] by simp 
985 

48757  986 
lemma fps_nth_deriv_sub[simp]: 
987 
"fps_nth_deriv n ((f:: ('a::comm_ring_1) fps)  g) = fps_nth_deriv n f  fps_nth_deriv n g" 

30488  988 
unfolding diff_minus fps_nth_deriv_add by simp 
29687  989 

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

48757  991 
by (induct n) simp_all 
29687  992 

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

48757  994 
by (induct n) simp_all 
995 

996 
lemma fps_nth_deriv_const[simp]: 

997 
"fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)" 

998 
by (cases n) simp_all 

999 

1000 
lemma fps_nth_deriv_mult_const_left[simp]: 

1001 
"fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f" 

29687  1002 
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp 
1003 

48757  1004 
lemma fps_nth_deriv_mult_const_right[simp]: 
1005 
"fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c" 

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

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

52891  1010 
proof  
1011 
{ 

1012 
assume "\<not> finite S" 

1013 
then have ?thesis by simp 

1014 
} 

29687  1015 
moreover 
48757  1016 
{ 
1017 
assume fS: "finite S" 

52891  1018 
have ?thesis by (induct rule: finite_induct[OF fS]) simp_all 
48757  1019 
} 
29687  1020 
ultimately show ?thesis by blast 
1021 
qed 

1022 

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

36350  1025 
by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult) 
29687  1026 

29906  1027 
subsection {* Powers*} 
29687  1028 

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

48757  1030 
by (induct n) (auto simp add: expand_fps_eq fps_mult_nth) 
29687  1031 

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

52891  1033 
proof (induct n) 
1034 
case 0 

1035 
then show ?case by simp 

29687  1036 
next 
1037 
case (Suc n) 

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

30488  1039 
show ?case unfolding power_Suc fps_mult_nth 
52891  1040 
using h `a$0 = 1` fps_power_zeroth_eq_one[OF `a$0=1`] 
1041 
by (simp add: field_simps) 

29687  1042 
qed 
1043 

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

48757  1045 
by (induct n) (auto simp add: fps_mult_nth) 
29687  1046 

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

48757  1048 
by (induct n) (auto simp add: fps_mult_nth) 
29687  1049 

31021  1050 
lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n" 
52891  1051 
by (induct n) (auto simp add: fps_mult_nth) 
1052 

1053 
lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)" 

1054 
apply (rule iffI) 

1055 
apply (induct n) 

1056 
apply (auto simp add: fps_mult_nth) 

1057 
apply (rule startsby_zero_power, simp_all) 

1058 
done 

29687  1059 

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

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

29687  1067 
let ?ths = "\<forall>m<k. a ^ k $ m = 0" 
52891  1068 
{ assume "k = 0" then have ?ths by simp } 
29687  1069 
moreover 
52891  1070 
{ 
1071 
fix l 

1072 
assume k: "k = Suc l" 

1073 
{ 

1074 
fix m 

1075 
assume mk: "m < k" 

1076 
{ 

1077 
assume "m = 0" 

1078 
then have "a^k $ m = 0" 

1079 
using startsby_zero_power[of a k] k a0 by simp 

1080 
} 

29687  1081 
moreover 
52891  1082 
{ 
1083 
assume m0: "m \<noteq> 0" 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

1085 
also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m  i))" by (simp add: fps_mult_nth) 
52891  1086 
also have "\<dots> = 0" 
1087 
apply (rule setsum_0') 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

1088 
apply auto 
51489  1089 
apply (case_tac "x = m") 
52891  1090 
using a0 apply simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

1091 
apply (rule H[rule_format]) 
52891  1092 
using a0 k mk apply auto 
1093 
done 

1094 
finally have "a^k $ m = 0" . 

1095 
} 

1096 
ultimately have "a^k $ m = 0" by blast 

1097 
} 

1098 
then have ?ths by blast 

1099 
} 

1100 
ultimately show ?ths by (cases k) auto 

29687  1101 
qed 
1102 

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

1106 
apply (rule setsum_mono_zero_right) 

1107 
using kn apply auto 

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

52891  1109 
apply arith 
1110 
done 

1111 

1112 
lemma startsby_zero_power_nth_same: 

1113 
assumes a0: "a$0 = (0::'a::{idom})" 

29687  1114 
shows "a^n $ n = (a$1) ^ n" 
52891  1115 
proof (induct n) 
1116 
case 0 

52902  1117 
then show ?case by simp 
29687  1118 
next 
1119 
case (Suc n) 

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

1122 
by (simp add: fps_mult_nth) 

29687  1123 
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n  i)) {n .. Suc n}" 
1124 
apply (rule setsum_mono_zero_right) 

1125 
apply simp 

1126 
apply clarsimp 

1127 
apply clarsimp 

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

1129 
apply arith 

1130 
done 

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

52891  1132 
finally show ?case using Suc.hyps by simp 
29687  1133 
qed 
1134 

1135 
lemma fps_inverse_power: 

31021  1136 
fixes a :: "('a::{field}) fps" 
29687  1137 
shows "inverse (a^n) = inverse a ^ n" 
52891  1138 
proof  
1139 
{ 

1140 
assume a0: "a$0 = 0" 

1141 
then have eq: "inverse a = 0" by (simp add: fps_inverse_def) 

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

29687  1143 
moreover 
52891  1144 
{ 
1145 
assume n: "n > 0" 

30488  1146 
from startsby_zero_power[OF a0 n] eq a0 n have ?thesis 
52891  1147 
by (simp add: fps_inverse_def) 
1148 
} 

1149 
ultimately have ?thesis by blast 

1150 
} 

29687  1151 
moreover 
52891  1152 
{ 
1153 
assume a0: "a$0 \<noteq> 0" 

29687  1154 
have ?thesis 
1155 
apply (rule fps_inverse_unique) 

1156 
apply (simp add: a0) 

1157 
unfolding power_mult_distrib[symmetric] 

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

1159 
apply simp_all 

1160 
apply (subst mult_commute) 

52891  1161 
apply (rule inverse_mult_eq_1[OF a0]) 
1162 
done 

1163 
} 

29687  1164 
ultimately show ?thesis by blast 
1165 
qed 

1166 

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

1169 
apply (induct n) 

52891  1170 
apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add) 
48757  1171 
apply (case_tac n) 
52891  1172 
apply (auto simp add: field_simps) 
48757  1173 
done 
29687  1174 

30488  1175 
lemma fps_inverse_deriv: 
29687  1176 
fixes a:: "('a :: field) fps" 
1177 
assumes a0: "a$0 \<noteq> 0" 

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

1179 
proof 

1180 
from inverse_mult_eq_1[OF a0] 

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

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

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

1184 
with inverse_mult_eq_1[OF a0] 

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

1186 
unfolding power2_eq_square 

36350  1187 
apply (simp add: field_simps) 
29687  1188 
by (simp add: mult_assoc[symmetric]) 
52902  1189 
hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a)  fps_deriv a * inverse a ^ 2 = 
1190 
0  fps_deriv a * inverse a ^ 2" 

29687  1191 
by simp 
52902  1192 
then show "fps_deriv (inverse a) =  fps_deriv a * inverse a ^ 2" 
1193 
by (simp add: field_simps) 

29687  1194 
qed 
1195 

30488  1196 
lemma fps_inverse_mult: 
29687  1197 
fixes a::"('a :: field) fps" 
1198 
shows "inverse (a * b) = inverse a * inverse b" 

1199 
proof 

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

29687  1202 
from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all 
52902  1203 
have ?thesis unfolding th by simp 
1204 
} 

29687  1205 
moreover 
52902  1206 
{ 
1207 
assume b0: "b$0 = 0" hence ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) 

29687  1208 
from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all 
52902  1209 
have ?thesis unfolding th by simp 
1210 
} 

29687  1211 
moreover 
52902  1212 
{ 
1213 
assume a0: "a$0 \<noteq> 0" and b0: "b$0 \<noteq> 0" 

29687  1214 
from a0 b0 have ab0:"(a*b) $ 0 \<noteq> 0" by (simp add: fps_mult_nth) 
30488  1215 
from inverse_mult_eq_1[OF ab0] 
29687  1216 
have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp 
1217 
then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" 

36350  1218 
by (simp add: field_simps) 
52902  1219 
then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp 
1220 
} 

1221 
ultimately show ?thesis by blast 

29687  1222 
qed 
1223 

30488  1224 
lemma fps_inverse_deriv': 
29687  1225 
fixes a:: "('a :: field) fps" 
1226 
assumes a0: "a$0 \<noteq> 0" 

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

1228 
using fps_inverse_deriv[OF a0] 

48757  1229 
unfolding power2_eq_square fps_divide_def fps_inverse_mult 
1230 
by simp 

29687  1231 

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

29687  1234 
shows "f * inverse f= 1" 
1235 
by (metis mult_commute inverse_mult_eq_1 f0) 

1236 

52902  1237 
lemma fps_divide_deriv: 
1238 
fixes a:: "('a :: field) fps" 

29687  1239 
assumes a0: "b$0 \<noteq> 0" 
1240 
shows "fps_deriv (a / b) = (fps_deriv a * b  a * fps_deriv b) / b ^ 2" 

1241 
using fps_inverse_deriv[OF a0] 

48757  1242 
by (simp add: fps_divide_def field_simps 
1243 
power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) 

30488  1244 

29687  1245 

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

1247 
by (simp add: fps_inverse_gp fps_eq_iff X_def) 
29687  1248 

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

52902  1250 
by (cases n) simp_all 
29687  1251 

1252 

1253 
lemma fps_inverse_X_plus1: 

31021  1254 
"inverse (1 + X) = Abs_fps (\<lambda>n. ( (1::'a::{field})) ^ n)" (is "_ = ?r") 
29687  1255 
proof 