author  eberlm <eberlm@in.tum.de> 
Tue, 04 Apr 2017 09:01:19 +0200  
changeset 65396  b42167902f57 
parent 64786  340db65fd2c1 
child 65398  a14fa655b48c 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Formal_Power_Series.thy 
29687  2 
Author: Amine Chaieb, University of Cambridge 
3 
*) 

4 

60501  5 
section \<open>A formalization of formal power series\<close> 
29687  6 

7 
theory Formal_Power_Series 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

8 
imports Complex_Main "~~/src/HOL/Number_Theory/Euclidean_Algorithm" 
29687  9 
begin 
10 

60501  11 

60500  12 
subsection \<open>The type of formal power series\<close> 
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 

60501  29 
text \<open>Definition of the basic elements 0 and 1 and the basic operations of addition, 
30 
negation and multiplication.\<close> 

29687  31 

36409  32 
instantiation fps :: (zero) zero 
29687  33 
begin 
60501  34 
definition fps_zero_def: "0 = Abs_fps (\<lambda>n. 0)" 
35 
instance .. 

29687  36 
end 
37 

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

38 
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

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

40 

36409  41 
instantiation fps :: ("{one, zero}") one 
29687  42 
begin 
60501  43 
definition fps_one_def: "1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)" 
44 
instance .. 

29687  45 
end 
46 

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

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

49 

54681  50 
instantiation fps :: (plus) plus 
29687  51 
begin 
60501  52 
definition fps_plus_def: "op + = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n + g $ n))" 
53 
instance .. 

29687  54 
end 
55 

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

56 
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

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

58 

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

59 
instantiation fps :: (minus) minus 
29687  60 
begin 
60501  61 
definition fps_minus_def: "op  = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n  g $ n))" 
62 
instance .. 

29687  63 
end 
64 

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

65 
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

66 
unfolding fps_minus_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 :: (uminus) uminus 
29687  69 
begin 
60501  70 
definition fps_uminus_def: "uminus = (\<lambda>f. Abs_fps (\<lambda>n.  (f $ n)))" 
71 
instance .. 

29687  72 
end 
73 

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

74 
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

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

76 

54681  77 
instantiation fps :: ("{comm_monoid_add, times}") times 
29687  78 
begin 
60501  79 
definition fps_times_def: "op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n  i)))" 
80 
instance .. 

29687  81 
end 
82 

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

83 
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

84 
unfolding fps_times_def by simp 
29687  85 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

86 
lemma fps_mult_nth_0 [simp]: "(f * g) $ 0 = f $ 0 * g $ 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

87 
unfolding fps_times_def by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

88 

52891  89 
declare atLeastAtMost_iff [presburger] 
90 
declare Bex_def [presburger] 

91 
declare Ball_def [presburger] 

29687  92 

29913  93 
lemma mult_delta_left: 
94 
fixes x y :: "'a::mult_zero" 

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

96 
by simp 

97 

98 
lemma mult_delta_right: 

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

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

101 
by simp 

102 

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

52891  105 

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

108 

60501  109 

110 
subsection \<open>Formal power series form a commutative ring with unity, if the range of sequences 

60500  111 
they represent is a commutative ring with unity\<close> 
29687  112 

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

113 
instance fps :: (semigroup_add) semigroup_add 
29687  114 
proof 
52891  115 
fix a b c :: "'a fps" 
116 
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

117 
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

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

119 

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

120 
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

121 
proof 
52891  122 
fix a b :: "'a fps" 
123 
show "a + b = b + a" 

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

124 
by (simp add: fps_ext add.commute) 
29687  125 
qed 
126 

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

127 
lemma fps_mult_assoc_lemma: 
53195  128 
fixes k :: nat 
129 
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

130 
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

131 
(\<Sum>j=0..k. \<Sum>i=0..k  j. f j i (n  j  i))" 
64267  132 
by (induct k) (simp_all add: Suc_diff_le sum.distrib add.assoc) 
29687  133 

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

134 
instance fps :: (semiring_0) semigroup_mult 
29687  135 
proof 
136 
fix a b c :: "'a fps" 

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

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

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

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

140 
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

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

142 
by (rule fps_mult_assoc_lemma) 
52891  143 
then show "((a * b) * c) $ n = (a * (b * c)) $ n" 
64267  144 
by (simp add: fps_mult_nth sum_distrib_left sum_distrib_right mult.assoc) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

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

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

147 

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

148 
lemma fps_mult_commute_lemma: 
52903  149 
fixes n :: nat 
150 
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

151 
shows "(\<Sum>i=0..n. f i (n  i)) = (\<Sum>i=0..n. f (n  i) i)" 
64267  152 
by (rule sum.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

153 

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

154 
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

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

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

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

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

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

160 
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

161 
by (rule fps_mult_commute_lemma) 
52891  162 
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

163 
by (simp add: fps_mult_nth mult.commute) 
29687  164 
qed 
165 
qed 

166 

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

167 
instance fps :: (monoid_add) monoid_add 
29687  168 
proof 
52891  169 
fix a :: "'a fps" 
170 
show "0 + a = a" by (simp add: fps_ext) 

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

29687  172 
qed 
173 

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

174 
instance fps :: (comm_monoid_add) comm_monoid_add 
29687  175 
proof 
52891  176 
fix a :: "'a fps" 
177 
show "0 + a = a" by (simp add: fps_ext) 

29687  178 
qed 
179 

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

180 
instance fps :: (semiring_1) monoid_mult 
29687  181 
proof 
52891  182 
fix a :: "'a fps" 
60501  183 
show "1 * a = a" 
64267  184 
by (simp add: fps_ext fps_mult_nth mult_delta_left sum.delta) 
60501  185 
show "a * 1 = a" 
64267  186 
by (simp add: fps_ext fps_mult_nth mult_delta_right sum.delta') 
29687  187 
qed 
188 

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

189 
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

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

191 
fix a b c :: "'a fps" 
60501  192 
show "b = c" if "a + b = a + c" 
193 
using that by (simp add: expand_fps_eq) 

194 
show "b = c" if "b + a = c + a" 

195 
using that by (simp add: expand_fps_eq) 

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

196 
qed 
29687  197 

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

198 
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

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

200 
fix a b c :: "'a fps" 
60501  201 
show "a + b  a = b" 
202 
by (simp add: expand_fps_eq) 

203 
show "a  b  c = a  (b + c)" 

204 
by (simp add: expand_fps_eq diff_diff_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_comm_monoid_add) cancel_comm_monoid_add .. 
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

208 

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

209 
instance fps :: (group_add) group_add 
29687  210 
proof 
52891  211 
fix a b :: "'a fps" 
212 
show " a + a = 0" by (simp add: fps_ext) 

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

213 
show "a +  b = a  b" by (simp add: fps_ext) 
29687  214 
qed 
215 

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

216 
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

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

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

221 
qed 
29687  222 

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

223 
instance fps :: (zero_neq_one) zero_neq_one 
60679  224 
by standard (simp add: expand_fps_eq) 
29687  225 

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

226 
instance fps :: (semiring_0) semiring 
29687  227 
proof 
228 
fix a b c :: "'a fps" 

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

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

231 
show "a * (b + c) = a * b + a * c" 
64267  232 
by (simp add: expand_fps_eq fps_mult_nth distrib_left sum.distrib) 
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 :: (semiring_0) semiring_0 
29687  236 
proof 
53195  237 
fix a :: "'a fps" 
60501  238 
show "0 * a = 0" 
239 
by (simp add: fps_ext fps_mult_nth) 

240 
show "a * 0 = 0" 

241 
by (simp add: fps_ext fps_mult_nth) 

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

243 

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

244 
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

245 

60867  246 
instance fps :: (semiring_1) semiring_1 .. 
247 

60501  248 

60500  249 
subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close> 
29687  250 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

251 
lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n  k))" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

252 
by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

253 

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

255 
by (simp add: expand_fps_eq) 
29687  256 

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

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

260 
let ?n = "LEAST n. f $ n \<noteq> 0" 
60501  261 
show ?rhs if ?lhs 
262 
proof  

263 
from that have "\<exists>n. f $ n \<noteq> 0" 

264 
by (simp add: fps_nonzero_nth) 

265 
then have "f $ ?n \<noteq> 0" 

266 
by (rule LeastI_ex) 

267 
moreover have "\<forall>m<?n. f $ m = 0" 

268 
by (auto dest: not_less_Least) 

269 
ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" .. 

270 
then show ?thesis .. 

271 
qed 

272 
show ?lhs if ?rhs 

273 
using that by (auto simp add: expand_fps_eq) 

29687  274 
qed 
275 

276 
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

277 
by (rule expand_fps_eq) 
29687  278 

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

280 
proof (cases "finite S") 
52891  281 
case True 
282 
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

283 
next 
52891  284 
case False 
285 
then show ?thesis by simp 

29687  286 
qed 
287 

60501  288 

289 
subsection \<open>Injection of the basic ring elements and multiplication by scalars\<close> 

29687  290 

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

292 

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

293 
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

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

295 

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

296 
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

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

298 

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

299 
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

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

301 

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

302 
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

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

304 

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

306 
by (simp add: fps_ext) 
52891  307 

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

309 
by (simp add: fps_ext) 
52891  310 

54681  311 
lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)" 
64267  312 
by (simp add: fps_eq_iff fps_mult_nth sum.neutral) 
29687  313 

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

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

317 

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

320 
by (simp add: fps_ext) 
29687  321 

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

323 
unfolding fps_eq_iff fps_mult_nth 
64267  324 
by (simp add: fps_const_def mult_delta_left sum.delta) 
29911
c790a70a3d19
declare fps_nth as a typedef morphism; clean up instance proofs
huffman
parents:
29906
diff
changeset

325 

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

327 
unfolding fps_eq_iff fps_mult_nth 
64267  328 
by (simp add: fps_const_def mult_delta_right sum.delta') 
29687  329 

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

330 
lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)$n = c* f$n" 
64267  331 
by (simp add: fps_mult_nth mult_delta_left sum.delta) 
29687  332 

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

333 
lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" 
64267  334 
by (simp add: fps_mult_nth mult_delta_right sum.delta') 
29687  335 

60501  336 

60500  337 
subsection \<open>Formal power series form an integral domain\<close> 
29687  338 

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

339 
instance fps :: (ring) ring .. 
29687  340 

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

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

342 
by (intro_classes, auto simp add: distrib_right) 
29687  343 

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

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

345 
by (intro_classes, auto simp add: distrib_right) 
29687  346 

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

347 
instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors 
29687  348 
proof 
349 
fix a b :: "'a fps" 

60501  350 
assume "a \<noteq> 0" and "b \<noteq> 0" 
351 
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" 

54681  352 
unfolding fps_nonzero_nth_minimal 
29687  353 
by blast+ 
60501  354 
have "(a * b) $ (i + j) = (\<Sum>k=0..i+j. a $ k * b $ (i + j  k))" 
29687  355 
by (rule fps_mult_nth) 
60501  356 
also have "\<dots> = (a $ i * b $ (i + j  i)) + (\<Sum>k\<in>{0..i+j}  {i}. a $ k * b $ (i + j  k))" 
64267  357 
by (rule sum.remove) simp_all 
60501  358 
also have "(\<Sum>k\<in>{0..i+j}{i}. a $ k * b $ (i + j  k)) = 0" 
64267  359 
proof (rule sum.neutral [rule_format]) 
60501  360 
fix k assume "k \<in> {0..i+j}  {i}" 
361 
then have "k < i \<or> i+jk < j" 

362 
by auto 

363 
then show "a $ k * b $ (i + j  k) = 0" 

364 
using i j by auto 

365 
qed 

366 
also have "a $ i * b $ (i + j  i) + 0 = a $ i * b $ j" 

367 
by simp 

368 
also have "a $ i * b $ j \<noteq> 0" 

369 
using i j by simp 

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

370 
finally have "(a*b) $ (i+j) \<noteq> 0" . 
60501  371 
then show "a * b \<noteq> 0" 
372 
unfolding fps_nonzero_nth by blast 

29687  373 
qed 
374 

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

375 
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

376 

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

377 
instance fps :: (idom) idom .. 
29687  378 

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

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

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

382 

60867  383 
lemma neg_numeral_fps_const: 
384 
"( numeral k :: 'a :: ring_1 fps) = fps_const ( numeral k)" 

385 
by (simp add: numeral_fps_const) 

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

386 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

387 
lemma fps_numeral_nth: "numeral n $ i = (if i = 0 then numeral n else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

388 
by (simp add: numeral_fps_const) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

389 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

390 
lemma fps_numeral_nth_0 [simp]: "numeral n $ 0 = numeral n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

391 
by (simp add: numeral_fps_const) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

392 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

393 
lemma fps_of_nat: "fps_const (of_nat c) = of_nat c" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

394 
by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

395 

65396
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
64786
diff
changeset

396 
lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \<noteq> 0" 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
64786
diff
changeset

397 
proof 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
64786
diff
changeset

398 
assume "numeral f = (0 :: 'a fps)" 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
64786
diff
changeset

399 
from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp 
b42167902f57
moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
eberlm <eberlm@in.tum.de>
parents:
64786
diff
changeset

400 
qed 
63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

401 

60501  402 

403 
subsection \<open>The eXtractor series X\<close> 

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

404 

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

407 

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

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

410 
lemma X_mult_nth [simp]: 

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

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

415 
by (simp add: fps_mult_nth) 

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

64267  417 
using False by (simp add: X_def mult_delta_left sum.delta) 
60501  418 
finally show ?thesis 
419 
using False by simp 

53195  420 
next 
421 
case True 

60501  422 
then show ?thesis 
423 
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

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

425 

48757  426 
lemma X_mult_right_nth[simp]: 
63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

427 
"((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n  1))" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

428 
proof  
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

429 
have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n  i = Suc 0 then 1 else 0))" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

430 
by (simp add: fps_times_def X_def) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

431 
also have "\<dots> = (\<Sum>i = 0..n. if i = n  1 then if n = 0 then 0 else a $ i else 0)" 
64267  432 
by (intro sum.cong) auto 
433 
also have "\<dots> = (if n = 0 then 0 else a $ (n  1))" by (simp add: sum.delta) 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

434 
finally show ?thesis . 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

435 
qed 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

436 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

437 
lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

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

439 

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

54452  443 
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

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

445 
case (Suc k) 
60501  446 
have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" for m 
447 
proof  

448 
have "(X^Suc k) $ m = (if m = 0 then 0 else (X^k) $ (m  1))" 

52891  449 
by (simp del: One_nat_def) 
60501  450 
then show ?thesis 
52891  451 
using Suc.hyps by (auto cong del: if_weak_cong) 
60501  452 
qed 
453 
then show ?case 

454 
by (simp add: fps_eq_iff) 

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

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

456 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

457 
lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

458 
by (simp add: X_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

459 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

460 
lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

461 
by (simp add: X_power_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

462 

60501  463 
lemma X_power_mult_nth: "(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

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

466 
unfolding power_Suc mult.assoc 
48757  467 
apply (case_tac n) 
468 
apply auto 

469 
done 

470 

471 
lemma X_power_mult_right_nth: 

54681  472 
"((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

473 
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

474 

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

475 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

476 
lemma X_neq_fps_const [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> fps_const c" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

477 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

478 
assume "(X::'a fps) = fps_const (c::'a)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

479 
hence "X$1 = (fps_const (c::'a))$1" by (simp only:) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

480 
thus False by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

481 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

482 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

483 
lemma X_neq_zero [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

484 
by (simp only: fps_const_0_eq_0[symmetric] X_neq_fps_const) simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

485 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

486 
lemma X_neq_one [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 1" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

487 
by (simp only: fps_const_1_eq_1[symmetric] X_neq_fps_const) simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

488 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

489 
lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

490 
by (simp only: numeral_fps_const X_neq_fps_const) simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

491 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

492 
lemma X_pow_eq_X_pow_iff [simp]: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

493 
"(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

494 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

495 
assume "(X :: 'a fps) ^ m = X ^ n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

496 
hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:) 
62390  497 
thus "m = n" by (simp split: if_split_asm) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

498 
qed simp_all 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

499 

877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

500 

877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

501 
subsection \<open>Subdegrees\<close> 
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

502 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

503 
definition subdegree :: "('a::zero) fps \<Rightarrow> nat" where 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

504 
"subdegree f = (if f = 0 then 0 else LEAST n. f$n \<noteq> 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

505 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

506 
lemma subdegreeI: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

507 
assumes "f $ d \<noteq> 0" and "\<And>i. i < d \<Longrightarrow> f $ i = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

508 
shows "subdegree f = d" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

509 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

510 
from assms(1) have "f \<noteq> 0" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

511 
moreover from assms(1) have "(LEAST i. f $ i \<noteq> 0) = d" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

512 
proof (rule Least_equality) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

513 
fix e assume "f $ e \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

514 
with assms(2) have "\<not>(e < d)" by blast 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

515 
thus "e \<ge> d" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

516 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

517 
ultimately show ?thesis unfolding subdegree_def by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

518 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

519 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

520 
lemma nth_subdegree_nonzero [simp,intro]: "f \<noteq> 0 \<Longrightarrow> f $ subdegree f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

521 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

522 
assume "f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

523 
hence "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

524 
also from \<open>f \<noteq> 0\<close> have "\<exists>n. f$n \<noteq> 0" using fps_nonzero_nth by blast 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

525 
from LeastI_ex[OF this] have "f $ (LEAST n. f $ n \<noteq> 0) \<noteq> 0" . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

526 
finally show ?thesis . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

527 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

528 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

529 
lemma nth_less_subdegree_zero [dest]: "n < subdegree f \<Longrightarrow> f $ n = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

530 
proof (cases "f = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

531 
assume "f \<noteq> 0" and less: "n < subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

532 
note less 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

533 
also from \<open>f \<noteq> 0\<close> have "subdegree f = (LEAST n. f $ n \<noteq> 0)" by (simp add: subdegree_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

534 
finally show "f $ n = 0" using not_less_Least by blast 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

535 
qed simp_all 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

536 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

537 
lemma subdegree_geI: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

538 
assumes "f \<noteq> 0" "\<And>i. i < n \<Longrightarrow> f$i = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

539 
shows "subdegree f \<ge> n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

540 
proof (rule ccontr) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

541 
assume "\<not>(subdegree f \<ge> n)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

542 
with assms(2) have "f $ subdegree f = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

543 
moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

544 
ultimately show False by contradiction 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

545 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

546 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

547 
lemma subdegree_greaterI: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

548 
assumes "f \<noteq> 0" "\<And>i. i \<le> n \<Longrightarrow> f$i = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

549 
shows "subdegree f > n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

550 
proof (rule ccontr) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

551 
assume "\<not>(subdegree f > n)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

552 
with assms(2) have "f $ subdegree f = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

553 
moreover from assms(1) have "f $ subdegree f \<noteq> 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

554 
ultimately show False by contradiction 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

555 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

556 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

557 
lemma subdegree_leI: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

558 
"f $ n \<noteq> 0 \<Longrightarrow> subdegree f \<le> n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

559 
by (rule leI) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

560 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

561 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

562 
lemma subdegree_0 [simp]: "subdegree 0 = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

563 
by (simp add: subdegree_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

564 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

565 
lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

566 
by (auto intro!: subdegreeI) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

567 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

568 
lemma subdegree_X [simp]: "subdegree (X :: ('a :: zero_neq_one) fps) = 1" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

569 
by (auto intro!: subdegreeI simp: X_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

570 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

571 
lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

572 
by (cases "c = 0") (auto intro!: subdegreeI) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

573 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

574 
lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

575 
by (simp add: numeral_fps_const) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

576 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

577 
lemma subdegree_eq_0_iff: "subdegree f = 0 \<longleftrightarrow> f = 0 \<or> f $ 0 \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

578 
proof (cases "f = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

579 
assume "f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

580 
thus ?thesis 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

581 
using nth_subdegree_nonzero[OF \<open>f \<noteq> 0\<close>] by (fastforce intro!: subdegreeI) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

582 
qed simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

583 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

584 
lemma subdegree_eq_0 [simp]: "f $ 0 \<noteq> 0 \<Longrightarrow> subdegree f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

585 
by (simp add: subdegree_eq_0_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

586 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

587 
lemma nth_subdegree_mult [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

588 
fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

589 
shows "(f * g) $ (subdegree f + subdegree g) = f $ subdegree f * g $ subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

590 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

591 
let ?n = "subdegree f + subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

592 
have "(f * g) $ ?n = (\<Sum>i=0..?n. f$i * g$(?ni))" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

593 
by (simp add: fps_mult_nth) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

594 
also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?ni) else 0)" 
64267  595 
proof (intro sum.cong) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

596 
fix x assume x: "x \<in> {0..?n}" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

597 
hence "x = subdegree f \<or> x < subdegree f \<or> ?n  x < subdegree g" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

598 
thus "f $ x * g $ (?n  x) = (if x = subdegree f then f $ x * g $ (?n  x) else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

599 
by (elim disjE conjE) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

600 
qed auto 
64267  601 
also have "... = f $ subdegree f * g $ subdegree g" by (simp add: sum.delta) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

602 
finally show ?thesis . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

603 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

604 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

605 
lemma subdegree_mult [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

606 
assumes "f \<noteq> 0" "g \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

607 
shows "subdegree ((f :: ('a :: {ring_no_zero_divisors}) fps) * g) = subdegree f + subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

608 
proof (rule subdegreeI) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

609 
let ?n = "subdegree f + subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

610 
have "(f * g) $ ?n = (\<Sum>i=0..?n. f$i * g$(?ni))" by (simp add: fps_mult_nth) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

611 
also have "... = (\<Sum>i=0..?n. if i = subdegree f then f$i * g$(?ni) else 0)" 
64267  612 
proof (intro sum.cong) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

613 
fix x assume x: "x \<in> {0..?n}" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

614 
hence "x = subdegree f \<or> x < subdegree f \<or> ?n  x < subdegree g" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

615 
thus "f $ x * g $ (?n  x) = (if x = subdegree f then f $ x * g $ (?n  x) else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

616 
by (elim disjE conjE) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

617 
qed auto 
64267  618 
also have "... = f $ subdegree f * g $ subdegree g" by (simp add: sum.delta) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

619 
also from assms have "... \<noteq> 0" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

620 
finally show "(f * g) $ (subdegree f + subdegree g) \<noteq> 0" . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

621 
next 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

622 
fix m assume m: "m < subdegree f + subdegree g" 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

623 
have "(f * g) $ m = (\<Sum>i=0..m. f$i * g$(mi))" by (simp add: fps_mult_nth) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

624 
also have "... = (\<Sum>i=0..m. 0)" 
64267  625 
proof (rule sum.cong) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

626 
fix i assume "i \<in> {0..m}" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

627 
with m have "i < subdegree f \<or> m  i < subdegree g" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

628 
thus "f$i * g$(mi) = 0" by (elim disjE) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

629 
qed auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

630 
finally show "(f * g) $ m = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

631 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

632 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

633 
lemma subdegree_power [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

634 
"subdegree ((f :: ('a :: ring_1_no_zero_divisors) fps) ^ n) = n * subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

635 
by (cases "f = 0"; induction n) simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

636 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

637 
lemma subdegree_uminus [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

638 
"subdegree ((f::('a::group_add) fps)) = subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

639 
by (simp add: subdegree_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

640 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

641 
lemma subdegree_minus_commute [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

642 
"subdegree (f(g::('a::group_add) fps)) = subdegree (g  f)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

643 
proof  
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

644 
have "f  g = (g  f)" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

645 
also have "subdegree ... = subdegree (g  f)" by (simp only: subdegree_uminus) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

646 
finally show ?thesis . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

647 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

648 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

649 
lemma subdegree_add_ge: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

650 
assumes "f \<noteq> (g :: ('a :: {group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

651 
shows "subdegree (f + g) \<ge> min (subdegree f) (subdegree g)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

652 
proof (rule subdegree_geI) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

653 
from assms show "f + g \<noteq> 0" by (subst (asm) eq_neg_iff_add_eq_0) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

654 
next 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

655 
fix i assume "i < min (subdegree f) (subdegree g)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

656 
hence "f $ i = 0" and "g $ i = 0" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

657 
thus "(f + g) $ i = 0" by force 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

658 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

659 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

660 
lemma subdegree_add_eq1: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

661 
assumes "f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

662 
assumes "subdegree f < subdegree (g :: ('a :: {group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

663 
shows "subdegree (f + g) = subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

664 
proof (rule antisym[OF subdegree_leI]) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

665 
from assms show "subdegree (f + g) \<ge> subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

666 
by (intro order.trans[OF min.boundedI subdegree_add_ge]) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

667 
from assms have "f $ subdegree f \<noteq> 0" "g $ subdegree f = 0" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

668 
thus "(f + g) $ subdegree f \<noteq> 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

669 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

670 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

671 
lemma subdegree_add_eq2: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

672 
assumes "g \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

673 
assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

674 
shows "subdegree (f + g) = subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

675 
using subdegree_add_eq1[OF assms] by (simp add: add.commute) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

676 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

677 
lemma subdegree_diff_eq1: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

678 
assumes "f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

679 
assumes "subdegree f < subdegree (g :: ('a :: {ab_group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

680 
shows "subdegree (f  g) = subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

681 
using subdegree_add_eq1[of f "g"] assms by (simp add: add.commute) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

682 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

683 
lemma subdegree_diff_eq2: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

684 
assumes "g \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

685 
assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

686 
shows "subdegree (f  g) = subdegree g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

687 
using subdegree_add_eq2[of "g" f] assms by (simp add: add.commute) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

688 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

689 
lemma subdegree_diff_ge [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

690 
assumes "f \<noteq> (g :: ('a :: {group_add}) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

691 
shows "subdegree (f  g) \<ge> min (subdegree f) (subdegree g)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

692 
using assms subdegree_add_ge[of f "g"] by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

693 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

694 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

695 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

696 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

697 
subsection \<open>Shifting and slicing\<close> 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

698 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

699 
definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

700 
"fps_shift n f = Abs_fps (\<lambda>i. f $ (i + n))" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

701 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

702 
lemma fps_shift_nth [simp]: "fps_shift n f $ i = f $ (i + n)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

703 
by (simp add: fps_shift_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

704 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

705 
lemma fps_shift_0 [simp]: "fps_shift 0 f = f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

706 
by (intro fps_ext) (simp add: fps_shift_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

707 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

708 
lemma fps_shift_zero [simp]: "fps_shift n 0 = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

709 
by (intro fps_ext) (simp add: fps_shift_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

710 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

711 
lemma fps_shift_one: "fps_shift n 1 = (if n = 0 then 1 else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

712 
by (intro fps_ext) (simp add: fps_shift_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

713 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

714 
lemma fps_shift_fps_const: "fps_shift n (fps_const c) = (if n = 0 then fps_const c else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

715 
by (intro fps_ext) (simp add: fps_shift_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

716 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

717 
lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

718 
by (simp add: numeral_fps_const fps_shift_fps_const) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

719 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

720 
lemma fps_shift_X_power [simp]: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

721 
"n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m  n) ::'a::comm_ring_1 fps)" 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

722 
by (intro fps_ext) (auto simp: fps_shift_def ) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

723 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

724 
lemma fps_shift_times_X_power: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

725 
"n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

726 
by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

727 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

728 
lemma fps_shift_times_X_power' [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

729 
"fps_shift n (f * X^n) = (f :: 'a :: comm_ring_1 fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

730 
by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

731 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

732 
lemma fps_shift_times_X_power'': 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

733 
"m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n  m) (f :: 'a :: comm_ring_1 fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

734 
by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

735 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

736 
lemma fps_shift_subdegree [simp]: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

737 
"n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps)  n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

738 
by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+ 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

739 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

740 
lemma subdegree_decompose: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

741 
"f = fps_shift (subdegree f) f * X ^ subdegree (f :: ('a :: comm_ring_1) fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

742 
by (rule fps_ext) (auto simp: X_power_mult_right_nth) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

743 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

744 
lemma subdegree_decompose': 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

745 
"n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * X^n" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

746 
by (rule fps_ext) (auto simp: X_power_mult_right_nth intro!: nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

747 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

748 
lemma fps_shift_fps_shift: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

749 
"fps_shift (m + n) f = fps_shift m (fps_shift n f)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

750 
by (rule fps_ext) (simp add: add_ac) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

751 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

752 
lemma fps_shift_add: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

753 
"fps_shift n (f + g) = fps_shift n f + fps_shift n g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

754 
by (simp add: fps_eq_iff) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

755 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

756 
lemma fps_shift_mult: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

757 
assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

758 
shows "fps_shift n (h*g) = h * fps_shift n g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

759 
proof  
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

760 
from assms have "g = fps_shift n g * X^n" by (rule subdegree_decompose') 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

761 
also have "h * ... = (h * fps_shift n g) * X^n" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

762 
also have "fps_shift n ... = h * fps_shift n g" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

763 
finally show ?thesis . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

764 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

765 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

766 
lemma fps_shift_mult_right: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

767 
assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

768 
shows "fps_shift n (g*h) = h * fps_shift n g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

769 
by (subst mult.commute, subst fps_shift_mult) (simp_all add: assms) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

770 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

771 
lemma nth_subdegree_zero_iff [simp]: "f $ subdegree f = 0 \<longleftrightarrow> f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

772 
by (cases "f = 0") auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

773 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

774 
lemma fps_shift_subdegree_zero_iff [simp]: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

775 
"fps_shift (subdegree f) f = 0 \<longleftrightarrow> f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

776 
by (subst (1) nth_subdegree_zero_iff[symmetric], cases "f = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

777 
(simp_all del: nth_subdegree_zero_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

778 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

779 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

780 
definition "fps_cutoff n f = Abs_fps (\<lambda>i. if i < n then f$i else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

781 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

782 
lemma fps_cutoff_nth [simp]: "fps_cutoff n f $ i = (if i < n then f$i else 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

783 
unfolding fps_cutoff_def by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

784 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

785 
lemma fps_cutoff_zero_iff: "fps_cutoff n f = 0 \<longleftrightarrow> (f = 0 \<or> n \<le> subdegree f)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

786 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

787 
assume A: "fps_cutoff n f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

788 
thus "f = 0 \<or> n \<le> subdegree f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

789 
proof (cases "f = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

790 
assume "f \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

791 
with A have "n \<le> subdegree f" 
62390  792 
by (intro subdegree_geI) (auto simp: fps_eq_iff split: if_split_asm) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

793 
thus ?thesis .. 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

794 
qed simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

795 
qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

796 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

797 
lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

798 
by (simp add: fps_eq_iff) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

799 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

800 
lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

801 
by (simp add: fps_eq_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

802 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

803 
lemma fps_cutoff_one: "fps_cutoff n 1 = (if n = 0 then 0 else 1)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

804 
by (simp add: fps_eq_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

805 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

806 
lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)" 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

807 
by (simp add: fps_eq_iff) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

808 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

809 
lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

810 
by (simp add: numeral_fps_const fps_cutoff_fps_const) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

811 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

812 
lemma fps_shift_cutoff: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

813 
"fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

814 
by (simp add: fps_eq_iff X_power_mult_right_nth) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

815 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

816 

60501  817 
subsection \<open>Formal Power series form a metric space\<close> 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

818 

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

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

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

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

823 

52891  824 
definition 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

825 
dist_fps_def: "dist (a :: 'a fps) b = (if a = b then 0 else inverse (2 ^ subdegree (a  b)))" 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

826 

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

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

829 

54681  830 
lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a" 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

831 
by (simp add: dist_fps_def) 
48757  832 

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

833 
instance .. 
48757  834 

30746  835 
end 
836 

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

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

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

839 

62101  840 
definition uniformity_fps_def [code del]: 
841 
"(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" 

842 

843 
definition open_fps_def' [code del]: 

844 
"open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)" 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

845 

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

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

847 
proof 
60501  848 
show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps" 
62390  849 
by (simp add: dist_fps_def split: if_split_asm) 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

850 
then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp 
60501  851 

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

852 
fix a b c :: "'a fps" 
60501  853 
consider "a = b"  "c = a \<or> c = b"  "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast 
854 
then show "dist a b \<le> dist a c + dist b c" 

855 
proof cases 

856 
case 1 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

857 
then show ?thesis by (simp add: dist_fps_def) 
60501  858 
next 
859 
case 2 

860 
then show ?thesis 

52891  861 
by (cases "c = a") (simp_all add: th dist_fps_sym) 
60501  862 
next 
60567  863 
case neq: 3 
60558  864 
have False if "dist a b > dist a c + dist b c" 
865 
proof  

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

866 
let ?n = "subdegree (a  b)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

867 
from neq have "dist a b > 0" "dist b c > 0" and "dist a c > 0" by (simp_all add: dist_fps_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

868 
with that have "dist a b > dist a c" and "dist a b > dist b c" by simp_all 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

869 
with neq have "?n < subdegree (a  c)" and "?n < subdegree (b  c)" 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

870 
by (simp_all add: dist_fps_def field_simps) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

871 
hence "(a  c) $ ?n = 0" and "(b  c) $ ?n = 0" 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

872 
by (simp_all only: nth_less_subdegree_zero) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

873 
hence "(a  b) $ ?n = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

874 
moreover from neq have "(a  b) $ ?n \<noteq> 0" by (intro nth_subdegree_nonzero) simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

875 
ultimately show False by contradiction 
60558  876 
qed 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

877 
thus ?thesis by (auto simp add: not_le[symmetric]) 
60501  878 
qed 
62101  879 
qed (rule open_fps_def' uniformity_fps_def)+ 
52891  880 

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

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

882 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

883 
declare uniformity_Abort[where 'a="'a :: comm_ring_1 fps", code] 
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

884 

62101  885 
lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" 
886 
unfolding open_dist ball_def subset_eq by simp 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

887 

60558  888 
text \<open>The infinite sums and justification of the notation in textbooks.\<close> 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

889 

52891  890 
lemma reals_power_lt_ex: 
54681  891 
fixes x y :: real 
892 
assumes xp: "x > 0" 

893 
and y1: "y > 1" 

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

894 
shows "\<exists>k>0. (1/y)^k < x" 
52891  895 
proof  
54681  896 
have yp: "y > 0" 
897 
using y1 by simp 

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

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

901 
from k have kp: "k > 0" 

902 
by simp 

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

904 
by simp 

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

906 
unfolding log_def 

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

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

910 
by simp 

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

911 
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

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

913 
then have "y ^ k * x > 1" 
52891  914 
unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp] 
915 
by simp 

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

60867  917 
by (simp add: field_simps) 
54681  918 
then show ?thesis 
919 
using kp by blast 

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

920 
qed 
52891  921 

64267  922 
lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n = 
54681  923 
(if n \<le> m then a$n else 0::'a::comm_ring_1)" 
64267  924 
apply (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong) 
925 
apply (simp add: sum.delta') 

48757  926 
done 
52891  927 

64267  928 
lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a" 
61969  929 
(is "?s \<longlonglongrightarrow> a") 
52891  930 
proof  
60558  931 
have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r 
932 
proof  

60501  933 
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" 
934 
using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto 

60558  935 
show ?thesis 
60501  936 
proof  
60558  937 
have "dist (?s n) a < r" if nn0: "n \<ge> n0" for n 
938 
proof  

939 
from that have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0" 

60501  940 
by (simp add: divide_simps) 
60558  941 
show ?thesis 
60501  942 
proof (cases "?s n = a") 
943 
case True 

944 
then show ?thesis 

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

946 
using \<open>r > 0\<close> by (simp del: dist_eq_0_iff) 

947 
next 

948 
case False 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

949 
from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n  a)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

950 
by (simp add: dist_fps_def field_simps) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

951 
from False have kn: "subdegree (?s n  a) > n" 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

952 
by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth) 
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

953 
then have "dist (?s n) a < (1/2)^n" 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

954 
by (simp add: field_simps dist_fps_def) 
60501  955 
also have "\<dots> \<le> (1/2)^n0" 
956 
using nn0 by (simp add: divide_simps) 

957 
also have "\<dots> < r" 

958 
using n0 by simp 

959 
finally show ?thesis . 

960 
qed 

60558  961 
qed 
60501  962 
then show ?thesis by blast 
963 
qed 

60558  964 
qed 
54681  965 
then show ?thesis 
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset

966 
unfolding lim_sequentially by blast 
52891  967 
qed 
31968
0314441a53a6
FPS form a metric space, which justifies the infinte sum notation
chaieb
parents:
31790
diff
changeset

968 

54681  969 

60501  970 
subsection \<open>Inverses of formal power series\<close> 
29687  971 

64267  972 
declare sum.cong[fundef_cong] 
29687  973 

60558  974 
instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse 
29687  975 
begin 
976 

52891  977 
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" 
978 
where 

29687  979 
"natfun_inverse f 0 = inverse (f$0)" 
64267  980 
 "natfun_inverse f n =  inverse (f$0) * sum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}" 
29687  981 

60501  982 
definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" 
983 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

984 
definition fps_divide_def: 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

985 
"f div g = (if g = 0 then 0 else 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

986 
let n = subdegree g; h = fps_shift n g 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

987 
in fps_shift n (f * inverse h))" 
36311
ed3a87a7f977
epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
haftmann
parents:
36309
diff
changeset

988 

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

990 

29687  991 
end 
992 

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

995 
by (simp add: fps_ext fps_inverse_def) 
29687  996 

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

998 
apply (auto simp add: expand_fps_eq fps_inverse_def) 
52891  999 
apply (case_tac n) 
1000 
apply auto 

1001 
done 

1002 

1003 
lemma inverse_mult_eq_1 [intro]: 

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

29687  1005 
shows "inverse f * f = 1" 
52891  1006 
proof  
54681  1007 
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

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

1012 
by (simp add: fps_mult_nth fps_inverse_def) 
60501  1013 
have "(inverse f * f)$n = 0" if np: "n > 0" for n 
1014 
proof  

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

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

1018 
by auto 

52891  1019 
from f0 np have th0: " (inverse f $ n) = 
64267  1020 
(sum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n}) / (f$0)" 
52891  1021 
by (cases n) (simp_all add: divide_inverse fps_inverse_def) 
29687  1022 
from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] 
64267  1023 
have th1: "sum (\<lambda>i. f$i * natfun_inverse f (n  i)) {1..n} =  (f$0) * (inverse f)$n" 
36350  1024 
by (simp add: field_simps) 
30488  1025 
have "(f * inverse f) $ n = (\<Sum>i = 0..n. f $i * natfun_inverse f (n  i))" 
29687  1026 
unfolding fps_mult_nth ifn .. 
52891  1027 
also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (ni))" 
46757  1028 
by (simp add: eq) 
54681  1029 
also have "\<dots> = 0" 
1030 
unfolding th1 ifn by simp 

60501  1031 
finally show ?thesis unfolding c . 
1032 
qed 

54681  1033 
with th0 show ?thesis 
1034 
by (simp add: fps_eq_iff) 

29687  1035 
qed 
1036 

60501  1037 
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

1038 
by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

1039 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1040 
lemma fps_inverse_nth_0 [simp]: "inverse f $ 0 = inverse (f $ 0 :: 'a :: division_ring)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1041 
by (simp add: fps_inverse_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1042 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1043 
lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::division_ring) fps) \<longleftrightarrow> f $ 0 = 0" 
60501  1044 
proof 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1045 
assume A: "inverse f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1046 
have "0 = inverse f $ 0" by (subst A) simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1047 
thus "f $ 0 = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1048 
qed (simp add: fps_inverse_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1049 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1050 
lemma fps_inverse_idempotent[intro, simp]: 
48757  1051 
assumes f0: "f$0 \<noteq> (0::'a::field)" 
29687  1052 
shows "inverse (inverse f) = f" 
52891  1053 
proof  
29687  1054 
from f0 have if0: "inverse f $ 0 \<noteq> 0" by simp 
30488  1055 
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] 
52891  1056 
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

1057 
by (simp add: ac_simps) 
54681  1058 
then show ?thesis 
1059 
using f0 unfolding mult_cancel_left by simp 

29687  1060 
qed 
1061 

48757  1062 
lemma fps_inverse_unique: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1063 
assumes fg: "(f :: 'a :: field fps) * g = 1" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1064 
shows "inverse f = g" 
52891  1065 
proof  
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1066 
have f0: "f $ 0 \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1067 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1068 
assume "f $ 0 = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1069 
hence "0 = (f * g) $ 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1070 
also from fg have "(f * g) $ 0 = 1" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1071 
finally show False by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1072 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1073 
from inverse_mult_eq_1[OF this] fg 
54681  1074 
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

1075 
by (simp add: ac_simps) 
54681  1076 
then show ?thesis 
1077 
using f0 

1078 
unfolding mult_cancel_right 

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

1079 
by (auto simp add: expand_fps_eq) 
29687  1080 
qed 
1081 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

1082 
lemma fps_inverse_eq_0: "f$0 = 0 \<Longrightarrow> inverse (f :: 'a :: division_ring fps) = 0" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

1083 
by simp 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63040
diff
changeset

1084 

64267  1085 
lemma sum_zero_lemma: 
60162  1086 
fixes n::nat 
1087 
assumes "0 < n" 

1088 
shows "(\<Sum>i = 0..n. if n = i then 1 else if n  i = 1 then  1 else 0) = (0::'a::field)" 

54681  1089 
proof  
60162  1090 
let ?f = "\<lambda>i. if n = i then 1 else if n  i = 1 then  1 else 0" 
1091 
let ?g = "\<lambda>i. if i = n then 1 else if i = n  1 then  1 else 0" 

29687  1092 
let ?h = "\<lambda>i. if i=n  1 then  1 else 0" 
64267  1093 
have th1: "sum ?f {0..n} = sum ?g {0..n}" 
1094 
by (rule sum.cong) auto 

1095 
have th2: "sum ?g {0..n  1} = sum ?h {0..n  1}" 

1096 
apply (rule sum.cong) 

60162  1097 
using assms 
54681  1098 
apply auto 
1099 
done 

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

1101 
by auto 

60162  1102 
from assms have d: "{0.. n  1} \<inter> {n} = {}" 
54681  1103 
by auto 
1104 
have f: "finite {0.. n  1}" "finite {n}" 

1105 
by auto 

60162  1106 
show ?thesis 
30488  1107 
unfolding th1 
64267  1108 
apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) 
29687  1109 
unfolding th2 
64267  1110 
apply (simp add: sum.delta) 
52891  1111 
done 
29687  1112 
qed 
1113 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1114 
lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1115 
proof (cases "f$0 = 0 \<or> g$0 = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1116 
assume "\<not>(f$0 = 0 \<or> g$0 = 0)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1117 
hence [simp]: "f$0 \<noteq> 0" "g$0 \<noteq> 0" by simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1118 
show ?thesis 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1119 
proof (rule fps_inverse_unique) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1120 
have "f * g * (inverse f * inverse g) = (inverse f * f) * (inverse g * g)" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1121 
also have "... = 1" by (subst (1 2) inverse_mult_eq_1) simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1122 
finally show "f * g * (inverse f * inverse g) = 1" . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1123 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1124 
next 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1125 
assume A: "f$0 = 0 \<or> g$0 = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1126 
hence "inverse (f * g) = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1127 
also from A have "... = inverse f * inverse g" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1128 
finally show "inverse (f * g) = inverse f * inverse g" . 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1129 
qed 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

1130 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1131 

60501  1132 
lemma fps_inverse_gp: "inverse (Abs_fps(\<lambda>n. (1::'a::field))) = 
1133 
Abs_fps (\<lambda>n. if n= 0 then 1 else if n=1 then  1 else 0)" 

60162  1134 
apply (rule fps_inverse_unique) 
64267  1135 
apply (simp_all add: fps_eq_iff fps_mult_nth sum_zero_lemma) 
60162  1136 
done 
1137 

61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1138 
lemma subdegree_inverse [simp]: "subdegree (inverse (f::'a::field fps)) = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1139 
proof (cases "f$0 = 0") 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1140 
assume nz: "f$0 \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1141 
hence "subdegree (inverse f) + subdegree f = subdegree (inverse f * f)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1142 
by (subst subdegree_mult) auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1143 
also from nz have "subdegree f = 0" by (simp add: subdegree_eq_0_iff) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1144 
also from nz have "inverse f * f = 1" by (rule inverse_mult_eq_1) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1145 
finally show "subdegree (inverse f) = 0" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1146 
qed (simp_all add: fps_inverse_def) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1147 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1148 
lemma fps_is_unit_iff [simp]: "(f :: 'a :: field fps) dvd 1 \<longleftrightarrow> f $ 0 \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1149 
proof 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1150 
assume "f dvd 1" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1151 
then obtain g where "1 = f * g" by (elim dvdE) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1152 
from this[symmetric] have "(f*g) $ 0 = 1" by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1153 
thus "f $ 0 \<noteq> 0" by auto 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1154 
next 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1155 
assume A: "f $ 0 \<noteq> 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1156 
thus "f dvd 1" by (simp add: inverse_mult_eq_1[OF A, symmetric]) 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1157 
qed 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1158 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1159 
lemma subdegree_eq_0' [simp]: "(f :: 'a :: field fps) dvd 1 \<Longrightarrow> subdegree f = 0" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1160 
by simp 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1161 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1162 
lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1163 
by (rule dvd_trans, subst fps_is_unit_iff) simp_all 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1164 

64592
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1165 
instantiation fps :: (field) normalization_semidom 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1166 
begin 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1167 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1168 
definition fps_unit_factor_def [simp]: 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1169 
"unit_factor f = fps_shift (subdegree f) f" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1170 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1171 
definition fps_normalize_def [simp]: 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1172 
"normalize f = (if f = 0 then 0 else X ^ subdegree f)" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1173 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1174 
instance proof 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1175 
fix f :: "'a fps" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1176 
show "unit_factor f * normalize f = f" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1177 
by (simp add: fps_shift_times_X_power) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1178 
next 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1179 
fix f g :: "'a fps" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1180 
show "unit_factor (f * g) = unit_factor f * unit_factor g" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1181 
proof (cases "f = 0 \<or> g = 0") 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1182 
assume "\<not>(f = 0 \<or> g = 0)" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1183 
thus "unit_factor (f * g) = unit_factor f * unit_factor g" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1184 
unfolding fps_unit_factor_def 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1185 
by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1186 
qed auto 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1187 
next 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1188 
fix f g :: "'a fps" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1189 
assume "g \<noteq> 0" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1190 
then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1191 
by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1192 
then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1193 
by (simp add: fps_shift_mult_right mult.commute) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1194 
with \<open>g \<noteq> 0\<close> show "f * g / g = f" 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1195 
by (simp add: fps_divide_def Let_def ac_simps) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1196 
qed (auto simp add: fps_divide_def Let_def) 
7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1197 

7759f1766189
more finegrained type class hierarchy for div and mod
haftmann
parents:
64272
diff
changeset

1198 
end 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1199 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1200 
instantiation fps :: (field) ring_div 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1201 
begin 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1202 

a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1203 
definition fps_mod_def: 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1204 
"f mod g = (if g = 0 then f else 
62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

1205 
let n = subdegree g; h = fps_shift n g 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1206 
in fps_cutoff n (f * inverse h) * h)" 
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1207 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

1208 
lemma fps_mod_eq_zero: 
61608
a0487caabb4a
subdegree/shift/cutoff and Euclidean ring instance for formal power series
eberlm
parents:
61585
diff
changeset

1209 
assumes "g \<noteq> 0" and "subdegree f \<ge> subdegree g" 