1 (* ========================================================================= *)
2 (* Naive quantifier elimination for complex numbers. *)
3 (* ========================================================================= *)
5 needs "Complex/fundamental.ml";;
7 let NULLSTELLENSATZ_LEMMA = prove
8 (`!n p q. (!x. (poly p x = Cx(&0)) ==> (poly q x = Cx(&0))) /\
9 (degree p = n) /\ ~(n = 0)
10 ==> p divides (q exp n)`,
11 MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
12 MAP_EVERY X_GEN_TAC [`p:complex list`; `q:complex list`] THEN
13 ASM_CASES_TAC `?a. poly p a = Cx(&0)` THENL
15 DISCH_THEN(K ALL_TAC) THEN
16 FIRST_ASSUM(MP_TAC o MATCH_MP
17 (ONCE_REWRITE_RULE[TAUT `a ==> b <=> ~b ==> ~a`]
18 FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT)) THEN
19 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
20 MAP_EVERY X_GEN_TAC [`k:complex`; `zeros:complex list`] THEN
21 STRIP_TAC THEN REWRITE_TAC[divides] THEN
22 EXISTS_TAC `[inv(k)] ** q exp n` THEN
23 ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN X_GEN_TAC `z:complex` THEN
24 ASM_SIMP_TAC[COMPLEX_MUL_ASSOC; COMPLEX_MUL_RINV; COMPLEX_MUL_LID;
25 poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID; POLY_0]] THEN
26 FIRST_X_ASSUM(X_CHOOSE_THEN `a:complex` MP_TAC) THEN
27 DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
28 GEN_REWRITE_TAC LAND_CONV [ORDER_ROOT] THEN
29 ASM_CASES_TAC `poly p = poly []` THEN ASM_REWRITE_TAC[] THENL
30 [ASM_SIMP_TAC[DEGREE_ZERO] THEN MESON_TAC[]; ALL_TAC] THEN
31 STRIP_TAC THEN STRIP_TAC THEN
32 MP_TAC(SPECL [`p:complex list`; `a:complex`; `order a p`] ORDER) THEN
33 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
34 FIRST_ASSUM(MP_TAC o SPEC `a:complex` o MATCH_MP ORDER_DEGREE) THEN
35 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
36 FIRST_ASSUM(MP_TAC o SPEC `a:complex`) THEN
37 REWRITE_TAC[ASSUME `poly p a = Cx(&0)`] THEN
38 REWRITE_TAC[POLY_LINEAR_DIVIDES] THEN
39 ASM_CASES_TAC `q:complex list = []` THENL
40 [DISCH_TAC THEN MATCH_MP_TAC POLY_DIVIDES_ZERO THEN
41 UNDISCH_TAC `~(n = 0)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
42 INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp] THEN DISCH_TAC THEN
43 REWRITE_TAC[FUN_EQ_THM; POLY_MUL; COMPLEX_MUL_LZERO; poly];
45 ASM_REWRITE_TAC[] THEN
46 DISCH_THEN(X_CHOOSE_THEN `r:complex list` SUBST_ALL_TAC) THEN
47 UNDISCH_TAC `[--a; Cx (&1)] exp (order a p) divides p` THEN
48 GEN_REWRITE_TAC LAND_CONV [divides] THEN
49 DISCH_THEN(X_CHOOSE_THEN `s:complex list` ASSUME_TAC) THEN
50 SUBGOAL_THEN `~(poly s = poly [])` ASSUME_TAC THENL
51 [DISCH_TAC THEN UNDISCH_TAC `~(poly p = poly [])` THEN
52 ASM_REWRITE_TAC[POLY_ENTIRE]; ALL_TAC] THEN
53 ASM_CASES_TAC `degree s = 0` THENL
54 [SUBGOAL_THEN `?k. ~(k = Cx(&0)) /\ (poly s = poly [k])` MP_TAC THENL
55 [EXISTS_TAC `LAST(normalize s)` THEN
56 ASM_SIMP_TAC[NORMAL_NORMALIZE; GSYM POLY_NORMALIZE_ZERO] THEN
57 GEN_REWRITE_TAC LAND_CONV [GSYM POLY_NORMALIZE] THEN
58 UNDISCH_TAC `degree s = 0` THEN
59 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
60 [POLY_NORMALIZE_ZERO]) THEN
61 REWRITE_TAC[degree] THEN
62 SPEC_TAC(`normalize s`,`s:complex list`) THEN
63 LIST_INDUCT_TAC THEN REWRITE_TAC[NOT_CONS_NIL] THEN
64 REWRITE_TAC[LENGTH; PRE; poly; LAST] THEN
65 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
66 ASM_REWRITE_TAC[LENGTH_EQ_NIL]; ALL_TAC] THEN
67 DISCH_THEN(X_CHOOSE_THEN `k:complex` STRIP_ASSUME_TAC) THEN
68 REWRITE_TAC[divides] THEN
69 EXISTS_TAC `[inv(k)] ** [--a; Cx (&1)] exp (n - order a p) ** r exp n` THEN
70 ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_EXP; COMPLEX_POW_MUL] THEN
71 X_GEN_TAC `z:complex` THEN
72 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC
73 `(a * b) * c * d * e = ((d * a) * (c * b)) * e`] THEN
74 AP_THM_TAC THEN AP_TERM_TAC THEN
75 REWRITE_TAC[GSYM COMPLEX_POW_ADD] THEN ASM_SIMP_TAC[SUB_ADD] THEN
76 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID; COMPLEX_MUL_RID] THEN
77 ASM_SIMP_TAC[COMPLEX_MUL_LINV; COMPLEX_MUL_RID]; ALL_TAC] THEN
78 SUBGOAL_THEN `degree s < n` ASSUME_TAC THENL
80 FIRST_ASSUM(SUBST1_TAC o MATCH_MP DEGREE_WELLDEF) THEN
81 REWRITE_TAC[LINEAR_POW_MUL_DEGREE] THEN
82 ASM_REWRITE_TAC[] THEN UNDISCH_TAC `~(order a p = 0)` THEN ARITH_TAC;
84 FIRST_X_ASSUM(MP_TAC o SPEC `degree s`) THEN ASM_REWRITE_TAC[] THEN
85 DISCH_THEN(MP_TAC o SPECL [`s:complex list`; `r:complex list`]) THEN
86 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
87 [X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
89 `!x. (poly p x = Cx(&0)) ==> (poly([--a; Cx (&1)] ** r) x = Cx(&0))` THEN
90 DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
91 ASM_REWRITE_TAC[POLY_MUL; COMPLEX_MUL_RID] THEN
92 REWRITE_TAC[COMPLEX_ENTIRE] THEN
93 MATCH_MP_TAC(TAUT `~a ==> (a \/ b ==> b)`) THEN
94 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
95 REWRITE_TAC[SIMPLE_COMPLEX_ARITH
96 `(--a + z * Cx(&1) = Cx(&0)) <=> (z = a)`] THEN
97 DISCH_THEN SUBST_ALL_TAC THEN
98 UNDISCH_TAC `poly s a = Cx (&0)` THEN
99 ASM_REWRITE_TAC[POLY_LINEAR_DIVIDES; DE_MORGAN_THM] THEN
100 CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
101 DISCH_THEN(X_CHOOSE_THEN `u:complex list` SUBST_ALL_TAC) THEN
102 UNDISCH_TAC `~([--a; Cx (&1)] exp SUC (order a p) divides p)` THEN
103 REWRITE_TAC[divides] THEN
104 EXISTS_TAC `u:complex list` THEN ASM_REWRITE_TAC[] THEN
105 REWRITE_TAC[POLY_MUL; poly_exp; COMPLEX_MUL_AC; FUN_EQ_THM];
107 REWRITE_TAC[divides] THEN
108 DISCH_THEN(X_CHOOSE_THEN `u:complex list` ASSUME_TAC) THEN
110 `u ** [--a; Cx(&1)] exp (n - order a p) ** r exp (n - degree s)` THEN
111 ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_EXP; COMPLEX_POW_MUL] THEN
112 X_GEN_TAC `z:complex` THEN
113 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC
114 `(ap * s) * u * anp * rns = (anp * ap) * rns * s * u`] THEN
115 REWRITE_TAC[GSYM COMPLEX_POW_ADD] THEN
116 ASM_SIMP_TAC[SUB_ADD] THEN AP_TERM_TAC THEN
117 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM POLY_MUL] THEN
118 SUBST1_TAC(SYM(ASSUME `poly (r exp degree s) = poly (s ** u)`)) THEN
119 REWRITE_TAC[POLY_EXP; GSYM COMPLEX_POW_ADD] THEN
120 ASM_SIMP_TAC[SUB_ADD; LT_IMP_LE]);;
122 let NULLSTELLENSATZ_UNIVARIATE = prove
123 (`!p q. (!x. (poly p x = Cx(&0)) ==> (poly q x = Cx(&0))) <=>
124 p divides (q exp (degree p)) \/
125 ((poly p = poly []) /\ (poly q = poly []))`,
126 REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THENL
127 [ASM_REWRITE_TAC[poly] THEN
128 FIRST_ASSUM(SUBST1_TAC o MATCH_MP DEGREE_WELLDEF) THEN
129 REWRITE_TAC[degree; normalize; LENGTH; ARITH; poly_exp] THEN
130 ASM_REWRITE_TAC[divides; FUN_EQ_THM; POLY_MUL; poly;
131 COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
132 REWRITE_TAC[CX_INJ; REAL_OF_NUM_EQ; ARITH]; ALL_TAC] THEN
133 ASM_CASES_TAC `degree p = 0` THENL
135 MP_TAC(SPECL [`degree p`; `p:complex list`; `q:complex list`]
136 NULLSTELLENSATZ_LEMMA) THEN
137 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EQ_TAC THEN ASM_REWRITE_TAC[] THEN
139 X_GEN_TAC `z:complex` THEN DISCH_TAC THEN MP_TAC th) THEN
140 ASM_REWRITE_TAC[divides; FUN_EQ_THM; POLY_MUL] THEN
141 DISCH_THEN(CHOOSE_THEN (MP_TAC o SPEC `z:complex`)) THEN
142 ASM_REWRITE_TAC[POLY_EXP; COMPLEX_MUL_LZERO; COMPLEX_POW_EQ_0]] THEN
143 ASM_REWRITE_TAC[poly_exp] THEN
144 SUBGOAL_THEN `?k. ~(k = Cx(&0)) /\ (poly p = poly [k])` MP_TAC THENL
145 [SUBST1_TAC(SYM(SPEC `p:complex list` POLY_NORMALIZE)) THEN
146 EXISTS_TAC `LAST(normalize p)` THEN
147 ASM_SIMP_TAC[NORMAL_NORMALIZE; GSYM POLY_NORMALIZE_ZERO] THEN
148 GEN_REWRITE_TAC LAND_CONV [GSYM POLY_NORMALIZE] THEN
149 UNDISCH_TAC `degree p = 0` THEN
150 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
151 [POLY_NORMALIZE_ZERO]) THEN
152 REWRITE_TAC[degree] THEN
153 SPEC_TAC(`normalize p`,`p:complex list`) THEN
154 LIST_INDUCT_TAC THEN REWRITE_TAC[NOT_CONS_NIL] THEN
155 REWRITE_TAC[LENGTH; PRE; poly; LAST] THEN
156 SIMP_TAC[LENGTH_EQ_NIL; POLY_NORMALIZE]; ALL_TAC] THEN
157 DISCH_THEN(X_CHOOSE_THEN `k:complex` STRIP_ASSUME_TAC) THEN
158 ASM_REWRITE_TAC[divides; poly; FUN_EQ_THM; POLY_MUL] THEN
159 ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
160 EXISTS_TAC `[inv(k)]` THEN
161 ASM_REWRITE_TAC[divides; poly; FUN_EQ_THM; POLY_MUL] THEN
162 ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
163 ASM_SIMP_TAC[COMPLEX_MUL_RINV]);;
165 (* ------------------------------------------------------------------------- *)
166 (* Useful lemma I should have proved ages ago. *)
167 (* ------------------------------------------------------------------------- *)
169 let CONSTANT_DEGREE = prove
170 (`!p. constant(poly p) <=> (degree p = 0)`,
171 GEN_TAC THEN REWRITE_TAC[constant] THEN EQ_TAC THENL
172 [DISCH_THEN(ASSUME_TAC o GSYM o SPEC `Cx(&0)`) THEN
173 SUBGOAL_THEN `degree [poly p (Cx(&0))] = 0` MP_TAC THENL
174 [REWRITE_TAC[degree; normalize] THEN
175 COND_CASES_TAC THEN REWRITE_TAC[LENGTH] THEN CONV_TAC NUM_REDUCE_CONV;
177 MATCH_MP_TAC(ARITH_RULE `(x = y) ==> (x = 0) ==> (y = 0)`) THEN
178 MATCH_MP_TAC DEGREE_WELLDEF THEN
179 REWRITE_TAC[FUN_EQ_THM; poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
180 FIRST_ASSUM(ACCEPT_TAC o GSYM);
181 ONCE_REWRITE_TAC[GSYM POLY_NORMALIZE] THEN REWRITE_TAC[degree] THEN
182 SPEC_TAC(`normalize p`,`l:complex list`) THEN
183 MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[poly] THEN
184 SIMP_TAC[LENGTH; PRE; LENGTH_EQ_NIL; poly; COMPLEX_MUL_RZERO]]);;
186 (* ------------------------------------------------------------------------- *)
187 (* It would be nicer to prove this without using algebraic closure... *)
188 (* ------------------------------------------------------------------------- *)
190 let DIVIDES_DEGREE_LEMMA = prove
191 (`!n p q. (degree(p) = n)
192 ==> n <= degree(p ** q) \/ (poly(p ** q) = poly [])`,
193 INDUCT_TAC THEN REWRITE_TAC[LE_0] THEN REPEAT STRIP_TAC THEN
194 MP_TAC(SPEC `p:complex list` FUNDAMENTAL_THEOREM_OF_ALGEBRA) THEN
195 ASM_REWRITE_TAC[CONSTANT_DEGREE; NOT_SUC] THEN
196 DISCH_THEN(X_CHOOSE_THEN `a:complex` MP_TAC) THEN
197 GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
198 DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THENL
199 [REWRITE_TAC[POLY_MUL; poly; COMPLEX_MUL_LZERO; FUN_EQ_THM];
201 DISCH_THEN(X_CHOOSE_THEN `r:complex list` SUBST_ALL_TAC) THEN
202 SUBGOAL_THEN `poly (([--a; Cx (&1)] ** r) ** q) =
203 poly ([--a; Cx (&1)] ** (r ** q))`
205 [REWRITE_TAC[FUN_EQ_THM; POLY_MUL; COMPLEX_MUL_ASSOC]; ALL_TAC] THEN
206 FIRST_ASSUM(SUBST1_TAC o MATCH_MP DEGREE_WELLDEF) THEN
207 ASM_REWRITE_TAC[] THEN
208 MP_TAC(SPECL [`r ** q`; `--a`] LINEAR_MUL_DEGREE) THEN
209 ASM_CASES_TAC `poly (r ** q) = poly []` THENL
210 [REWRITE_TAC[FUN_EQ_THM] THEN
211 ONCE_REWRITE_TAC[POLY_MUL] THEN ASM_REWRITE_TAC[] THEN
212 REWRITE_TAC[poly; COMPLEX_MUL_RZERO]; ALL_TAC] THEN
213 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
214 SUBGOAL_THEN `n <= degree(r ** q) \/ (poly(r ** q) = poly [])` MP_TAC THENL
216 REWRITE_TAC[ARITH_RULE `SUC n <= m + 1 <=> n <= m`] THEN
217 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
218 REWRITE_TAC[FUN_EQ_THM] THEN
219 ONCE_REWRITE_TAC[POLY_MUL] THEN ASM_REWRITE_TAC[] THEN
220 REWRITE_TAC[poly; COMPLEX_MUL_RZERO]] THEN
221 MP_TAC(SPECL [`r:complex list`; `--a`] LINEAR_MUL_DEGREE) THEN ANTS_TAC THENL
222 [UNDISCH_TAC `~(poly (r ** q) = poly [])` THEN
223 REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN
224 SIMP_TAC[poly; FUN_EQ_THM; POLY_MUL; COMPLEX_ENTIRE]; ALL_TAC] THEN
225 DISCH_THEN SUBST_ALL_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
226 UNDISCH_TAC `degree r + 1 = SUC n` THEN ARITH_TAC);;
228 let DIVIDES_DEGREE = prove
229 (`!p q. p divides q ==> degree(p) <= degree(q) \/ (poly q = poly [])`,
230 REPEAT GEN_TAC THEN REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
231 X_GEN_TAC `r:complex list` THEN DISCH_TAC THEN
232 FIRST_ASSUM(SUBST1_TAC o MATCH_MP DEGREE_WELLDEF) THEN ASM_REWRITE_TAC[] THEN
233 ASM_MESON_TAC[DIVIDES_DEGREE_LEMMA]);;
235 (* ------------------------------------------------------------------------- *)
236 (* Arithmetic operations on multivariate polynomials. *)
237 (* ------------------------------------------------------------------------- *)
239 let MPOLY_BASE_CONV =
241 (`Cx(&0) = poly [] x`,
245 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID])
247 (`x = poly [Cx(&0); Cx(&1)] x`,
248 REWRITE_TAC[poly; COMPLEX_ADD_LID; COMPLEX_MUL_RZERO] THEN
249 REWRITE_TAC[COMPLEX_ADD_RID; COMPLEX_MUL_RID])
250 and zero_tm = `Cx(&0)`
251 and c_tm = `c:complex`
252 and x_tm = `x:complex` in
253 let rec MPOLY_BASE_CONV avs tm =
254 if avs = [] then REFL tm
255 else if tm = zero_tm then INST [hd avs,x_tm] pth_0
256 else if tm = hd avs then
257 let th1 = INST [tm,x_tm] pth_var in
260 (COMB2_CONV (RAND_CONV (MPOLY_BASE_CONV (tl avs)))
261 (LAND_CONV (MPOLY_BASE_CONV (tl avs)))))
265 let th1 = MPOLY_BASE_CONV (tl avs) tm in
266 let th2 = INST [hd avs,x_tm; rand(concl th1),c_tm] pth_1 in
270 let MPOLY_NORM_CONV =
272 (`poly [Cx(&0)] x = poly [] x`,
273 REWRITE_TAC[poly; COMPLEX_ADD_RID; COMPLEX_MUL_RZERO])
275 (`poly [poly [] y] x = poly [] x`,
276 REWRITE_TAC[poly; COMPLEX_ADD_RID; COMPLEX_MUL_RZERO]) in
277 let conv_fwd = REWR_CONV(CONJUNCT2 poly)
278 and conv_bck = REWR_CONV(GSYM(CONJUNCT2 poly))
279 and conv_0 = GEN_REWRITE_CONV I [pth_0]
280 and conv_1 = GEN_REWRITE_CONV I [pth_1] in
281 let rec NORM0_CONV tm =
283 (conv_fwd THENC RAND_CONV(RAND_CONV NORM0_CONV) THENC conv_bck THENC
284 TRY_CONV NORM0_CONV)) tm
287 (conv_fwd THENC RAND_CONV(RAND_CONV NORM1_CONV) THENC conv_bck THENC
288 TRY_CONV NORM1_CONV)) tm in
289 fun avs -> TRY_CONV(if avs = [] then NORM0_CONV else NORM1_CONV);;
291 let MPOLY_ADD_CONV,MPOLY_TADD_CONV =
292 let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES))
293 and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)]
294 and add_conv = REWR_CONV(GSYM POLY_ADD) in
295 let rec MPOLY_ADD_CONV avs tm =
296 if avs = [] then COMPLEX_RAT_ADD_CONV tm else
297 (add_conv THENC LAND_CONV(MPOLY_TADD_CONV avs) THENC
298 MPOLY_NORM_CONV (tl avs)) tm
299 and MPOLY_TADD_CONV avs tm =
302 LAND_CONV (MPOLY_ADD_CONV (tl avs)) THENC
303 RAND_CONV (MPOLY_TADD_CONV avs))) tm in
304 MPOLY_ADD_CONV,MPOLY_TADD_CONV;;
306 let MPOLY_CMUL_CONV,MPOLY_TCMUL_CONV,MPOLY_MUL_CONV,MPOLY_TMUL_CONV =
307 let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul]
308 and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul]
309 and cmul_conv = REWR_CONV(GSYM POLY_CMUL)
310 and mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES]
311 and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)]
312 and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)]
313 and mul_conv = REWR_CONV(GSYM POLY_MUL) in
314 let rec MPOLY_CMUL_CONV avs tm =
315 (cmul_conv THENC LAND_CONV(MPOLY_TCMUL_CONV avs)) tm
316 and MPOLY_TCMUL_CONV avs tm =
319 LAND_CONV (MPOLY_MUL_CONV (tl avs)) THENC
320 RAND_CONV (MPOLY_TCMUL_CONV avs))) tm
321 and MPOLY_MUL_CONV avs tm =
322 if avs = [] then COMPLEX_RAT_MUL_CONV tm else
323 (mul_conv THENC LAND_CONV(MPOLY_TMUL_CONV avs)) tm
324 and MPOLY_TMUL_CONV avs tm =
326 (mul_conv1 THENC MPOLY_TCMUL_CONV avs) ORELSEC
328 COMB2_CONV (RAND_CONV(MPOLY_TCMUL_CONV avs))
329 (COMB2_CONV (RAND_CONV(MPOLY_BASE_CONV (tl avs)))
330 (MPOLY_TMUL_CONV avs)) THENC
331 MPOLY_TADD_CONV avs)) tm in
332 MPOLY_CMUL_CONV,MPOLY_TCMUL_CONV,MPOLY_MUL_CONV,MPOLY_TMUL_CONV;;
336 (`(poly p x - poly q x) = (poly p x + Cx(--(&1)) * poly q x)`,
337 SIMPLE_COMPLEX_ARITH_TAC) in
338 let APPLY_PTH_CONV = REWR_CONV pth in
341 RAND_CONV(LAND_CONV (MPOLY_BASE_CONV (tl avs)) THENC
342 MPOLY_CMUL_CONV avs) THENC
346 let cnv_0 = GEN_REWRITE_CONV I [CONJUNCT1 complex_pow]
347 and cnv_1 = GEN_REWRITE_CONV I [CONJUNCT2 complex_pow] in
348 let rec MPOLY_POW_CONV avs tm =
349 try (cnv_0 THENC MPOLY_BASE_CONV avs) tm with Failure _ ->
350 (RAND_CONV num_CONV THENC
351 cnv_1 THENC (RAND_CONV (MPOLY_POW_CONV avs)) THENC
352 MPOLY_MUL_CONV avs) tm in
355 (* ------------------------------------------------------------------------- *)
356 (* Recursive conversion to polynomial form. *)
357 (* ------------------------------------------------------------------------- *)
360 let ELIM_SUB_CONV = REWR_CONV
361 (SIMPLE_COMPLEX_ARITH `x - y = x + Cx(--(&1)) * y`)
362 and ELIM_NEG_CONV = REWR_CONV
363 (SIMPLE_COMPLEX_ARITH `--x = Cx(--(&1)) * x`)
364 and ELIM_POW_0_CONV = GEN_REWRITE_CONV I [CONJUNCT1 complex_pow]
365 and ELIM_POW_1_CONV =
366 RAND_CONV num_CONV THENC GEN_REWRITE_CONV I [CONJUNCT2 complex_pow] in
367 let rec ELIM_POW_CONV tm =
368 (ELIM_POW_0_CONV ORELSEC (ELIM_POW_1_CONV THENC RAND_CONV ELIM_POW_CONV))
370 let polynet = itlist (uncurry net_of_conv)
371 [`x pow n`,(fun cnv avs -> LAND_CONV (cnv avs) THENC MPOLY_POW_CONV avs);
372 `x * y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_MUL_CONV avs);
373 `x + y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_ADD_CONV avs);
374 `x - y`,(fun cnv avs -> BINOP_CONV (cnv avs) THENC MPOLY_SUB_CONV avs);
375 `--x`,(fun cnv avs -> ELIM_NEG_CONV THENC (cnv avs))]
377 let rec POLYNATE_CONV avs tm =
378 try snd(hd(lookup tm polynet)) POLYNATE_CONV avs tm
379 with Failure _ -> MPOLY_BASE_CONV avs tm in
382 (* ------------------------------------------------------------------------- *)
383 (* Cancellation conversion. *)
384 (* ------------------------------------------------------------------------- *)
388 (`(poly p x = Cx(&0)) ==> (poly (CONS (Cx(&0)) p) x = Cx(&0))`,
389 SIMP_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_LID]) in
390 let MATCH_pth = MATCH_MP pth in
392 let th1 = MATCH_pth th in
393 CONV_RULE(funpow 3 LAND_CONV (MPOLY_BASE_CONV (tl avs))) th1;;
395 let POLY_CANCEL_EQ_CONV =
397 (`(p = Cx(&0)) /\ ~(a = Cx(&0))
398 ==> !q b. (q = Cx(&0)) <=> (a * q - b * p = Cx(&0))`,
399 SIMP_TAC[COMPLEX_MUL_RZERO; COMPLEX_SUB_RZERO; COMPLEX_ENTIRE]) in
400 let MATCH_CANCEL_THM = MATCH_MP pth_1 in
401 let rec POLY_CANCEL_EQ_CONV avs n ath eth tm =
402 let m = length(dest_list(lhand(lhand tm))) in
403 if m < n then REFL tm else
404 let th1 = funpow (m - n) (POLY_PAD_RULE avs) eth in
405 let th2 = MATCH_CANCEL_THM (CONJ th1 ath) in
406 let th3 = SPECL [lhs tm; last(dest_list(lhand(lhs tm)))] th2 in
407 let th4 = CONV_RULE(RAND_CONV(LAND_CONV
408 (BINOP_CONV(MPOLY_CMUL_CONV avs)))) th3 in
409 let th5 = CONV_RULE(RAND_CONV(LAND_CONV (MPOLY_SUB_CONV avs))) th4 in
410 TRANS th5 (POLY_CANCEL_EQ_CONV avs n ath eth (rand(concl th5))) in
411 POLY_CANCEL_EQ_CONV;;
415 (`(poly [] x = Cx(&0)) /\
417 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]) in
418 let REWRITE_pth = GEN_REWRITE_CONV LAND_CONV [pth] in
419 let rec RESOLVE_EQ asm tm =
420 try EQT_INTRO(find (fun th -> concl th = tm) asm) with Failure _ ->
421 let tm' = mk_neg tm in
422 try EQF_INTRO(find (fun th -> concl th = tm') asm) with Failure _ ->
423 try let th1 = REWRITE_pth tm in
424 TRANS th1 (RESOLVE_EQ asm (rand(concl th1)))
425 with Failure _ -> COMPLEX_RAT_EQ_CONV tm in
428 let RESOLVE_EQ asm tm =
429 let th = RESOLVE_EQ_RAW asm tm in
430 try EQF_ELIM th with Failure _ -> EQT_ELIM th;;
432 let RESOLVE_EQ_THEN =
433 let MATCH_pth = MATCH_MP
434 (TAUT `(p ==> (q <=> q1)) /\ (~p ==> (q <=> q2))
435 ==> (q <=> (p /\ q1 \/ ~p /\ q2))`) in
436 fun asm tm yfn nfn ->
437 try let th = RESOLVE_EQ asm tm in
438 if is_neg(concl th) then nfn (th::asm) th else yfn (th::asm) th
440 let tm' = mk_neg tm in
441 let yth = DISCH tm (yfn (ASSUME tm :: asm) (ASSUME tm))
442 and nth = DISCH tm' (nfn (ASSUME tm' :: asm) (ASSUME tm')) in
443 MATCH_pth (CONJ yth nth);;
445 let POLY_CANCEL_ENE_CONV avs n ath eth tm =
446 if is_neg tm then RAND_CONV(POLY_CANCEL_EQ_CONV avs n ath eth) tm
447 else POLY_CANCEL_EQ_CONV avs n ath eth tm;;
450 let NEGATE_NEGATE_RULE = GEN_REWRITE_RULE I [TAUT `p <=> (~p <=> F)`] in
452 try let th = RESOLVE_EQ asm (rand tm) in
453 if is_neg(concl th) then EQT_INTRO th
454 else NEGATE_NEGATE_RULE th
455 with Failure _ -> REFL tm;;
457 (* ------------------------------------------------------------------------- *)
458 (* Conversion for division of polynomials. *)
459 (* ------------------------------------------------------------------------- *)
461 let LAST_CONV = GEN_REWRITE_CONV REPEATC [LAST_CLAUSES];;
464 let cnv_0 = GEN_REWRITE_CONV I [CONJUNCT1 LENGTH]
465 and cnv_1 = GEN_REWRITE_CONV I [CONJUNCT2 LENGTH] in
466 let rec LENGTH_CONV tm =
467 try cnv_0 tm with Failure _ ->
468 (cnv_1 THENC RAND_CONV LENGTH_CONV THENC NUM_SUC_CONV) tm in
471 let EXPAND_EX_BETA_CONV =
472 let pth = prove(`EX P [c] = P c`,REWRITE_TAC[EX]) in
473 let cnv_0 = GEN_REWRITE_CONV I [CONJUNCT1 EX]
474 and cnv_1 = GEN_REWRITE_CONV I [pth]
475 and cnv_2 = GEN_REWRITE_CONV I [CONJUNCT2 EX] in
476 let rec EXPAND_EX_BETA_CONV tm =
477 try (cnv_1 THENC BETA_CONV) tm with Failure _ -> try
478 (cnv_2 THENC COMB2_CONV (RAND_CONV BETA_CONV)
479 EXPAND_EX_BETA_CONV) tm
480 with Failure _ -> cnv_0 tm in
481 EXPAND_EX_BETA_CONV;;
483 let POLY_DIVIDES_PAD_RULE =
485 (`p divides q ==> p divides (CONS (Cx(&0)) q)`,
486 REWRITE_TAC[divides; FUN_EQ_THM; POLY_MUL; poly; COMPLEX_ADD_LID] THEN
487 DISCH_THEN(X_CHOOSE_THEN `r:complex list` ASSUME_TAC) THEN
488 EXISTS_TAC `[Cx(&0); Cx(&1)] ** r` THEN
489 ASM_REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_LID; COMPLEX_ADD_RID;
490 COMPLEX_MUL_RID; POLY_MUL] THEN
491 REWRITE_TAC[COMPLEX_MUL_AC]) in
492 let APPLY_pth = MATCH_MP pth in
495 (CONV_RULE(RAND_CONV(LAND_CONV(MPOLY_BASE_CONV (tl avs)))) o APPLY_pth)
496 (SPEC tm POLY_DIVIDES_REFL);;
498 let POLY_DIVIDES_PAD_CONST_RULE =
500 (`p divides q ==> !a. p divides (a ## q)`,
501 REWRITE_TAC[FUN_EQ_THM; divides; POLY_CMUL; POLY_MUL] THEN
502 DISCH_THEN(X_CHOOSE_THEN `r:complex list` ASSUME_TAC) THEN
503 X_GEN_TAC `a:complex` THEN EXISTS_TAC `[a] ** r` THEN
504 ASM_REWRITE_TAC[POLY_MUL; poly] THEN SIMPLE_COMPLEX_ARITH_TAC) in
505 let APPLY_pth = MATCH_MP pth in
507 let th1 = POLY_DIVIDES_PAD_RULE avs n tm in
508 let th2 = SPEC a (APPLY_pth th1) in
509 CONV_RULE(RAND_CONV(MPOLY_TCMUL_CONV avs)) th2;;
511 let EXPAND_EX_BETA_RESOLVE_CONV asm tm =
512 let th1 = EXPAND_EX_BETA_CONV tm in
513 let djs = disjuncts(rand(concl th1)) in
514 let th2 = end_itlist MK_DISJ (map (RESOLVE_NE asm) djs) in
517 let POLY_DIVIDES_CONV =
519 (`LENGTH q < LENGTH p
520 ==> ~(LAST p = Cx(&0))
521 ==> (p divides q <=> ~(EX (\c. ~(c = Cx(&0))) q))`,
522 REPEAT STRIP_TAC THEN REWRITE_TAC[NOT_EX; GSYM POLY_ZERO] THEN EQ_TAC THENL
524 SIMP_TAC[divides; POLY_MUL; FUN_EQ_THM] THEN
525 DISCH_TAC THEN EXISTS_TAC `[]:complex list` THEN
526 REWRITE_TAC[poly; COMPLEX_MUL_RZERO]] THEN
527 DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_DEGREE) THEN
528 MATCH_MP_TAC(TAUT `(~b ==> ~a) ==> (a \/ b ==> b)`) THEN
529 DISCH_TAC THEN REWRITE_TAC[NOT_LE] THEN ASM_SIMP_TAC[NORMAL_DEGREE] THEN
530 REWRITE_TAC[degree] THEN
531 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
532 `lq < lp ==> ~(lq = 0) /\ dq <= lq - 1 ==> dq < lp - 1`)) THEN
533 CONJ_TAC THENL [ASM_MESON_TAC[LENGTH_EQ_NIL]; ALL_TAC] THEN
534 MATCH_MP_TAC(ARITH_RULE `m <= n ==> PRE m <= n - 1`) THEN
535 REWRITE_TAC[LENGTH_NORMALIZE_LE]) in
536 let APPLY_pth0 = PART_MATCH (lhand o rand o rand) pth_0 in
540 ==> (!x. a * poly q x - poly p' x = poly r x)
541 ==> (p divides q <=> p divides r)`,
542 DISCH_TAC THEN REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
543 X_GEN_TAC `t:complex list` THEN DISCH_THEN SUBST1_TAC THEN
544 REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
545 DISCH_THEN(fun th -> REWRITE_TAC[GSYM th]) THEN EQ_TAC THEN
546 DISCH_THEN(X_CHOOSE_THEN `s:complex list` MP_TAC) THENL
547 [DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
548 EXISTS_TAC `a ## s ++ --(Cx(&1)) ## t` THEN
549 REWRITE_TAC[POLY_MUL; POLY_ADD; POLY_CMUL] THEN
550 REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC;
551 REWRITE_TAC[POLY_MUL] THEN DISCH_TAC THEN
552 EXISTS_TAC `[inv(a)] ** (t ++ s)` THEN
553 X_GEN_TAC `z:complex` THEN
554 ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
555 REWRITE_TAC[POLY_MUL; POLY_ADD; GSYM COMPLEX_MUL_ASSOC] THEN
556 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
557 SUBGOAL_THEN `a * poly q z = (poly t z + poly s z) * poly p z`
559 [FIRST_ASSUM(MP_TAC o SPEC `z:complex`) THEN SIMPLE_COMPLEX_ARITH_TAC;
561 DISCH_THEN(MP_TAC o AP_TERM `( * ) (inv a)`) THEN
562 ASM_SIMP_TAC[COMPLEX_MUL_ASSOC; COMPLEX_MUL_LINV; COMPLEX_MUL_LID]]) in
563 let MATCH_pth1 = MATCH_MP pth_1 in
564 let rec DIVIDE_STEP_CONV avs sfn n tm =
565 let m = length(dest_list(rand tm)) in
566 if m < n then REFL tm else
567 let th1 = POLY_DIVIDES_PAD_CONST_RULE avs (m - n)
568 (last(dest_list(rand tm))) (lhand tm) in
569 let th2 = MATCH_MP (sfn tm) th1 in
570 let av,bod = dest_forall(lhand(concl th2)) in
571 let tm1 = vsubst [hd avs,av] (lhand bod) in
572 let th3 = (LAND_CONV (MPOLY_CMUL_CONV avs) THENC MPOLY_SUB_CONV avs) tm1 in
573 let th4 = MATCH_MP th2 (GEN (hd avs) th3) in
574 TRANS th4 (DIVIDE_STEP_CONV avs sfn n (rand(concl th4))) in
575 let zero_tm = `Cx(&0)` in
577 let ath = RESOLVE_EQ asm (mk_eq(last(dest_list(lhand tm)),zero_tm)) in
578 let sfn = PART_MATCH (lhand o rand o rand) (MATCH_pth1 ath)
579 and n = length(dest_list(lhand tm)) in
580 let th1 = DIVIDE_STEP_CONV avs sfn n tm in
581 let th2 = APPLY_pth0 (rand(concl th1)) in
582 let th3 = (BINOP_CONV LENGTH_CONV THENC NUM_LT_CONV) (lhand(concl th2)) in
583 let th4 = MP th2 (EQT_ELIM th3) in
584 let th5 = CONV_RULE(LAND_CONV(RAND_CONV(LAND_CONV LAST_CONV))) th4 in
585 let th6 = TRANS th1 (MP th5 ath) in
586 CONV_RULE(RAND_CONV(RAND_CONV(EXPAND_EX_BETA_RESOLVE_CONV asm))) th6;;
588 (* ------------------------------------------------------------------------- *)
589 (* Apply basic Nullstellensatz principle. *)
590 (* ------------------------------------------------------------------------- *)
592 let BASIC_QUELIM_CONV =
594 (`((?x. (poly p x = Cx(&0)) /\ ~(poly [] x = Cx(&0))) <=> F) /\
595 ((?x. ~(poly [] x = Cx(&0))) <=> F) /\
596 ((?x. ~(poly [c] x = Cx(&0))) <=> ~(c = Cx(&0))) /\
597 ((?x. (poly [] x = Cx(&0))) <=> T) /\
598 ((?x. (poly [c] x = Cx(&0))) <=> (c = Cx(&0)))`,
599 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]) in
600 let APPLY_pth1 = GEN_REWRITE_CONV I [pth_1] in
602 (`~(LAST(CONS a (CONS b p)) = Cx(&0))
603 ==> ((?x. poly (CONS a (CONS b p)) x = Cx(&0)) <=> T)`,
604 REPEAT STRIP_TAC THEN
605 MP_TAC(SPEC `CONS (a:complex) (CONS b p)`
606 FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT) THEN
607 REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
608 REWRITE_TAC[NOT_EXISTS_THM; CONS_11] THEN
609 REPEAT STRIP_TAC THEN
610 SUBGOAL_THEN `~(ALL (\c. c = Cx(&0)) (CONS b p))`
611 (fun th -> MP_TAC th THEN ASM_REWRITE_TAC[]) THEN
612 UNDISCH_TAC `~(LAST (CONS a (CONS b p)) = Cx (&0))` THEN
613 ONCE_REWRITE_TAC[LAST] THEN REWRITE_TAC[NOT_CONS_NIL] THEN
614 REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
615 SPEC_TAC(`p:complex list`,`p:complex list`) THEN
616 LIST_INDUCT_TAC THEN ONCE_REWRITE_TAC[LAST] THEN
617 REWRITE_TAC[ALL; NOT_CONS_NIL] THEN
618 STRIP_TAC THEN FIRST_ASSUM(UNDISCH_TAC o check is_imp o concl) THEN
619 REWRITE_TAC[LAST] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ALL]) in
620 let APPLY_pth2 = PART_MATCH (lhand o rand) pth_2 in
622 (`(?x. ~(poly p x = Cx(&0))) <=> EX (\c. ~(c = Cx(&0))) p`,
623 REWRITE_TAC[GSYM NOT_FORALL_THM] THEN
624 ONCE_REWRITE_TAC[TAUT `(~a <=> b) <=> (a <=> ~b)`] THEN
625 REWRITE_TAC[NOT_EX; GSYM POLY_ZERO; poly; FUN_EQ_THM]) in
626 let APPLY_pth2b = GEN_REWRITE_CONV I [pth_2b] in
628 (`~(LAST(CONS a p) = Cx(&0))
629 ==> ((?x. (poly (CONS a p) x = Cx(&0)) /\ ~(poly q x = Cx(&0))) <=>
630 ~((CONS a p) divides (q exp (LENGTH p))))`,
631 REPEAT STRIP_TAC THEN
632 MP_TAC(SPECL [`CONS (a:complex) p`; `q:complex list`]
633 NULLSTELLENSATZ_UNIVARIATE) THEN
634 ASM_SIMP_TAC[degree; NORMALIZE_EQ; LENGTH; PRE] THEN
635 SUBGOAL_THEN `~(poly (CONS a p) = poly [])`
636 (fun th -> REWRITE_TAC[th] THEN MESON_TAC[]) THEN
637 REWRITE_TAC[POLY_ZERO] THEN POP_ASSUM MP_TAC THEN
638 SPEC_TAC(`p:complex list`,`p:complex list`) THEN
639 REWRITE_TAC[LAST] THEN
640 LIST_INDUCT_TAC THEN REWRITE_TAC[LAST; ALL; NOT_CONS_NIL] THEN
641 POP_ASSUM MP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[ALL] THEN
643 let APPLY_pth3 = PART_MATCH (lhand o rand) pth_3 in
644 let POLY_EXP_DIVIDES_CONV =
646 (`(!x. (poly (q exp n) x = poly r x))
647 ==> (p divides (q exp n) <=> p divides r)`,
648 SIMP_TAC[divides; POLY_EXP; FUN_EQ_THM]) in
649 let APPLY_pth4 = MATCH_MP pth_4
651 and REWR_POLY_EXP_CONV = REWR_CONV POLY_EXP in
652 let POLY_EXP_DIVIDES_CONV avs tm =
653 let tm1 = mk_comb(mk_comb(poly_tm,rand tm),hd avs) in
654 let th1 = REWR_POLY_EXP_CONV tm1 in
655 let th2 = TRANS th1 (MPOLY_POW_CONV avs (rand(concl th1))) in
656 PART_MATCH lhand (APPLY_pth4 (GEN (hd avs) th2)) tm in
657 POLY_EXP_DIVIDES_CONV in
659 try APPLY_pth1 tm with Failure _ ->
660 try let th1 = APPLY_pth2 tm in
661 let th2 = CONV_RULE(LAND_CONV(RAND_CONV(LAND_CONV LAST_CONV))) th1 in
662 let th3 = try MATCH_MP th2 (RESOLVE_EQ asm (rand(lhand(concl th2))))
663 with Failure _ -> failwith "Sanity failure (2a)" in
665 with Failure _ -> try
666 let th1 = APPLY_pth2b tm in
667 TRANS th1 (EXPAND_EX_BETA_RESOLVE_CONV asm (rand(concl th1)))
669 let th1 = APPLY_pth3 tm in
670 let th2 = CONV_RULE(LAND_CONV(RAND_CONV(LAND_CONV LAST_CONV))) th1 in
671 let th3 = try MATCH_MP th2 (RESOLVE_EQ asm (rand(lhand(concl th2))))
672 with Failure _ -> failwith "Sanity failure (2b)" in
673 let th4 = CONV_RULE (funpow 4 RAND_CONV LENGTH_CONV) th3 in
675 CONV_RULE(RAND_CONV(RAND_CONV(POLY_EXP_DIVIDES_CONV avs))) th4 in
676 CONV_RULE(RAND_CONV(RAND_CONV(POLY_DIVIDES_CONV asm avs))) th5;;
678 (* ------------------------------------------------------------------------- *)
679 (* Put into canonical form by multiplying inequalities. *)
680 (* ------------------------------------------------------------------------- *)
682 let POLY_NE_MULT_CONV =
684 (`~(poly p x = Cx(&0)) /\ ~(poly q x = Cx(&0)) <=>
685 ~(poly p x * poly q x = Cx(&0))`,
686 REWRITE_TAC[COMPLEX_ENTIRE; DE_MORGAN_THM]) in
687 let APPLY_pth = REWR_CONV pth in
688 let rec POLY_NE_MULT_CONV avs tm =
689 if not(is_conj tm) then REFL tm else
690 let l,r = dest_conj tm in
691 let th1 = MK_COMB(AP_TERM (rator(rator tm)) (POLY_NE_MULT_CONV avs l),
692 POLY_NE_MULT_CONV avs r) in
693 let th2 = TRANS th1 (APPLY_pth (rand(concl th1))) in
694 CONV_RULE(RAND_CONV(RAND_CONV(LAND_CONV(MPOLY_MUL_CONV avs)))) th2 in
697 let CORE_QUELIM_CONV =
698 let CONJ_AC_RULE = AC CONJ_ACI in
699 let CORE_QUELIM_CONV asm avs tm =
700 let ev,bod = dest_exists tm in
701 let cjs = conjuncts bod in
702 let eqs,neqs = partition is_eq cjs in
704 let th1 = MK_EXISTS ev (POLY_NE_MULT_CONV avs bod) in
705 TRANS th1 (BASIC_QUELIM_CONV asm avs (rand(concl th1)))
706 else if length eqs > 1 then failwith "CORE_QUELIM_CONV: Sanity failure"
707 else if neqs = [] then BASIC_QUELIM_CONV asm avs tm else
708 let tm1 = mk_conj(hd eqs,list_mk_conj neqs) in
709 let th1 = CONJ_AC_RULE(mk_eq(bod,tm1)) in
710 let th2 = CONV_RULE(funpow 2 RAND_CONV(POLY_NE_MULT_CONV avs)) th1 in
711 let th3 = MK_EXISTS ev th2 in
712 TRANS th3 (BASIC_QUELIM_CONV asm avs (rand(concl th3))) in
715 (* ------------------------------------------------------------------------- *)
716 (* Main elimination coversion (for a single quantifier). *)
717 (* ------------------------------------------------------------------------- *)
720 let DNE_RULE = GEN_REWRITE_RULE I
721 [TAUT `((p <=> T) <=> (~p <=> F)) /\ ((p <=> F) <=> (~p <=> T))`] in
723 if is_neg tm then DNE_RULE(RESOLVE_EQ_RAW asm (rand tm))
724 else RESOLVE_EQ_RAW asm tm;;
726 let COMPLEX_QUELIM_CONV =
728 (`((poly [] x = Cx(&0)) <=> T) /\
729 ((poly [] x = Cx(&0)) /\ p <=> p)`,
732 (`(~(poly [] x = Cx(&0)) <=> F) /\
733 (~(poly [] x = Cx(&0)) /\ p <=> F)`,
736 (`(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`,
738 and zero_tm = `Cx(&0)`
740 let ELIM_ZERO_RULE = GEN_REWRITE_RULE RAND_CONV [pth_0]
741 and ELIM_NONZERO_RULE = GEN_REWRITE_RULE RAND_CONV [pth_1]
742 and INCORP_ASSUM_THM = MATCH_MP pth_2
743 and CONJ_AC_RULE = AC CONJ_ACI in
744 let POLY_CONST_CONV =
746 (`((poly [c] x = y) <=> (c = y)) /\
747 (~(poly [c] x = y) <=> ~(c = y))`,
748 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]) in
749 TRY_CONV(GEN_REWRITE_CONV I [pth]) in
750 let EXISTS_TRIV_CONV = REWR_CONV EXISTS_SIMP
751 and EXISTS_PUSH_CONV = REWR_CONV RIGHT_EXISTS_AND_THM
752 and AND_SIMP_CONV = GEN_REWRITE_CONV DEPTH_CONV
753 [TAUT `(p /\ F <=> F) /\ (p /\ T <=> p) /\
754 (F /\ p <=> F) /\ (T /\ p <=> p)`]
755 and RESOLVE_OR_CONST_CONV asm tm =
756 try RESOLVE_EQ_NE asm tm with Failure _ -> POLY_CONST_CONV tm
757 and false_tm = `F` in
758 let rec COMPLEX_QUELIM_CONV asm avs tm =
759 let ev,bod = dest_exists tm in
760 let cjs = conjuncts bod in
761 let cjs_set = setify cjs in
762 if length cjs_set < length cjs then
763 let th1 = CONJ_AC_RULE(mk_eq(bod,list_mk_conj cjs_set)) in
764 let th2 = MK_EXISTS ev th1 in
765 TRANS th2 (COMPLEX_QUELIM_CONV asm avs (rand(concl th2)))
767 let eqs,neqs = partition is_eq cjs in
768 let lens = map (length o dest_list o lhand o lhs) eqs
769 and nens = map (length o dest_list o lhand o lhs o rand) neqs in
770 try let zeq = el (index 0 lens) eqs in
771 if cjs = [zeq] then BASIC_QUELIM_CONV asm avs tm else
772 let cjs' = zeq::(subtract cjs [zeq]) in
773 let th1 = ELIM_ZERO_RULE(CONJ_AC_RULE(mk_eq(bod,list_mk_conj cjs'))) in
774 let th2 = MK_EXISTS ev th1 in
775 TRANS th2 (COMPLEX_QUELIM_CONV asm avs (rand(concl th2)))
776 with Failure _ -> try
777 let zne = el (index 0 nens) neqs in
778 if cjs = [zne] then BASIC_QUELIM_CONV asm avs tm else
779 let cjs' = zne::(subtract cjs [zne]) in
780 let th1 = ELIM_NONZERO_RULE
781 (CONJ_AC_RULE(mk_eq(bod,list_mk_conj cjs'))) in
782 CONV_RULE (RAND_CONV EXISTS_TRIV_CONV) (MK_EXISTS ev th1)
783 with Failure _ -> try
784 let ones = map snd (filter (fun (n,_) -> n = 1)
785 (zip lens eqs @ zip nens neqs)) in
786 if ones = [] then failwith "" else
787 let cjs' = subtract cjs ones in
789 let th1 = MK_EXISTS ev (SUBS_CONV(map POLY_CONST_CONV cjs) bod) in
790 TRANS th1 (EXISTS_TRIV_CONV (rand(concl th1)))
792 let tha = SUBS_CONV (map (RESOLVE_OR_CONST_CONV asm) ones)
793 (list_mk_conj ones) in
794 let thb = CONV_RULE (RAND_CONV AND_SIMP_CONV) tha in
795 if rand(concl thb) = false_tm then
796 let thc = MK_CONJ thb (REFL(list_mk_conj cjs')) in
797 let thd = CONV_RULE(RAND_CONV AND_SIMP_CONV) thc in
798 let the = CONJ_AC_RULE(mk_eq(bod,lhand(concl thd))) in
799 let thf = MK_EXISTS ev (TRANS the thd) in
800 CONV_RULE(RAND_CONV EXISTS_TRIV_CONV) thf
802 let thc = MK_CONJ thb (REFL(list_mk_conj cjs')) in
803 let thd = CONJ_AC_RULE(mk_eq(bod,lhand(concl thc))) in
804 let the = MK_EXISTS ev (TRANS thd thc) in
805 let th4 = TRANS the(EXISTS_PUSH_CONV(rand(concl the))) in
806 let tm4 = rand(concl th4) in
807 let th5 = COMPLEX_QUELIM_CONV asm avs (rand tm4) in
808 TRANS th4 (AP_TERM (rator tm4) th5)
812 (let ceq = mk_eq(last(dest_list(lhand(lhs(hd eqs)))),zero_tm) in
813 try concl(RESOLVE_EQ asm ceq) = mk_neg ceq with Failure _ -> false) &
814 (let h = hd lens in forall (fun n -> n < h) nens))
816 CORE_QUELIM_CONV asm avs tm
818 let n = end_itlist min lens in
819 let eq = el (index n lens) eqs in
820 let pol = lhand(lhand eq) in
821 let atm = last(dest_list pol) in
822 let zeq = mk_eq(atm,zero_tm) in
823 RESOLVE_EQ_THEN asm zeq
825 let th0 = TRANS yth (MPOLY_BASE_CONV (tl avs) zero_tm) in
828 (LAND_CONV o LAND_CONV o funpow (n - 1) RAND_CONV o LAND_CONV)
830 let th2 = LAND_CONV(MPOLY_NORM_CONV avs) (rand(concl th1)) in
831 let th3 = MK_EXISTS ev (SUBS_CONV[TRANS th1 th2] bod) in
832 TRANS th3 (COMPLEX_QUELIM_CONV asm' avs (rand(concl th3))))
834 let oth = subtract cjs [eq] in
835 if oth = [] then COMPLEX_QUELIM_CONV asm' avs tm else
836 let eth = ASSUME eq in
837 let ths = map (POLY_CANCEL_ENE_CONV avs n nth eth) oth in
838 let th1 = DISCH eq (end_itlist MK_CONJ ths) in
839 let th2 = INCORP_ASSUM_THM th1 in
840 let th3 = TRANS (CONJ_AC_RULE(mk_eq(bod,lhand(concl th2)))) th2 in
841 let th4 = MK_EXISTS ev th3 in
842 TRANS th4 (COMPLEX_QUELIM_CONV asm' avs (rand(concl th4)))) in
843 fun asm avs -> time(COMPLEX_QUELIM_CONV asm avs);;
845 (* ------------------------------------------------------------------------- *)
846 (* NNF conversion doing "conditionals" ~(p /\ q \/ ~p /\ r) intelligently. *)
847 (* ------------------------------------------------------------------------- *)
850 let NOT_EXISTS_UNIQUE_THM = prove
851 (`~(?!x. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`,
852 REWRITE_TAC[EXISTS_UNIQUE_THM; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
853 REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; CONJ_ASSOC]) in
856 TAUT `~(p /\ q) <=> ~p \/ ~q`;
857 TAUT `~(p \/ q) <=> ~p /\ ~q`;
858 TAUT `~(p ==> q) <=> p /\ ~q`;
859 TAUT `p ==> q <=> ~p \/ q`;
863 NOT_EXISTS_UNIQUE_THM;
864 TAUT `~(p <=> q) <=> (p /\ ~q) \/ (~p /\ q)`;
865 TAUT `(p <=> q) <=> (p /\ q) \/ (~p /\ ~q)`;
866 TAUT `~(p /\ q \/ ~p /\ r) <=> p /\ ~q \/ ~p /\ ~r`] in
867 GEN_REWRITE_CONV TOP_SWEEP_CONV tauts;;
869 (* ------------------------------------------------------------------------- *)
870 (* Overall procedure for multiple quantifiers in any first order formula. *)
871 (* ------------------------------------------------------------------------- *)
873 let FULL_COMPLEX_QUELIM_CONV =
874 let ELIM_FORALL_CONV =
875 let pth = prove(`(!x. P x) <=> ~(?x. ~(P x))`,MESON_TAC[]) in
878 let pth = SIMPLE_COMPLEX_ARITH `(x = y) <=> (x - y = Cx(&0))`
879 and zero_tm = `Cx(&0)` in
880 let REWR_pth = REWR_CONV pth in
882 if rand tm = zero_tm then LAND_CONV(POLYNATE_CONV avs) tm
883 else (REWR_pth THENC LAND_CONV(POLYNATE_CONV avs)) tm in
885 GEN_REWRITE_CONV TOP_DEPTH_CONV (basic_rewrites()) THENC
886 NNF_COND_CONV THENC DNF_CONV in
887 let DISTRIB_EXISTS_CONV = GEN_REWRITE_CONV I [EXISTS_OR_THM] in
888 let TRIV_EXISTS_CONV = GEN_REWRITE_CONV I [EXISTS_SIMP] in
889 let complex_ty = `:complex` in
890 let FINAL_SIMP_CONV =
891 GEN_REWRITE_CONV DEPTH_CONV [CX_INJ] THENC
892 REAL_RAT_REDUCE_CONV THENC
893 GEN_REWRITE_CONV TOP_DEPTH_CONV (basic_rewrites()) in
894 let rec FULL_COMPLEX_QUELIM_CONV avs tm =
896 let th1 = ELIM_FORALL_CONV tm in
897 let th2 = FULL_COMPLEX_QUELIM_CONV avs (rand(concl th1)) in
899 else if is_neg tm then
900 AP_TERM (rator tm) (FULL_COMPLEX_QUELIM_CONV avs (rand tm))
901 else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
902 let lop,r = dest_comb tm in
903 let op,l = dest_comb lop in
904 let thl = FULL_COMPLEX_QUELIM_CONV avs l
905 and thr = FULL_COMPLEX_QUELIM_CONV avs r in
906 MK_COMB(AP_TERM(rator(rator tm)) thl,thr)
907 else if is_exists tm then
908 let ev,bod = dest_exists tm in
909 let th0 = FULL_COMPLEX_QUELIM_CONV (ev::avs) bod in
910 let th1 = MK_EXISTS ev (CONV_RULE(RAND_CONV SIMP_DNF_CONV) th0) in
911 TRANS th1 (DISTRIB_AND_COMPLEX_QUELIM_CONV (ev::avs) (rand(concl th1)))
912 else if is_eq tm then
914 else failwith "unexpected type of formula"
915 and DISTRIB_AND_COMPLEX_QUELIM_CONV avs tm =
916 try TRIV_EXISTS_CONV tm
917 with Failure _ -> try
918 (DISTRIB_EXISTS_CONV THENC
919 BINOP_CONV (DISTRIB_AND_COMPLEX_QUELIM_CONV avs)) tm
920 with Failure _ -> COMPLEX_QUELIM_CONV [] avs tm in
922 let avs = filter (fun t -> type_of t = complex_ty) (frees tm) in
923 (FULL_COMPLEX_QUELIM_CONV avs THENC FINAL_SIMP_CONV) tm;;