Complex/quelim.ml

   1 (* ========================================================================= *)
   2 (* Naive quantifier elimination for complex numbers.                         *)
   3 (* ========================================================================= *)
   4
   5 needs "Complex/fundamental.ml";;
   6
   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
  14    [ALL_TAC;
  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];
  44     ALL_TAC] THEN
  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
  79    [EXPAND_TAC "n" THEN
  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;
  83     ALL_TAC] THEN
  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
  88     UNDISCH_TAC
  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];
 106     ALL_TAC] THEN
 107   REWRITE_TAC[divides] THEN
 108   DISCH_THEN(X_CHOOSE_THEN `u:complex list` ASSUME_TAC) THEN
 109   EXISTS_TAC
 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]);;
 121
 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
 134    [ALL_TAC;
 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
 138     DISCH_THEN(fun th ->
 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]);;
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* Useful lemma I should have proved ages ago.                               *)
 167 (* ------------------------------------------------------------------------- *)
 168
 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;
 176       ALL_TAC] THEN
 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]]);;
 185
 186 (* ------------------------------------------------------------------------- *)
 187 (* It would be nicer to prove this without using algebraic closure...        *)
 188 (* ------------------------------------------------------------------------- *)
 189
 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];
 200     ALL_TAC] THEN
 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))`
 204   ASSUME_TAC THENL
 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
 215    [ALL_TAC;
 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);;
 227
 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]);;
 234
 235 (* ------------------------------------------------------------------------- *)
 236 (* Arithmetic operations on multivariate polynomials.                        *)
 237 (* ------------------------------------------------------------------------- *)
 238
 239 let MPOLY_BASE_CONV =
 240   let pth_0 = prove
 241    (`Cx(&0) = poly [] x`,
 242     REWRITE_TAC[poly])
 243   and pth_1 = prove
 244    (`c = poly [c] x`,
 245     REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID])
 246   and pth_var = prove
 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
 258       let th2 =
 259         (LAND_CONV
 260           (COMB2_CONV (RAND_CONV (MPOLY_BASE_CONV (tl avs)))
 261                       (LAND_CONV (MPOLY_BASE_CONV (tl avs)))))
 262         (rand(concl th1)) in
 263       TRANS th1 th2
 264     else
 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
 267       TRANS th1 th2 in
 268   MPOLY_BASE_CONV;;
 269
 270 let MPOLY_NORM_CONV =
 271   let pth_0 = prove
 272    (`poly [Cx(&0)] x = poly [] x`,
 273     REWRITE_TAC[poly; COMPLEX_ADD_RID; COMPLEX_MUL_RZERO])
 274   and pth_1 = prove
 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 =
 282    (conv_0 ORELSEC
 283     (conv_fwd THENC RAND_CONV(RAND_CONV NORM0_CONV) THENC conv_bck THENC
 284      TRY_CONV NORM0_CONV)) tm
 285   and NORM1_CONV tm =
 286    (conv_1 ORELSEC
 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);;
 290
 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 =
 300     (add_conv0 ORELSEC
 301       (add_conv1 THENC
 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;;
 305
 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 =
 317     (cmul_conv0 ORELSEC
 318       (cmul_conv1 THENC
 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 =
 325     (mul_conv0 ORELSEC
 326      (mul_conv1 THENC MPOLY_TCMUL_CONV avs) ORELSEC
 327      (mul_conv2 THENC
 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;;
 333
 334 let MPOLY_SUB_CONV =
 335   let pth = prove
 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
 339   fun avs ->
 340      APPLY_PTH_CONV THENC
 341      RAND_CONV(LAND_CONV (MPOLY_BASE_CONV (tl avs)) THENC
 342                MPOLY_CMUL_CONV avs) THENC
 343      MPOLY_ADD_CONV avs;;
 344
 345 let MPOLY_POW_CONV =
 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
 353   MPOLY_POW_CONV;;
 354
 355 (* ------------------------------------------------------------------------- *)
 356 (* Recursive conversion to polynomial form.                                  *)
 357 (* ------------------------------------------------------------------------- *)
 358
 359 let POLYNATE_CONV =
 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))
 369     tm in
 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))]
 376     empty_net in
 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
 380   POLYNATE_CONV;;
 381
 382 (* ------------------------------------------------------------------------- *)
 383 (* Cancellation conversion.                                                  *)
 384 (* ------------------------------------------------------------------------- *)
 385
 386 let POLY_PAD_RULE =
 387   let pth = prove
 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
 391   fun avs th ->
 392      let th1 = MATCH_pth th in
 393      CONV_RULE(funpow 3 LAND_CONV (MPOLY_BASE_CONV (tl avs))) th1;;
 394
 395 let POLY_CANCEL_EQ_CONV =
 396   let pth_1 = prove
 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;;
 412
 413 let RESOLVE_EQ_RAW =
 414   let pth = prove
 415    (`(poly [] x = Cx(&0)) /\
 416      (poly [c] x = c)`,
 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
 426   RESOLVE_EQ;;
 427
 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;;
 431
 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
 439     with Failure _ ->
 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);;
 444
 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;;
 448
 449 let RESOLVE_NE =
 450   let NEGATE_NEGATE_RULE = GEN_REWRITE_RULE I [TAUT `p <=> (~p <=> F)`] in
 451   fun asm tm ->
 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;;
 456
 457 (* ------------------------------------------------------------------------- *)
 458 (* Conversion for division of polynomials.                                   *)
 459 (* ------------------------------------------------------------------------- *)
 460
 461 let LAST_CONV = GEN_REWRITE_CONV REPEATC [LAST_CLAUSES];;
 462
 463 let LENGTH_CONV =
 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
 469   LENGTH_CONV;;
 470
 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;;
 482
 483 let POLY_DIVIDES_PAD_RULE =
 484   let pth = prove
 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
 493   fun avs n tm ->
 494     funpow n
 495      (CONV_RULE(RAND_CONV(LAND_CONV(MPOLY_BASE_CONV (tl avs)))) o APPLY_pth)
 496      (SPEC tm POLY_DIVIDES_REFL);;
 497
 498 let POLY_DIVIDES_PAD_CONST_RULE =
 499   let pth = prove
 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
 506   fun avs n a tm ->
 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;;
 510
 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
 515   TRANS th1 th2;;
 516
 517 let POLY_DIVIDES_CONV =
 518   let pth_0 = prove
 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
 523      [ALL_TAC;
 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
 537   let pth_1 = prove
 538    (`~(a = Cx(&0))
 539      ==> p divides p'
 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`
 558       MP_TAC THENL
 559        [FIRST_ASSUM(MP_TAC o SPEC `z:complex`) THEN SIMPLE_COMPLEX_ARITH_TAC;
 560         ALL_TAC] THEN
 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
 576   fun asm avs tm ->
 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;;
 587
 588 (* ------------------------------------------------------------------------- *)
 589 (* Apply basic Nullstellensatz principle.                                    *)
 590 (* ------------------------------------------------------------------------- *)
 591
 592 let BASIC_QUELIM_CONV =
 593   let pth_1 = prove
 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
 601   let pth_2 = prove
 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
 621   let pth_2b = prove
 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
 627   let pth_3 = prove
 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
 642     CONV_TAC TAUT) in
 643   let APPLY_pth3 = PART_MATCH (lhand o rand) pth_3 in
 644   let POLY_EXP_DIVIDES_CONV =
 645     let pth_4 = prove
 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
 650     and poly_tm = `poly`
 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
 658   fun asm avs tm ->
 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
 664         th3
 665     with Failure _ -> try
 666         let th1 = APPLY_pth2b tm in
 667         TRANS th1 (EXPAND_EX_BETA_RESOLVE_CONV asm (rand(concl th1)))
 668     with Failure _ ->
 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
 674         let th5 =
 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;;
 677
 678 (* ------------------------------------------------------------------------- *)
 679 (* Put into canonical form by multiplying inequalities.                      *)
 680 (* ------------------------------------------------------------------------- *)
 681
 682 let POLY_NE_MULT_CONV =
 683   let pth = prove
 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
 695   POLY_NE_MULT_CONV;;
 696
 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
 703     if eqs = [] then
 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
 713   CORE_QUELIM_CONV;;
 714
 715 (* ------------------------------------------------------------------------- *)
 716 (* Main elimination coversion (for a single quantifier).                     *)
 717 (* ------------------------------------------------------------------------- *)
 718
 719 let RESOLVE_EQ_NE =
 720   let DNE_RULE = GEN_REWRITE_RULE I
 721    [TAUT `((p <=> T) <=> (~p <=> F)) /\ ((p <=> F) <=> (~p <=> T))`] in
 722   fun asm tm ->
 723     if is_neg tm then DNE_RULE(RESOLVE_EQ_RAW asm (rand tm))
 724     else RESOLVE_EQ_RAW asm tm;;
 725
 726 let COMPLEX_QUELIM_CONV =
 727   let pth_0 = prove
 728    (`((poly [] x = Cx(&0)) <=> T) /\
 729      ((poly [] x = Cx(&0)) /\ p <=> p)`,
 730     REWRITE_TAC[poly])
 731   and pth_1 = prove
 732    (`(~(poly [] x = Cx(&0)) <=> F) /\
 733      (~(poly [] x = Cx(&0)) /\ p <=> F)`,
 734     REWRITE_TAC[poly])
 735   and pth_2 = prove
 736    (`(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`,
 737     CONV_TAC TAUT)
 738   and zero_tm = `Cx(&0)`
 739   and true_tm = `T` in
 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 =
 745     let pth = prove
 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)))
 766     else
 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
 788         if cjs' = [] then
 789           let th1 = MK_EXISTS ev (SUBS_CONV(map POLY_CONST_CONV cjs) bod) in
 790           TRANS th1 (EXISTS_TRIV_CONV (rand(concl th1)))
 791         else
 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
 801           else
 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)
 809     with Failure _ ->
 810     if eqs = [] or
 811        (length eqs = 1 &
 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))
 815     then
 816       CORE_QUELIM_CONV asm avs tm
 817     else
 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
 824        (fun asm' yth ->
 825           let th0 = TRANS yth (MPOLY_BASE_CONV (tl avs) zero_tm) in
 826           let th1 =
 827             GEN_REWRITE_CONV
 828              (LAND_CONV o LAND_CONV o funpow (n - 1) RAND_CONV o LAND_CONV)
 829              [th0] eq in
 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))))
 833        (fun asm' nth ->
 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);;
 844
 845 (* ------------------------------------------------------------------------- *)
 846 (* NNF conversion doing "conditionals" ~(p /\ q \/ ~p /\ r) intelligently.   *)
 847 (* ------------------------------------------------------------------------- *)
 848
 849 let NNF_COND_CONV =
 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
 854   let tauts =
 855     [TAUT `~(~p) <=> p`;
 856      TAUT `~(p /\ q) <=> ~p \/ ~q`;
 857      TAUT `~(p \/ q) <=> ~p /\ ~q`;
 858      TAUT `~(p ==> q) <=> p /\ ~q`;
 859      TAUT `p ==> q <=> ~p \/ q`;
 860      NOT_FORALL_THM;
 861      NOT_EXISTS_THM;
 862      EXISTS_UNIQUE_THM;
 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;;
 868
 869 (* ------------------------------------------------------------------------- *)
 870 (* Overall procedure for multiple quantifiers in any first order formula.    *)
 871 (* ------------------------------------------------------------------------- *)
 872
 873 let FULL_COMPLEX_QUELIM_CONV =
 874   let ELIM_FORALL_CONV =
 875     let pth = prove(`(!x. P x) <=> ~(?x. ~(P x))`,MESON_TAC[]) in
 876     REWR_CONV pth in
 877   let ELIM_EQ_CONV =
 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
 881     fun avs tm ->
 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
 884   let SIMP_DNF_CONV =
 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 =
 895      if is_forall tm then
 896         let th1 = ELIM_FORALL_CONV tm in
 897         let th2 = FULL_COMPLEX_QUELIM_CONV avs (rand(concl th1)) in
 898         TRANS th1 th2
 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
 913         ELIM_EQ_CONV avs tm
 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
 921   fun tm ->
 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;;