author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 35849 | b5522b51cb1e |
child 39159 | 0dec18004e75 |
permissions | -rw-r--r-- |
35849 | 1 |
(* Author: Clemens Ballarin, started 23 June 1999 |
2 |
||
3 |
Experimental theory: long division of polynomials. |
|
7998 | 4 |
*) |
5 |
||
35849 | 6 |
theory LongDiv |
7 |
imports PolyHomo |
|
8 |
begin |
|
7998 | 9 |
|
21423 | 10 |
definition |
11 |
lcoeff :: "'a::ring up => 'a" where |
|
12 |
"lcoeff p = coeff p (deg p)" |
|
7998 | 13 |
|
21423 | 14 |
definition |
15 |
eucl_size :: "'a::zero up => nat" where |
|
16 |
"eucl_size p = (if p = 0 then 0 else deg p + 1)" |
|
14723 | 17 |
|
18 |
lemma SUM_shrink_below_lemma: |
|
19 |
"!! f::(nat=>'a::ring). (ALL i. i < m --> f i = 0) --> |
|
20 |
setsum (%i. f (i+m)) {..d} = setsum f {..m+d}" |
|
21 |
apply (induct_tac d) |
|
15481 | 22 |
apply (induct_tac m) |
21423 | 23 |
apply simp |
24 |
apply force |
|
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
21423
diff
changeset
|
25 |
apply (simp add: add_commute [of m]) |
21423 | 26 |
done |
27 |
||
28 |
lemma SUM_extend_below: |
|
29 |
"!! f::(nat=>'a::ring). |
|
30 |
[| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] |
|
31 |
==> P (setsum f {..n})" |
|
32 |
by (simp add: SUM_shrink_below_lemma add_diff_inverse leD) |
|
33 |
||
34 |
lemma up_repr2D: |
|
35 |
"!! p::'a::ring up. |
|
36 |
[| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] |
|
37 |
==> P p" |
|
38 |
by (simp add: up_repr_le) |
|
39 |
||
40 |
||
41 |
(* Start of LongDiv *) |
|
42 |
||
43 |
lemma deg_lcoeff_cancel: |
|
44 |
"!!p::('a::ring up). |
|
45 |
[| deg p <= deg r; deg q <= deg r; |
|
46 |
coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> |
|
47 |
deg (p + q) < deg r" |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
22384
diff
changeset
|
48 |
apply (rule le_less_trans [of _ "deg r - 1"]) |
21423 | 49 |
prefer 2 |
50 |
apply arith |
|
51 |
apply (rule deg_aboveI) |
|
52 |
apply (case_tac "deg r = m") |
|
53 |
apply clarify |
|
54 |
apply simp |
|
55 |
(* case "deg q ~= m" *) |
|
56 |
apply (subgoal_tac "deg p < m & deg q < m") |
|
57 |
apply (simp (no_asm_simp) add: deg_aboveD) |
|
58 |
apply arith |
|
59 |
done |
|
60 |
||
61 |
lemma deg_lcoeff_cancel2: |
|
62 |
"!!p::('a::ring up). |
|
63 |
[| deg p <= deg r; deg q <= deg r; |
|
64 |
p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> |
|
65 |
deg (p + q) < deg r" |
|
66 |
apply (rule deg_lcoeff_cancel) |
|
67 |
apply assumption+ |
|
68 |
apply (rule classical) |
|
69 |
apply clarify |
|
70 |
apply (erule notE) |
|
71 |
apply (rule_tac p = p in up_repr2D, assumption) |
|
72 |
apply (rule_tac p = q in up_repr2D, assumption) |
|
73 |
apply (rotate_tac -1) |
|
74 |
apply (simp add: smult_l_minus) |
|
75 |
done |
|
76 |
||
77 |
lemma long_div_eucl_size: |
|
78 |
"!!g::('a::ring up). g ~= 0 ==> |
|
79 |
Ex (% (q, r, k). |
|
80 |
(lcoeff g)^k *s f = q * g + r & (eucl_size r < eucl_size g))" |
|
81 |
apply (rule_tac P = "%f. Ex (% (q, r, k) . (lcoeff g) ^k *s f = q * g + r & (eucl_size r < eucl_size g))" in wf_induct) |
|
82 |
(* TO DO: replace by measure_induct *) |
|
83 |
apply (rule_tac f = eucl_size in wf_measure) |
|
84 |
apply (case_tac "eucl_size x < eucl_size g") |
|
85 |
apply (rule_tac x = "(0, x, 0)" in exI) |
|
86 |
apply (simp (no_asm_simp)) |
|
87 |
(* case "eucl_size x >= eucl_size g" *) |
|
88 |
apply (drule_tac x = "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g" in spec) |
|
89 |
apply (erule impE) |
|
90 |
apply (simp (no_asm_use) add: inv_image_def measure_def lcoeff_def) |
|
91 |
apply (case_tac "x = 0") |
|
92 |
apply (rotate_tac -1) |
|
93 |
apply (simp add: eucl_size_def) |
|
94 |
(* case "x ~= 0 *) |
|
95 |
apply (rotate_tac -1) |
|
96 |
apply (simp add: eucl_size_def) |
|
97 |
apply (rule impI) |
|
98 |
apply (rule deg_lcoeff_cancel2) |
|
99 |
(* replace by linear arithmetic??? *) |
|
100 |
apply (rule_tac [2] le_trans) |
|
101 |
apply (rule_tac [2] deg_smult_ring) |
|
102 |
prefer 2 |
|
103 |
apply simp |
|
104 |
apply (simp (no_asm)) |
|
105 |
apply (rule le_trans) |
|
106 |
apply (rule deg_mult_ring) |
|
107 |
apply (rule le_trans) |
|
108 |
(**) |
|
109 |
apply (rule add_le_mono) |
|
110 |
apply (rule le_refl) |
|
111 |
(* term order forces to use this instead of add_le_mono1 *) |
|
112 |
apply (rule deg_monom_ring) |
|
113 |
apply (simp (no_asm_simp)) |
|
114 |
apply force |
|
115 |
apply (simp (no_asm)) |
|
116 |
(**) |
|
117 |
(* This change is probably caused by application of commutativity *) |
|
118 |
apply (rule_tac m = "deg g" and n = "deg x" in SUM_extend) |
|
119 |
apply (simp (no_asm)) |
|
120 |
apply (simp (no_asm_simp)) |
|
121 |
apply arith |
|
122 |
apply (rule_tac m = "deg g" and n = "deg g" in SUM_extend_below) |
|
123 |
apply (rule le_refl) |
|
124 |
apply (simp (no_asm_simp)) |
|
125 |
apply arith |
|
126 |
apply (simp (no_asm)) |
|
127 |
(**) |
|
128 |
(* end of subproof deg f1 < deg f *) |
|
129 |
apply (erule exE) |
|
130 |
apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI) |
|
131 |
apply clarify |
|
132 |
apply (drule sym) |
|
26342 | 133 |
apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}] |
21423 | 134 |
delsimprocs [ring_simproc]) 1 *}) |
26342 | 135 |
apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) |
136 |
apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr", |
|
30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
27214
diff
changeset
|
137 |
thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"] |
21423 | 138 |
delsimprocs [ring_simproc]) 1 *}) |
30968
10fef94f40fc
adaptions due to rearrangment of power operation
haftmann
parents:
27214
diff
changeset
|
139 |
apply (simp add: smult_assoc1 [symmetric]) |
21423 | 140 |
done |
141 |
||
27214 | 142 |
ML {* |
143 |
bind_thm ("long_div_ring_aux", |
|
144 |
simplify (@{simpset} addsimps [@{thm eucl_size_def}] |
|
145 |
delsimprocs [ring_simproc]) (@{thm long_div_eucl_size})) |
|
146 |
*} |
|
21423 | 147 |
|
148 |
lemma long_div_ring: |
|
149 |
"!!g::('a::ring up). g ~= 0 ==> |
|
150 |
Ex (% (q, r, k). |
|
151 |
(lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))" |
|
27214 | 152 |
apply (frule_tac f = f in long_div_ring_aux) |
26342 | 153 |
apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *}) |
21423 | 154 |
apply (case_tac "aa = 0") |
155 |
apply blast |
|
156 |
(* case "aa ~= 0 *) |
|
157 |
apply (rotate_tac -1) |
|
158 |
apply auto |
|
159 |
done |
|
160 |
||
161 |
(* Next one fails *) |
|
162 |
lemma long_div_unit: |
|
163 |
"!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> |
|
164 |
Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))" |
|
165 |
apply (frule_tac f = "f" in long_div_ring) |
|
166 |
apply (erule exE) |
|
167 |
apply (rule_tac x = "((% (q,r,k) . (inverse (lcoeff g ^k) *s q)) x, (% (q,r,k) . inverse (lcoeff g ^k) *s r) x) " in exI) |
|
168 |
apply clarify |
|
169 |
apply (rule conjI) |
|
170 |
apply (drule sym) |
|
171 |
apply (tactic {* asm_simp_tac |
|
26342 | 172 |
(@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"] |
21423 | 173 |
delsimprocs [ring_simproc]) 1 *}) |
174 |
apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric]) |
|
175 |
(* degree property *) |
|
176 |
apply (erule disjE) |
|
177 |
apply (simp (no_asm_simp)) |
|
178 |
apply (rule disjI2) |
|
179 |
apply (rule le_less_trans) |
|
180 |
apply (rule deg_smult_ring) |
|
181 |
apply (simp (no_asm_simp)) |
|
182 |
done |
|
183 |
||
184 |
lemma long_div_theorem: |
|
185 |
"!!g::('a::field up). g ~= 0 ==> |
|
186 |
Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))" |
|
187 |
apply (rule long_div_unit) |
|
188 |
apply assumption |
|
189 |
apply (simp (no_asm_simp) add: lcoeff_def lcoeff_nonzero field_ax) |
|
190 |
done |
|
191 |
||
192 |
lemma uminus_zero: "- (0::'a::ring) = 0" |
|
193 |
by simp |
|
194 |
||
195 |
lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b" |
|
196 |
apply (rule_tac s = "a - (a - b) " in trans) |
|
26342 | 197 |
apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) |
21423 | 198 |
apply simp |
199 |
apply (simp (no_asm)) |
|
200 |
done |
|
201 |
||
202 |
lemma eq_imp_diff_zero: "!!a::'a::ring. a = b ==> a + (-b) = 0" |
|
203 |
by simp |
|
204 |
||
205 |
lemma long_div_quo_unique: |
|
206 |
"!!g::('a::field up). [| g ~= 0; |
|
207 |
f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); |
|
208 |
f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2" |
|
209 |
apply (subgoal_tac "(q1 - q2) * g = r2 - r1") (* 1 *) |
|
210 |
apply (erule_tac V = "f = ?x" in thin_rl) |
|
211 |
apply (erule_tac V = "f = ?x" in thin_rl) |
|
212 |
apply (rule diff_zero_imp_eq) |
|
213 |
apply (rule classical) |
|
214 |
apply (erule disjE) |
|
215 |
(* r1 = 0 *) |
|
216 |
apply (erule disjE) |
|
217 |
(* r2 = 0 *) |
|
26342 | 218 |
apply (tactic {* asm_full_simp_tac (@{simpset} |
21423 | 219 |
addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"] |
220 |
delsimprocs [ring_simproc]) 1 *}) |
|
221 |
(* r2 ~= 0 *) |
|
222 |
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) |
|
26342 | 223 |
apply (tactic {* asm_full_simp_tac (@{simpset} addsimps |
21423 | 224 |
[thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) |
225 |
(* r1 ~=0 *) |
|
226 |
apply (erule disjE) |
|
227 |
(* r2 = 0 *) |
|
228 |
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) |
|
26342 | 229 |
apply (tactic {* asm_full_simp_tac (@{simpset} addsimps |
21423 | 230 |
[thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) |
231 |
(* r2 ~= 0 *) |
|
232 |
apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) |
|
26342 | 233 |
apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"] |
21423 | 234 |
delsimprocs [ring_simproc]) 1 *}) |
235 |
apply (drule order_eq_refl [THEN add_leD2]) |
|
236 |
apply (drule leD) |
|
237 |
apply (erule notE, rule deg_add [THEN le_less_trans]) |
|
238 |
apply (simp (no_asm_simp)) |
|
239 |
(* proof of 1 *) |
|
240 |
apply (rule diff_zero_imp_eq) |
|
241 |
apply hypsubst |
|
242 |
apply (drule_tac a = "?x+?y" in eq_imp_diff_zero) |
|
243 |
apply simp |
|
244 |
done |
|
245 |
||
246 |
lemma long_div_rem_unique: |
|
247 |
"!!g::('a::field up). [| g ~= 0; |
|
248 |
f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); |
|
249 |
f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2" |
|
250 |
apply (subgoal_tac "q1 = q2") |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
22384
diff
changeset
|
251 |
apply (metis a_comm a_lcancel m_comm) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
22384
diff
changeset
|
252 |
apply (metis a_comm l_zero long_div_quo_unique m_comm conc) |
14723 | 253 |
done |
7998 | 254 |
|
255 |
end |