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