author | haftmann |
Sun, 08 Oct 2017 22:28:22 +0200 | |
changeset 66817 | 0b12755ccbb2 |
parent 66480 | 4b8d1df8933b |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
65435 | 1 |
(* Title: HOL/Computational_Algebra/Polynomial_FPS.thy |
65366 | 2 |
Author: Manuel Eberl, TU München |
63317 | 3 |
*) |
4 |
||
5 |
section \<open>Converting polynomials to formal power series\<close> |
|
65366 | 6 |
|
63317 | 7 |
theory Polynomial_FPS |
65366 | 8 |
imports Polynomial Formal_Power_Series |
63317 | 9 |
begin |
10 |
||
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
11 |
context |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
12 |
includes fps_notation |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
13 |
begin |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
14 |
|
63319 | 15 |
definition fps_of_poly where |
16 |
"fps_of_poly p = Abs_fps (coeff p)" |
|
63317 | 17 |
|
63319 | 18 |
lemma fps_of_poly_eq_iff: "fps_of_poly p = fps_of_poly q \<longleftrightarrow> p = q" |
19 |
by (simp add: fps_of_poly_def poly_eq_iff fps_eq_iff) |
|
63317 | 20 |
|
63319 | 21 |
lemma fps_of_poly_nth [simp]: "fps_of_poly p $ n = coeff p n" |
22 |
by (simp add: fps_of_poly_def) |
|
63317 | 23 |
|
63319 | 24 |
lemma fps_of_poly_const: "fps_of_poly [:c:] = fps_const c" |
63317 | 25 |
proof (subst fps_eq_iff, clarify) |
63319 | 26 |
fix n :: nat show "fps_of_poly [:c:] $ n = fps_const c $ n" |
27 |
by (cases n) (auto simp: fps_of_poly_def) |
|
63317 | 28 |
qed |
29 |
||
63319 | 30 |
lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0" |
31 |
by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp |
|
63317 | 32 |
|
63319 | 33 |
lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1" |
65486 | 34 |
by (simp add: fps_eq_iff) |
63317 | 35 |
|
63319 | 36 |
lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1" |
37 |
by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) |
|
63317 | 38 |
(simp add: one_poly_def) |
39 |
||
63319 | 40 |
lemma fps_of_poly_numeral [simp]: "fps_of_poly (numeral n) = numeral n" |
41 |
by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly) |
|
63317 | 42 |
|
63319 | 43 |
lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n" |
44 |
by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly) |
|
63317 | 45 |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
46 |
lemma fps_of_poly_fps_X [simp]: "fps_of_poly [:0, 1:] = fps_X" |
63319 | 47 |
by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split) |
63317 | 48 |
|
63319 | 49 |
lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q" |
50 |
by (simp add: fps_of_poly_def plus_poly.rep_eq fps_plus_def) |
|
63317 | 51 |
|
63319 | 52 |
lemma fps_of_poly_diff: "fps_of_poly (p - q) = fps_of_poly p - fps_of_poly q" |
53 |
by (simp add: fps_of_poly_def minus_poly.rep_eq fps_minus_def) |
|
63317 | 54 |
|
63319 | 55 |
lemma fps_of_poly_uminus: "fps_of_poly (-p) = -fps_of_poly p" |
56 |
by (simp add: fps_of_poly_def uminus_poly.rep_eq fps_uminus_def) |
|
63317 | 57 |
|
63319 | 58 |
lemma fps_of_poly_mult: "fps_of_poly (p * q) = fps_of_poly p * fps_of_poly q" |
59 |
by (simp add: fps_of_poly_def fps_times_def fps_eq_iff coeff_mult atLeast0AtMost) |
|
63317 | 60 |
|
63319 | 61 |
lemma fps_of_poly_smult: |
62 |
"fps_of_poly (smult c p) = fps_const c * fps_of_poly p" |
|
63 |
using fps_of_poly_mult[of "[:c:]" p] by (simp add: fps_of_poly_mult fps_of_poly_const) |
|
63317 | 64 |
|
64267 | 65 |
lemma fps_of_poly_sum: "fps_of_poly (sum f A) = sum (\<lambda>x. fps_of_poly (f x)) A" |
63319 | 66 |
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_add) |
63317 | 67 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63539
diff
changeset
|
68 |
lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)" |
63319 | 69 |
by (induction xs) (simp_all add: fps_of_poly_add) |
63317 | 70 |
|
64272 | 71 |
lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A" |
63319 | 72 |
by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult) |
63317 | 73 |
|
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63539
diff
changeset
|
74 |
lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)" |
63319 | 75 |
by (induction xs) (simp_all add: fps_of_poly_mult) |
63317 | 76 |
|
63319 | 77 |
lemma fps_of_poly_pCons: |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
78 |
"fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * fps_X" |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
79 |
by (subst fps_mult_fps_X_commute [symmetric], intro fps_ext) |
63319 | 80 |
(auto simp: fps_of_poly_def coeff_pCons split: nat.split) |
63317 | 81 |
|
63319 | 82 |
lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)" |
83 |
by (intro fps_ext) (simp add: fps_of_poly_nth coeff_pderiv) |
|
63317 | 84 |
|
63319 | 85 |
lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n" |
86 |
by (induction n) (simp_all add: fps_of_poly_mult) |
|
63317 | 87 |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
88 |
lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * fps_X ^ n" |
63317 | 89 |
by (intro fps_ext) simp_all |
90 |
||
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
91 |
lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = fps_X ^ n" |
63319 | 92 |
by (simp add: fps_of_poly_monom) |
63317 | 93 |
|
63319 | 94 |
lemma fps_of_poly_div: |
63317 | 95 |
assumes "(q :: 'a :: field poly) dvd p" |
63319 | 96 |
shows "fps_of_poly (p div q) = fps_of_poly p / fps_of_poly q" |
63317 | 97 |
proof (cases "q = 0") |
98 |
case False |
|
63319 | 99 |
from False fps_of_poly_eq_iff[of q 0] have nz: "fps_of_poly q \<noteq> 0" by simp |
63317 | 100 |
from assms have "p = (p div q) * q" by simp |
63319 | 101 |
also have "fps_of_poly \<dots> = fps_of_poly (p div q) * fps_of_poly q" |
102 |
by (simp add: fps_of_poly_mult) |
|
103 |
also from nz have "\<dots> / fps_of_poly q = fps_of_poly (p div q)" |
|
64240 | 104 |
by (intro nonzero_mult_div_cancel_right) (auto simp: fps_of_poly_0) |
63317 | 105 |
finally show ?thesis .. |
106 |
qed simp |
|
107 |
||
63319 | 108 |
lemma fps_of_poly_divide_numeral: |
109 |
"fps_of_poly (smult (inverse (numeral c :: 'a :: field)) p) = fps_of_poly p / numeral c" |
|
63317 | 110 |
proof - |
111 |
have "smult (inverse (numeral c)) p = [:inverse (numeral c):] * p" by simp |
|
63319 | 112 |
also have "fps_of_poly \<dots> = fps_of_poly p / numeral c" |
113 |
by (subst fps_of_poly_mult) (simp add: numeral_fps_const fps_of_poly_pCons) |
|
63317 | 114 |
finally show ?thesis by simp |
115 |
qed |
|
116 |
||
117 |
||
63319 | 118 |
lemma subdegree_fps_of_poly: |
63317 | 119 |
assumes "p \<noteq> 0" |
120 |
defines "n \<equiv> Polynomial.order 0 p" |
|
63319 | 121 |
shows "subdegree (fps_of_poly p) = n" |
63317 | 122 |
proof (rule subdegreeI) |
123 |
from assms have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff) |
|
63319 | 124 |
thus zero: "fps_of_poly p $ i = 0" if "i < n" for i |
63317 | 125 |
using that by (simp add: monom_1_dvd_iff') |
126 |
||
127 |
from assms have "\<not>monom 1 (Suc n) dvd p" |
|
128 |
by (auto simp: monom_1_dvd_iff simp del: power_Suc) |
|
63539 | 129 |
then obtain k where k: "k \<le> n" "fps_of_poly p $ k \<noteq> 0" |
63317 | 130 |
by (auto simp: monom_1_dvd_iff' less_Suc_eq_le) |
63539 | 131 |
with zero[of k] have "k = n" by linarith |
132 |
with k show "fps_of_poly p $ n \<noteq> 0" by simp |
|
63317 | 133 |
qed |
134 |
||
63319 | 135 |
lemma fps_of_poly_dvd: |
63317 | 136 |
assumes "p dvd q" |
63319 | 137 |
shows "fps_of_poly (p :: 'a :: field poly) dvd fps_of_poly q" |
63317 | 138 |
proof (cases "p = 0 \<or> q = 0") |
139 |
case False |
|
63319 | 140 |
with assms fps_of_poly_eq_iff[of p 0] fps_of_poly_eq_iff[of q 0] show ?thesis |
141 |
by (auto simp: fps_dvd_iff subdegree_fps_of_poly dvd_imp_order_le) |
|
63317 | 142 |
qed (insert assms, auto) |
143 |
||
144 |
||
63319 | 145 |
lemmas fps_of_poly_simps = |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
146 |
fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_fps_X |
63319 | 147 |
fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult |
64272 | 148 |
fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list |
63319 | 149 |
fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom |
150 |
fps_of_poly_divide_numeral |
|
63317 | 151 |
|
63319 | 152 |
lemma fps_of_poly_pcompose: |
63317 | 153 |
assumes "coeff q 0 = (0 :: 'a :: idom)" |
63319 | 154 |
shows "fps_of_poly (pcompose p q) = fps_compose (fps_of_poly p) (fps_of_poly q)" |
63317 | 155 |
using assms by (induction p rule: pCons_induct) |
63319 | 156 |
(auto simp: pcompose_pCons fps_of_poly_simps fps_of_poly_pCons |
63317 | 157 |
fps_compose_add_distrib fps_compose_mult_distrib) |
158 |
||
159 |
lemmas reify_fps_atom = |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
160 |
fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_fps_X |
63317 | 161 |
|
162 |
||
163 |
text \<open> |
|
164 |
The following simproc can reduce the equality of two polynomial FPSs two equality of the |
|
165 |
respective polynomials. A polynomial FPS is one that only has finitely many non-zero |
|
63319 | 166 |
coefficients and can therefore be written as @{term "fps_of_poly p"} for some |
64911 | 167 |
polynomial \<open>p\<close>. |
63317 | 168 |
|
169 |
This may sound trivial, but it covers a number of annoying side conditions like |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
170 |
@{term "1 + fps_X \<noteq> 0"} that would otherwise not be solved automatically. |
63317 | 171 |
\<close> |
172 |
||
173 |
ML \<open> |
|
174 |
||
175 |
(* TODO: Support for division *) |
|
176 |
signature POLY_FPS = sig |
|
177 |
||
178 |
val reify_conv : conv |
|
179 |
val eq_conv : conv |
|
180 |
val eq_simproc : cterm -> thm option |
|
181 |
||
182 |
end |
|
183 |
||
184 |
||
185 |
structure Poly_Fps = struct |
|
186 |
||
187 |
fun const_binop_conv s conv ct = |
|
188 |
case Thm.term_of ct of |
|
189 |
(Const (s', _) $ _ $ _) => |
|
190 |
if s = s' then |
|
191 |
Conv.binop_conv conv ct |
|
192 |
else |
|
193 |
raise CTERM ("const_binop_conv", [ct]) |
|
194 |
| _ => raise CTERM ("const_binop_conv", [ct]) |
|
195 |
||
196 |
fun reify_conv ct = |
|
197 |
let |
|
198 |
val rewr = Conv.rewrs_conv o map (fn thm => thm RS @{thm eq_reflection}) |
|
199 |
val un = Conv.arg_conv reify_conv |
|
200 |
val bin = Conv.binop_conv reify_conv |
|
201 |
in |
|
202 |
case Thm.term_of ct of |
|
63319 | 203 |
(Const (@{const_name "fps_of_poly"}, _) $ _) => ct |> Conv.all_conv |
63317 | 204 |
| (Const (@{const_name "Groups.plus"}, _) $ _ $ _) => ct |> ( |
63319 | 205 |
bin then_conv rewr @{thms fps_of_poly_add [symmetric]}) |
63317 | 206 |
| (Const (@{const_name "Groups.uminus"}, _) $ _) => ct |> ( |
63319 | 207 |
un then_conv rewr @{thms fps_of_poly_uminus [symmetric]}) |
63317 | 208 |
| (Const (@{const_name "Groups.minus"}, _) $ _ $ _) => ct |> ( |
63319 | 209 |
bin then_conv rewr @{thms fps_of_poly_diff [symmetric]}) |
63317 | 210 |
| (Const (@{const_name "Groups.times"}, _) $ _ $ _) => ct |> ( |
63319 | 211 |
bin then_conv rewr @{thms fps_of_poly_mult [symmetric]}) |
63317 | 212 |
| (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _)) |
213 |
=> ct |> (Conv.fun_conv (Conv.arg_conv reify_conv) |
|
63319 | 214 |
then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]}) |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
215 |
| (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "fps_X"},_) $ _) => ct |> ( |
63319 | 216 |
rewr @{thms fps_of_poly_monom' [symmetric]}) |
63317 | 217 |
| (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> ( |
218 |
Conv.fun_conv (Conv.arg_conv reify_conv) |
|
63319 | 219 |
then_conv rewr @{thms fps_of_poly_power [symmetric]}) |
63317 | 220 |
| _ => ct |> ( |
221 |
rewr @{thms reify_fps_atom [symmetric]}) |
|
222 |
end |
|
223 |
||
224 |
||
225 |
fun eq_conv ct = |
|
226 |
case Thm.term_of ct of |
|
227 |
(Const (@{const_name "HOL.eq"}, _) $ _ $ _) => ct |> ( |
|
228 |
Conv.binop_conv reify_conv |
|
63319 | 229 |
then_conv Conv.rewr_conv @{thm fps_of_poly_eq_iff[THEN eq_reflection]}) |
63317 | 230 |
| _ => raise CTERM ("poly_fps_eq_conv", [ct]) |
231 |
||
232 |
val eq_simproc = try eq_conv |
|
233 |
||
234 |
end |
|
235 |
\<close> |
|
236 |
||
237 |
simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close> |
|
238 |
||
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
239 |
lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = fps_X + fps_const a" |
63317 | 240 |
by simp |
241 |
||
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
242 |
lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * fps_X" |
63317 | 243 |
by simp |
244 |
||
63319 | 245 |
lemma fps_of_poly_cutoff [simp]: |
246 |
"fps_of_poly (poly_cutoff n p) = fps_cutoff n (fps_of_poly p)" |
|
63317 | 247 |
by (simp add: fps_eq_iff coeff_poly_cutoff) |
248 |
||
63319 | 249 |
lemma fps_of_poly_shift [simp]: "fps_of_poly (poly_shift n p) = fps_shift n (fps_of_poly p)" |
63317 | 250 |
by (simp add: fps_eq_iff coeff_poly_shift) |
251 |
||
252 |
||
253 |
definition poly_subdegree :: "'a::zero poly \<Rightarrow> nat" where |
|
63319 | 254 |
"poly_subdegree p = subdegree (fps_of_poly p)" |
63317 | 255 |
|
256 |
lemma coeff_less_poly_subdegree: |
|
257 |
"k < poly_subdegree p \<Longrightarrow> coeff p k = 0" |
|
63319 | 258 |
unfolding poly_subdegree_def using nth_less_subdegree_zero[of k "fps_of_poly p"] by simp |
63317 | 259 |
|
260 |
(* TODO: Move ? *) |
|
261 |
definition prefix_length :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
262 |
"prefix_length P xs = length (takeWhile P xs)" |
|
263 |
||
264 |
primrec prefix_length_aux :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
265 |
"prefix_length_aux P acc [] = acc" |
|
266 |
| "prefix_length_aux P acc (x#xs) = (if P x then prefix_length_aux P (Suc acc) xs else acc)" |
|
267 |
||
268 |
lemma prefix_length_aux_correct: "prefix_length_aux P acc xs = prefix_length P xs + acc" |
|
269 |
by (induction xs arbitrary: acc) (simp_all add: prefix_length_def) |
|
270 |
||
271 |
lemma prefix_length_code [code]: "prefix_length P xs = prefix_length_aux P 0 xs" |
|
272 |
by (simp add: prefix_length_aux_correct) |
|
273 |
||
274 |
lemma prefix_length_le_length: "prefix_length P xs \<le> length xs" |
|
275 |
by (induction xs) (simp_all add: prefix_length_def) |
|
276 |
||
277 |
lemma prefix_length_less_length: "(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> prefix_length P xs < length xs" |
|
278 |
by (induction xs) (simp_all add: prefix_length_def) |
|
279 |
||
280 |
lemma nth_prefix_length: |
|
281 |
"(\<exists>x\<in>set xs. \<not>P x) \<Longrightarrow> \<not>P (xs ! prefix_length P xs)" |
|
282 |
by (induction xs) (simp_all add: prefix_length_def) |
|
283 |
||
284 |
lemma nth_less_prefix_length: |
|
285 |
"n < prefix_length P xs \<Longrightarrow> P (xs ! n)" |
|
286 |
by (induction xs arbitrary: n) |
|
287 |
(auto simp: prefix_length_def nth_Cons split: if_splits nat.splits) |
|
288 |
(* END TODO *) |
|
289 |
||
290 |
lemma poly_subdegree_code [code]: "poly_subdegree p = prefix_length (op = 0) (coeffs p)" |
|
291 |
proof (cases "p = 0") |
|
292 |
case False |
|
293 |
note [simp] = this |
|
294 |
define n where "n = prefix_length (op = 0) (coeffs p)" |
|
295 |
from False have "\<exists>k. coeff p k \<noteq> 0" by (auto simp: poly_eq_iff) |
|
296 |
hence ex: "\<exists>x\<in>set (coeffs p). x \<noteq> 0" by (auto simp: coeffs_def) |
|
297 |
hence n_less: "n < length (coeffs p)" and nonzero: "coeffs p ! n \<noteq> 0" |
|
298 |
unfolding n_def by (auto intro!: prefix_length_less_length nth_prefix_length) |
|
299 |
show ?thesis unfolding poly_subdegree_def |
|
300 |
proof (intro subdegreeI) |
|
63319 | 301 |
from n_less have "fps_of_poly p $ n = coeffs p ! n" |
63317 | 302 |
by (subst coeffs_nth) (simp_all add: degree_eq_length_coeffs) |
63319 | 303 |
with nonzero show "fps_of_poly p $ prefix_length (op = 0) (coeffs p) \<noteq> 0" |
63317 | 304 |
unfolding n_def by simp |
305 |
next |
|
306 |
fix k assume A: "k < prefix_length (op = 0) (coeffs p)" |
|
307 |
also have "\<dots> \<le> length (coeffs p)" by (rule prefix_length_le_length) |
|
63319 | 308 |
finally show "fps_of_poly p $ k = 0" |
63317 | 309 |
using nth_less_prefix_length[OF A] |
310 |
by (simp add: coeffs_nth degree_eq_length_coeffs) |
|
311 |
qed |
|
312 |
qed (simp_all add: poly_subdegree_def prefix_length_def) |
|
313 |
||
314 |
end |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
315 |
|
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
65486
diff
changeset
|
316 |
end |