29451
|
1 |
(* Title: HOL/Polynomial.thy
|
|
2 |
Author: Brian Huffman
|
|
3 |
Based on an earlier development by Clemens Ballarin
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Univariate Polynomials *}
|
|
7 |
|
|
8 |
theory Polynomial
|
|
9 |
imports Plain SetInterval
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsection {* Definition of type @{text poly} *}
|
|
13 |
|
|
14 |
typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
|
|
15 |
morphisms coeff Abs_poly
|
|
16 |
by auto
|
|
17 |
|
|
18 |
lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
|
|
19 |
by (simp add: coeff_inject [symmetric] expand_fun_eq)
|
|
20 |
|
|
21 |
lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
|
|
22 |
by (simp add: expand_poly_eq)
|
|
23 |
|
|
24 |
|
|
25 |
subsection {* Degree of a polynomial *}
|
|
26 |
|
|
27 |
definition
|
|
28 |
degree :: "'a::zero poly \<Rightarrow> nat" where
|
|
29 |
"degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
|
|
30 |
|
|
31 |
lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
|
|
32 |
proof -
|
|
33 |
have "coeff p \<in> Poly"
|
|
34 |
by (rule coeff)
|
|
35 |
hence "\<exists>n. \<forall>i>n. coeff p i = 0"
|
|
36 |
unfolding Poly_def by simp
|
|
37 |
hence "\<forall>i>degree p. coeff p i = 0"
|
|
38 |
unfolding degree_def by (rule LeastI_ex)
|
|
39 |
moreover assume "degree p < n"
|
|
40 |
ultimately show ?thesis by simp
|
|
41 |
qed
|
|
42 |
|
|
43 |
lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
|
|
44 |
by (erule contrapos_np, rule coeff_eq_0, simp)
|
|
45 |
|
|
46 |
lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
|
|
47 |
unfolding degree_def by (erule Least_le)
|
|
48 |
|
|
49 |
lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
|
|
50 |
unfolding degree_def by (drule not_less_Least, simp)
|
|
51 |
|
|
52 |
|
|
53 |
subsection {* The zero polynomial *}
|
|
54 |
|
|
55 |
instantiation poly :: (zero) zero
|
|
56 |
begin
|
|
57 |
|
|
58 |
definition
|
|
59 |
zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"
|
|
60 |
|
|
61 |
instance ..
|
|
62 |
end
|
|
63 |
|
|
64 |
lemma coeff_0 [simp]: "coeff 0 n = 0"
|
|
65 |
unfolding zero_poly_def
|
|
66 |
by (simp add: Abs_poly_inverse Poly_def)
|
|
67 |
|
|
68 |
lemma degree_0 [simp]: "degree 0 = 0"
|
|
69 |
by (rule order_antisym [OF degree_le le0]) simp
|
|
70 |
|
|
71 |
lemma leading_coeff_neq_0:
|
|
72 |
assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
|
|
73 |
proof (cases "degree p")
|
|
74 |
case 0
|
|
75 |
from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
|
|
76 |
by (simp add: expand_poly_eq)
|
|
77 |
then obtain n where "coeff p n \<noteq> 0" ..
|
|
78 |
hence "n \<le> degree p" by (rule le_degree)
|
|
79 |
with `coeff p n \<noteq> 0` and `degree p = 0`
|
|
80 |
show "coeff p (degree p) \<noteq> 0" by simp
|
|
81 |
next
|
|
82 |
case (Suc n)
|
|
83 |
from `degree p = Suc n` have "n < degree p" by simp
|
|
84 |
hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
|
|
85 |
then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
|
|
86 |
from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp
|
|
87 |
also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)
|
|
88 |
finally have "degree p = i" .
|
|
89 |
with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
|
|
90 |
qed
|
|
91 |
|
|
92 |
lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
|
|
93 |
by (cases "p = 0", simp, simp add: leading_coeff_neq_0)
|
|
94 |
|
|
95 |
|
|
96 |
subsection {* List-style constructor for polynomials *}
|
|
97 |
|
|
98 |
definition
|
|
99 |
pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
|
|
100 |
where
|
|
101 |
[code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
|
|
102 |
|
|
103 |
lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
|
|
104 |
unfolding Poly_def by (auto split: nat.split)
|
|
105 |
|
|
106 |
lemma coeff_pCons:
|
|
107 |
"coeff (pCons a p) = nat_case a (coeff p)"
|
|
108 |
unfolding pCons_def
|
|
109 |
by (simp add: Abs_poly_inverse Poly_nat_case coeff)
|
|
110 |
|
|
111 |
lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
|
|
112 |
by (simp add: coeff_pCons)
|
|
113 |
|
|
114 |
lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
|
|
115 |
by (simp add: coeff_pCons)
|
|
116 |
|
|
117 |
lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
|
|
118 |
by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)
|
|
119 |
|
|
120 |
lemma degree_pCons_eq:
|
|
121 |
"p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
|
|
122 |
apply (rule order_antisym [OF degree_pCons_le])
|
|
123 |
apply (rule le_degree, simp)
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma degree_pCons_0: "degree (pCons a 0) = 0"
|
|
127 |
apply (rule order_antisym [OF _ le0])
|
|
128 |
apply (rule degree_le, simp add: coeff_pCons split: nat.split)
|
|
129 |
done
|
|
130 |
|
|
131 |
lemma degree_pCons_eq_if:
|
|
132 |
"degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
|
|
133 |
apply (cases "p = 0", simp_all)
|
|
134 |
apply (rule order_antisym [OF _ le0])
|
|
135 |
apply (rule degree_le, simp add: coeff_pCons split: nat.split)
|
|
136 |
apply (rule order_antisym [OF degree_pCons_le])
|
|
137 |
apply (rule le_degree, simp)
|
|
138 |
done
|
|
139 |
|
|
140 |
lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
|
|
141 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
142 |
|
|
143 |
lemma pCons_eq_iff [simp]:
|
|
144 |
"pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
|
|
145 |
proof (safe)
|
|
146 |
assume "pCons a p = pCons b q"
|
|
147 |
then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
|
|
148 |
then show "a = b" by simp
|
|
149 |
next
|
|
150 |
assume "pCons a p = pCons b q"
|
|
151 |
then have "\<forall>n. coeff (pCons a p) (Suc n) =
|
|
152 |
coeff (pCons b q) (Suc n)" by simp
|
|
153 |
then show "p = q" by (simp add: expand_poly_eq)
|
|
154 |
qed
|
|
155 |
|
|
156 |
lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
|
|
157 |
using pCons_eq_iff [of a p 0 0] by simp
|
|
158 |
|
|
159 |
lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
|
|
160 |
unfolding Poly_def
|
|
161 |
by (clarify, rule_tac x=n in exI, simp)
|
|
162 |
|
|
163 |
lemma pCons_cases [cases type: poly]:
|
|
164 |
obtains (pCons) a q where "p = pCons a q"
|
|
165 |
proof
|
|
166 |
show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
|
|
167 |
by (rule poly_ext)
|
|
168 |
(simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
|
|
169 |
split: nat.split)
|
|
170 |
qed
|
|
171 |
|
|
172 |
lemma pCons_induct [case_names 0 pCons, induct type: poly]:
|
|
173 |
assumes zero: "P 0"
|
|
174 |
assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
|
|
175 |
shows "P p"
|
|
176 |
proof (induct p rule: measure_induct_rule [where f=degree])
|
|
177 |
case (less p)
|
|
178 |
obtain a q where "p = pCons a q" by (rule pCons_cases)
|
|
179 |
have "P q"
|
|
180 |
proof (cases "q = 0")
|
|
181 |
case True
|
|
182 |
then show "P q" by (simp add: zero)
|
|
183 |
next
|
|
184 |
case False
|
|
185 |
then have "degree (pCons a q) = Suc (degree q)"
|
|
186 |
by (rule degree_pCons_eq)
|
|
187 |
then have "degree q < degree p"
|
|
188 |
using `p = pCons a q` by simp
|
|
189 |
then show "P q"
|
|
190 |
by (rule less.hyps)
|
|
191 |
qed
|
|
192 |
then have "P (pCons a q)"
|
|
193 |
by (rule pCons)
|
|
194 |
then show ?case
|
|
195 |
using `p = pCons a q` by simp
|
|
196 |
qed
|
|
197 |
|
|
198 |
|
|
199 |
subsection {* Monomials *}
|
|
200 |
|
|
201 |
definition
|
|
202 |
monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
|
|
203 |
"monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"
|
|
204 |
|
|
205 |
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
|
|
206 |
unfolding monom_def
|
|
207 |
by (subst Abs_poly_inverse, auto simp add: Poly_def)
|
|
208 |
|
|
209 |
lemma monom_0: "monom a 0 = pCons a 0"
|
|
210 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
211 |
|
|
212 |
lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
|
|
213 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
214 |
|
|
215 |
lemma monom_eq_0 [simp]: "monom 0 n = 0"
|
|
216 |
by (rule poly_ext) simp
|
|
217 |
|
|
218 |
lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
|
|
219 |
by (simp add: expand_poly_eq)
|
|
220 |
|
|
221 |
lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
|
|
222 |
by (simp add: expand_poly_eq)
|
|
223 |
|
|
224 |
lemma degree_monom_le: "degree (monom a n) \<le> n"
|
|
225 |
by (rule degree_le, simp)
|
|
226 |
|
|
227 |
lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
|
|
228 |
apply (rule order_antisym [OF degree_monom_le])
|
|
229 |
apply (rule le_degree, simp)
|
|
230 |
done
|
|
231 |
|
|
232 |
|
|
233 |
subsection {* Addition and subtraction *}
|
|
234 |
|
|
235 |
instantiation poly :: (comm_monoid_add) comm_monoid_add
|
|
236 |
begin
|
|
237 |
|
|
238 |
definition
|
|
239 |
plus_poly_def [code del]:
|
|
240 |
"p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"
|
|
241 |
|
|
242 |
lemma Poly_add:
|
|
243 |
fixes f g :: "nat \<Rightarrow> 'a"
|
|
244 |
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
|
|
245 |
unfolding Poly_def
|
|
246 |
apply (clarify, rename_tac m n)
|
|
247 |
apply (rule_tac x="max m n" in exI, simp)
|
|
248 |
done
|
|
249 |
|
|
250 |
lemma coeff_add [simp]:
|
|
251 |
"coeff (p + q) n = coeff p n + coeff q n"
|
|
252 |
unfolding plus_poly_def
|
|
253 |
by (simp add: Abs_poly_inverse coeff Poly_add)
|
|
254 |
|
|
255 |
instance proof
|
|
256 |
fix p q r :: "'a poly"
|
|
257 |
show "(p + q) + r = p + (q + r)"
|
|
258 |
by (simp add: expand_poly_eq add_assoc)
|
|
259 |
show "p + q = q + p"
|
|
260 |
by (simp add: expand_poly_eq add_commute)
|
|
261 |
show "0 + p = p"
|
|
262 |
by (simp add: expand_poly_eq)
|
|
263 |
qed
|
|
264 |
|
|
265 |
end
|
|
266 |
|
|
267 |
instantiation poly :: (ab_group_add) ab_group_add
|
|
268 |
begin
|
|
269 |
|
|
270 |
definition
|
|
271 |
uminus_poly_def [code del]:
|
|
272 |
"- p = Abs_poly (\<lambda>n. - coeff p n)"
|
|
273 |
|
|
274 |
definition
|
|
275 |
minus_poly_def [code del]:
|
|
276 |
"p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"
|
|
277 |
|
|
278 |
lemma Poly_minus:
|
|
279 |
fixes f :: "nat \<Rightarrow> 'a"
|
|
280 |
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
|
|
281 |
unfolding Poly_def by simp
|
|
282 |
|
|
283 |
lemma Poly_diff:
|
|
284 |
fixes f g :: "nat \<Rightarrow> 'a"
|
|
285 |
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
|
|
286 |
unfolding diff_minus by (simp add: Poly_add Poly_minus)
|
|
287 |
|
|
288 |
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
|
|
289 |
unfolding uminus_poly_def
|
|
290 |
by (simp add: Abs_poly_inverse coeff Poly_minus)
|
|
291 |
|
|
292 |
lemma coeff_diff [simp]:
|
|
293 |
"coeff (p - q) n = coeff p n - coeff q n"
|
|
294 |
unfolding minus_poly_def
|
|
295 |
by (simp add: Abs_poly_inverse coeff Poly_diff)
|
|
296 |
|
|
297 |
instance proof
|
|
298 |
fix p q :: "'a poly"
|
|
299 |
show "- p + p = 0"
|
|
300 |
by (simp add: expand_poly_eq)
|
|
301 |
show "p - q = p + - q"
|
|
302 |
by (simp add: expand_poly_eq diff_minus)
|
|
303 |
qed
|
|
304 |
|
|
305 |
end
|
|
306 |
|
|
307 |
lemma add_pCons [simp]:
|
|
308 |
"pCons a p + pCons b q = pCons (a + b) (p + q)"
|
|
309 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
310 |
|
|
311 |
lemma minus_pCons [simp]:
|
|
312 |
"- pCons a p = pCons (- a) (- p)"
|
|
313 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
314 |
|
|
315 |
lemma diff_pCons [simp]:
|
|
316 |
"pCons a p - pCons b q = pCons (a - b) (p - q)"
|
|
317 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
318 |
|
|
319 |
lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
|
|
320 |
by (rule degree_le, auto simp add: coeff_eq_0)
|
|
321 |
|
29453
|
322 |
lemma degree_add_less:
|
|
323 |
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
|
|
324 |
by (auto intro: le_less_trans degree_add_le)
|
|
325 |
|
29451
|
326 |
lemma degree_add_eq_right:
|
|
327 |
"degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
|
|
328 |
apply (cases "q = 0", simp)
|
|
329 |
apply (rule order_antisym)
|
|
330 |
apply (rule ord_le_eq_trans [OF degree_add_le])
|
|
331 |
apply simp
|
|
332 |
apply (rule le_degree)
|
|
333 |
apply (simp add: coeff_eq_0)
|
|
334 |
done
|
|
335 |
|
|
336 |
lemma degree_add_eq_left:
|
|
337 |
"degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
|
|
338 |
using degree_add_eq_right [of q p]
|
|
339 |
by (simp add: add_commute)
|
|
340 |
|
|
341 |
lemma degree_minus [simp]: "degree (- p) = degree p"
|
|
342 |
unfolding degree_def by simp
|
|
343 |
|
|
344 |
lemma degree_diff_le: "degree (p - q) \<le> max (degree p) (degree q)"
|
|
345 |
using degree_add_le [where p=p and q="-q"]
|
|
346 |
by (simp add: diff_minus)
|
|
347 |
|
29453
|
348 |
lemma degree_diff_less:
|
|
349 |
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
|
|
350 |
by (auto intro: le_less_trans degree_diff_le)
|
|
351 |
|
29451
|
352 |
lemma add_monom: "monom a n + monom b n = monom (a + b) n"
|
|
353 |
by (rule poly_ext) simp
|
|
354 |
|
|
355 |
lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
|
|
356 |
by (rule poly_ext) simp
|
|
357 |
|
|
358 |
lemma minus_monom: "- monom a n = monom (-a) n"
|
|
359 |
by (rule poly_ext) simp
|
|
360 |
|
|
361 |
lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
|
|
362 |
by (cases "finite A", induct set: finite, simp_all)
|
|
363 |
|
|
364 |
lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
|
|
365 |
by (rule poly_ext) (simp add: coeff_setsum)
|
|
366 |
|
|
367 |
|
|
368 |
subsection {* Multiplication by a constant *}
|
|
369 |
|
|
370 |
definition
|
|
371 |
smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
|
|
372 |
"smult a p = Abs_poly (\<lambda>n. a * coeff p n)"
|
|
373 |
|
|
374 |
lemma Poly_smult:
|
|
375 |
fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
|
|
376 |
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
|
|
377 |
unfolding Poly_def
|
|
378 |
by (clarify, rule_tac x=n in exI, simp)
|
|
379 |
|
|
380 |
lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
|
|
381 |
unfolding smult_def
|
|
382 |
by (simp add: Abs_poly_inverse Poly_smult coeff)
|
|
383 |
|
|
384 |
lemma degree_smult_le: "degree (smult a p) \<le> degree p"
|
|
385 |
by (rule degree_le, simp add: coeff_eq_0)
|
|
386 |
|
|
387 |
lemma smult_smult: "smult a (smult b p) = smult (a * b) p"
|
|
388 |
by (rule poly_ext, simp add: mult_assoc)
|
|
389 |
|
|
390 |
lemma smult_0_right [simp]: "smult a 0 = 0"
|
|
391 |
by (rule poly_ext, simp)
|
|
392 |
|
|
393 |
lemma smult_0_left [simp]: "smult 0 p = 0"
|
|
394 |
by (rule poly_ext, simp)
|
|
395 |
|
|
396 |
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
|
|
397 |
by (rule poly_ext, simp)
|
|
398 |
|
|
399 |
lemma smult_add_right:
|
|
400 |
"smult a (p + q) = smult a p + smult a q"
|
|
401 |
by (rule poly_ext, simp add: ring_simps)
|
|
402 |
|
|
403 |
lemma smult_add_left:
|
|
404 |
"smult (a + b) p = smult a p + smult b p"
|
|
405 |
by (rule poly_ext, simp add: ring_simps)
|
|
406 |
|
|
407 |
lemma smult_minus_right:
|
|
408 |
"smult (a::'a::comm_ring) (- p) = - smult a p"
|
|
409 |
by (rule poly_ext, simp)
|
|
410 |
|
|
411 |
lemma smult_minus_left:
|
|
412 |
"smult (- a::'a::comm_ring) p = - smult a p"
|
|
413 |
by (rule poly_ext, simp)
|
|
414 |
|
|
415 |
lemma smult_diff_right:
|
|
416 |
"smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
|
|
417 |
by (rule poly_ext, simp add: ring_simps)
|
|
418 |
|
|
419 |
lemma smult_diff_left:
|
|
420 |
"smult (a - b::'a::comm_ring) p = smult a p - smult b p"
|
|
421 |
by (rule poly_ext, simp add: ring_simps)
|
|
422 |
|
|
423 |
lemma smult_pCons [simp]:
|
|
424 |
"smult a (pCons b p) = pCons (a * b) (smult a p)"
|
|
425 |
by (rule poly_ext, simp add: coeff_pCons split: nat.split)
|
|
426 |
|
|
427 |
lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
|
|
428 |
by (induct n, simp add: monom_0, simp add: monom_Suc)
|
|
429 |
|
|
430 |
|
|
431 |
subsection {* Multiplication of polynomials *}
|
|
432 |
|
|
433 |
lemma Poly_mult_lemma:
|
|
434 |
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0" and m n :: nat
|
|
435 |
assumes "\<forall>i>m. f i = 0"
|
|
436 |
assumes "\<forall>j>n. g j = 0"
|
|
437 |
shows "\<forall>k>m+n. (\<Sum>i\<le>k. f i * g (k-i)) = 0"
|
|
438 |
proof (clarify)
|
|
439 |
fix k :: nat
|
|
440 |
assume "m + n < k"
|
|
441 |
show "(\<Sum>i\<le>k. f i * g (k - i)) = 0"
|
|
442 |
proof (rule setsum_0' [rule_format])
|
|
443 |
fix i :: nat
|
|
444 |
assume "i \<in> {..k}" hence "i \<le> k" by simp
|
|
445 |
with `m + n < k` have "m < i \<or> n < k - i" by arith
|
|
446 |
thus "f i * g (k - i) = 0"
|
|
447 |
using prems by auto
|
|
448 |
qed
|
|
449 |
qed
|
|
450 |
|
|
451 |
lemma Poly_mult:
|
|
452 |
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0"
|
|
453 |
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i * g (n-i)) \<in> Poly"
|
|
454 |
unfolding Poly_def
|
|
455 |
by (safe, rule exI, rule Poly_mult_lemma)
|
|
456 |
|
|
457 |
lemma poly_mult_assoc_lemma:
|
|
458 |
fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
|
|
459 |
shows "(\<Sum>j\<le>k. \<Sum>i\<le>j. f i (j - i) (n - j)) =
|
|
460 |
(\<Sum>j\<le>k. \<Sum>i\<le>k - j. f j i (n - j - i))"
|
|
461 |
proof (induct k)
|
|
462 |
case 0 show ?case by simp
|
|
463 |
next
|
|
464 |
case (Suc k) thus ?case
|
|
465 |
by (simp add: Suc_diff_le setsum_addf add_assoc
|
|
466 |
cong: strong_setsum_cong)
|
|
467 |
qed
|
|
468 |
|
|
469 |
lemma poly_mult_commute_lemma:
|
|
470 |
fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
|
|
471 |
shows "(\<Sum>i\<le>n. f i (n - i)) = (\<Sum>i\<le>n. f (n - i) i)"
|
|
472 |
proof (rule setsum_reindex_cong)
|
|
473 |
show "inj_on (\<lambda>i. n - i) {..n}"
|
|
474 |
by (rule inj_onI) simp
|
|
475 |
show "{..n} = (\<lambda>i. n - i) ` {..n}"
|
|
476 |
by (auto, rule_tac x="n - x" in image_eqI, simp_all)
|
|
477 |
next
|
|
478 |
fix i assume "i \<in> {..n}"
|
|
479 |
hence "n - (n - i) = i" by simp
|
|
480 |
thus "f (n - i) i = f (n - i) (n - (n - i))" by simp
|
|
481 |
qed
|
|
482 |
|
|
483 |
text {* TODO: move to appropriate theory *}
|
|
484 |
lemma setsum_atMost_Suc_shift:
|
|
485 |
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
|
|
486 |
shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
|
|
487 |
proof (induct n)
|
|
488 |
case 0 show ?case by simp
|
|
489 |
next
|
|
490 |
case (Suc n) note IH = this
|
|
491 |
have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
|
|
492 |
by (rule setsum_atMost_Suc)
|
|
493 |
also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
|
|
494 |
by (rule IH)
|
|
495 |
also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
|
|
496 |
f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
|
|
497 |
by (rule add_assoc)
|
|
498 |
also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
|
|
499 |
by (rule setsum_atMost_Suc [symmetric])
|
|
500 |
finally show ?case .
|
|
501 |
qed
|
|
502 |
|
|
503 |
instantiation poly :: (comm_semiring_0) comm_semiring_0
|
|
504 |
begin
|
|
505 |
|
|
506 |
definition
|
|
507 |
times_poly_def:
|
|
508 |
"p * q = Abs_poly (\<lambda>n. \<Sum>i\<le>n. coeff p i * coeff q (n-i))"
|
|
509 |
|
|
510 |
lemma coeff_mult:
|
|
511 |
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
|
|
512 |
unfolding times_poly_def
|
|
513 |
by (simp add: Abs_poly_inverse coeff Poly_mult)
|
|
514 |
|
|
515 |
instance proof
|
|
516 |
fix p q r :: "'a poly"
|
|
517 |
show 0: "0 * p = 0"
|
|
518 |
by (simp add: expand_poly_eq coeff_mult)
|
|
519 |
show "p * 0 = 0"
|
|
520 |
by (simp add: expand_poly_eq coeff_mult)
|
|
521 |
show "(p + q) * r = p * r + q * r"
|
|
522 |
by (simp add: expand_poly_eq coeff_mult left_distrib setsum_addf)
|
|
523 |
show "(p * q) * r = p * (q * r)"
|
|
524 |
proof (rule poly_ext)
|
|
525 |
fix n :: nat
|
|
526 |
have "(\<Sum>j\<le>n. \<Sum>i\<le>j. coeff p i * coeff q (j - i) * coeff r (n - j)) =
|
|
527 |
(\<Sum>j\<le>n. \<Sum>i\<le>n - j. coeff p j * coeff q i * coeff r (n - j - i))"
|
|
528 |
by (rule poly_mult_assoc_lemma)
|
|
529 |
thus "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
|
|
530 |
by (simp add: coeff_mult setsum_right_distrib
|
|
531 |
setsum_left_distrib mult_assoc)
|
|
532 |
qed
|
|
533 |
show "p * q = q * p"
|
|
534 |
proof (rule poly_ext)
|
|
535 |
fix n :: nat
|
|
536 |
have "(\<Sum>i\<le>n. coeff p i * coeff q (n - i)) =
|
|
537 |
(\<Sum>i\<le>n. coeff p (n - i) * coeff q i)"
|
|
538 |
by (rule poly_mult_commute_lemma)
|
|
539 |
thus "coeff (p * q) n = coeff (q * p) n"
|
|
540 |
by (simp add: coeff_mult mult_commute)
|
|
541 |
qed
|
|
542 |
qed
|
|
543 |
|
|
544 |
end
|
|
545 |
|
|
546 |
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
|
|
547 |
apply (rule degree_le, simp add: coeff_mult)
|
|
548 |
apply (rule Poly_mult_lemma)
|
|
549 |
apply (simp_all add: coeff_eq_0)
|
|
550 |
done
|
|
551 |
|
|
552 |
lemma mult_pCons_left [simp]:
|
|
553 |
"pCons a p * q = smult a q + pCons 0 (p * q)"
|
|
554 |
apply (rule poly_ext)
|
|
555 |
apply (case_tac n)
|
|
556 |
apply (simp add: coeff_mult)
|
|
557 |
apply (simp add: coeff_mult setsum_atMost_Suc_shift
|
|
558 |
del: setsum_atMost_Suc)
|
|
559 |
done
|
|
560 |
|
|
561 |
lemma mult_pCons_right [simp]:
|
|
562 |
"p * pCons a q = smult a p + pCons 0 (p * q)"
|
|
563 |
using mult_pCons_left [of a q p] by (simp add: mult_commute)
|
|
564 |
|
|
565 |
lemma mult_smult_left: "smult a p * q = smult a (p * q)"
|
|
566 |
by (induct p, simp, simp add: smult_add_right smult_smult)
|
|
567 |
|
|
568 |
lemma mult_smult_right: "p * smult a q = smult a (p * q)"
|
|
569 |
using mult_smult_left [of a q p] by (simp add: mult_commute)
|
|
570 |
|
|
571 |
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
|
|
572 |
by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
|
|
573 |
|
|
574 |
|
|
575 |
subsection {* The unit polynomial and exponentiation *}
|
|
576 |
|
|
577 |
instantiation poly :: (comm_semiring_1) comm_semiring_1
|
|
578 |
begin
|
|
579 |
|
|
580 |
definition
|
|
581 |
one_poly_def:
|
|
582 |
"1 = pCons 1 0"
|
|
583 |
|
|
584 |
instance proof
|
|
585 |
fix p :: "'a poly" show "1 * p = p"
|
|
586 |
unfolding one_poly_def
|
|
587 |
by simp
|
|
588 |
next
|
|
589 |
show "0 \<noteq> (1::'a poly)"
|
|
590 |
unfolding one_poly_def by simp
|
|
591 |
qed
|
|
592 |
|
|
593 |
end
|
|
594 |
|
|
595 |
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
|
|
596 |
unfolding one_poly_def
|
|
597 |
by (simp add: coeff_pCons split: nat.split)
|
|
598 |
|
|
599 |
lemma degree_1 [simp]: "degree 1 = 0"
|
|
600 |
unfolding one_poly_def
|
|
601 |
by (rule degree_pCons_0)
|
|
602 |
|
|
603 |
instantiation poly :: (comm_semiring_1) recpower
|
|
604 |
begin
|
|
605 |
|
|
606 |
primrec power_poly where
|
|
607 |
power_poly_0: "(p::'a poly) ^ 0 = 1"
|
|
608 |
| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"
|
|
609 |
|
|
610 |
instance
|
|
611 |
by default simp_all
|
|
612 |
|
|
613 |
end
|
|
614 |
|
|
615 |
instance poly :: (comm_ring) comm_ring ..
|
|
616 |
|
|
617 |
instance poly :: (comm_ring_1) comm_ring_1 ..
|
|
618 |
|
|
619 |
instantiation poly :: (comm_ring_1) number_ring
|
|
620 |
begin
|
|
621 |
|
|
622 |
definition
|
|
623 |
"number_of k = (of_int k :: 'a poly)"
|
|
624 |
|
|
625 |
instance
|
|
626 |
by default (rule number_of_poly_def)
|
|
627 |
|
|
628 |
end
|
|
629 |
|
|
630 |
|
|
631 |
subsection {* Polynomials form an integral domain *}
|
|
632 |
|
|
633 |
lemma coeff_mult_degree_sum:
|
|
634 |
"coeff (p * q) (degree p + degree q) =
|
|
635 |
coeff p (degree p) * coeff q (degree q)"
|
|
636 |
apply (simp add: coeff_mult)
|
|
637 |
apply (subst setsum_diff1' [where a="degree p"])
|
|
638 |
apply simp
|
|
639 |
apply simp
|
|
640 |
apply (subst setsum_0' [rule_format])
|
|
641 |
apply clarsimp
|
|
642 |
apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q - a")
|
|
643 |
apply (force simp add: coeff_eq_0)
|
|
644 |
apply arith
|
|
645 |
apply simp
|
|
646 |
done
|
|
647 |
|
|
648 |
instance poly :: (idom) idom
|
|
649 |
proof
|
|
650 |
fix p q :: "'a poly"
|
|
651 |
assume "p \<noteq> 0" and "q \<noteq> 0"
|
|
652 |
have "coeff (p * q) (degree p + degree q) =
|
|
653 |
coeff p (degree p) * coeff q (degree q)"
|
|
654 |
by (rule coeff_mult_degree_sum)
|
|
655 |
also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
|
|
656 |
using `p \<noteq> 0` and `q \<noteq> 0` by simp
|
|
657 |
finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
|
|
658 |
thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
|
|
659 |
qed
|
|
660 |
|
|
661 |
lemma degree_mult_eq:
|
|
662 |
fixes p q :: "'a::idom poly"
|
|
663 |
shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
|
|
664 |
apply (rule order_antisym [OF degree_mult_le le_degree])
|
|
665 |
apply (simp add: coeff_mult_degree_sum)
|
|
666 |
done
|
|
667 |
|
|
668 |
lemma dvd_imp_degree_le:
|
|
669 |
fixes p q :: "'a::idom poly"
|
|
670 |
shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
|
|
671 |
by (erule dvdE, simp add: degree_mult_eq)
|
|
672 |
|
|
673 |
|
|
674 |
subsection {* Long division of polynomials *}
|
|
675 |
|
|
676 |
definition
|
|
677 |
divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
|
|
678 |
where
|
|
679 |
"divmod_poly_rel x y q r \<longleftrightarrow>
|
|
680 |
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
|
|
681 |
|
|
682 |
lemma divmod_poly_rel_0:
|
|
683 |
"divmod_poly_rel 0 y 0 0"
|
|
684 |
unfolding divmod_poly_rel_def by simp
|
|
685 |
|
|
686 |
lemma divmod_poly_rel_by_0:
|
|
687 |
"divmod_poly_rel x 0 0 x"
|
|
688 |
unfolding divmod_poly_rel_def by simp
|
|
689 |
|
|
690 |
lemma eq_zero_or_degree_less:
|
|
691 |
assumes "degree p \<le> n" and "coeff p n = 0"
|
|
692 |
shows "p = 0 \<or> degree p < n"
|
|
693 |
proof (cases n)
|
|
694 |
case 0
|
|
695 |
with `degree p \<le> n` and `coeff p n = 0`
|
|
696 |
have "coeff p (degree p) = 0" by simp
|
|
697 |
then have "p = 0" by simp
|
|
698 |
then show ?thesis ..
|
|
699 |
next
|
|
700 |
case (Suc m)
|
|
701 |
have "\<forall>i>n. coeff p i = 0"
|
|
702 |
using `degree p \<le> n` by (simp add: coeff_eq_0)
|
|
703 |
then have "\<forall>i\<ge>n. coeff p i = 0"
|
|
704 |
using `coeff p n = 0` by (simp add: le_less)
|
|
705 |
then have "\<forall>i>m. coeff p i = 0"
|
|
706 |
using `n = Suc m` by (simp add: less_eq_Suc_le)
|
|
707 |
then have "degree p \<le> m"
|
|
708 |
by (rule degree_le)
|
|
709 |
then have "degree p < n"
|
|
710 |
using `n = Suc m` by (simp add: less_Suc_eq_le)
|
|
711 |
then show ?thesis ..
|
|
712 |
qed
|
|
713 |
|
|
714 |
lemma divmod_poly_rel_pCons:
|
|
715 |
assumes rel: "divmod_poly_rel x y q r"
|
|
716 |
assumes y: "y \<noteq> 0"
|
|
717 |
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
|
|
718 |
shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
|
|
719 |
(is "divmod_poly_rel ?x y ?q ?r")
|
|
720 |
proof -
|
|
721 |
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
|
|
722 |
using assms unfolding divmod_poly_rel_def by simp_all
|
|
723 |
|
|
724 |
have 1: "?x = ?q * y + ?r"
|
|
725 |
using b x by simp
|
|
726 |
|
|
727 |
have 2: "?r = 0 \<or> degree ?r < degree y"
|
|
728 |
proof (rule eq_zero_or_degree_less)
|
|
729 |
have "degree ?r \<le> max (degree (pCons a r)) (degree (smult b y))"
|
|
730 |
by (rule degree_diff_le)
|
|
731 |
also have "\<dots> \<le> degree y"
|
|
732 |
proof (rule min_max.le_supI)
|
|
733 |
show "degree (pCons a r) \<le> degree y"
|
|
734 |
using r by (auto simp add: degree_pCons_eq_if)
|
|
735 |
show "degree (smult b y) \<le> degree y"
|
|
736 |
by (rule degree_smult_le)
|
|
737 |
qed
|
|
738 |
finally show "degree ?r \<le> degree y" .
|
|
739 |
next
|
|
740 |
show "coeff ?r (degree y) = 0"
|
|
741 |
using `y \<noteq> 0` unfolding b by simp
|
|
742 |
qed
|
|
743 |
|
|
744 |
from 1 2 show ?thesis
|
|
745 |
unfolding divmod_poly_rel_def
|
|
746 |
using `y \<noteq> 0` by simp
|
|
747 |
qed
|
|
748 |
|
|
749 |
lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"
|
|
750 |
apply (cases "y = 0")
|
|
751 |
apply (fast intro!: divmod_poly_rel_by_0)
|
|
752 |
apply (induct x)
|
|
753 |
apply (fast intro!: divmod_poly_rel_0)
|
|
754 |
apply (fast intro!: divmod_poly_rel_pCons)
|
|
755 |
done
|
|
756 |
|
|
757 |
lemma divmod_poly_rel_unique:
|
|
758 |
assumes 1: "divmod_poly_rel x y q1 r1"
|
|
759 |
assumes 2: "divmod_poly_rel x y q2 r2"
|
|
760 |
shows "q1 = q2 \<and> r1 = r2"
|
|
761 |
proof (cases "y = 0")
|
|
762 |
assume "y = 0" with assms show ?thesis
|
|
763 |
by (simp add: divmod_poly_rel_def)
|
|
764 |
next
|
|
765 |
assume [simp]: "y \<noteq> 0"
|
|
766 |
from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
|
|
767 |
unfolding divmod_poly_rel_def by simp_all
|
|
768 |
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
|
|
769 |
unfolding divmod_poly_rel_def by simp_all
|
|
770 |
from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
|
|
771 |
by (simp add: ring_simps)
|
|
772 |
from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
|
29453
|
773 |
by (auto intro: degree_diff_less)
|
29451
|
774 |
|
|
775 |
show "q1 = q2 \<and> r1 = r2"
|
|
776 |
proof (rule ccontr)
|
|
777 |
assume "\<not> (q1 = q2 \<and> r1 = r2)"
|
|
778 |
with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
|
|
779 |
with r3 have "degree (r2 - r1) < degree y" by simp
|
|
780 |
also have "degree y \<le> degree (q1 - q2) + degree y" by simp
|
|
781 |
also have "\<dots> = degree ((q1 - q2) * y)"
|
|
782 |
using `q1 \<noteq> q2` by (simp add: degree_mult_eq)
|
|
783 |
also have "\<dots> = degree (r2 - r1)"
|
|
784 |
using q3 by simp
|
|
785 |
finally have "degree (r2 - r1) < degree (r2 - r1)" .
|
|
786 |
then show "False" by simp
|
|
787 |
qed
|
|
788 |
qed
|
|
789 |
|
|
790 |
lemmas divmod_poly_rel_unique_div =
|
|
791 |
divmod_poly_rel_unique [THEN conjunct1, standard]
|
|
792 |
|
|
793 |
lemmas divmod_poly_rel_unique_mod =
|
|
794 |
divmod_poly_rel_unique [THEN conjunct2, standard]
|
|
795 |
|
|
796 |
instantiation poly :: (field) ring_div
|
|
797 |
begin
|
|
798 |
|
|
799 |
definition div_poly where
|
|
800 |
[code del]: "x div y = (THE q. \<exists>r. divmod_poly_rel x y q r)"
|
|
801 |
|
|
802 |
definition mod_poly where
|
|
803 |
[code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"
|
|
804 |
|
|
805 |
lemma div_poly_eq:
|
|
806 |
"divmod_poly_rel x y q r \<Longrightarrow> x div y = q"
|
|
807 |
unfolding div_poly_def
|
|
808 |
by (fast elim: divmod_poly_rel_unique_div)
|
|
809 |
|
|
810 |
lemma mod_poly_eq:
|
|
811 |
"divmod_poly_rel x y q r \<Longrightarrow> x mod y = r"
|
|
812 |
unfolding mod_poly_def
|
|
813 |
by (fast elim: divmod_poly_rel_unique_mod)
|
|
814 |
|
|
815 |
lemma divmod_poly_rel:
|
|
816 |
"divmod_poly_rel x y (x div y) (x mod y)"
|
|
817 |
proof -
|
|
818 |
from divmod_poly_rel_exists
|
|
819 |
obtain q r where "divmod_poly_rel x y q r" by fast
|
|
820 |
thus ?thesis
|
|
821 |
by (simp add: div_poly_eq mod_poly_eq)
|
|
822 |
qed
|
|
823 |
|
|
824 |
instance proof
|
|
825 |
fix x y :: "'a poly"
|
|
826 |
show "x div y * y + x mod y = x"
|
|
827 |
using divmod_poly_rel [of x y]
|
|
828 |
by (simp add: divmod_poly_rel_def)
|
|
829 |
next
|
|
830 |
fix x :: "'a poly"
|
|
831 |
have "divmod_poly_rel x 0 0 x"
|
|
832 |
by (rule divmod_poly_rel_by_0)
|
|
833 |
thus "x div 0 = 0"
|
|
834 |
by (rule div_poly_eq)
|
|
835 |
next
|
|
836 |
fix y :: "'a poly"
|
|
837 |
have "divmod_poly_rel 0 y 0 0"
|
|
838 |
by (rule divmod_poly_rel_0)
|
|
839 |
thus "0 div y = 0"
|
|
840 |
by (rule div_poly_eq)
|
|
841 |
next
|
|
842 |
fix x y z :: "'a poly"
|
|
843 |
assume "y \<noteq> 0"
|
|
844 |
hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)"
|
|
845 |
using divmod_poly_rel [of x y]
|
|
846 |
by (simp add: divmod_poly_rel_def left_distrib)
|
|
847 |
thus "(x + z * y) div y = z + x div y"
|
|
848 |
by (rule div_poly_eq)
|
|
849 |
qed
|
|
850 |
|
|
851 |
end
|
|
852 |
|
|
853 |
lemma degree_mod_less:
|
|
854 |
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
|
|
855 |
using divmod_poly_rel [of x y]
|
|
856 |
unfolding divmod_poly_rel_def by simp
|
|
857 |
|
|
858 |
lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
|
|
859 |
proof -
|
|
860 |
assume "degree x < degree y"
|
|
861 |
hence "divmod_poly_rel x y 0 x"
|
|
862 |
by (simp add: divmod_poly_rel_def)
|
|
863 |
thus "x div y = 0" by (rule div_poly_eq)
|
|
864 |
qed
|
|
865 |
|
|
866 |
lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
|
|
867 |
proof -
|
|
868 |
assume "degree x < degree y"
|
|
869 |
hence "divmod_poly_rel x y 0 x"
|
|
870 |
by (simp add: divmod_poly_rel_def)
|
|
871 |
thus "x mod y = x" by (rule mod_poly_eq)
|
|
872 |
qed
|
|
873 |
|
|
874 |
lemma mod_pCons:
|
|
875 |
fixes a and x
|
|
876 |
assumes y: "y \<noteq> 0"
|
|
877 |
defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
|
|
878 |
shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
|
|
879 |
unfolding b
|
|
880 |
apply (rule mod_poly_eq)
|
|
881 |
apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl])
|
|
882 |
done
|
|
883 |
|
|
884 |
|
|
885 |
subsection {* Evaluation of polynomials *}
|
|
886 |
|
|
887 |
definition
|
|
888 |
poly :: "'a::{comm_semiring_1,recpower} poly \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
889 |
"poly p = (\<lambda>x. \<Sum>n\<le>degree p. coeff p n * x ^ n)"
|
|
890 |
|
|
891 |
lemma poly_0 [simp]: "poly 0 x = 0"
|
|
892 |
unfolding poly_def by simp
|
|
893 |
|
|
894 |
lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
|
|
895 |
unfolding poly_def
|
|
896 |
by (simp add: degree_pCons_eq_if setsum_atMost_Suc_shift power_Suc
|
|
897 |
setsum_left_distrib setsum_right_distrib mult_ac
|
|
898 |
del: setsum_atMost_Suc)
|
|
899 |
|
|
900 |
lemma poly_1 [simp]: "poly 1 x = 1"
|
|
901 |
unfolding one_poly_def by simp
|
|
902 |
|
|
903 |
lemma poly_monom: "poly (monom a n) x = a * x ^ n"
|
|
904 |
by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
|
|
905 |
|
|
906 |
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
|
|
907 |
apply (induct p arbitrary: q, simp)
|
|
908 |
apply (case_tac q, simp, simp add: ring_simps)
|
|
909 |
done
|
|
910 |
|
|
911 |
lemma poly_minus [simp]:
|
|
912 |
fixes x :: "'a::{comm_ring_1,recpower}"
|
|
913 |
shows "poly (- p) x = - poly p x"
|
|
914 |
by (induct p, simp_all)
|
|
915 |
|
|
916 |
lemma poly_diff [simp]:
|
|
917 |
fixes x :: "'a::{comm_ring_1,recpower}"
|
|
918 |
shows "poly (p - q) x = poly p x - poly q x"
|
|
919 |
by (simp add: diff_minus)
|
|
920 |
|
|
921 |
lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
|
|
922 |
by (cases "finite A", induct set: finite, simp_all)
|
|
923 |
|
|
924 |
lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
|
|
925 |
by (induct p, simp, simp add: ring_simps)
|
|
926 |
|
|
927 |
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
|
|
928 |
by (induct p, simp_all, simp add: ring_simps)
|
|
929 |
|
|
930 |
end
|