author  paulson <lp15@cam.ac.uk> 
Wed, 18 Mar 2015 14:13:27 +0000  
changeset 59741  5b762cd73a8e 
parent 59730  b7c394c7a619 
child 59815  cce82e360c2f 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Formal_Power_Series.thy 
29687  2 
Author: Amine Chaieb, University of Cambridge 
3 
*) 

4 

58881  5 
section{* A formalization of formal power series *} 
29687  6 

7 
theory Formal_Power_Series 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
58881
diff
changeset

8 
imports Complex_Main 
29687  9 
begin 
10 

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

49834  13 
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

14 
morphisms fps_nth Abs_fps 
29687  15 
by simp 
16 

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

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

18 

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

19 
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

20 
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

21 

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

22 
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

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

24 

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

25 
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

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

27 

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

29687  30 

36409  31 
instantiation fps :: (zero) zero 
29687  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 

36409  43 
instantiation fps :: ("{one, zero}") one 
29687  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 

54681  55 
instantiation fps :: (plus) plus 
29687  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 

54681  91 
instantiation fps :: ("{comm_monoid_add, times}") times 
29687  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 

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

105 
declare Ball_def [presburger] 

29687  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 

52891  119 

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

122 

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

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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

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

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

132 

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

133 
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

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

137 
by (simp add: fps_ext add.commute) 
29687  138 
qed 
139 

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

140 
lemma fps_mult_assoc_lemma: 
53195  141 
fixes k :: nat 
142 
and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" 

29911
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))" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

145 
by (induct k) (simp_all add: Suc_diff_le setsum.distrib 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" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

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: 
52903  162 
fixes n :: nat 
163 
and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" 

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

164 
shows "(\<Sum>i=0..n. f i (n  i)) = (\<Sum>i=0..n. f (n  i) i)" 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56480
diff
changeset

165 
by (rule setsum.reindex_bij_witness[where i="op  n" and j="op  n"]) auto 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

166 

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

167 
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

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

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

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

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

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

173 
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

174 
by (rule fps_mult_commute_lemma) 
52891  175 
then show "(a * b) $ n = (b * a) $ n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

176 
by (simp add: fps_mult_nth mult.commute) 
29687  177 
qed 
178 
qed 

179 

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

180 
instance fps :: (monoid_add) monoid_add 
29687  181 
proof 
52891  182 
fix a :: "'a fps" 
183 
show "0 + a = a" by (simp add: fps_ext) 

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

29687  185 
qed 
186 

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

187 
instance fps :: (comm_monoid_add) comm_monoid_add 
29687  188 
proof 
52891  189 
fix a :: "'a fps" 
190 
show "0 + a = a" by (simp add: fps_ext) 

29687  191 
qed 
192 

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

193 
instance fps :: (semiring_1) monoid_mult 
29687  194 
proof 
52891  195 
fix a :: "'a fps" 
57418  196 
show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) 
197 
show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') 

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

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

202 
fix a b c :: "'a fps" 
52891  203 
{ assume "a + b = a + c" then show "b = c" by (simp add: expand_fps_eq) } 
204 
{ 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

205 
qed 
29687  206 

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

207 
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

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

209 
fix a b c :: "'a fps" 
52891  210 
assume "a + b = a + c" 
211 
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

212 
qed 
29687  213 

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

214 
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

215 

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

216 
instance fps :: (group_add) group_add 
29687  217 
proof 
52891  218 
fix a b :: "'a fps" 
219 
show " a + a = 0" by (simp add: fps_ext) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53374
diff
changeset

220 
show "a +  b = a  b" by (simp add: fps_ext) 
29687  221 
qed 
222 

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

223 
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

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

225 
fix a b :: "'a fps" 
52891  226 
show " a + a = 0" by (simp add: fps_ext) 
227 
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

228 
qed 
29687  229 

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

230 
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

231 
by default (simp add: expand_fps_eq) 
29687  232 

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

233 
instance fps :: (semiring_0) semiring 
29687  234 
proof 
235 
fix a b c :: "'a fps" 

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

236 
show "(a + b) * c = a * c + b * c" 
57418  237 
by (simp add: expand_fps_eq fps_mult_nth distrib_right setsum.distrib) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

238 
show "a * (b + c) = a * b + a * c" 
57418  239 
by (simp add: expand_fps_eq fps_mult_nth distrib_left setsum.distrib) 
29687  240 
qed 
241 

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

242 
instance fps :: (semiring_0) semiring_0 
29687  243 
proof 
53195  244 
fix a :: "'a fps" 
52891  245 
show "0 * a = 0" by (simp add: fps_ext fps_mult_nth) 
246 
show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth) 

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

248 

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

249 
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

250 

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

253 
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

254 
by (simp add: expand_fps_eq) 
29687  255 

52902  256 
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

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

258 
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

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

260 
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

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

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

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

264 
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

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

266 
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

267 
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

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

269 
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

270 
then show "f \<noteq> 0" by (auto simp add: expand_fps_eq) 
29687  271 
qed 
272 

273 
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

274 
by (rule expand_fps_eq) 
29687  275 

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

277 
proof (cases "finite S") 
52891  278 
case True 
279 
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

280 
next 
52891  281 
case False 
282 
then show ?thesis by simp 

29687  283 
qed 
284 

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

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

288 

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

289 
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

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

291 

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

292 
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

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

294 

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

295 
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

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

297 

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

298 
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

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

300 

54681  301 
lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + 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

302 
by (simp add: fps_ext) 
52891  303 

54681  304 
lemma fps_const_sub [simp]: "fps_const (c::'a::group_add)  fps_const d = fps_const (c  d)" 
31369
8b460fd12100
Reverses idempotent; radical of E; generalized logarithm;
chaieb
parents:
31199
diff
changeset

305 
by (simp add: fps_ext) 
52891  306 

54681  307 
lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)" 
57418  308 
by (simp add: fps_eq_iff fps_mult_nth setsum.neutral) 
29687  309 

54681  310 
lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f = 
48757  311 
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

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

313 

54681  314 
lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) = 
48757  315 
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

316 
by (simp add: fps_ext) 
29687  317 

54681  318 
lemma fps_const_mult_left: "fps_const (c::'a::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

319 
unfolding fps_eq_iff fps_mult_nth 
57418  320 
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

321 

54681  322 
lemma fps_const_mult_right: "f * fps_const (c::'a::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

323 
unfolding fps_eq_iff fps_mult_nth 
57418  324 
by (simp add: fps_const_def mult_delta_right setsum.delta') 
29687  325 

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

326 
lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n" 
57418  327 
by (simp add: fps_mult_nth mult_delta_left setsum.delta) 
29687  328 

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

329 
lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" 
57418  330 
by (simp add: fps_mult_nth mult_delta_right setsum.delta') 
29687  331 

29906  332 
subsection {* Formal power series form an integral domain*} 
29687  333 

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

334 
instance fps :: (ring) ring .. 
29687  335 

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

336 
instance fps :: (ring_1) ring_1 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53374
diff
changeset

337 
by (intro_classes, auto simp add: distrib_right) 
29687  338 

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

339 
instance fps :: (comm_ring_1) comm_ring_1 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53374
diff
changeset

340 
by (intro_classes, auto simp add: distrib_right) 
29687  341 

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

342 
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors 
29687  343 
proof 
344 
fix a b :: "'a fps" 

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

54681  346 
then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0" and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0" 
347 
unfolding fps_nonzero_nth_minimal 

29687  348 
by blast+ 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

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

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

353 
also have "(\<Sum>k\<in>{0..i+j}{i}. a$k * b$(i+jk)) = 0" 
57418  354 
proof (rule setsum.neutral [rule_format]) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

355 
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

356 
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

357 
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

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

359 
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

360 
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

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

364 

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

365 
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

366 

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

367 
instance fps :: (idom) idom .. 
29687  368 

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

369 
lemma numeral_fps_const: "numeral k = fps_const (numeral k)" 
48757  370 
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

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

372 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54452
diff
changeset

373 
lemma neg_numeral_fps_const: " numeral k = fps_const ( numeral k)" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54452
diff
changeset

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

375 

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

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

377 

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

380 

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

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

383 
lemma X_mult_nth [simp]: 

54681  384 
"(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n  1))" 
53195  385 
proof (cases "n = 0") 
386 
case False 

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

388 
by (simp add: fps_mult_nth) 

389 
also have "\<dots> = f $ (n  1)" 

57418  390 
using False by (simp add: X_def mult_delta_left setsum.delta) 
53195  391 
finally show ?thesis using False by simp 
392 
next 

393 
case True 

394 
then show ?thesis by (simp add: fps_mult_nth X_def) 

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

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

396 

48757  397 
lemma X_mult_right_nth[simp]: 
54681  398 
"((f :: 'a::comm_semiring_1 fps) * X) $n = (if n = 0 then 0 else f $ (n  1))" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

399 
by (metis X_mult_nth mult.commute) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

400 

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

54452  404 
then show ?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

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

406 
case (Suc k) 
52891  407 
{ 
408 
fix m 

54681  409 
have "(X^Suc k) $ m = (if m = 0 then 0::'a else (X^k) $ (m  1))" 
52891  410 
by (simp del: One_nat_def) 
54681  411 
then have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" 
52891  412 
using Suc.hyps by (auto cong del: if_weak_cong) 
413 
} 

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

414 
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

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

416 

48757  417 
lemma X_power_mult_nth: 
54681  418 
"(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

419 
apply (induct k arbitrary: n) 
52891  420 
apply simp 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

421 
unfolding power_Suc mult.assoc 
48757  422 
apply (case_tac n) 
423 
apply auto 

424 
done 

425 

426 
lemma X_power_mult_right_nth: 

54681  427 
"((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n  k))" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

428 
by (metis X_power_mult_nth mult.commute) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

429 

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

430 

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

431 
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

432 

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

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

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

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

437 

52891  438 
definition 
54681  439 
dist_fps_def: "dist (a :: 'a fps) b = 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

440 
(if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST 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

441 

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

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

444 

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

446 
apply (auto simp add: dist_fps_def) 
54681  447 
apply (rule cong[OF refl, where x="(\<lambda>n. a $ n \<noteq> b $ n)"]) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

448 
apply (rule ext) 
48757  449 
apply auto 
450 
done 

451 

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

452 
instance .. 
48757  453 

30746  454 
end 
455 

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

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

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

458 

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

459 
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

460 

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

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

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

464 
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

465 
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

466 
next 
48757  467 
{ 
468 
fix a b :: "'a fps" 

469 
{ 

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

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

474 
moreover 

475 
{ 

476 
assume d: "dist a b = 0" 

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

480 
} 

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

482 
} 

483 
note th = this 

484 
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

485 
fix a b c :: "'a fps" 
48757  486 
{ 
52891  487 
assume "a = b" 
488 
then have "dist a b = 0" unfolding th . 

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

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

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

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

498 
moreover 
52891  499 
{ 
500 
assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c" 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

501 
def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

502 
then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

503 
by (auto dest: not_less_Least) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

504 

c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

505 
from ab ac bc 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

506 
have dab: "dist a b = inverse (2 ^ n a b)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

507 
and dac: "dist a c = inverse (2 ^ n a c)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

508 
and dbc: "dist b c = inverse (2 ^ n b c)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

509 
by (simp_all add: dist_fps_def n_def fps_eq_iff) 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

510 
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

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

512 
from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" 
52891  513 
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

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

515 
have th1: "\<And>n. (2::real)^n >0" by auto 
52891  516 
{ 
517 
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

518 
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

519 
using pos by auto 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

520 
from gt have gtn: "n a b < n b c" "n a b < n a c" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

521 
unfolding dab dbc dac by (auto simp add: th1) 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

522 
from n'[OF gtn(2)] n'(1)[OF gtn(1)] 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

523 
have "a $ n a b = b $ n a b" by simp 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

524 
moreover have "a $ n a b \<noteq> b $ n a b" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

525 
unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

526 
ultimately have False by contradiction 
52891  527 
} 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

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

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

531 
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

532 
qed 
52891  533 

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

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

535 

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

536 
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

537 

52891  538 
lemma reals_power_lt_ex: 
54681  539 
fixes x y :: real 
540 
assumes xp: "x > 0" 

541 
and y1: "y > 1" 

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

542 
shows "\<exists>k>0. (1/y)^k < x" 
52891  543 
proof  
54681  544 
have yp: "y > 0" 
545 
using y1 by simp 

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

546 
from reals_Archimedean2[of "max 0 ( log y x) + 1"] 
54681  547 
obtain k :: nat where k: "real k > max 0 ( log y x) + 1" 
548 
by blast 

549 
from k have kp: "k > 0" 

550 
by simp 

551 
from k have "real k >  log y x" 

552 
by simp 

553 
then have "ln y * real k >  ln x" 

554 
unfolding log_def 

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

555 
using ln_gt_zero_iff[OF yp] y1 
54681  556 
by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric]) 
557 
then have "ln y * real k + ln x > 0" 

558 
by simp 

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

559 
then have "exp (real k * ln y + ln x) > exp 0" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

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

561 
then have "y ^ k * x > 1" 
52891  562 
unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp] 
563 
by simp 

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

36350  565 
by (simp add: field_simps nonzero_power_divide) 
54681  566 
then show ?thesis 
567 
using kp by blast 

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

568 
qed 
52891  569 

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

572 

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

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

574 
by (simp add: X_power_iff) 
52891  575 

54452  576 
lemma fps_sum_rep_nth: "(setsum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n = 
54681  577 
(if n \<le> m then a$n else 0::'a::comm_ring_1)" 
52891  578 
apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong) 
57418  579 
apply (simp add: setsum.delta') 
48757  580 
done 
52891  581 

54452  582 
lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) > a" 
52902  583 
(is "?s > a") 
52891  584 
proof  
585 
{ 

54681  586 
fix r :: real 
52891  587 
assume rp: "r > 0" 
588 
have th0: "(2::real) > 1" by simp 

589 
from reals_power_lt_ex[OF rp th0] 

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

591 
{ 

54681  592 
fix n :: nat 
52891  593 
assume nn0: "n \<ge> n0" 
54452  594 
then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0" 
59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset

595 
by (simp add: divide_simps) 
52891  596 
{ 
597 
assume "?s n = a" 

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

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

600 
using rp by (simp del: dist_eq_0_iff) 

601 
} 

602 
moreover 

603 
{ 

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

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

605 
def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i" 
52891  606 
from neq have dth: "dist (?s n) a = (1/2)^k" 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

607 
by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

608 

c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

609 
from neq have kn: "k > n" 
54681  610 
by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff 
611 
split: split_if_asm intro: LeastI2_ex) 

612 
then have "dist (?s n) a < (1/2)^n" 

59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset

613 
unfolding dth by (simp add: divide_simps) 
54681  614 
also have "\<dots> \<le> (1/2)^n0" 
59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset

615 
using nn0 by (simp add: divide_simps) 
54681  616 
also have "\<dots> < r" 
617 
using n0 by simp 

52891  618 
finally have "dist (?s n) a < r" . 
619 
} 

54681  620 
ultimately have "dist (?s n) a < r" 
621 
by blast 

52891  622 
} 
54681  623 
then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r" 
624 
by blast 

52891  625 
} 
54681  626 
then show ?thesis 
627 
unfolding LIMSEQ_def by blast 

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

629 

54681  630 

29906  631 
subsection{* Inverses of formal power series *} 
29687  632 

57418  633 
declare setsum.cong[fundef_cong] 
29687  634 

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

635 
instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse 
29687  636 
begin 
637 

52891  638 
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" 
639 
where 

29687  640 
"natfun_inverse f 0 = inverse (f$0)" 
30488  641 
 "natfun_inverse f n =  inverse (f$0) * setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}" 
29687  642 

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

645 

646 
definition 

647 
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

648 

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

650 

29687  651 
end 
652 

52891  653 
lemma fps_inverse_zero [simp]: 
54681  654 
"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

655 
by (simp add: fps_ext fps_inverse_def) 
29687  656 

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

658 
apply (auto simp add: expand_fps_eq fps_inverse_def) 
52891  659 
apply (case_tac n) 
660 
apply auto 

661 
done 

662 

663 
lemma inverse_mult_eq_1 [intro]: 

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

29687  665 
shows "inverse f * f = 1" 
52891  666 
proof  
54681  667 
have c: "inverse f * f = f * inverse f" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

668 
by (simp add: mult.commute) 
30488  669 
from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n" 
29687  670 
by (simp add: fps_inverse_def) 
671 
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

672 
by (simp add: fps_mult_nth fps_inverse_def) 
52891  673 
{ 
674 
fix n :: nat 

675 
assume np: "n > 0" 

54681  676 
from np have eq: "{0..n} = {0} \<union> {1 .. n}" 
677 
by auto 

678 
have d: "{0} \<inter> {1 .. n} = {}" 

679 
by auto 

52891  680 
from f0 np have th0: " (inverse f $ n) = 
29687  681 
(setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}) / (f$0)" 
52891  682 
by (cases n) (simp_all add: divide_inverse fps_inverse_def) 
29687  683 
from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] 
52891  684 
have th1: "setsum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n} =  (f$0) * (inverse f)$n" 
36350  685 
by (simp add: field_simps) 
30488  686 
have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n  i))" 
29687  687 
unfolding fps_mult_nth ifn .. 
52891  688 
also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (ni))" 
46757  689 
by (simp add: eq) 
54681  690 
also have "\<dots> = 0" 
691 
unfolding th1 ifn by simp 

692 
finally have "(inverse f * f)$n = 0" 

693 
unfolding c . 

52891  694 
} 
54681  695 
with th0 show ?thesis 
696 
by (simp add: fps_eq_iff) 

29687  697 
qed 
698 

699 
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

700 
by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) 
29687  701 

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

52891  703 
proof  
704 
{ 

54681  705 
assume "f $ 0 = 0" 
706 
then have "inverse f = 0" 

707 
by (simp add: fps_inverse_def) 

52891  708 
} 
29687  709 
moreover 
52891  710 
{ 
54681  711 
assume h: "inverse f = 0" 
712 
assume c: "f $0 \<noteq> 0" 

713 
from inverse_mult_eq_1[OF c] h have False 

714 
by simp 

52891  715 
} 
29687  716 
ultimately show ?thesis by blast 
717 
qed 

718 

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

29687  721 
shows "inverse (inverse f) = f" 
52891  722 
proof  
29687  723 
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp 
30488  724 
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] 
52891  725 
have "inverse f * f = inverse f * inverse (inverse f)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

726 
by (simp add: ac_simps) 
54681  727 
then show ?thesis 
728 
using f0 unfolding mult_cancel_left by simp 

29687  729 
qed 
730 

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

29687  734 
shows "inverse f = g" 
52891  735 
proof  
29687  736 
from inverse_mult_eq_1[OF f0] fg 
54681  737 
have th0: "inverse f * f = g * f" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

738 
by (simp add: ac_simps) 
54681  739 
then show ?thesis 
740 
using f0 

741 
unfolding mult_cancel_right 

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

742 
by (auto simp add: expand_fps_eq) 
29687  743 
qed 
744 

30488  745 
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) 
52902  746 
= Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then  1 else 0)" 
29687  747 
apply (rule fps_inverse_unique) 
748 
apply simp 

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

749 
apply (simp add: fps_eq_iff fps_mult_nth) 
54681  750 
apply clarsimp 
751 
proof  

52891  752 
fix n :: nat 
753 
assume n: "n > 0" 

54681  754 
let ?f = "\<lambda>i. if n = i then (1::'a) else if n  i = 1 then  1 else 0" 
29687  755 
let ?g = "\<lambda>i. if i = n then 1 else if i=n  1 then  1 else 0" 
756 
let ?h = "\<lambda>i. if i=n  1 then  1 else 0" 

30488  757 
have th1: "setsum ?f {0..n} = setsum ?g {0..n}" 
57418  758 
by (rule setsum.cong) auto 
30488  759 
have th2: "setsum ?g {0..n  1} = setsum ?h {0..n  1}" 
54681  760 
apply (insert n) 
57418  761 
apply (rule setsum.cong) 
54681  762 
apply auto 
763 
done 

764 
have eq: "{0 .. n} = {0.. n  1} \<union> {n}" 

765 
by auto 

766 
from n have d: "{0.. n  1} \<inter> {n} = {}" 

767 
by auto 

768 
have f: "finite {0.. n  1}" "finite {n}" 

769 
by auto 

29687  770 
show "setsum ?f {0..n} = 0" 
30488  771 
unfolding th1 
57418  772 
apply (simp add: setsum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) 
29687  773 
unfolding th2 
57418  774 
apply (simp add: setsum.delta) 
52891  775 
done 
29687  776 
qed 
777 

54681  778 

779 
subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *} 

29687  780 

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

782 

54681  783 
lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)" 
48757  784 
by (simp add: fps_deriv_def) 
785 

786 
lemma fps_deriv_linear[simp]: 

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

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

36350  789 
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) 
29687  790 

30488  791 
lemma fps_deriv_mult[simp]: 
54681  792 
fixes f :: "'a::comm_ring_1 fps" 
29687  793 
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" 
52891  794 
proof  
29687  795 
let ?D = "fps_deriv" 
54681  796 
{ 
797 
fix n :: nat 

29687  798 
let ?Zn = "{0 ..n}" 
799 
let ?Zn1 = "{0 .. n + 1}" 

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

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

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

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

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

57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56480
diff
changeset

806 
by (rule setsum.reindex_bij_witness[where i="op  (n + 1)" and j="op  (n + 1)"]) auto 
52891  807 
have s1: "setsum (\<lambda>i. f $ i * g $ (n + 1  i)) ?Zn1 = 
808 
setsum (\<lambda>i. f $ (n + 1  i) * g $ i) ?Zn1" 

57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56480
diff
changeset

809 
by (rule setsum.reindex_bij_witness[where i="op  (n + 1)" and j="op  (n + 1)"]) auto 
52891  810 
have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

811 
by (simp only: mult.commute) 
29687  812 
also have "\<dots> = (\<Sum>i = 0..n. ?g i)" 
57418  813 
by (simp add: fps_mult_nth setsum.distrib[symmetric]) 
29687  814 
also have "\<dots> = setsum ?h {0..n+1}" 
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56480
diff
changeset

815 
by (rule setsum.reindex_bij_witness_not_neutral 
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56480
diff
changeset

816 
[where S'="{}" and T'="{0}" and j="Suc" and i="\<lambda>i. i  1"]) auto 
29687  817 
also have "\<dots> = (fps_deriv (f * g)) $ n" 
57418  818 
apply (simp only: fps_deriv_nth fps_mult_nth setsum.distrib) 
29687  819 
unfolding s0 s1 
57418  820 
unfolding setsum.distrib[symmetric] setsum_right_distrib 
821 
apply (rule setsum.cong) 

52891  822 
apply (auto simp add: of_nat_diff field_simps) 
823 
done 

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

825 
} 

30488  826 
then show ?thesis unfolding fps_eq_iff by auto 
29687  827 
qed 
828 

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

829 
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

830 
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

831 

54681  832 
lemma fps_deriv_neg[simp]: 
833 
"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

834 
by (simp add: fps_eq_iff fps_deriv_def) 
52891  835 

54681  836 
lemma fps_deriv_add[simp]: 
837 
"fps_deriv ((f:: 'a::comm_ring_1 fps) + g) = fps_deriv f + fps_deriv g" 

29687  838 
using fps_deriv_linear[of 1 f 1 g] by simp 
839 

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53374
diff
changeset

842 
using fps_deriv_add [of f " g"] by simp 
29687  843 

844 
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

845 
by (simp add: fps_ext fps_deriv_def fps_const_def) 
29687  846 

48757  847 
lemma fps_deriv_mult_const_left[simp]: 
54681  848 
"fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f" 
29687  849 
by simp 
850 

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

852 
by (simp add: fps_deriv_def fps_eq_iff) 

853 

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

855 
by (simp add: fps_deriv_def fps_eq_iff ) 

856 

48757  857 
lemma fps_deriv_mult_const_right[simp]: 
54681  858 
"fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c" 
29687  859 
by simp 
860 

48757  861 
lemma fps_deriv_setsum: 
54681  862 
"fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: 'a::comm_ring_1 fps)) S" 
53195  863 
proof (cases "finite S") 
864 
case False 

865 
then show ?thesis by simp 

866 
next 

867 
case True 

868 
show ?thesis by (induct rule: finite_induct [OF True]) simp_all 

29687  869 
qed 
870 

52902  871 
lemma fps_deriv_eq_0_iff [simp]: 
54681  872 
"fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})" 
52902  873 
proof  
52891  874 
{ 
875 
assume "f = fps_const (f$0)" 

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

877 
then have "fps_deriv f = 0" by simp 

878 
} 

29687  879 
moreover 
52891  880 
{ 
881 
assume z: "fps_deriv f = 0" 

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

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

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

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

52891  887 
apply simp 
888 
done 

889 
} 

29687  890 
ultimately show ?thesis by blast 
891 
qed 

892 

30488  893 
lemma fps_deriv_eq_iff: 
54681  894 
fixes f :: "'a::{idom,semiring_char_0} fps" 
29687  895 
shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0  g$0) + g)" 
52891  896 
proof  
52903  897 
have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f  g) = 0" 
898 
by simp 

54681  899 
also have "\<dots> \<longleftrightarrow> f  g = fps_const ((f  g) $ 0)" 
52903  900 
unfolding fps_deriv_eq_0_iff .. 
36350  901 
finally show ?thesis by (simp add: field_simps) 
29687  902 
qed 
903 

48757  904 
lemma fps_deriv_eq_iff_ex: 
54681  905 
"(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)" 
53195  906 
by (auto simp: fps_deriv_eq_iff) 
48757  907 

908 

54681  909 
fun fps_nth_deriv :: "nat \<Rightarrow> 'a::semiring_1 fps \<Rightarrow> 'a fps" 
48757  910 
where 
29687  911 
"fps_nth_deriv 0 f = f" 
912 
 "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" 

913 

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

48757  915 
by (induct n arbitrary: f) auto 
916 

917 
lemma fps_nth_deriv_linear[simp]: 

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

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

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

921 

922 
lemma fps_nth_deriv_neg[simp]: 

54681  923 
"fps_nth_deriv n ( (f :: 'a::comm_ring_1 fps)) =  (fps_nth_deriv n f)" 
48757  924 
by (induct n arbitrary: f) simp_all 
925 

926 
lemma fps_nth_deriv_add[simp]: 

54681  927 
"fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g" 
29687  928 
using fps_nth_deriv_linear[of n 1 f 1 g] by simp 
929 

48757  930 
lemma fps_nth_deriv_sub[simp]: 
54681  931 
"fps_nth_deriv n ((f :: 'a::comm_ring_1 fps)  g) = fps_nth_deriv n f  fps_nth_deriv n g" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53374
diff
changeset

932 
using fps_nth_deriv_add [of n f " g"] by simp 
29687  933 

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

48757  935 
by (induct n) simp_all 
29687  936 

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

48757  938 
by (induct n) simp_all 
939 

940 
lemma fps_nth_deriv_const[simp]: 

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

942 
by (cases n) simp_all 

943 

944 
lemma fps_nth_deriv_mult_const_left[simp]: 

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

29687  946 
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp 
947 

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

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

950 
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult.commute) 
29687  951 

48757  952 
lemma fps_nth_deriv_setsum: 
54681  953 
"fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: 'a::comm_ring_1 fps)) S" 
52903  954 
proof (cases "finite S") 
955 
case True 

956 
show ?thesis by (induct rule: finite_induct [OF True]) simp_all 

957 
next 

958 
case False 

959 
then show ?thesis by simp 

29687  960 
qed 
961 

48757  962 
lemma fps_deriv_maclauren_0: 
54681  963 
"(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) $ 0 = of_nat (fact k) * f $ k" 
36350  964 
by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult) 
29687  965 

54681  966 

967 
subsection {* Powers *} 

29687  968 

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

48757  970 
by (induct n) (auto simp add: expand_fps_eq fps_mult_nth) 
29687  971 

54681  972 
lemma fps_power_first_eq: "(a :: 'a::comm_ring_1 fps) $ 0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1" 
52891  973 
proof (induct n) 
974 
case 0 

975 
then show ?case by simp 

29687  976 
next 
977 
case (Suc n) 

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

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

29687  982 
qed 
983 

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

48757  985 
by (induct n) (auto simp add: fps_mult_nth) 
29687  986 

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

48757  988 
by (induct n) (auto simp add: fps_mult_nth) 
29687  989 

54681  990 
lemma startsby_power:"a $0 = (v::'a::comm_ring_1) \<Longrightarrow> a^n $0 = v^n" 
52891  991 
by (induct n) (auto simp add: fps_mult_nth) 
992 

54681  993 
lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::idom) \<longleftrightarrow> n \<noteq> 0 \<and> a$0 = 0" 
52891  994 
apply (rule iffI) 
995 
apply (induct n) 

996 
apply (auto simp add: fps_mult_nth) 

997 
apply (rule startsby_zero_power, simp_all) 

998 
done 

29687  999 

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

30488  1003 
using a0 
54681  1004 
proof (induct k rule: nat_less_induct) 
52891  1005 
fix k 
54681  1006 
assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0" 
29687  1007 
let ?ths = "\<forall>m<k. a ^ k $ m = 0" 
54681  1008 
{ 
1009 
assume "k = 0" 

1010 
then have ?ths by simp 

1011 
} 

29687  1012 
moreover 
52891  1013 
{ 
1014 
fix l 

1015 
assume k: "k = Suc l" 

1016 
{ 

1017 
fix m 

1018 
assume mk: "m < k" 

1019 
{ 

1020 
assume "m = 0" 

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

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

1023 
} 

29687  1024 
moreover 
52891  1025 
{ 
1026 
assume m0: "m \<noteq> 0" 

54681  1027 
have "a ^k $ m = (a^l * a) $m" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

1028 
by (simp add: k mult.commute) 
54681  1029 
also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m  i))" 
1030 
by (simp add: fps_mult_nth) 

52891  1031 
also have "\<dots> = 0" 
57418  1032 
apply (rule setsum.neutral) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

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

1036 
apply (rule H[rule_format]) 
52891  1037 
using a0 k mk apply auto 
1038 
done 

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

1040 
} 

54681  1041 
ultimately have "a^k $ m = 0" 
1042 
by blast 

52891  1043 
} 
1044 
then have ?ths by blast 

1045 
} 

54681  1046 
ultimately show ?ths 
1047 
by (cases k) auto 

29687  1048 
qed 
1049 

30488  1050 
lemma startsby_zero_setsum_depends: 
54681  1051 
assumes a0: "a $0 = (0::'a::idom)" 
1052 
and kn: "n \<ge> k" 

29687  1053 
shows "setsum (\<lambda>i. (a ^ i)$k) {0 .. n} = setsum (\<lambda>i. (a ^ i)$k) {0 .. k}" 
57418  1054 
apply (rule setsum.mono_neutral_right) 
54681  1055 
using kn 
1056 
apply auto 

29687  1057 
apply (rule startsby_zero_power_prefix[rule_format, OF a0]) 
52891  1058 
apply arith 
1059 
done 

1060 

1061 
lemma startsby_zero_power_nth_same: 

54681  1062 
assumes a0: "a$0 = (0::'a::idom)" 
29687  1063 
shows "a^n $ n = (a$1) ^ n" 
52891  1064 
proof (induct n) 
1065 
case 0 

52902  1066 
then show ?case by simp 
29687  1067 
next 
1068 
case (Suc n) 

54681  1069 
have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" 
1070 
by (simp add: field_simps) 

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

29687  1073 
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n  i)) {n .. Suc n}" 
57418  1074 
apply (rule setsum.mono_neutral_right) 
29687  1075 
apply simp 
1076 
apply clarsimp 

1077 
apply clarsimp 

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

1079 
apply arith 

1080 
done 

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

1083 
finally show ?case 

1084 
using Suc.hyps by simp 

29687  1085 
qed 
1086 

1087 
lemma fps_inverse_power: 

54681  1088 
fixes a :: "'a::field fps" 
29687  1089 
shows "inverse (a^n) = inverse a ^ n" 
52891  1090 
proof  
1091 
{ 

1092 
assume a0: "a$0 = 0" 

54681  1093 
then have eq: "inverse a = 0" 
1094 
by (simp add: fps_inverse_def) 

1095 
{ 

1096 
assume "n = 0" 

1097 
then have ?thesis by simp 

1098 
} 

29687  1099 
moreover 
52891  1100 
{ 
1101 
assume n: "n > 0" 

30488  1102 
from startsby_zero_power[OF a0 n] eq a0 n have ?thesis 
52891  1103 
by (simp add: fps_inverse_def) 
1104 
} 

1105 
ultimately have ?thesis by blast 

1106 
} 

29687  1107 
moreover 
52891  1108 
{ 
1109 
assume a0: "a$0 \<noteq> 0" 

29687  1110 
have ?thesis 
1111 
apply (rule fps_inverse_unique) 

1112 
apply (simp add: a0) 

1113 
unfolding power_mult_distrib[symmetric] 

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

1115 
apply simp_all 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

1116 
apply (subst mult.commute) 
52891  1117 
apply (rule inverse_mult_eq_1[OF a0]) 
1118 
done 

1119 
} 

29687  1120 
ultimately show ?thesis by blast 
1121 
qed 

1122 

48757  1123 
lemma fps_deriv_power: 
54681  1124 
"fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n  1)" 
48757  1125 
apply (induct n) 
52891  1126 
apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add) 
48757  1127 
apply (case_tac n) 
52891  1128 
apply (auto simp add: field_simps) 
48757  1129 
done 
29687  1130 

30488  1131 
lemma fps_inverse_deriv: 
54681  1132 
fixes a :: "'a::field fps" 
29687  1133 
assumes a0: "a$0 \<noteq> 0" 
53077  1134 
shows "fps_deriv (inverse a) =  fps_deriv a * (inverse a)\<^sup>2" 
54681  1135 
proof  
29687  1136 
from inverse_mult_eq_1[OF a0] 
1137 
have "fps_deriv (inverse a * a) = 0" by simp 

54452  1138 
then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" 
1139 
by simp 

1140 
then have "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" 

1141 
by simp 

29687  1142 
with inverse_mult_eq_1[OF a0] 
53077  1143 
have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0" 
29687  1144 
unfolding power2_eq_square 
36350  1145 
apply (simp add: field_simps) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

1146 
apply (simp add: mult.assoc[symmetric]) 
52903  1147 
done 
53077  1148 
then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a)  fps_deriv a * (inverse a)\<^sup>2 = 
1149 
0  fps_deriv a * (inverse a)\<^sup>2" 

29687  1150 
by simp 
53077  1151 
then show "fps_deriv (inverse a) =  fps_deriv a * (inverse a)\<^sup>2" 
52902  1152 
by (simp add: field_simps) 
29687  1153 
qed 
1154 

30488  1155 
lemma fps_inverse_mult: 
54681  1156 
fixes a :: "'a::field fps" 
29687  1157 
shows "inverse (a * b) = inverse a * inverse b" 
52903  1158 
proof  
52902  1159 
{ 
54452  1160 
assume a0: "a$0 = 0" 
1161 
then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) 

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

29687  1165 
moreover 
52902  1166 
{ 
54452  1167 
assume b0: "b$0 = 0" 
1168 
then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) 

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

29687  1172 
moreover 
52902  1173 
{ 
1174 
assume a0: "a$0 \<noteq> 0" and b0: "b$0 \<noteq> 0" 

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

36350  1179 
by (simp add: field_simps) 
52902  1180 
then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp 
1181 
} 

1182 
ultimately show ?thesis by blast 

29687  1183 
qed 
1184 

30488  1185 
lemma fps_inverse_deriv': 
54681  1186 
fixes a :: "'a::field fps" 
29687  1187 
assumes a0: "a$0 \<noteq> 0" 
53077  1188 
shows "fps_deriv (inverse a) =  fps_deriv a / a\<^sup>2" 
29687  1189 
using fps_inverse_deriv[OF a0] 
48757  1190 
unfolding power2_eq_square fps_divide_def fps_inverse_mult 
1191 
by simp 

29687  1192 

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

29687  1195 
shows "f * inverse f= 1" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

1196 
by (metis mult.commute inverse_mult_eq_1 f0) 
29687  1197 

52902  1198 
lemma fps_divide_deriv: 
54681  1199 
fixes a :: "'a::field fps" 
29687  1200 
assumes a0: "b$0 \<noteq> 0" 
53077  1201 
shows "fps_deriv (a / b) = (fps_deriv a * b  a * fps_deriv b) / b\<^sup>2" 
29687  1202 
using fps_inverse_deriv[OF a0] 
48757  1203 
by (simp add: fps_divide_def field_simps 
1204 
power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) 

30488  1205 

29687  1206 

54681  1207 
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

1208 
by (simp add: fps_inverse_gp fps_eq_iff X_def) 
29687  1209 

1210 
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  1211 
by (cases n) simp_all 
29687  1212 

1213 

1214 
lemma fps_inverse_X_plus1: 

54681  1215 
"inverse (1 + X) = Abs_fps (\<lambda>n. ( (1::'a::field)) ^ n)" (is "_ = ?r") 
1216 
proof  

29687  1217 
have eq: "(1 + X) * ?r = 1" 
1218 
unfolding minus_one_power_iff 

36350  1219 
by (auto simp add: field_simps fps_eq_iff) 
54681  1220 
show ?thesis 
1221 
by (auto simp add: eq intro: fps_inverse_unique) 

29687  1222 
qed 
1223 

30488  1224 

29906  1225 
subsection{* Integration *} 
31273  1226 

52903  1227 
definition fps_integral :: "'a::field_char_0 fps \<Rightarrow> 'a \<Rightarrow> 'a fps" 
1228 
where "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n  1) / of_nat n))" 

29687  1229 

31273  1230 
lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a" 
1231 
unfolding fps_integral_def fps_deriv_def 

1232 
by (simp add: fps_eq_iff del: of_nat_Suc) 

29687  1233 
