|
1 (* |
|
2 Degree of polynomials |
|
3 $Id$ |
|
4 written by Clemens Ballarin, started 22 January 1997 |
|
5 *) |
|
6 |
|
7 (* Relating degree and bound *) |
|
8 |
|
9 goal ProtoPoly.thy |
|
10 "!! f. [| bound m f; f n ~= <0> |] ==> n <= m"; |
|
11 by (rtac classical 1); |
|
12 by (dtac not_leE 1); |
|
13 by (dtac boundD 1 THEN atac 1); |
|
14 by (etac notE 1); |
|
15 by (assume_tac 1); |
|
16 qed "below_bound"; |
|
17 |
|
18 goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)"; |
|
19 by (rtac exE 1); |
|
20 by (rtac LeastI 2); |
|
21 by (assume_tac 2); |
|
22 by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); |
|
23 by (rtac (rewrite_rule [UP_def] Rep_UP) 1); |
|
24 qed "Least_is_bound"; |
|
25 |
|
26 Goalw [coeff_def, deg_def] |
|
27 "!! p. ALL m. n < m --> coeff m p = <0> ==> deg p <= n"; |
|
28 by (rtac Least_le 1); |
|
29 by (Fast_tac 1); |
|
30 qed "deg_aboveI"; |
|
31 |
|
32 Goalw [coeff_def, deg_def] |
|
33 "!! p. (n ~= 0 --> coeff n p ~= <0>) ==> n <= deg p"; |
|
34 by (case_tac "n = 0" 1); |
|
35 (* Case n=0 *) |
|
36 by (Asm_simp_tac 1); |
|
37 (* Case n~=0 *) |
|
38 by (rotate_tac 1 1); |
|
39 by (Asm_full_simp_tac 1); |
|
40 by (rtac below_bound 1); |
|
41 by (assume_tac 2); |
|
42 by (rtac Least_is_bound 1); |
|
43 qed "deg_belowI"; |
|
44 |
|
45 Goalw [coeff_def, deg_def] |
|
46 "!! p. deg p < m ==> coeff m p = <0>"; |
|
47 by (rtac exE 1); (* create !! x. *) |
|
48 by (rtac boundD 2); |
|
49 by (assume_tac 3); |
|
50 by (rtac LeastI 2); |
|
51 by (assume_tac 2); |
|
52 by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); |
|
53 by (rtac (rewrite_rule [UP_def] Rep_UP) 1); |
|
54 qed "deg_aboveD"; |
|
55 |
|
56 Goalw [deg_def] |
|
57 "!! p. deg p = Suc y ==> ~ bound y (Rep_UP p)"; |
|
58 by (rtac not_less_Least 1); |
|
59 by (Asm_simp_tac 1); |
|
60 val lemma1 = result(); |
|
61 |
|
62 Goalw [deg_def, coeff_def] |
|
63 "!! p. deg p = Suc y ==> coeff (deg p) p ~= <0>"; |
|
64 by (rtac classical 1); |
|
65 by (dtac notnotD 1); |
|
66 by (cut_inst_tac [("p", "p")] Least_is_bound 1); |
|
67 by (subgoal_tac "bound y (Rep_UP p)" 1); |
|
68 (* prove subgoal *) |
|
69 by (rtac boundI 2); |
|
70 by (case_tac "Suc y < m" 2); |
|
71 (* first case *) |
|
72 by (rtac boundD 2); |
|
73 by (assume_tac 2); |
|
74 by (Asm_simp_tac 2); |
|
75 (* second case *) |
|
76 by (dtac leI 2); |
|
77 by (dtac Suc_leI 2); |
|
78 by (dtac le_anti_sym 2); |
|
79 by (assume_tac 2); |
|
80 by (Asm_full_simp_tac 2); |
|
81 (* end prove subgoal *) |
|
82 by (fold_goals_tac [deg_def]); |
|
83 by (dtac lemma1 1); |
|
84 by (etac notE 1); |
|
85 by (assume_tac 1); |
|
86 val lemma2 = result(); |
|
87 |
|
88 Goal |
|
89 "!! p. deg p ~= 0 ==> coeff (deg p) p ~= <0>"; |
|
90 by (rtac lemma2 1); |
|
91 by (Full_simp_tac 1); |
|
92 by (dtac Suc_pred 1); |
|
93 by (rtac sym 1); |
|
94 by (Asm_simp_tac 1); |
|
95 qed "deg_lcoeff"; |
|
96 |
|
97 Goal |
|
98 "!! p. p ~= <0> ==> coeff (deg p) p ~= <0>"; |
|
99 by (etac contrapos 1); |
|
100 by (ftac contrapos2 1); |
|
101 by (rtac deg_lcoeff 1); |
|
102 by (assume_tac 1); |
|
103 by (rtac up_eqI 1); |
|
104 by (case_tac "n=0" 1); |
|
105 by (rotate_tac ~2 1); |
|
106 by (Asm_full_simp_tac 1); |
|
107 by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
108 qed "nonzero_lcoeff"; |
|
109 |
|
110 Goal "(deg p <= n) = bound n (Rep_UP p)"; |
|
111 by (rtac iffI 1); |
|
112 (* ==> *) |
|
113 by (rtac boundI 1); |
|
114 by (fold_goals_tac [coeff_def]); |
|
115 by (rtac deg_aboveD 1); |
|
116 by (fast_arith_tac 1); |
|
117 (* <== *) |
|
118 by (rtac deg_aboveI 1); |
|
119 by (rewtac coeff_def); |
|
120 by (Fast_tac 1); |
|
121 qed "deg_above_is_bound"; |
|
122 |
|
123 (* Lemmas on the degree function *) |
|
124 |
|
125 Goalw [max_def] |
|
126 "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)"; |
|
127 by (case_tac "deg p <= deg q" 1); |
|
128 (* case deg p <= deg q *) |
|
129 by (rtac deg_aboveI 1); |
|
130 by (Asm_simp_tac 1); |
|
131 by (strip_tac 1); |
|
132 by (dtac le_less_trans 1); |
|
133 by (assume_tac 1); |
|
134 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
135 (* case deg p > deg q *) |
|
136 by (rtac deg_aboveI 1); |
|
137 by (Asm_simp_tac 1); |
|
138 by (dtac not_leE 1); |
|
139 by (strip_tac 1); |
|
140 by (dtac less_trans 1); |
|
141 by (assume_tac 1); |
|
142 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
143 qed "deg_add"; |
|
144 |
|
145 Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q"; |
|
146 by (rtac order_antisym 1); |
|
147 by (rtac le_trans 1); |
|
148 by (rtac deg_add 1); |
|
149 by (Asm_simp_tac 1); |
|
150 by (rtac deg_belowI 1); |
|
151 by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1); |
|
152 qed "deg_add_equal"; |
|
153 |
|
154 Goal "deg (monom m::'a::ring up) = m"; |
|
155 by (rtac le_anti_sym 1); |
|
156 (* <= *) |
|
157 by (asm_simp_tac |
|
158 (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1); |
|
159 (* >= *) |
|
160 by (asm_simp_tac |
|
161 (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1); |
|
162 qed "deg_monom"; |
|
163 |
|
164 Goal "!! a::'a::ring. deg (const a) = 0"; |
|
165 by (rtac le_anti_sym 1); |
|
166 by (rtac deg_aboveI 1); |
|
167 by (simp_tac (simpset() addsimps [less_not_refl2]) 1); |
|
168 by (rtac deg_belowI 1); |
|
169 by (simp_tac (simpset() addsimps [less_not_refl2]) 1); |
|
170 qed "deg_const"; |
|
171 |
|
172 Goal "deg (<0>::'a::ringS up) = 0"; |
|
173 by (rtac le_anti_sym 1); |
|
174 by (rtac deg_aboveI 1); |
|
175 by (Simp_tac 1); |
|
176 by (rtac deg_belowI 1); |
|
177 by (Simp_tac 1); |
|
178 qed "deg_zero"; |
|
179 |
|
180 Goal "deg (<1>::'a::ring up) = 0"; |
|
181 by (rtac le_anti_sym 1); |
|
182 by (rtac deg_aboveI 1); |
|
183 by (simp_tac (simpset() addsimps [less_not_refl2]) 1); |
|
184 by (rtac deg_belowI 1); |
|
185 by (Simp_tac 1); |
|
186 qed "deg_one"; |
|
187 |
|
188 Goal "!!p::('a::ring) up. deg (-p) = deg p"; |
|
189 by (rtac le_anti_sym 1); |
|
190 (* <= *) |
|
191 by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1); |
|
192 by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1); |
|
193 qed "deg_uminus"; |
|
194 |
|
195 Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus]; |
|
196 |
|
197 Goal |
|
198 "!! a::'a::ring. deg (a *s p) <= (if a = <0> then 0 else deg p)"; |
|
199 by (case_tac "a = <0>" 1); |
|
200 by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1)); |
|
201 qed "deg_smult_ring"; |
|
202 |
|
203 Goal |
|
204 "!! a::'a::domain. deg (a *s p) = (if a = <0> then 0 else deg p)"; |
|
205 by (rtac le_anti_sym 1); |
|
206 by (rtac deg_smult_ring 1); |
|
207 by (case_tac "a = <0>" 1); |
|
208 by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1)); |
|
209 qed "deg_smult"; |
|
210 |
|
211 Goal |
|
212 "!! p::'a::ring up. [| deg p + deg q < k |] ==> \ |
|
213 \ coeff i p * coeff (k - i) q = <0>"; |
|
214 by (simp_tac (simpset() addsimps [coeff_def]) 1); |
|
215 by (rtac bound_mult_zero 1); |
|
216 by (assume_tac 3); |
|
217 by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); |
|
218 by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); |
|
219 qed "deg_above_mult_zero"; |
|
220 |
|
221 Goal |
|
222 "!! p::'a::ring up. deg (p * q) <= deg p + deg q"; |
|
223 by (rtac deg_aboveI 1); |
|
224 by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1); |
|
225 qed "deg_mult_ring"; |
|
226 |
|
227 goal Main.thy |
|
228 "!!k::nat. k < n ==> m < n + m - k"; |
|
229 by (arith_tac 1); |
|
230 qed "less_add_diff"; |
|
231 |
|
232 Goal "!!p. coeff n p ~= <0> ==> n <= deg p"; |
|
233 (* More general than deg_belowI, and simplifies the next proof! *) |
|
234 by (rtac deg_belowI 1); |
|
235 by (Fast_tac 1); |
|
236 qed "deg_below2I"; |
|
237 |
|
238 Goal |
|
239 "!! p::'a::domain up. \ |
|
240 \ [| p ~= <0>; q ~= <0> |] ==> deg (p * q) = deg p + deg q"; |
|
241 by (rtac le_anti_sym 1); |
|
242 by (rtac deg_mult_ring 1); |
|
243 (* deg p + deg q <= deg (p * q) *) |
|
244 by (rtac deg_below2I 1); |
|
245 by (Simp_tac 1); |
|
246 (* |
|
247 by (rtac conjI 1); |
|
248 by (rtac impI 1); |
|
249 *) |
|
250 by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); |
|
251 by (rtac le_add1 1); |
|
252 by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); |
|
253 by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); |
|
254 by (rtac le_refl 1); |
|
255 by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); |
|
256 by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); |
|
257 (* |
|
258 by (rtac impI 1); |
|
259 by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); |
|
260 by (rtac le_add1 1); |
|
261 by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); |
|
262 by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); |
|
263 by (rtac le_refl 1); |
|
264 by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); |
|
265 by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); |
|
266 *) |
|
267 qed "deg_mult"; |
|
268 |
|
269 Addsimps [deg_smult, deg_mult]; |
|
270 |
|
271 (* Representation theorems about polynomials *) |
|
272 |
|
273 goal PolyRing.thy |
|
274 "!! p::nat=>'a::ring up. coeff k (SUM n p) = SUM n (%i. coeff k (p i))"; |
|
275 by (nat_ind_tac "n" 1); |
|
276 (* Base case *) |
|
277 by (Simp_tac 1); |
|
278 (* Induction step *) |
|
279 by (Asm_simp_tac 1); |
|
280 qed "coeff_SUM"; |
|
281 |
|
282 goal UnivPoly.thy |
|
283 "!! f::(nat=>'a::ring). \ |
|
284 \ bound n f ==> SUM n (%i. if i = x then f i else <0>) = f x"; |
|
285 by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1); |
|
286 by (auto_tac |
|
287 (claset() addDs [not_leE], |
|
288 simpset() setloop (split_tac [expand_if]))); |
|
289 qed "bound_SUM_if"; |
|
290 |
|
291 Goal |
|
292 "!! p::'a::ring up. deg p <= n ==> SUM n (%i. coeff i p *s monom i) = p"; |
|
293 by (rtac up_eqI 1); |
|
294 by (simp_tac (simpset() addsimps [coeff_SUM]) 1); |
|
295 by (rtac trans 1); |
|
296 by (res_inst_tac [("x", "na")] bound_SUM_if 2); |
|
297 by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2); |
|
298 by (rtac SUM_cong 1); |
|
299 by (rtac refl 1); |
|
300 by (asm_simp_tac |
|
301 (simpset() setloop (split_tac [expand_if])) 1); |
|
302 qed "up_repr"; |
|
303 |
|
304 Goal |
|
305 "!! p::'a::ring up. [| deg p <= n; P p |] ==> \ |
|
306 \ P (SUM n (%i. coeff i p *s monom i))"; |
|
307 by (asm_simp_tac (simpset() addsimps [up_repr]) 1); |
|
308 qed "up_reprD"; |
|
309 |
|
310 Goal |
|
311 "!! p::'a::ring up. [| deg p <= n; P (SUM n (%i. coeff i p *s monom i)) |] \ |
|
312 \ ==> P p"; |
|
313 by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1); |
|
314 qed "up_repr2D"; |
|
315 |
|
316 (* |
|
317 Goal |
|
318 "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \ |
|
319 \ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \ |
|
320 \ = (coeff k f = coeff k g) |
|
321 ... |
|
322 qed "up_unique"; |
|
323 *) |
|
324 |
|
325 (* Polynomials over integral domains are again integral domains *) |
|
326 |
|
327 Goal "!!p::'a::domain up. p * q = <0> ==> p = <0> | q = <0>"; |
|
328 by (rtac classical 1); |
|
329 by (subgoal_tac "deg p = 0 & deg q = 0" 1); |
|
330 by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1); |
|
331 by (Asm_simp_tac 1); |
|
332 by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1); |
|
333 by (Asm_simp_tac 1); |
|
334 by (subgoal_tac "coeff 0 p = <0> | coeff 0 q = <0>" 1); |
|
335 by (SELECT_GOAL (auto_tac (claset() addIs [up_eqI], simpset())) 1); |
|
336 by (rtac integral 1); |
|
337 by (subgoal_tac "coeff 0 (p * q) = <0>" 1); |
|
338 by (Full_simp_tac 1); |
|
339 by (Asm_simp_tac 1); |
|
340 |
|
341 by (dres_inst_tac [("f", "deg")] arg_cong 1); |
|
342 by (Asm_full_simp_tac 1); |
|
343 qed "up_integral"; |
|
344 |
|
345 Goal "!! a::'a::domain. a *s p = <0> ==> a = <0> | p = <0>"; |
|
346 by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); |
|
347 by (dtac up_integral 1); |
|
348 by Auto_tac; |
|
349 by (rtac (const_inj RS injD) 1); |
|
350 by (Simp_tac 1); |
|
351 qed "smult_integral"; |
|
352 |
|
353 (* Divisibility and degree *) |
|
354 |
|
355 Goalw [dvd_def] |
|
356 "!! p::'a::domain up. [| p dvd q; q ~= <0> |] ==> deg p <= deg q"; |
|
357 by (etac exE 1); |
|
358 by (hyp_subst_tac 1); |
|
359 by (case_tac "p = <0>" 1); |
|
360 by (Asm_simp_tac 1); |
|
361 by (dtac r_nullD 1); |
|
362 by (asm_simp_tac (simpset() addsimps [le_add1]) 1); |
|
363 qed "dvd_imp_deg"; |