author | haftmann |
Mon, 27 Apr 2009 10:11:44 +0200 | |
changeset 31001 | 7e6ffd8f51a9 |
parent 30968 | 10fef94f40fc |
child 31021 | 53642251a04f |
permissions | -rw-r--r-- |
13936 | 1 |
(* |
2 |
Title: Univariate Polynomials |
|
3 |
Author: Clemens Ballarin, started 9 December 1996 |
|
4 |
Copyright: Clemens Ballarin |
|
5 |
*) |
|
6 |
||
7 |
header {* Univariate Polynomials *} |
|
8 |
||
15481 | 9 |
theory UnivPoly2 |
10 |
imports "../abstract/Abstract" |
|
11 |
begin |
|
13936 | 12 |
|
16640
03bdf544a552
Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents:
16052
diff
changeset
|
13 |
(* With this variant of setsum_cong, assumptions |
13936 | 14 |
like i:{m..n} get simplified (to m <= i & i <= n). *) |
15 |
||
16640
03bdf544a552
Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents:
16052
diff
changeset
|
16 |
declare strong_setsum_cong [cong] |
13936 | 17 |
|
18 |
section {* Definition of type up *} |
|
19 |
||
21423 | 20 |
definition |
21 |
bound :: "[nat, nat => 'a::zero] => bool" where |
|
22 |
"bound n f = (ALL i. n < i --> f i = 0)" |
|
13936 | 23 |
|
24 |
lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f" |
|
21423 | 25 |
unfolding bound_def by blast |
13936 | 26 |
|
27 |
lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P" |
|
21423 | 28 |
unfolding bound_def by blast |
13936 | 29 |
|
30 |
lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0" |
|
21423 | 31 |
unfolding bound_def by blast |
13936 | 32 |
|
33 |
lemma bound_below: |
|
34 |
assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m" |
|
35 |
proof (rule classical) |
|
36 |
assume "~ ?thesis" |
|
37 |
then have "m < n" by arith |
|
38 |
with bound have "f n = 0" .. |
|
39 |
with nonzero show ?thesis by contradiction |
|
40 |
qed |
|
41 |
||
42 |
typedef (UP) |
|
21423 | 43 |
('a) up = "{f :: nat => 'a::zero. EX n. bound n f}" |
44 |
by (rule+) (* Question: what does trace_rule show??? *) |
|
45 |
||
13936 | 46 |
|
47 |
section {* Constants *} |
|
48 |
||
21423 | 49 |
definition |
50 |
coeff :: "['a up, nat] => ('a::zero)" where |
|
51 |
"coeff p n = Rep_UP p n" |
|
13936 | 52 |
|
21423 | 53 |
definition |
54 |
monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where |
|
55 |
"monom a n = Abs_UP (%i. if i=n then a else 0)" |
|
56 |
||
57 |
definition |
|
58 |
smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where |
|
59 |
"a *s p = Abs_UP (%i. a * Rep_UP p i)" |
|
13936 | 60 |
|
61 |
lemma coeff_bound_ex: "EX n. bound n (coeff p)" |
|
62 |
proof - |
|
63 |
have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) |
|
64 |
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast |
|
65 |
then show ?thesis .. |
|
66 |
qed |
|
67 |
||
68 |
lemma bound_coeff_obtain: |
|
69 |
assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" |
|
70 |
proof - |
|
71 |
have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) |
|
72 |
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast |
|
73 |
with prem show P . |
|
74 |
qed |
|
75 |
||
21423 | 76 |
|
13936 | 77 |
text {* Ring operations *} |
78 |
||
25762 | 79 |
instantiation up :: (zero) zero |
80 |
begin |
|
81 |
||
82 |
definition |
|
83 |
up_zero_def: "0 = monom 0 0" |
|
84 |
||
85 |
instance .. |
|
86 |
||
87 |
end |
|
88 |
||
89 |
instantiation up :: ("{one, zero}") one |
|
90 |
begin |
|
91 |
||
92 |
definition |
|
93 |
up_one_def: "1 = monom 1 0" |
|
94 |
||
95 |
instance .. |
|
96 |
||
97 |
end |
|
98 |
||
99 |
instantiation up :: ("{plus, zero}") plus |
|
100 |
begin |
|
101 |
||
102 |
definition |
|
103 |
up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)" |
|
104 |
||
105 |
instance .. |
|
13936 | 106 |
|
25762 | 107 |
end |
108 |
||
109 |
instantiation up :: ("{one, times, uminus, zero}") uminus |
|
110 |
begin |
|
111 |
||
112 |
definition |
|
113 |
(* note: - 1 is different from -1; latter is of class number *) |
|
114 |
up_uminus_def:"- p = (- 1) *s p" |
|
115 |
(* easier to use than "Abs_UP (%i. - Rep_UP p i)" *) |
|
116 |
||
117 |
instance .. |
|
118 |
||
119 |
end |
|
120 |
||
121 |
instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus |
|
122 |
begin |
|
123 |
||
124 |
definition |
|
125 |
up_minus_def: "(a :: 'a up) - b = a + (-b)" |
|
126 |
||
127 |
instance .. |
|
128 |
||
129 |
end |
|
130 |
||
131 |
instantiation up :: ("{times, comm_monoid_add}") times |
|
132 |
begin |
|
133 |
||
134 |
definition |
|
135 |
up_mult_def: "p * q = Abs_UP (%n::nat. setsum |
|
13936 | 136 |
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})" |
25762 | 137 |
|
138 |
instance .. |
|
139 |
||
140 |
end |
|
141 |
||
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27540
diff
changeset
|
142 |
instance up :: ("{times, comm_monoid_add}") Ring_and_Field.dvd .. |
26563 | 143 |
|
144 |
instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse |
|
25762 | 145 |
begin |
146 |
||
147 |
definition |
|
148 |
up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then |
|
149 |
THE x. a * x = 1 else 0)" |
|
13936 | 150 |
|
25762 | 151 |
definition |
152 |
up_divide_def: "(a :: 'a up) / b = a * inverse b" |
|
153 |
||
154 |
instance .. |
|
155 |
||
156 |
end |
|
13936 | 157 |
|
21423 | 158 |
|
13936 | 159 |
subsection {* Effect of operations on coefficients *} |
160 |
||
161 |
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)" |
|
162 |
proof - |
|
163 |
have "(%n. if n = m then a else 0) : UP" |
|
164 |
using UP_def by force |
|
165 |
from this show ?thesis |
|
166 |
by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP) |
|
167 |
qed |
|
168 |
||
169 |
lemma coeff_zero [simp]: "coeff 0 n = 0" |
|
170 |
proof (unfold up_zero_def) |
|
171 |
qed simp |
|
172 |
||
173 |
lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)" |
|
174 |
proof (unfold up_one_def) |
|
175 |
qed simp |
|
176 |
||
177 |
(* term order |
|
178 |
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" |
|
179 |
proof - |
|
180 |
have "!!f. f : UP ==> (%n. a * f n) : UP" |
|
29667 | 181 |
by (unfold UP_def) (force simp add: algebra_simps) |
13936 | 182 |
*) (* this force step is slow *) |
183 |
(* then show ?thesis |
|
184 |
apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) |
|
185 |
qed |
|
186 |
*) |
|
187 |
lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" |
|
188 |
proof - |
|
189 |
have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP" |
|
29667 | 190 |
by (unfold UP_def) (force simp add: algebra_simps) |
13936 | 191 |
(* this force step is slow *) |
192 |
then show ?thesis |
|
193 |
by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) |
|
194 |
qed |
|
195 |
||
196 |
lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)" |
|
197 |
proof - |
|
198 |
{ |
|
199 |
fix f g |
|
200 |
assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" |
|
201 |
have "(%i. f i + g i) : UP" |
|
202 |
proof - |
|
203 |
from fup obtain n where boundn: "bound n f" |
|
204 |
by (unfold UP_def) fast |
|
205 |
from gup obtain m where boundm: "bound m g" |
|
206 |
by (unfold UP_def) fast |
|
207 |
have "bound (max n m) (%i. (f i + g i))" |
|
208 |
proof |
|
209 |
fix i |
|
210 |
assume "max n m < i" |
|
211 |
with boundn and boundm show "f i + g i = 0" |
|
29667 | 212 |
by (fastsimp simp add: algebra_simps) |
13936 | 213 |
qed |
214 |
then show "(%i. (f i + g i)) : UP" |
|
215 |
by (unfold UP_def) fast |
|
216 |
qed |
|
217 |
} |
|
218 |
then show ?thesis |
|
219 |
by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP) |
|
220 |
qed |
|
221 |
||
222 |
lemma coeff_mult [simp]: |
|
223 |
"coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)" |
|
224 |
proof - |
|
225 |
{ |
|
226 |
fix f g |
|
227 |
assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" |
|
228 |
have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" |
|
229 |
proof - |
|
230 |
from fup obtain n where "bound n f" |
|
231 |
by (unfold UP_def) fast |
|
232 |
from gup obtain m where "bound m g" |
|
233 |
by (unfold UP_def) fast |
|
234 |
have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})" |
|
235 |
proof |
|
236 |
fix k |
|
237 |
assume bound: "n + m < k" |
|
238 |
{ |
|
239 |
fix i |
|
240 |
have "f i * g (k-i) = 0" |
|
241 |
proof cases |
|
242 |
assume "n < i" |
|
29667 | 243 |
with `bound n f` show ?thesis by (auto simp add: algebra_simps) |
13936 | 244 |
next |
245 |
assume "~ (n < i)" |
|
246 |
with bound have "m < k-i" by arith |
|
29667 | 247 |
with `bound m g` show ?thesis by (auto simp add: algebra_simps) |
13936 | 248 |
qed |
249 |
} |
|
250 |
then show "setsum (%i. f i * g (k-i)) {..k} = 0" |
|
29667 | 251 |
by (simp add: algebra_simps) |
13936 | 252 |
qed |
253 |
then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" |
|
254 |
by (unfold UP_def) fast |
|
255 |
qed |
|
256 |
} |
|
257 |
then show ?thesis |
|
258 |
by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP) |
|
259 |
qed |
|
260 |
||
261 |
lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)" |
|
29667 | 262 |
by (unfold up_uminus_def) (simp add: algebra_simps) |
13936 | 263 |
|
264 |
(* Other lemmas *) |
|
265 |
||
266 |
lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q" |
|
267 |
proof - |
|
268 |
have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse) |
|
269 |
also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def) |
|
270 |
also have "... = q" by (simp add: Rep_UP_inverse) |
|
271 |
finally show ?thesis . |
|
272 |
qed |
|
273 |
||
26480 | 274 |
(* ML {* Addsimprocs [ring_simproc] *} *) |
13936 | 275 |
|
276 |
instance up :: (ring) ring |
|
277 |
proof |
|
278 |
fix p q r :: "'a::ring up" |
|
279 |
show "(p + q) + r = p + (q + r)" |
|
280 |
by (rule up_eqI) simp |
|
281 |
show "0 + p = p" |
|
282 |
by (rule up_eqI) simp |
|
283 |
show "(-p) + p = 0" |
|
284 |
by (rule up_eqI) simp |
|
285 |
show "p + q = q + p" |
|
286 |
by (rule up_eqI) simp |
|
287 |
show "(p * q) * r = p * (q * r)" |
|
288 |
proof (rule up_eqI) |
|
289 |
fix n |
|
290 |
{ |
|
291 |
fix k and a b c :: "nat=>'a::ring" |
|
292 |
have "k <= n ==> |
|
293 |
setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = |
|
294 |
setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}" |
|
295 |
(is "_ ==> ?eq k") |
|
296 |
proof (induct k) |
|
297 |
case 0 show ?case by simp |
|
298 |
next |
|
299 |
case (Suc k) |
|
300 |
then have "k <= n" by arith |
|
301 |
then have "?eq k" by (rule Suc) |
|
302 |
then show ?case |
|
303 |
by (simp add: Suc_diff_le natsum_ldistr) |
|
304 |
qed |
|
305 |
} |
|
306 |
then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n" |
|
307 |
by simp |
|
308 |
qed |
|
309 |
show "1 * p = p" |
|
310 |
proof (rule up_eqI) |
|
311 |
fix n |
|
312 |
show "coeff (1 * p) n = coeff p n" |
|
313 |
proof (cases n) |
|
314 |
case 0 then show ?thesis by simp |
|
315 |
next |
|
16052 | 316 |
case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2) |
13936 | 317 |
qed |
318 |
qed |
|
319 |
show "(p + q) * r = p * r + q * r" |
|
320 |
by (rule up_eqI) simp |
|
30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30012
diff
changeset
|
321 |
show "\<And>q. p * q = q * p" |
13936 | 322 |
proof (rule up_eqI) |
30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30012
diff
changeset
|
323 |
fix q |
13936 | 324 |
fix n |
325 |
{ |
|
326 |
fix k |
|
327 |
fix a b :: "nat=>'a::ring" |
|
328 |
have "k <= n ==> |
|
329 |
setsum (%i. a i * b (n-i)) {..k} = |
|
330 |
setsum (%i. a (k-i) * b (i+n-k)) {..k}" |
|
331 |
(is "_ ==> ?eq k") |
|
332 |
proof (induct k) |
|
333 |
case 0 show ?case by simp |
|
334 |
next |
|
335 |
case (Suc k) then show ?case by (subst natsum_Suc2) simp |
|
336 |
qed |
|
337 |
} |
|
338 |
then show "coeff (p * q) n = coeff (q * p) n" |
|
339 |
by simp |
|
340 |
qed |
|
341 |
||
342 |
show "p - q = p + (-q)" |
|
343 |
by (simp add: up_minus_def) |
|
344 |
show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)" |
|
345 |
by (simp add: up_inverse_def) |
|
346 |
show "p / q = p * inverse q" |
|
347 |
by (simp add: up_divide_def) |
|
27540 | 348 |
qed |
13936 | 349 |
|
31001 | 350 |
instance up :: (ring) recpower proof |
351 |
qed simp_all |
|
30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
30012
diff
changeset
|
352 |
|
13936 | 353 |
(* Further properties of monom *) |
354 |
||
355 |
lemma monom_zero [simp]: |
|
356 |
"monom 0 n = 0" |
|
357 |
by (simp add: monom_def up_zero_def) |
|
358 |
(* term order: application of coeff_mult goes wrong: rule not symmetric |
|
359 |
lemma monom_mult_is_smult: |
|
360 |
"monom (a::'a::ring) 0 * p = a *s p" |
|
361 |
proof (rule up_eqI) |
|
362 |
fix k |
|
363 |
show "coeff (monom a 0 * p) k = coeff (a *s p) k" |
|
364 |
proof (cases k) |
|
365 |
case 0 then show ?thesis by simp |
|
366 |
next |
|
367 |
case Suc then show ?thesis by simp |
|
368 |
qed |
|
369 |
qed |
|
370 |
*) |
|
26480 | 371 |
ML {* Delsimprocs [ring_simproc] *} |
13936 | 372 |
|
373 |
lemma monom_mult_is_smult: |
|
374 |
"monom (a::'a::ring) 0 * p = a *s p" |
|
375 |
proof (rule up_eqI) |
|
376 |
fix k |
|
377 |
have "coeff (p * monom a 0) k = coeff (a *s p) k" |
|
378 |
proof (cases k) |
|
379 |
case 0 then show ?thesis by simp ring |
|
380 |
next |
|
30012 | 381 |
case Suc then show ?thesis by simp (ring, simp) |
13936 | 382 |
qed |
383 |
then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring |
|
384 |
qed |
|
385 |
||
26480 | 386 |
ML {* Addsimprocs [ring_simproc] *} |
13936 | 387 |
|
388 |
lemma monom_add [simp]: |
|
389 |
"monom (a + b) n = monom (a::'a::ring) n + monom b n" |
|
390 |
by (rule up_eqI) simp |
|
391 |
||
392 |
lemma monom_mult_smult: |
|
393 |
"monom (a * b) n = a *s monom (b::'a::ring) n" |
|
394 |
by (rule up_eqI) simp |
|
395 |
||
396 |
lemma monom_uminus [simp]: |
|
397 |
"monom (-a) n = - monom (a::'a::ring) n" |
|
398 |
by (rule up_eqI) simp |
|
399 |
||
400 |
lemma monom_one [simp]: |
|
401 |
"monom 1 0 = 1" |
|
402 |
by (simp add: up_one_def) |
|
403 |
||
404 |
lemma monom_inj: |
|
405 |
"(monom a n = monom b n) = (a = b)" |
|
406 |
proof |
|
407 |
assume "monom a n = monom b n" |
|
408 |
then have "coeff (monom a n) n = coeff (monom b n) n" by simp |
|
409 |
then show "a = b" by simp |
|
410 |
next |
|
411 |
assume "a = b" then show "monom a n = monom b n" by simp |
|
412 |
qed |
|
413 |
||
414 |
(* Properties of *s: |
|
415 |
Polynomials form a module *) |
|
416 |
||
417 |
lemma smult_l_distr: |
|
418 |
"(a + b::'a::ring) *s p = a *s p + b *s p" |
|
419 |
by (rule up_eqI) simp |
|
420 |
||
421 |
lemma smult_r_distr: |
|
422 |
"(a::'a::ring) *s (p + q) = a *s p + a *s q" |
|
423 |
by (rule up_eqI) simp |
|
424 |
||
425 |
lemma smult_assoc1: |
|
426 |
"(a * b::'a::ring) *s p = a *s (b *s p)" |
|
427 |
by (rule up_eqI) simp |
|
428 |
||
429 |
lemma smult_one [simp]: |
|
430 |
"(1::'a::ring) *s p = p" |
|
431 |
by (rule up_eqI) simp |
|
432 |
||
433 |
(* Polynomials form an algebra *) |
|
434 |
||
26480 | 435 |
ML {* Delsimprocs [ring_simproc] *} |
13936 | 436 |
|
437 |
lemma smult_assoc2: |
|
438 |
"(a *s p) * q = (a::'a::ring) *s (p * q)" |
|
439 |
by (rule up_eqI) (simp add: natsum_rdistr m_assoc) |
|
440 |
(* Simproc fails. *) |
|
441 |
||
26480 | 442 |
ML {* Addsimprocs [ring_simproc] *} |
13936 | 443 |
|
444 |
(* the following can be derived from the above ones, |
|
445 |
for generality reasons, it is therefore done *) |
|
446 |
||
447 |
lemma smult_l_null [simp]: |
|
448 |
"(0::'a::ring) *s p = 0" |
|
449 |
proof - |
|
450 |
fix a |
|
451 |
have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp |
|
452 |
also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr) |
|
453 |
also have "... = 0" by simp |
|
454 |
finally show ?thesis . |
|
455 |
qed |
|
456 |
||
457 |
lemma smult_r_null [simp]: |
|
458 |
"(a::'a::ring) *s 0 = 0"; |
|
459 |
proof - |
|
460 |
fix p |
|
461 |
have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp |
|
462 |
also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr) |
|
463 |
also have "... = 0" by simp |
|
464 |
finally show ?thesis . |
|
465 |
qed |
|
466 |
||
467 |
lemma smult_l_minus: |
|
468 |
"(-a::'a::ring) *s p = - (a *s p)" |
|
469 |
proof - |
|
470 |
have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp |
|
471 |
also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr) |
|
472 |
also have "... = -(a *s p)" by simp |
|
473 |
finally show ?thesis . |
|
474 |
qed |
|
475 |
||
476 |
lemma smult_r_minus: |
|
477 |
"(a::'a::ring) *s (-p) = - (a *s p)" |
|
478 |
proof - |
|
479 |
have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp |
|
480 |
also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr) |
|
481 |
also have "... = -(a *s p)" by simp |
|
482 |
finally show ?thesis . |
|
483 |
qed |
|
484 |
||
485 |
section {* The degree function *} |
|
486 |
||
21423 | 487 |
definition |
488 |
deg :: "('a::zero) up => nat" where |
|
489 |
"deg p = (LEAST n. bound n (coeff p))" |
|
13936 | 490 |
|
491 |
lemma deg_aboveI: |
|
492 |
"(!!m. n < m ==> coeff p m = 0) ==> deg p <= n" |
|
493 |
by (unfold deg_def) (fast intro: Least_le) |
|
494 |
||
495 |
lemma deg_aboveD: |
|
23350 | 496 |
assumes "deg p < m" shows "coeff p m = 0" |
13936 | 497 |
proof - |
498 |
obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain) |
|
499 |
then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI) |
|
23350 | 500 |
then show "coeff p m = 0" using `deg p < m` by (rule boundD) |
13936 | 501 |
qed |
502 |
||
503 |
lemma deg_belowI: |
|
504 |
assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p" |
|
505 |
(* logically, this is a slightly stronger version of deg_aboveD *) |
|
506 |
proof (cases "n=0") |
|
507 |
case True then show ?thesis by simp |
|
508 |
next |
|
509 |
case False then have "coeff p n ~= 0" by (rule prem) |
|
510 |
then have "~ deg p < n" by (fast dest: deg_aboveD) |
|
511 |
then show ?thesis by arith |
|
512 |
qed |
|
513 |
||
514 |
lemma lcoeff_nonzero_deg: |
|
515 |
assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0" |
|
516 |
proof - |
|
517 |
obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0" |
|
518 |
proof - |
|
519 |
have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" |
|
520 |
by arith (* make public?, why does proof not work with "1" *) |
|
521 |
from deg have "deg p - 1 < (LEAST n. bound n (coeff p))" |
|
522 |
by (unfold deg_def) arith |
|
523 |
then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least) |
|
524 |
then have "EX m. deg p - 1 < m & coeff p m ~= 0" |
|
525 |
by (unfold bound_def) fast |
|
526 |
then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus) |
|
23350 | 527 |
then show ?thesis by (auto intro: that) |
13936 | 528 |
qed |
529 |
with deg_belowI have "deg p = m" by fastsimp |
|
530 |
with m_coeff show ?thesis by simp |
|
531 |
qed |
|
532 |
||
533 |
lemma lcoeff_nonzero_nonzero: |
|
534 |
assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0" |
|
535 |
proof - |
|
536 |
have "EX m. coeff p m ~= 0" |
|
537 |
proof (rule classical) |
|
538 |
assume "~ ?thesis" |
|
539 |
then have "p = 0" by (auto intro: up_eqI) |
|
540 |
with nonzero show ?thesis by contradiction |
|
541 |
qed |
|
542 |
then obtain m where coeff: "coeff p m ~= 0" .. |
|
543 |
then have "m <= deg p" by (rule deg_belowI) |
|
544 |
then have "m = 0" by (simp add: deg) |
|
545 |
with coeff show ?thesis by simp |
|
546 |
qed |
|
547 |
||
548 |
lemma lcoeff_nonzero: |
|
549 |
"p ~= 0 ==> coeff p (deg p) ~= 0" |
|
550 |
proof (cases "deg p = 0") |
|
551 |
case True |
|
552 |
assume "p ~= 0" |
|
553 |
with True show ?thesis by (simp add: lcoeff_nonzero_nonzero) |
|
554 |
next |
|
555 |
case False |
|
556 |
assume "p ~= 0" |
|
557 |
with False show ?thesis by (simp add: lcoeff_nonzero_deg) |
|
558 |
qed |
|
559 |
||
560 |
lemma deg_eqI: |
|
561 |
"[| !!m. n < m ==> coeff p m = 0; |
|
562 |
!!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n" |
|
563 |
by (fast intro: le_anti_sym deg_aboveI deg_belowI) |
|
564 |
||
565 |
(* Degree and polynomial operations *) |
|
566 |
||
567 |
lemma deg_add [simp]: |
|
568 |
"deg ((p::'a::ring up) + q) <= max (deg p) (deg q)" |
|
569 |
proof (cases "deg p <= deg q") |
|
570 |
case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) |
|
571 |
next |
|
572 |
case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD) |
|
573 |
qed |
|
574 |
||
575 |
lemma deg_monom_ring: |
|
576 |
"deg (monom a n::'a::ring up) <= n" |
|
577 |
by (rule deg_aboveI) simp |
|
578 |
||
579 |
lemma deg_monom [simp]: |
|
580 |
"a ~= 0 ==> deg (monom a n::'a::ring up) = n" |
|
581 |
by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) |
|
582 |
||
583 |
lemma deg_const [simp]: |
|
584 |
"deg (monom (a::'a::ring) 0) = 0" |
|
585 |
proof (rule le_anti_sym) |
|
586 |
show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp |
|
587 |
next |
|
588 |
show "0 <= deg (monom a 0)" by (rule deg_belowI) simp |
|
589 |
qed |
|
590 |
||
591 |
lemma deg_zero [simp]: |
|
592 |
"deg 0 = 0" |
|
593 |
proof (rule le_anti_sym) |
|
594 |
show "deg 0 <= 0" by (rule deg_aboveI) simp |
|
595 |
next |
|
596 |
show "0 <= deg 0" by (rule deg_belowI) simp |
|
597 |
qed |
|
598 |
||
599 |
lemma deg_one [simp]: |
|
600 |
"deg 1 = 0" |
|
601 |
proof (rule le_anti_sym) |
|
602 |
show "deg 1 <= 0" by (rule deg_aboveI) simp |
|
603 |
next |
|
604 |
show "0 <= deg 1" by (rule deg_belowI) simp |
|
605 |
qed |
|
606 |
||
607 |
lemma uminus_monom: |
|
608 |
"!!a::'a::ring. (-a = 0) = (a = 0)" |
|
609 |
proof |
|
610 |
fix a::"'a::ring" |
|
611 |
assume "a = 0" |
|
612 |
then show "-a = 0" by simp |
|
613 |
next |
|
614 |
fix a::"'a::ring" |
|
615 |
assume "- a = 0" |
|
616 |
then have "-(- a) = 0" by simp |
|
617 |
then show "a = 0" by simp |
|
618 |
qed |
|
619 |
||
620 |
lemma deg_uminus [simp]: |
|
621 |
"deg (-p::('a::ring) up) = deg p" |
|
622 |
proof (rule le_anti_sym) |
|
623 |
show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD) |
|
624 |
next |
|
625 |
show "deg p <= deg (- p)" |
|
626 |
by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom) |
|
627 |
qed |
|
628 |
||
629 |
lemma deg_smult_ring: |
|
630 |
"deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)" |
|
631 |
proof (cases "a = 0") |
|
632 |
qed (simp add: deg_aboveI deg_aboveD)+ |
|
633 |
||
634 |
lemma deg_smult [simp]: |
|
635 |
"deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)" |
|
636 |
proof (rule le_anti_sym) |
|
637 |
show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring) |
|
638 |
next |
|
639 |
show "(if a = 0 then 0 else deg p) <= deg (a *s p)" |
|
640 |
proof (cases "a = 0") |
|
641 |
qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff) |
|
642 |
qed |
|
643 |
||
644 |
lemma deg_mult_ring: |
|
645 |
"deg (p * q::'a::ring up) <= deg p + deg q" |
|
646 |
proof (rule deg_aboveI) |
|
647 |
fix m |
|
648 |
assume boundm: "deg p + deg q < m" |
|
649 |
{ |
|
650 |
fix k i |
|
651 |
assume boundk: "deg p + deg q < k" |
|
652 |
then have "coeff p i * coeff q (k - i) = 0" |
|
653 |
proof (cases "deg p < i") |
|
654 |
case True then show ?thesis by (simp add: deg_aboveD) |
|
655 |
next |
|
656 |
case False with boundk have "deg q < k - i" by arith |
|
657 |
then show ?thesis by (simp add: deg_aboveD) |
|
658 |
qed |
|
659 |
} |
|
660 |
(* This is similar to bound_mult_zero and deg_above_mult_zero in the old |
|
661 |
proofs. *) |
|
662 |
with boundm show "coeff (p * q) m = 0" by simp |
|
663 |
qed |
|
664 |
||
665 |
lemma deg_mult [simp]: |
|
666 |
"[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q" |
|
667 |
proof (rule le_anti_sym) |
|
668 |
show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring) |
|
669 |
next |
|
670 |
let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))" |
|
671 |
assume nz: "p ~= 0" "q ~= 0" |
|
672 |
have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith |
|
673 |
show "deg p + deg q <= deg (p * q)" |
|
674 |
proof (rule deg_belowI, simp) |
|
675 |
have "setsum ?s {.. deg p + deg q} |
|
15045 | 676 |
= setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})" |
13936 | 677 |
by (simp only: ivl_disj_un_one) |
678 |
also have "... = setsum ?s {deg p .. deg p + deg q}" |
|
679 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one |
|
680 |
setsum_0 deg_aboveD less_add_diff) |
|
15045 | 681 |
also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})" |
13936 | 682 |
by (simp only: ivl_disj_un_singleton) |
683 |
also have "... = coeff p (deg p) * coeff q (deg q)" |
|
684 |
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton |
|
685 |
setsum_0 deg_aboveD) |
|
686 |
finally have "setsum ?s {.. deg p + deg q} |
|
687 |
= coeff p (deg p) * coeff q (deg q)" . |
|
688 |
with nz show "setsum ?s {.. deg p + deg q} ~= 0" |
|
689 |
by (simp add: integral_iff lcoeff_nonzero) |
|
690 |
qed |
|
691 |
qed |
|
692 |
||
693 |
lemma coeff_natsum: |
|
694 |
"((coeff (setsum p A) k)::'a::ring) = |
|
695 |
setsum (%i. coeff (p i) k) A" |
|
696 |
proof (cases "finite A") |
|
697 |
case True then show ?thesis by induct auto |
|
698 |
next |
|
699 |
case False then show ?thesis by (simp add: setsum_def) |
|
700 |
qed |
|
701 |
(* Instance of a more general result!!! *) |
|
702 |
||
703 |
(* |
|
704 |
lemma coeff_natsum: |
|
705 |
"((coeff (setsum p {..n::nat}) k)::'a::ring) = |
|
706 |
setsum (%i. coeff (p i) k) {..n}" |
|
707 |
by (induct n) auto |
|
708 |
*) |
|
709 |
||
710 |
lemma up_repr: |
|
711 |
"setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p" |
|
712 |
proof (rule up_eqI) |
|
713 |
let ?s = "(%i. monom (coeff p i) i)" |
|
714 |
fix k |
|
715 |
show "coeff (setsum ?s {..deg p}) k = coeff p k" |
|
716 |
proof (cases "k <= deg p") |
|
717 |
case True |
|
718 |
hence "coeff (setsum ?s {..deg p}) k = |
|
15045 | 719 |
coeff (setsum ?s ({..k} Un {k<..deg p})) k" |
13936 | 720 |
by (simp only: ivl_disj_un_one) |
721 |
also from True |
|
722 |
have "... = coeff (setsum ?s {..k}) k" |
|
723 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2 |
|
724 |
setsum_0 coeff_natsum ) |
|
725 |
also |
|
15045 | 726 |
have "... = coeff (setsum ?s ({..<k} Un {k})) k" |
13936 | 727 |
by (simp only: ivl_disj_un_singleton) |
728 |
also have "... = coeff p k" |
|
729 |
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton |
|
730 |
setsum_0 coeff_natsum deg_aboveD) |
|
731 |
finally show ?thesis . |
|
732 |
next |
|
733 |
case False |
|
734 |
hence "coeff (setsum ?s {..deg p}) k = |
|
15045 | 735 |
coeff (setsum ?s ({..<deg p} Un {deg p})) k" |
13936 | 736 |
by (simp only: ivl_disj_un_singleton) |
737 |
also from False have "... = coeff p k" |
|
738 |
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton |
|
739 |
setsum_0 coeff_natsum deg_aboveD) |
|
740 |
finally show ?thesis . |
|
741 |
qed |
|
742 |
qed |
|
743 |
||
744 |
lemma up_repr_le: |
|
745 |
"deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p" |
|
746 |
proof - |
|
747 |
let ?s = "(%i. monom (coeff p i) i)" |
|
748 |
assume "deg p <= n" |
|
15045 | 749 |
then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})" |
13936 | 750 |
by (simp only: ivl_disj_un_one) |
751 |
also have "... = setsum ?s {..deg p}" |
|
752 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one |
|
753 |
setsum_0 deg_aboveD) |
|
754 |
also have "... = p" by (rule up_repr) |
|
755 |
finally show ?thesis . |
|
756 |
qed |
|
757 |
||
758 |
instance up :: ("domain") "domain" |
|
759 |
proof |
|
760 |
show "1 ~= (0::'a up)" |
|
761 |
proof (* notI is applied here *) |
|
762 |
assume "1 = (0::'a up)" |
|
763 |
hence "coeff 1 0 = (coeff 0 0::'a)" by simp |
|
764 |
hence "1 = (0::'a)" by simp |
|
765 |
with one_not_zero show "False" by contradiction |
|
766 |
qed |
|
767 |
next |
|
768 |
fix p q :: "'a::domain up" |
|
769 |
assume pq: "p * q = 0" |
|
770 |
show "p = 0 | q = 0" |
|
771 |
proof (rule classical) |
|
772 |
assume c: "~ (p = 0 | q = 0)" |
|
773 |
then have "deg p + deg q = deg (p * q)" by simp |
|
774 |
also from pq have "... = 0" by simp |
|
775 |
finally have "deg p + deg q = 0" . |
|
776 |
then have f1: "deg p = 0 & deg q = 0" by simp |
|
777 |
from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}" |
|
778 |
by (simp only: up_repr_le) |
|
779 |
also have "... = monom (coeff p 0) 0" by simp |
|
780 |
finally have p: "p = monom (coeff p 0) 0" . |
|
781 |
from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}" |
|
782 |
by (simp only: up_repr_le) |
|
783 |
also have "... = monom (coeff q 0) 0" by simp |
|
784 |
finally have q: "q = monom (coeff q 0) 0" . |
|
785 |
have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp |
|
786 |
also from pq have "... = 0" by simp |
|
787 |
finally have "coeff p 0 * coeff q 0 = 0" . |
|
788 |
then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff) |
|
789 |
with p q show "p = 0 | q = 0" by fastsimp |
|
790 |
qed |
|
791 |
qed |
|
792 |
||
793 |
lemma monom_inj_zero: |
|
794 |
"(monom a n = 0) = (a = 0)" |
|
795 |
proof - |
|
796 |
have "(monom a n = 0) = (monom a n = monom 0 n)" by simp |
|
797 |
also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero) |
|
798 |
finally show ?thesis . |
|
799 |
qed |
|
800 |
(* term order: makes this simpler!!! |
|
801 |
lemma smult_integral: |
|
802 |
"(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" |
|
803 |
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast |
|
804 |
*) |
|
805 |
lemma smult_integral: |
|
806 |
"(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" |
|
807 |
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) |
|
808 |
||
21423 | 809 |
|
810 |
(* Divisibility and degree *) |
|
811 |
||
812 |
lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q" |
|
813 |
apply (unfold dvd_def) |
|
814 |
apply (erule exE) |
|
815 |
apply hypsubst |
|
816 |
apply (case_tac "p = 0") |
|
817 |
apply (case_tac [2] "k = 0") |
|
818 |
apply auto |
|
819 |
done |
|
820 |
||
14590 | 821 |
end |