author | wenzelm |
Sun, 30 Jan 2011 13:02:18 +0100 | |
changeset 41648 | 6d736d983d5c |
parent 35849 | b5522b51cb1e |
child 41959 | b460124855b8 |
permissions | -rw-r--r-- |
35849 | 1 |
(* Title: Univariate Polynomials |
2 |
Author: Clemens Ballarin, started 9 December 1996 |
|
3 |
Copyright: Clemens Ballarin |
|
13936 | 4 |
*) |
5 |
||
6 |
header {* Univariate Polynomials *} |
|
7 |
||
15481 | 8 |
theory UnivPoly2 |
9 |
imports "../abstract/Abstract" |
|
10 |
begin |
|
13936 | 11 |
|
16640
03bdf544a552
Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents:
16052
diff
changeset
|
12 |
(* With this variant of setsum_cong, assumptions |
13936 | 13 |
like i:{m..n} get simplified (to m <= i & i <= n). *) |
14 |
||
16640
03bdf544a552
Removed setsubgoaler hack (thanks to strong_setsum_cong).
berghofe
parents:
16052
diff
changeset
|
15 |
declare strong_setsum_cong [cong] |
13936 | 16 |
|
35849 | 17 |
|
13936 | 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 |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
50 |
coeff :: "['a up, nat] => ('a::zero)" |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
51 |
where "coeff p n = Rep_UP p n" |
13936 | 52 |
|
21423 | 53 |
definition |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
54 |
monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
55 |
where "monom a n = Abs_UP (%i. if i=n then a else 0)" |
21423 | 56 |
|
57 |
definition |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
58 |
smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
59 |
where "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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
103 |
up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)" |
25762 | 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 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
135 |
up_mult_def: "p * q = Abs_UP (%n::nat. setsum |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
136 |
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})" |
25762 | 137 |
|
138 |
instance .. |
|
139 |
||
140 |
end |
|
141 |
||
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
33657
diff
changeset
|
142 |
instance up :: ("{times, comm_monoid_add}") Rings.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 |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
152 |
up_divide_def: "(a :: 'a up) / b = a * inverse b" |
25762 | 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" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
204 |
by (unfold UP_def) fast |
13936 | 205 |
from gup obtain m where boundm: "bound m g" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
206 |
by (unfold UP_def) fast |
13936 | 207 |
have "bound (max n m) (%i. (f i + g i))" |
208 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
209 |
fix i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
210 |
assume "max n m < i" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
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" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
215 |
by (unfold UP_def) fast |
13936 | 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" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
231 |
by (unfold UP_def) fast |
13936 | 232 |
from gup obtain m where "bound m g" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
233 |
by (unfold UP_def) fast |
13936 | 234 |
have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})" |
235 |
proof |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
236 |
fix k |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
237 |
assume bound: "n + m < k" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
238 |
{ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
239 |
fix i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
240 |
have "f i * g (k-i) = 0" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
241 |
proof cases |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
242 |
assume "n < i" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
243 |
with `bound n f` show ?thesis by (auto simp add: algebra_simps) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
244 |
next |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
245 |
assume "~ (n < i)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
246 |
with bound have "m < k-i" by arith |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
247 |
with `bound m g` show ?thesis by (auto simp add: algebra_simps) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
248 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
249 |
} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
250 |
then show "setsum (%i. f i * g (k-i)) {..k} = 0" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
251 |
by (simp add: algebra_simps) |
13936 | 252 |
qed |
253 |
then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
254 |
by (unfold UP_def) fast |
13936 | 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 ==> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
293 |
setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
294 |
setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
295 |
(is "_ ==> ?eq k") |
13936 | 296 |
proof (induct k) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
297 |
case 0 show ?case by simp |
13936 | 298 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
299 |
case (Suc k) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
300 |
then have "k <= n" by arith |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
301 |
then have "?eq k" by (rule Suc) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
302 |
then show ?case |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
303 |
by (simp add: Suc_diff_le natsum_ldistr) |
13936 | 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 ==> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
329 |
setsum (%i. a i * b (n-i)) {..k} = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
330 |
setsum (%i. a (k-i) * b (i+n-k)) {..k}" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
331 |
(is "_ ==> ?eq k") |
13936 | 332 |
proof (induct k) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
333 |
case 0 show ?case by simp |
13936 | 334 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32456
diff
changeset
|
335 |
case (Suc k) then show ?case by (subst natsum_Suc2) simp |
13936 | 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 |
|
350 |
(* Further properties of monom *) |
|
351 |
||
352 |
lemma monom_zero [simp]: |
|
353 |
"monom 0 n = 0" |
|
354 |
by (simp add: monom_def up_zero_def) |
|
355 |
(* term order: application of coeff_mult goes wrong: rule not symmetric |
|
356 |
lemma monom_mult_is_smult: |
|
357 |
"monom (a::'a::ring) 0 * p = a *s p" |
|
358 |
proof (rule up_eqI) |
|
359 |
fix k |
|
360 |
show "coeff (monom a 0 * p) k = coeff (a *s p) k" |
|
361 |
proof (cases k) |
|
362 |
case 0 then show ?thesis by simp |
|
363 |
next |
|
364 |
case Suc then show ?thesis by simp |
|
365 |
qed |
|
366 |
qed |
|
367 |
*) |
|
26480 | 368 |
ML {* Delsimprocs [ring_simproc] *} |
13936 | 369 |
|
370 |
lemma monom_mult_is_smult: |
|
371 |
"monom (a::'a::ring) 0 * p = a *s p" |
|
372 |
proof (rule up_eqI) |
|
373 |
fix k |
|
374 |
have "coeff (p * monom a 0) k = coeff (a *s p) k" |
|
375 |
proof (cases k) |
|
376 |
case 0 then show ?thesis by simp ring |
|
377 |
next |
|
30012 | 378 |
case Suc then show ?thesis by simp (ring, simp) |
13936 | 379 |
qed |
380 |
then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring |
|
381 |
qed |
|
382 |
||
26480 | 383 |
ML {* Addsimprocs [ring_simproc] *} |
13936 | 384 |
|
385 |
lemma monom_add [simp]: |
|
386 |
"monom (a + b) n = monom (a::'a::ring) n + monom b n" |
|
387 |
by (rule up_eqI) simp |
|
388 |
||
389 |
lemma monom_mult_smult: |
|
390 |
"monom (a * b) n = a *s monom (b::'a::ring) n" |
|
391 |
by (rule up_eqI) simp |
|
392 |
||
393 |
lemma monom_uminus [simp]: |
|
394 |
"monom (-a) n = - monom (a::'a::ring) n" |
|
395 |
by (rule up_eqI) simp |
|
396 |
||
397 |
lemma monom_one [simp]: |
|
398 |
"monom 1 0 = 1" |
|
399 |
by (simp add: up_one_def) |
|
400 |
||
401 |
lemma monom_inj: |
|
402 |
"(monom a n = monom b n) = (a = b)" |
|
403 |
proof |
|
404 |
assume "monom a n = monom b n" |
|
405 |
then have "coeff (monom a n) n = coeff (monom b n) n" by simp |
|
406 |
then show "a = b" by simp |
|
407 |
next |
|
408 |
assume "a = b" then show "monom a n = monom b n" by simp |
|
409 |
qed |
|
410 |
||
411 |
(* Properties of *s: |
|
412 |
Polynomials form a module *) |
|
413 |
||
414 |
lemma smult_l_distr: |
|
415 |
"(a + b::'a::ring) *s p = a *s p + b *s p" |
|
416 |
by (rule up_eqI) simp |
|
417 |
||
418 |
lemma smult_r_distr: |
|
419 |
"(a::'a::ring) *s (p + q) = a *s p + a *s q" |
|
420 |
by (rule up_eqI) simp |
|
421 |
||
422 |
lemma smult_assoc1: |
|
423 |
"(a * b::'a::ring) *s p = a *s (b *s p)" |
|
424 |
by (rule up_eqI) simp |
|
425 |
||
426 |
lemma smult_one [simp]: |
|
427 |
"(1::'a::ring) *s p = p" |
|
428 |
by (rule up_eqI) simp |
|
429 |
||
430 |
(* Polynomials form an algebra *) |
|
431 |
||
26480 | 432 |
ML {* Delsimprocs [ring_simproc] *} |
13936 | 433 |
|
434 |
lemma smult_assoc2: |
|
435 |
"(a *s p) * q = (a::'a::ring) *s (p * q)" |
|
436 |
by (rule up_eqI) (simp add: natsum_rdistr m_assoc) |
|
437 |
(* Simproc fails. *) |
|
438 |
||
26480 | 439 |
ML {* Addsimprocs [ring_simproc] *} |
13936 | 440 |
|
441 |
(* the following can be derived from the above ones, |
|
442 |
for generality reasons, it is therefore done *) |
|
443 |
||
444 |
lemma smult_l_null [simp]: |
|
445 |
"(0::'a::ring) *s p = 0" |
|
446 |
proof - |
|
447 |
fix a |
|
448 |
have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp |
|
449 |
also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr) |
|
450 |
also have "... = 0" by simp |
|
451 |
finally show ?thesis . |
|
452 |
qed |
|
453 |
||
454 |
lemma smult_r_null [simp]: |
|
455 |
"(a::'a::ring) *s 0 = 0"; |
|
456 |
proof - |
|
457 |
fix p |
|
458 |
have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp |
|
459 |
also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr) |
|
460 |
also have "... = 0" by simp |
|
461 |
finally show ?thesis . |
|
462 |
qed |
|
463 |
||
464 |
lemma smult_l_minus: |
|
465 |
"(-a::'a::ring) *s p = - (a *s p)" |
|
466 |
proof - |
|
467 |
have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp |
|
468 |
also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr) |
|
469 |
also have "... = -(a *s p)" by simp |
|
470 |
finally show ?thesis . |
|
471 |
qed |
|
472 |
||
473 |
lemma smult_r_minus: |
|
474 |
"(a::'a::ring) *s (-p) = - (a *s p)" |
|
475 |
proof - |
|
476 |
have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp |
|
477 |
also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr) |
|
478 |
also have "... = -(a *s p)" by simp |
|
479 |
finally show ?thesis . |
|
480 |
qed |
|
481 |
||
35849 | 482 |
|
13936 | 483 |
section {* The degree function *} |
484 |
||
21423 | 485 |
definition |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
486 |
deg :: "('a::zero) up => nat" |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35050
diff
changeset
|
487 |
where "deg p = (LEAST n. bound n (coeff p))" |
13936 | 488 |
|
489 |
lemma deg_aboveI: |
|
490 |
"(!!m. n < m ==> coeff p m = 0) ==> deg p <= n" |
|
491 |
by (unfold deg_def) (fast intro: Least_le) |
|
492 |
||
493 |
lemma deg_aboveD: |
|
23350 | 494 |
assumes "deg p < m" shows "coeff p m = 0" |
13936 | 495 |
proof - |
496 |
obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain) |
|
497 |
then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI) |
|
23350 | 498 |
then show "coeff p m = 0" using `deg p < m` by (rule boundD) |
13936 | 499 |
qed |
500 |
||
501 |
lemma deg_belowI: |
|
502 |
assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p" |
|
503 |
(* logically, this is a slightly stronger version of deg_aboveD *) |
|
504 |
proof (cases "n=0") |
|
505 |
case True then show ?thesis by simp |
|
506 |
next |
|
507 |
case False then have "coeff p n ~= 0" by (rule prem) |
|
508 |
then have "~ deg p < n" by (fast dest: deg_aboveD) |
|
509 |
then show ?thesis by arith |
|
510 |
qed |
|
511 |
||
512 |
lemma lcoeff_nonzero_deg: |
|
513 |
assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0" |
|
514 |
proof - |
|
515 |
obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0" |
|
516 |
proof - |
|
517 |
have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" |
|
518 |
by arith (* make public?, why does proof not work with "1" *) |
|
519 |
from deg have "deg p - 1 < (LEAST n. bound n (coeff p))" |
|
520 |
by (unfold deg_def) arith |
|
521 |
then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least) |
|
522 |
then have "EX m. deg p - 1 < m & coeff p m ~= 0" |
|
523 |
by (unfold bound_def) fast |
|
524 |
then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus) |
|
23350 | 525 |
then show ?thesis by (auto intro: that) |
13936 | 526 |
qed |
527 |
with deg_belowI have "deg p = m" by fastsimp |
|
528 |
with m_coeff show ?thesis by simp |
|
529 |
qed |
|
530 |
||
531 |
lemma lcoeff_nonzero_nonzero: |
|
532 |
assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0" |
|
533 |
proof - |
|
534 |
have "EX m. coeff p m ~= 0" |
|
535 |
proof (rule classical) |
|
536 |
assume "~ ?thesis" |
|
537 |
then have "p = 0" by (auto intro: up_eqI) |
|
538 |
with nonzero show ?thesis by contradiction |
|
539 |
qed |
|
540 |
then obtain m where coeff: "coeff p m ~= 0" .. |
|
541 |
then have "m <= deg p" by (rule deg_belowI) |
|
542 |
then have "m = 0" by (simp add: deg) |
|
543 |
with coeff show ?thesis by simp |
|
544 |
qed |
|
545 |
||
546 |
lemma lcoeff_nonzero: |
|
547 |
"p ~= 0 ==> coeff p (deg p) ~= 0" |
|
548 |
proof (cases "deg p = 0") |
|
549 |
case True |
|
550 |
assume "p ~= 0" |
|
551 |
with True show ?thesis by (simp add: lcoeff_nonzero_nonzero) |
|
552 |
next |
|
553 |
case False |
|
554 |
assume "p ~= 0" |
|
555 |
with False show ?thesis by (simp add: lcoeff_nonzero_deg) |
|
556 |
qed |
|
557 |
||
558 |
lemma deg_eqI: |
|
559 |
"[| !!m. n < m ==> coeff p m = 0; |
|
560 |
!!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n" |
|
33657 | 561 |
by (fast intro: le_antisym deg_aboveI deg_belowI) |
13936 | 562 |
|
563 |
(* Degree and polynomial operations *) |
|
564 |
||
565 |
lemma deg_add [simp]: |
|
566 |
"deg ((p::'a::ring up) + q) <= max (deg p) (deg q)" |
|
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
31021
diff
changeset
|
567 |
by (rule deg_aboveI) (simp add: deg_aboveD) |
13936 | 568 |
|
569 |
lemma deg_monom_ring: |
|
570 |
"deg (monom a n::'a::ring up) <= n" |
|
571 |
by (rule deg_aboveI) simp |
|
572 |
||
573 |
lemma deg_monom [simp]: |
|
574 |
"a ~= 0 ==> deg (monom a n::'a::ring up) = n" |
|
33657 | 575 |
by (fastsimp intro: le_antisym deg_aboveI deg_belowI) |
13936 | 576 |
|
577 |
lemma deg_const [simp]: |
|
578 |
"deg (monom (a::'a::ring) 0) = 0" |
|
33657 | 579 |
proof (rule le_antisym) |
13936 | 580 |
show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp |
581 |
next |
|
582 |
show "0 <= deg (monom a 0)" by (rule deg_belowI) simp |
|
583 |
qed |
|
584 |
||
585 |
lemma deg_zero [simp]: |
|
586 |
"deg 0 = 0" |
|
33657 | 587 |
proof (rule le_antisym) |
13936 | 588 |
show "deg 0 <= 0" by (rule deg_aboveI) simp |
589 |
next |
|
590 |
show "0 <= deg 0" by (rule deg_belowI) simp |
|
591 |
qed |
|
592 |
||
593 |
lemma deg_one [simp]: |
|
594 |
"deg 1 = 0" |
|
33657 | 595 |
proof (rule le_antisym) |
13936 | 596 |
show "deg 1 <= 0" by (rule deg_aboveI) simp |
597 |
next |
|
598 |
show "0 <= deg 1" by (rule deg_belowI) simp |
|
599 |
qed |
|
600 |
||
601 |
lemma uminus_monom: |
|
602 |
"!!a::'a::ring. (-a = 0) = (a = 0)" |
|
603 |
proof |
|
604 |
fix a::"'a::ring" |
|
605 |
assume "a = 0" |
|
606 |
then show "-a = 0" by simp |
|
607 |
next |
|
608 |
fix a::"'a::ring" |
|
609 |
assume "- a = 0" |
|
610 |
then have "-(- a) = 0" by simp |
|
611 |
then show "a = 0" by simp |
|
612 |
qed |
|
613 |
||
614 |
lemma deg_uminus [simp]: |
|
615 |
"deg (-p::('a::ring) up) = deg p" |
|
33657 | 616 |
proof (rule le_antisym) |
13936 | 617 |
show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD) |
618 |
next |
|
619 |
show "deg p <= deg (- p)" |
|
620 |
by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom) |
|
621 |
qed |
|
622 |
||
623 |
lemma deg_smult_ring: |
|
624 |
"deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)" |
|
625 |
proof (cases "a = 0") |
|
626 |
qed (simp add: deg_aboveI deg_aboveD)+ |
|
627 |
||
628 |
lemma deg_smult [simp]: |
|
629 |
"deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)" |
|
33657 | 630 |
proof (rule le_antisym) |
13936 | 631 |
show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring) |
632 |
next |
|
633 |
show "(if a = 0 then 0 else deg p) <= deg (a *s p)" |
|
634 |
proof (cases "a = 0") |
|
635 |
qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff) |
|
636 |
qed |
|
637 |
||
638 |
lemma deg_mult_ring: |
|
639 |
"deg (p * q::'a::ring up) <= deg p + deg q" |
|
640 |
proof (rule deg_aboveI) |
|
641 |
fix m |
|
642 |
assume boundm: "deg p + deg q < m" |
|
643 |
{ |
|
644 |
fix k i |
|
645 |
assume boundk: "deg p + deg q < k" |
|
646 |
then have "coeff p i * coeff q (k - i) = 0" |
|
647 |
proof (cases "deg p < i") |
|
648 |
case True then show ?thesis by (simp add: deg_aboveD) |
|
649 |
next |
|
650 |
case False with boundk have "deg q < k - i" by arith |
|
651 |
then show ?thesis by (simp add: deg_aboveD) |
|
652 |
qed |
|
653 |
} |
|
654 |
(* This is similar to bound_mult_zero and deg_above_mult_zero in the old |
|
655 |
proofs. *) |
|
656 |
with boundm show "coeff (p * q) m = 0" by simp |
|
657 |
qed |
|
658 |
||
659 |
lemma deg_mult [simp]: |
|
660 |
"[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q" |
|
33657 | 661 |
proof (rule le_antisym) |
13936 | 662 |
show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring) |
663 |
next |
|
664 |
let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))" |
|
665 |
assume nz: "p ~= 0" "q ~= 0" |
|
666 |
have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith |
|
667 |
show "deg p + deg q <= deg (p * q)" |
|
668 |
proof (rule deg_belowI, simp) |
|
669 |
have "setsum ?s {.. deg p + deg q} |
|
15045 | 670 |
= setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})" |
13936 | 671 |
by (simp only: ivl_disj_un_one) |
672 |
also have "... = setsum ?s {deg p .. deg p + deg q}" |
|
673 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one |
|
674 |
setsum_0 deg_aboveD less_add_diff) |
|
15045 | 675 |
also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})" |
13936 | 676 |
by (simp only: ivl_disj_un_singleton) |
677 |
also have "... = coeff p (deg p) * coeff q (deg q)" |
|
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
678 |
by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD) |
13936 | 679 |
finally have "setsum ?s {.. deg p + deg q} |
680 |
= coeff p (deg p) * coeff q (deg q)" . |
|
681 |
with nz show "setsum ?s {.. deg p + deg q} ~= 0" |
|
682 |
by (simp add: integral_iff lcoeff_nonzero) |
|
683 |
qed |
|
684 |
qed |
|
685 |
||
686 |
lemma coeff_natsum: |
|
687 |
"((coeff (setsum p A) k)::'a::ring) = |
|
688 |
setsum (%i. coeff (p i) k) A" |
|
689 |
proof (cases "finite A") |
|
690 |
case True then show ?thesis by induct auto |
|
691 |
next |
|
692 |
case False then show ?thesis by (simp add: setsum_def) |
|
693 |
qed |
|
694 |
(* Instance of a more general result!!! *) |
|
695 |
||
696 |
(* |
|
697 |
lemma coeff_natsum: |
|
698 |
"((coeff (setsum p {..n::nat}) k)::'a::ring) = |
|
699 |
setsum (%i. coeff (p i) k) {..n}" |
|
700 |
by (induct n) auto |
|
701 |
*) |
|
702 |
||
703 |
lemma up_repr: |
|
704 |
"setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p" |
|
705 |
proof (rule up_eqI) |
|
706 |
let ?s = "(%i. monom (coeff p i) i)" |
|
707 |
fix k |
|
708 |
show "coeff (setsum ?s {..deg p}) k = coeff p k" |
|
709 |
proof (cases "k <= deg p") |
|
710 |
case True |
|
711 |
hence "coeff (setsum ?s {..deg p}) k = |
|
15045 | 712 |
coeff (setsum ?s ({..k} Un {k<..deg p})) k" |
13936 | 713 |
by (simp only: ivl_disj_un_one) |
714 |
also from True |
|
715 |
have "... = coeff (setsum ?s {..k}) k" |
|
716 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2 |
|
717 |
setsum_0 coeff_natsum ) |
|
718 |
also |
|
15045 | 719 |
have "... = coeff (setsum ?s ({..<k} Un {k})) k" |
13936 | 720 |
by (simp only: ivl_disj_un_singleton) |
721 |
also have "... = coeff p k" |
|
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
722 |
by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD) |
13936 | 723 |
finally show ?thesis . |
724 |
next |
|
725 |
case False |
|
726 |
hence "coeff (setsum ?s {..deg p}) k = |
|
15045 | 727 |
coeff (setsum ?s ({..<deg p} Un {deg p})) k" |
13936 | 728 |
by (simp only: ivl_disj_un_singleton) |
729 |
also from False have "... = coeff p k" |
|
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
730 |
by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD) |
13936 | 731 |
finally show ?thesis . |
732 |
qed |
|
733 |
qed |
|
734 |
||
735 |
lemma up_repr_le: |
|
736 |
"deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p" |
|
737 |
proof - |
|
738 |
let ?s = "(%i. monom (coeff p i) i)" |
|
739 |
assume "deg p <= n" |
|
15045 | 740 |
then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})" |
13936 | 741 |
by (simp only: ivl_disj_un_one) |
742 |
also have "... = setsum ?s {..deg p}" |
|
743 |
by (simp add: setsum_Un_disjoint ivl_disj_int_one |
|
744 |
setsum_0 deg_aboveD) |
|
745 |
also have "... = p" by (rule up_repr) |
|
746 |
finally show ?thesis . |
|
747 |
qed |
|
748 |
||
749 |
instance up :: ("domain") "domain" |
|
750 |
proof |
|
751 |
show "1 ~= (0::'a up)" |
|
752 |
proof (* notI is applied here *) |
|
753 |
assume "1 = (0::'a up)" |
|
754 |
hence "coeff 1 0 = (coeff 0 0::'a)" by simp |
|
755 |
hence "1 = (0::'a)" by simp |
|
756 |
with one_not_zero show "False" by contradiction |
|
757 |
qed |
|
758 |
next |
|
759 |
fix p q :: "'a::domain up" |
|
760 |
assume pq: "p * q = 0" |
|
761 |
show "p = 0 | q = 0" |
|
762 |
proof (rule classical) |
|
763 |
assume c: "~ (p = 0 | q = 0)" |
|
764 |
then have "deg p + deg q = deg (p * q)" by simp |
|
765 |
also from pq have "... = 0" by simp |
|
766 |
finally have "deg p + deg q = 0" . |
|
767 |
then have f1: "deg p = 0 & deg q = 0" by simp |
|
768 |
from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}" |
|
769 |
by (simp only: up_repr_le) |
|
770 |
also have "... = monom (coeff p 0) 0" by simp |
|
771 |
finally have p: "p = monom (coeff p 0) 0" . |
|
772 |
from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}" |
|
773 |
by (simp only: up_repr_le) |
|
774 |
also have "... = monom (coeff q 0) 0" by simp |
|
775 |
finally have q: "q = monom (coeff q 0) 0" . |
|
776 |
have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp |
|
777 |
also from pq have "... = 0" by simp |
|
778 |
finally have "coeff p 0 * coeff q 0 = 0" . |
|
779 |
then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff) |
|
780 |
with p q show "p = 0 | q = 0" by fastsimp |
|
781 |
qed |
|
782 |
qed |
|
783 |
||
784 |
lemma monom_inj_zero: |
|
785 |
"(monom a n = 0) = (a = 0)" |
|
786 |
proof - |
|
787 |
have "(monom a n = 0) = (monom a n = monom 0 n)" by simp |
|
788 |
also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero) |
|
789 |
finally show ?thesis . |
|
790 |
qed |
|
791 |
(* term order: makes this simpler!!! |
|
792 |
lemma smult_integral: |
|
793 |
"(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" |
|
794 |
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast |
|
795 |
*) |
|
796 |
lemma smult_integral: |
|
797 |
"(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" |
|
798 |
by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) |
|
799 |
||
21423 | 800 |
|
801 |
(* Divisibility and degree *) |
|
802 |
||
803 |
lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q" |
|
804 |
apply (unfold dvd_def) |
|
805 |
apply (erule exE) |
|
806 |
apply hypsubst |
|
807 |
apply (case_tac "p = 0") |
|
808 |
apply (case_tac [2] "k = 0") |
|
809 |
apply auto |
|
810 |
done |
|
811 |
||
14590 | 812 |
end |