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