Complex/fundamental.ml

   1 (* ========================================================================= *)
   2 (* Fundamental theorem of algebra.                                           *)
   3 (* ========================================================================= *)
   4
   5 needs "Complex/complex_transc.ml";;
   6 needs "Complex/cpoly.ml";;
   7
   8 prioritize_complex();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* A cute trick to reduce magnitude of unimodular number.                    *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let SQRT_SOS_LT_1 = prove
  15  (`!x y. sqrt(x pow 2 + y pow 2) < &1 <=> x pow 2 + y pow 2 < &1`,
  16   REPEAT GEN_TAC THEN
  17   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN
  18   REWRITE_TAC[REAL_POW_2] THEN
  19   SIMP_TAC[SQRT_MONO_LT_EQ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
  20
  21 let SQRT_SOS_EQ_1 = prove
  22  (`!x y. (sqrt(x pow 2 + y pow 2) = &1) <=> (x pow 2 + y pow 2 = &1)`,
  23   REPEAT GEN_TAC THEN
  24   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN
  25   REWRITE_TAC[REAL_POW_2] THEN
  26   SIMP_TAC[SQRT_INJ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
  27
  28 let UNIMODULAR_REDUCE_NORM = prove
  29  (`!z. (norm(z) = &1)
  30        ==> norm(z + Cx(&1)) < &1 \/
  31            norm(z - Cx(&1)) < &1 \/
  32            norm(z + ii) < &1 \/
  33            norm(z - ii) < &1`,
  34   GEN_TAC THEN
  35   REWRITE_TAC[ii; CX_DEF; complex_add; complex_sub; complex_neg; complex_norm;
  36         RE; IM; REAL_ADD_RID; REAL_NEG_0; SQRT_SOS_LT_1; SQRT_SOS_EQ_1] THEN
  37   SIMP_TAC[REAL_POW_2;
  38            REAL_ARITH `a * a + (b + c) * (b + c) =
  39                        (a * a + b * b) + (&2 * b * c + c * c)`;
  40            REAL_ARITH `(b + c) * (b + c) + a * a =
  41                        (b * b + a * a) + (&2 * b * c + c * c)`] THEN
  42   DISCH_TAC THEN REWRITE_TAC[REAL_ARITH `&1 + x < &1 <=> &0 < --x`] THEN
  43   REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
  44   REWRITE_TAC[REAL_MUL_RID] THEN
  45   MATCH_MP_TAC(REAL_ARITH
  46     `~(abs(a) <= &1 /\ abs(b) <= &1)
  47      ==> &0 < --a + --(&1) \/ &0 < a + --(&1) \/
  48          &0 < --b + --(&1) \/ &0 < b + --(&1)`) THEN
  49   STRIP_TAC THEN UNDISCH_TAC `Re z * Re z + Im z * Im z = &1` THEN
  50   REWRITE_TAC[] THEN
  51   MATCH_MP_TAC(REAL_ARITH
  52    `(&2 * r) * (&2 * r) <= &1 /\ (&2 * i) * (&2 * i) <= &1
  53     ==> ~(r * r + i * i = &1)`) THEN
  54   REWRITE_TAC[GSYM REAL_POW_2] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
  55   ASM_SIMP_TAC[REAL_POW_1_LE; REAL_ABS_POS]);;
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* Hence we can always reduce modulus of 1 + b z^n if nonzero                *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61 let REDUCE_POLY_SIMPLE = prove
  62  (`!b n. ~(b = Cx(&0)) /\ ~(n = 0)
  63          ==> ?z. norm(Cx(&1) + b * z pow n) < &1`,
  64   GEN_TAC THEN MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
  65   ASM_CASES_TAC `EVEN(n)` THENL
  66    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
  67     DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
  68     FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
  69     ASM_SIMP_TAC[ARITH_RULE `~(2 * m = 0) ==> m < 2 * m /\ ~(m = 0)`] THEN
  70     DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN EXISTS_TAC `csqrt w` THEN
  71     ASM_REWRITE_TAC[GSYM COMPLEX_POW_POW; CSQRT]; ALL_TAC] THEN
  72   MP_TAC(SPEC `Cx(norm b) / b` UNIMODULAR_REDUCE_NORM) THEN ANTS_TAC THENL
  73    [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX] THEN
  74     ASM_SIMP_TAC[COMPLEX_ABS_NORM; REAL_DIV_REFL; COMPLEX_NORM_ZERO];
  75     ALL_TAC] THEN DISCH_TAC THEN
  76   SUBGOAL_THEN `?v. norm(Cx(norm b) / b + v pow n) < &1` MP_TAC THENL
  77    [SUBGOAL_THEN `(Cx(&1) pow n = Cx(&1)) /\
  78                   (--Cx(&1) pow n = --Cx(&1)) /\
  79                   (((ii pow n = ii) /\ (--ii pow n = --ii)) \/
  80                    ((ii pow n = --ii) /\ (--ii pow n = ii)))`
  81     MP_TAC THENL
  82      [ALL_TAC;
  83       RULE_ASSUM_TAC(REWRITE_RULE[complex_sub]) THEN ASM_MESON_TAC[]] THEN
  84     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN
  85     SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
  86     X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN
  87     REWRITE_TAC[complex_pow; COMPLEX_POW_NEG; EVEN; EVEN_MULT; ARITH_EVEN] THEN
  88     REWRITE_TAC[GSYM COMPLEX_POW_POW] THEN
  89     REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_POW_II_2; COMPLEX_MUL_LID;
  90                 COMPLEX_POW_NEG] THEN
  91     COND_CASES_TAC THEN
  92     REWRITE_TAC[COMPLEX_MUL_RID; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG];
  93     ALL_TAC] THEN
  94   DISCH_THEN(X_CHOOSE_THEN `v:complex` ASSUME_TAC) THEN
  95   EXISTS_TAC `v / Cx(root(n) (norm b))` THEN
  96   REWRITE_TAC[COMPLEX_POW_DIV; GSYM CX_POW] THEN
  97   SUBGOAL_THEN `root n (norm b) pow n = norm b` SUBST1_TAC THENL
  98    [UNDISCH_TAC `~(EVEN n)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
  99     INDUCT_TAC THEN SIMP_TAC[EVEN; ROOT_POW_POS; COMPLEX_NORM_POS];
 100     ALL_TAC] THEN
 101   MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `norm(Cx(norm b) / b)` THEN
 102   REWRITE_TAC[GSYM COMPLEX_NORM_MUL; COMPLEX_ADD_LDISTRIB] THEN
 103   REWRITE_TAC[COMPLEX_MUL_RID; REAL_MUL_RID] THEN
 104   SUBGOAL_THEN `norm(Cx(norm b) / b) = &1` SUBST1_TAC THENL
 105    [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX; COMPLEX_ABS_NORM] THEN
 106     ASM_SIMP_TAC[REAL_DIV_REFL; COMPLEX_NORM_ZERO]; ALL_TAC] THEN
 107   REWRITE_TAC[REAL_LT_01; complex_div] THEN
 108   ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC
 109    `(m * b') * b * p * m' = (m * m') * (b * b') * p`] THEN
 110   ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_LID;
 111                CX_INJ; COMPLEX_NORM_ZERO] THEN
 112   ASM_REWRITE_TAC[GSYM complex_div]);;
 113
 114 (* ------------------------------------------------------------------------- *)
 115 (* Basic lemmas about polynomials.                                           *)
 116 (* ------------------------------------------------------------------------- *)
 117
 118 let POLY_CMUL_MAP = prove
 119  (`!p c x. poly (MAP (( * ) c) p) x = c * poly p x`,
 120   LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; poly; COMPLEX_MUL_RZERO] THEN
 121   ASM_REWRITE_TAC[COMPLEX_ADD_LDISTRIB] THEN REWRITE_TAC[COMPLEX_MUL_AC]);;
 122
 123 let POLY_0 = prove
 124  (`!p x. ALL (\b. b = Cx(&0)) p ==> (poly p x = Cx(&0))`,
 125   LIST_INDUCT_TAC THEN
 126   ASM_SIMP_TAC[ALL; poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]);;
 127
 128 let POLY_BOUND_EXISTS = prove
 129  (`!p r. ?m. &0 < m /\ !z. norm(z) <= r ==> norm(poly p z) <= m`,
 130   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
 131   LIST_INDUCT_TAC THENL
 132    [EXISTS_TAC `&1` THEN REWRITE_TAC[poly; COMPLEX_NORM_CX] THEN
 133     REWRITE_TAC[REAL_ABS_NUM; REAL_LT_01; REAL_POS]; ALL_TAC] THEN
 134   POP_ASSUM(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
 135   EXISTS_TAC `&1 + norm(h) + abs(r * m)` THEN
 136   ASM_SIMP_TAC[REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 < &1 + x + y`;
 137                REAL_ABS_POS; COMPLEX_NORM_POS] THEN
 138   X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
 139   REWRITE_TAC[poly] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
 140   EXISTS_TAC `norm(h) + norm(z * poly t z)` THEN
 141   REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN
 142   MATCH_MP_TAC(REAL_ARITH `y <= z ==> x + y <= &1 + x + abs(z)`) THEN
 143   REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
 144   ASM_SIMP_TAC[COMPLEX_NORM_POS]);;
 145
 146 (* ------------------------------------------------------------------------- *)
 147 (* Offsetting the variable in a polynomial gives another of same degree.     *)
 148 (* ------------------------------------------------------------------------- *)
 149
 150 let POLY_OFFSET_LEMMA = prove
 151  (`!a p. ?b q. (LENGTH q = LENGTH p) /\
 152                !x. poly (CONS b q) x = (a + x) * poly p x`,
 153   GEN_TAC THEN LIST_INDUCT_TAC THENL
 154    [EXISTS_TAC `Cx(&0)` THEN EXISTS_TAC `[]:complex list` THEN
 155     REWRITE_TAC[poly; LENGTH; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID];
 156     ALL_TAC] THEN
 157   POP_ASSUM STRIP_ASSUME_TAC THEN
 158   EXISTS_TAC `a * h` THEN EXISTS_TAC `CONS (b + h) q` THEN
 159   ASM_REWRITE_TAC[LENGTH; poly] THEN X_GEN_TAC `x:complex ` THEN
 160   FIRST_ASSUM(MP_TAC o SPEC `x:complex`) THEN
 161   REWRITE_TAC[poly] THEN DISCH_THEN(MP_TAC o AP_TERM `( * ) x`) THEN
 162   SIMPLE_COMPLEX_ARITH_TAC);;
 163
 164 let POLY_OFFSET = prove
 165  (`!a p. ?q. (LENGTH q = LENGTH p) /\ !x. poly q x = poly p (a + x)`,
 166   GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; poly] THENL
 167    [EXISTS_TAC `[]:complex list` THEN REWRITE_TAC[poly; LENGTH]; ALL_TAC] THEN
 168   POP_ASSUM(X_CHOOSE_THEN `p:complex list` (STRIP_ASSUME_TAC o GSYM)) THEN
 169   ASM_REWRITE_TAC[] THEN
 170   MP_TAC(SPECL [`a:complex`; `p:complex list`] POLY_OFFSET_LEMMA) THEN
 171   DISCH_THEN(X_CHOOSE_THEN `b:complex` (X_CHOOSE_THEN `r: complex list`
 172         (STRIP_ASSUME_TAC o GSYM))) THEN
 173   EXISTS_TAC `CONS (h + b) r` THEN ASM_REWRITE_TAC[LENGTH] THEN
 174   REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 175
 176 (* ------------------------------------------------------------------------- *)
 177 (* Bolzano-Weierstrass type property for closed disc in complex plane.       *)
 178 (* ------------------------------------------------------------------------- *)
 179
 180 let METRIC_BOUND_LEMMA = prove
 181  (`!x y. norm(x - y) <= abs(Re(x) - Re(y)) + abs(Im(x) - Im(y))`,
 182   REPEAT GEN_TAC THEN REWRITE_TAC[complex_norm] THEN
 183   MATCH_MP_TAC(REAL_ARITH
 184    `a <= abs(abs x + abs y) ==> a <= abs x + abs y`) THEN
 185   GEN_REWRITE_TAC RAND_CONV [GSYM POW_2_SQRT_ABS] THEN
 186   MATCH_MP_TAC SQRT_MONO_LE THEN
 187   SIMP_TAC[REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
 188   REWRITE_TAC[complex_add; complex_sub; complex_neg; RE; IM] THEN
 189   REWRITE_TAC[GSYM real_sub] THEN
 190   REWRITE_TAC[REAL_ARITH `(a + b) * (a + b) = a * a + b * b + &2 * a * b`] THEN
 191   REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
 192   REWRITE_TAC[REAL_ARITH `a + b <= abs a + abs b + &2 * abs c`]);;
 193
 194 let BOLZANO_WEIERSTRASS_COMPLEX_DISC = prove
 195  (`!s r. (!n. norm(s n) <= r)
 196          ==> ?f z. subseq f /\
 197                    !e. &0 < e ==> ?N. !n. n >= N ==> norm(s(f n) - z) < e`,
 198   REPEAT STRIP_TAC THEN
 199   MP_TAC(SPEC `Re o (s:num->complex)` SEQ_MONOSUB) THEN
 200   DISCH_THEN(X_CHOOSE_THEN `f:num->num` MP_TAC) THEN
 201   REWRITE_TAC[o_THM] THEN STRIP_TAC THEN
 202   MP_TAC(SPEC `Im o (s:num->complex) o (f:num->num)` SEQ_MONOSUB) THEN
 203   DISCH_THEN(X_CHOOSE_THEN `g:num->num` MP_TAC) THEN
 204   REWRITE_TAC[o_THM] THEN STRIP_TAC THEN
 205   EXISTS_TAC `(f:num->num) o (g:num->num)` THEN
 206   SUBGOAL_THEN `convergent (\n. Re(s(f n :num))) /\
 207                 convergent (\n. Im(s((f:num->num)(g n))))`
 208   MP_TAC THENL
 209    [CONJ_TAC THEN MATCH_MP_TAC SEQ_BCONV THEN ASM_REWRITE_TAC[bounded] THEN
 210     MAP_EVERY EXISTS_TAC [`r + &1`; `&0`; `0`] THEN
 211     REWRITE_TAC[GE; LE_0; MR1_DEF; REAL_SUB_LZERO; REAL_ABS_NEG] THEN
 212     X_GEN_TAC `n:num` THEN
 213     W(fun (_,w) -> FIRST_ASSUM(MP_TAC o SPEC (funpow 3 rand (lhand w)))) THEN
 214     REWRITE_TAC[complex_norm] THEN
 215     MATCH_MP_TAC(REAL_ARITH `a <= b ==> b <= r ==> a < r + &1`) THEN
 216     GEN_REWRITE_TAC LAND_CONV [GSYM POW_2_SQRT_ABS] THEN
 217     MATCH_MP_TAC SQRT_MONO_LE THEN
 218     REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_LE_ADDR; REAL_LE_ADDL];
 219     ALL_TAC] THEN
 220   REWRITE_TAC[convergent; SEQ; GE] THEN
 221   DISCH_THEN(CONJUNCTS_THEN2
 222     (X_CHOOSE_TAC `x:real`) (X_CHOOSE_TAC `y:real`)) THEN
 223   EXISTS_TAC `complex(x,y)` THEN CONJ_TAC THENL
 224    [MAP_EVERY UNDISCH_TAC [`subseq f`; `subseq g`] THEN
 225     REWRITE_TAC[subseq; o_THM] THEN MESON_TAC[]; ALL_TAC] THEN
 226   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 227   UNDISCH_TAC
 228    `!e. &0 < e
 229         ==> (?N. !n. N <= n ==> abs(Re(s ((f:num->num) n)) - x) < e)` THEN
 230   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
 231   FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
 232   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 233   DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
 234   EXISTS_TAC `N1 + N2:num` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 235   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * e / &2` THEN
 236   CONJ_TAC THENL
 237    [ALL_TAC;
 238     SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH; REAL_LE_REFL]] THEN
 239   W(MP_TAC o PART_MATCH lhand METRIC_BOUND_LEMMA o lhand o snd) THEN
 240   MATCH_MP_TAC(REAL_ARITH
 241     `a < c /\ b < c ==> x <= a + b ==> x < &2 * c`) THEN
 242   REWRITE_TAC[o_THM; RE; IM] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 243   ASM_MESON_TAC[LE_ADD; SEQ_SUBLE; LE_TRANS; ADD_SYM]);;
 244
 245 (* ------------------------------------------------------------------------- *)
 246 (* Polynomial is continuous.                                                 *)
 247 (* ------------------------------------------------------------------------- *)
 248
 249 let POLY_CONT = prove
 250  (`!p z e. &0 < e
 251            ==> ?d. &0 < d /\ !w. &0 < norm(w - z) /\ norm(w - z) < d
 252                    ==> norm(poly p w - poly p z) < e`,
 253   REPEAT STRIP_TAC THEN
 254   MP_TAC(SPECL [`z:complex`; `p:complex list`] POLY_OFFSET) THEN
 255   DISCH_THEN(X_CHOOSE_THEN `q:complex list` (MP_TAC o CONJUNCT2)) THEN
 256   DISCH_THEN(MP_TAC o GEN `w:complex` o SYM o SPEC `w - z`) THEN
 257   REWRITE_TAC[COMPLEX_SUB_ADD2] THEN
 258   DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
 259   REWRITE_TAC[COMPLEX_SUB_REFL] THEN
 260   SPEC_TAC(`q:complex list`,`p:complex list`) THEN
 261   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly] THENL
 262    [EXISTS_TAC `e:real` THEN
 263     ASM_REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_NORM_CX; REAL_ABS_NUM];
 264     ALL_TAC] THEN
 265   REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; COMPLEX_ADD_SUB] THEN
 266   MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN
 267   DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
 268   MP_TAC(SPECL [`&1`; `e / m:real`] REAL_DOWN2) THEN
 269   ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_01] THEN
 270   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
 271   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `w:complex` THEN
 272   STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
 273   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `d * m:real` THEN
 274   ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
 275   ASM_MESON_TAC[REAL_LT_TRANS; REAL_LT_IMP_LE; COMPLEX_NORM_POS]);;
 276
 277 (* ------------------------------------------------------------------------- *)
 278 (* Hence a polynomial attains minimum on a closed disc in the complex plane. *)
 279 (* ------------------------------------------------------------------------- *)
 280
 281 let POLY_MINIMUM_MODULUS_DISC = prove
 282  (`!p r. ?z. !w. norm(w) <= r ==> norm(poly p z) <= norm(poly p w)`,
 283   let lemma = prove
 284    (`P /\ (m = --x) /\ --x < y <=> (--x = m) /\ P /\ m < y`,
 285     MESON_TAC[]) in
 286   REPEAT GEN_TAC THEN
 287   ASM_CASES_TAC `&0 <= r` THENL
 288    [ALL_TAC; ASM_MESON_TAC[COMPLEX_NORM_POS; REAL_LE_TRANS]] THEN
 289   MP_TAC(SPEC `\x. ?z. norm(z) <= r /\ (norm(poly p z) = --x)`
 290     REAL_SUP_EXISTS) THEN
 291   REWRITE_TAC[] THEN ANTS_TAC THENL
 292    [CONJ_TAC THENL
 293      [MAP_EVERY EXISTS_TAC [`--norm(poly p (Cx(&0)))`; `Cx(&0)`] THEN
 294       ASM_REWRITE_TAC[REAL_NEG_NEG; COMPLEX_NORM_CX; REAL_ABS_NUM];
 295       EXISTS_TAC `&1` THEN
 296       REWRITE_TAC[REAL_ARITH `(a = --b) <=> (--b = a:real)`] THEN
 297       REWRITE_TAC[REAL_ARITH `x < &1 <=>  --(&1) < --x`] THEN
 298       SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 299       SIMP_TAC[REAL_ARITH `&0 <= x ==> --(&1) < x`; COMPLEX_NORM_POS]];
 300     ALL_TAC] THEN
 301   DISCH_THEN(X_CHOOSE_THEN `s:real` MP_TAC) THEN
 302   ONCE_REWRITE_TAC[REAL_ARITH `a < b <=> --b < --a:real`] THEN
 303   ABBREV_TAC `m = --s:real` THEN
 304   DISCH_THEN(MP_TAC o GEN `y:real` o SPEC `--y:real`) THEN
 305   REWRITE_TAC[REAL_NEG_NEG] THEN
 306   REWRITE_TAC[LEFT_AND_EXISTS_THM; GSYM CONJ_ASSOC; lemma] THEN
 307   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 308   ONCE_REWRITE_TAC[REAL_ARITH `(--a = b) <=> (a = --b:real)`] THEN
 309   REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
 310   DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `m:real` th)) THEN
 311   REWRITE_TAC[REAL_LT_REFL; NOT_EXISTS_THM] THEN
 312   REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN
 313   REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
 314   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `m + inv(&(SUC n))`) THEN
 315   REWRITE_TAC[REAL_LT_ADDR; REAL_LT_INV_EQ; REAL_OF_NUM_LT; LT_0] THEN
 316   REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
 317   DISCH_THEN(X_CHOOSE_THEN `s:num->complex` STRIP_ASSUME_TAC) THEN
 318   MP_TAC(SPECL [`s:num->complex`; `r:real`]
 319     BOLZANO_WEIERSTRASS_COMPLEX_DISC) THEN ASM_REWRITE_TAC[] THEN
 320   DISCH_THEN(X_CHOOSE_THEN `f:num->num` (X_CHOOSE_THEN `z:complex`
 321     STRIP_ASSUME_TAC)) THEN
 322   EXISTS_TAC `z:complex` THEN X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
 323   SUBGOAL_THEN `norm(poly p z) = m` (fun th -> ASM_SIMP_TAC[th]) THEN
 324   MATCH_MP_TAC(REAL_ARITH `~(&0 < abs(a - b)) ==> (a = b)`) THEN DISCH_TAC THEN
 325   ABBREV_TAC `e = abs(norm(poly p z) - m)` THEN
 326   MP_TAC(SPECL [`p:complex list`; `z:complex`; `e / &2`] POLY_CONT) THEN
 327   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 328   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 329   SUBGOAL_THEN `!w. norm(w - z) < d ==> norm(poly p w - poly p z) < e / &2`
 330   MP_TAC THENL
 331    [X_GEN_TAC `u:complex` THEN
 332     ASM_CASES_TAC `u = z:complex` THEN
 333     ASM_SIMP_TAC[COMPLEX_SUB_REFL; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH;
 334                  COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
 335     DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 336     ASM_REWRITE_TAC[COMPLEX_NORM_NZ; COMPLEX_SUB_0]; ALL_TAC] THEN
 337   FIRST_ASSUM(K ALL_TAC o check (is_conj o lhand o
 338     snd o dest_forall o concl)) THEN
 339   DISCH_TAC THEN
 340   FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[GE] THEN
 341   DISCH_THEN(X_CHOOSE_THEN `N1:num` ASSUME_TAC) THEN
 342   MP_TAC(SPEC `&2 / e` REAL_ARCH_SIMPLE) THEN
 343   DISCH_THEN(X_CHOOSE_THEN `N2:num` ASSUME_TAC) THEN
 344   SUBGOAL_THEN `norm(poly p (s((f:num->num) (N1 + N2))) - poly p z) < e / &2`
 345   MP_TAC THENL
 346    [FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[LE_ADD]; ALL_TAC] THEN
 347   MATCH_MP_TAC(REAL_ARITH
 348    `!m. abs(norm(psfn) - m) < e2 /\
 349         &2 * e2 <= abs(norm(psfn) - m) + norm(psfn - pz)
 350         ==> norm(psfn - pz) < e2 ==> F`) THEN
 351   EXISTS_TAC `m:real` THEN CONJ_TAC THENL
 352    [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&(SUC(N1 + N2)))` THEN
 353     CONJ_TAC THENL
 354      [MATCH_MP_TAC(REAL_ARITH
 355        `m <= x /\ x < m + e ==> abs(x - m:real) < e`) THEN
 356       ASM_SIMP_TAC[] THEN
 357       MATCH_MP_TAC REAL_LTE_TRANS THEN
 358       EXISTS_TAC `m + inv(&(SUC(f(N1 + N2:num))))` THEN
 359       ASM_REWRITE_TAC[REAL_LE_LADD] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
 360       ASM_SIMP_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; LT_0; LE_SUC; SEQ_SUBLE];
 361       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN
 362       MATCH_MP_TAC REAL_LE_INV2 THEN
 363       ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
 364       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N2` THEN
 365       ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC]; ALL_TAC] THEN
 366   SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH] THEN
 367   EXPAND_TAC "e" THEN
 368   MATCH_MP_TAC(REAL_ARITH
 369    `abs(norm(psfn) - norm(pz)) <= norm(psfn - pz)
 370     ==> abs(norm(pz) - m) <= abs(norm(psfn) - m) + norm(psfn - pz)`) THEN
 371   REWRITE_TAC[COMPLEX_NORM_ABS_NORM]);;
 372
 373 (* ------------------------------------------------------------------------- *)
 374 (* Nonzero polynomial in z goes to infinity as z does.                       *)
 375 (* ------------------------------------------------------------------------- *)
 376
 377 let POLY_INFINITY = prove
 378  (`!p a. EX (\b. ~(b = Cx(&0))) p
 379          ==> !d. ?r. !z. r <= norm(z) ==> d <= norm(poly (CONS a p) z)`,
 380   LIST_INDUCT_TAC THEN REWRITE_TAC[EX] THEN X_GEN_TAC `a:complex` THEN
 381   ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THEN ASM_REWRITE_TAC[] THENL
 382    [X_GEN_TAC `d:real` THEN
 383     FIRST_X_ASSUM(MP_TAC o SPEC `h:complex`) THEN ASM_REWRITE_TAC[] THEN
 384     DISCH_THEN(X_CHOOSE_TAC `r:real` o SPEC `d + norm(a)`) THEN
 385     EXISTS_TAC `&1 + abs(r)` THEN X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
 386     ONCE_REWRITE_TAC[poly] THEN
 387     MATCH_MP_TAC REAL_LE_TRANS THEN
 388     EXISTS_TAC `norm(z * poly (CONS h t) z) - norm(a)` THEN CONJ_TAC THENL
 389      [ALL_TAC;
 390       ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN
 391       REWRITE_TAC[REAL_LE_SUB_RADD; COMPLEX_NORM_TRIANGLE_SUB]] THEN
 392     REWRITE_TAC[REAL_LE_SUB_LADD] THEN
 393     MATCH_MP_TAC REAL_LE_TRANS THEN
 394     EXISTS_TAC `&1 * norm(poly (CONS h t) z)` THEN CONJ_TAC THENL
 395      [REWRITE_TAC[REAL_MUL_LID] THEN FIRST_ASSUM MATCH_MP_TAC THEN
 396       ASM_SIMP_TAC[REAL_ARITH `&1 + abs(r) <= x ==> r <= x`];
 397       REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
 398       REWRITE_TAC[COMPLEX_NORM_POS] THEN
 399       ASM_MESON_TAC[REAL_ARITH `&1 + abs(r) <= x ==> &1 <= x`]];
 400     RULE_ASSUM_TAC(REWRITE_RULE[NOT_EX]) THEN
 401     ASM_SIMP_TAC[poly; POLY_0; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
 402     DISCH_TAC THEN X_GEN_TAC `d:real` THEN
 403     EXISTS_TAC `(abs(d) + norm(a)) / norm(h)` THEN X_GEN_TAC `z:complex` THEN
 404     ASM_SIMP_TAC[REAL_LE_LDIV_EQ; COMPLEX_NORM_NZ; GSYM COMPLEX_NORM_MUL] THEN
 405     MATCH_MP_TAC(REAL_ARITH
 406      `mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh`) THEN
 407     ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN
 408     REWRITE_TAC[COMPLEX_NORM_TRIANGLE_SUB]]);;
 409
 410 (* ------------------------------------------------------------------------- *)
 411 (* Hence polynomial's modulus attains its minimum somewhere.                 *)
 412 (* ------------------------------------------------------------------------- *)
 413
 414 let POLY_MINIMUM_MODULUS = prove
 415  (`!p. ?z. !w. norm(poly p z) <= norm(poly p w)`,
 416   LIST_INDUCT_TAC THEN REWRITE_TAC[poly; REAL_LE_REFL] THEN
 417   ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THENL
 418    [FIRST_ASSUM(MP_TAC o SPEC `h:complex` o MATCH_MP POLY_INFINITY) THEN
 419     DISCH_THEN(MP_TAC o SPEC `norm(poly (CONS h t) (Cx(&0)))`) THEN
 420     DISCH_THEN(X_CHOOSE_THEN `r:real` ASSUME_TAC) THEN
 421     MP_TAC(SPECL [`CONS (h:complex) t`; `abs(r)`]
 422        POLY_MINIMUM_MODULUS_DISC) THEN
 423     REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN
 424     ASM_MESON_TAC[REAL_ARITH `r <= z \/ z <= abs(r)`; REAL_LE_TRANS;
 425                   COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_ABS_POS];
 426     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
 427     REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o MATCH_MP POLY_0) THEN
 428     ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; REAL_LE_REFL]]);;
 429
 430 (* ------------------------------------------------------------------------- *)
 431 (* Constant function (non-syntactic characterization).                       *)
 432 (* ------------------------------------------------------------------------- *)
 433
 434 let constant = new_definition
 435   `constant f = !w z. f(w) = f(z)`;;
 436
 437 let NONCONSTANT_LENGTH = prove
 438  (`!p. ~constant(poly p) ==> 2 <= LENGTH p`,
 439   REWRITE_TAC[constant] THEN
 440   LIST_INDUCT_TAC THEN REWRITE_TAC[poly] THEN
 441   REWRITE_TAC[LENGTH; ARITH_RULE `2 <= SUC n <=> ~(n = 0)`] THEN
 442   SIMP_TAC[TAUT `~a ==> ~b <=> b ==> a`; LENGTH_EQ_NIL; poly] THEN
 443   REWRITE_TAC[COMPLEX_MUL_RZERO]);;
 444
 445 (* ------------------------------------------------------------------------- *)
 446 (* Decomposition of polynomial, skipping zero coefficients after the first.  *)
 447 (* ------------------------------------------------------------------------- *)
 448
 449 let POLY_DECOMPOSE_LEMMA = prove
 450  (`!p. ~(!z. ~(z = Cx(&0)) ==> (poly p z = Cx(&0)))
 451        ==> ?k a q. ~(a = Cx(&0)) /\
 452                    (SUC(LENGTH q + k) = LENGTH p) /\
 453                    !z. poly p z = z pow k * poly (CONS a q) z`,
 454   LIST_INDUCT_TAC THENL [REWRITE_TAC[poly]; ALL_TAC] THEN
 455   ASM_CASES_TAC `h = Cx(&0)` THENL
 456    [GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [poly] THEN
 457     ASM_SIMP_TAC[COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN
 458     DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 459     DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
 460      (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN
 461     MAP_EVERY EXISTS_TAC [`k + 1`; `a:complex`; `q:complex list`] THEN
 462     ASM_REWRITE_TAC[poly; LENGTH; GSYM ADD1; ADD_CLAUSES] THEN
 463     REWRITE_TAC[COMPLEX_ADD_LID; complex_pow; GSYM COMPLEX_MUL_ASSOC];
 464     DISCH_THEN(K ALL_TAC) THEN
 465     MAP_EVERY EXISTS_TAC [`0`; `h:complex`; `t:complex list`] THEN
 466     ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID; ADD_CLAUSES; LENGTH]]);;
 467
 468 let POLY_DECOMPOSE = prove
 469  (`!p. ~constant(poly p)
 470        ==> ?k a q. ~(a = Cx(&0)) /\ ~(k = 0) /\
 471                    (LENGTH q + k + 1 = LENGTH p) /\
 472                    !z. poly p z = poly p (Cx(&0)) +
 473                                   z pow k * poly (CONS a q) z`,
 474   LIST_INDUCT_TAC THENL [REWRITE_TAC[constant; poly]; ALL_TAC] THEN
 475   POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN
 476   MP_TAC(SPEC `t:complex list` POLY_DECOMPOSE_LEMMA) THEN ANTS_TAC THENL
 477    [POP_ASSUM MP_TAC THEN REWRITE_TAC[constant; poly] THEN
 478     REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`; COMPLEX_EQ_ADD_LCANCEL] THEN
 479     SIMP_TAC[TAUT `~a ==> b <=> a \/ b`; GSYM COMPLEX_ENTIRE]; ALL_TAC] THEN
 480   DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
 481      (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN
 482   MAP_EVERY EXISTS_TAC [`SUC k`; `a:complex`; `q:complex list`] THEN
 483   ASM_REWRITE_TAC[ADD_CLAUSES; GSYM ADD1; LENGTH; NOT_SUC] THEN
 484   ASM_REWRITE_TAC[poly; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; complex_pow] THEN
 485   REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC]);;
 486
 487 let POLY_REPLICATE_APPEND = prove
 488  (`!n p x. poly (APPEND (REPLICATE n (Cx(&0))) p) x = x pow n * poly p x`,
 489   INDUCT_TAC THEN
 490   REWRITE_TAC[REPLICATE; APPEND; complex_pow; COMPLEX_MUL_LID] THEN
 491   ASM_REWRITE_TAC[poly; COMPLEX_ADD_LID] THEN REWRITE_TAC[COMPLEX_MUL_ASSOC]);;
 492
 493 (* ------------------------------------------------------------------------- *)
 494 (* Fundamental theorem.                                                      *)
 495 (* ------------------------------------------------------------------------- *)
 496
 497 let FUNDAMENTAL_THEOREM_OF_ALGEBRA = prove
 498  (`!p. ~constant(poly p) ==> ?z. poly p z = Cx(&0)`,
 499   SUBGOAL_THEN
 500    `!n p. (LENGTH p = n) /\ ~constant(poly p) ==> ?z. poly p z = Cx(&0)`
 501    (fun th -> MESON_TAC[th]) THEN
 502   MATCH_MP_TAC num_WF THEN
 503   X_GEN_TAC `n:num` THEN STRIP_TAC THEN
 504   X_GEN_TAC `p:complex list` THEN STRIP_TAC THEN
 505   FIRST_ASSUM(MP_TAC o MATCH_MP NONCONSTANT_LENGTH) THEN
 506   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 507   X_CHOOSE_TAC `c:complex` (SPEC `p:complex list` POLY_MINIMUM_MODULUS) THEN
 508   ASM_CASES_TAC `poly p c = Cx(&0)` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 509   MP_TAC(SPECL [`c:complex`; `p:complex list`] POLY_OFFSET) THEN
 510   DISCH_THEN(X_CHOOSE_THEN `q:complex list` MP_TAC) THEN
 511   DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) ASSUME_TAC) THEN
 512   SUBGOAL_THEN `~constant(poly q)` ASSUME_TAC THENL
 513    [UNDISCH_TAC `~(constant(poly p))` THEN
 514     SUBGOAL_THEN `!z. poly q (z - c) = poly p z`
 515       (fun th -> MESON_TAC[th; constant]) THEN
 516     ASM_MESON_TAC[SIMPLE_COMPLEX_ARITH `a + (x - a) = x`]; ALL_TAC] THEN
 517   SUBGOAL_THEN `poly p c = poly q (Cx(&0))` SUBST_ALL_TAC THENL
 518    [ASM_MESON_TAC[COMPLEX_ADD_RID]; ALL_TAC] THEN
 519   SUBGOAL_THEN `!w. norm(poly q (Cx(&0))) <= norm(poly q w)` MP_TAC THENL
 520    [ASM_MESON_TAC[]; ALL_TAC] THEN
 521   POP_ASSUM_LIST(MAP_EVERY (fun th ->
 522     if free_in `p:complex list` (concl th)
 523     then ALL_TAC else ASSUME_TAC th)) THEN
 524   MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
 525   REWRITE_TAC[NOT_FORALL_THM; REAL_NOT_LE] THEN
 526   ABBREV_TAC `a0 = poly q (Cx(&0))` THEN
 527   SUBGOAL_THEN
 528    `!z. poly q z = poly (MAP (( * ) (inv(a0))) q) z * a0`
 529   ASSUME_TAC THENL
 530    [REWRITE_TAC[POLY_CMUL_MAP] THEN
 531     ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `(a * b) * c = b * c * a`] THEN
 532     ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_RID];
 533     ALL_TAC] THEN
 534   ABBREV_TAC `r = MAP (( * ) (inv(a0))) q` THEN
 535   SUBGOAL_THEN `LENGTH(q:complex list) = LENGTH(r:complex list)`
 536   SUBST_ALL_TAC THENL
 537    [EXPAND_TAC "r" THEN REWRITE_TAC[LENGTH_MAP]; ALL_TAC] THEN
 538   SUBGOAL_THEN `~(constant(poly r))` ASSUME_TAC THENL
 539    [UNDISCH_TAC `~constant(poly q)` THEN
 540     ASM_REWRITE_TAC[constant; COMPLEX_EQ_MUL_RCANCEL] THEN MESON_TAC[];
 541     ALL_TAC] THEN
 542   SUBGOAL_THEN `poly r (Cx(&0)) = Cx(&1)` ASSUME_TAC THENL
 543    [FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN
 544     ASM_REWRITE_TAC[] THEN
 545     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM COMPLEX_MUL_LID] THEN
 546     ASM_SIMP_TAC[COMPLEX_EQ_MUL_RCANCEL]; ALL_TAC] THEN
 547   ASM_REWRITE_TAC[] THEN
 548   POP_ASSUM_LIST(MAP_EVERY (fun th ->
 549     if free_in `q:complex list` (concl th)
 550     then ALL_TAC else ASSUME_TAC th)) THEN
 551   ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; COMPLEX_NORM_NZ; COMPLEX_NORM_MUL;
 552                REAL_DIV_REFL; COMPLEX_NORM_ZERO] THEN
 553   FIRST_ASSUM(MP_TAC o MATCH_MP POLY_DECOMPOSE) THEN
 554   DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
 555         (X_CHOOSE_THEN `s:complex list` MP_TAC))) THEN
 556   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 557   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 558   DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) MP_TAC) THEN
 559   DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[] THEN
 560   ASM_CASES_TAC `k + 1 = n` THENL
 561    [UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN
 562     ASM_REWRITE_TAC[ARITH_RULE `(s + m = m) <=> (s = 0)`; LENGTH_EQ_NIL] THEN
 563     REWRITE_TAC[LENGTH_EQ_NIL] THEN DISCH_THEN SUBST1_TAC THEN
 564     REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
 565     ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
 566     MATCH_MP_TAC REDUCE_POLY_SIMPLE THEN ASM_REWRITE_TAC[] THEN
 567     MAP_EVERY UNDISCH_TAC [`k + 1 = n`; `2 <= n`] THEN ARITH_TAC; ALL_TAC] THEN
 568   FIRST_X_ASSUM(MP_TAC o SPEC `k + 1`) THEN ANTS_TAC THENL
 569    [UNDISCH_TAC `~(k + 1 = n)` THEN
 570     UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN ARITH_TAC;
 571     ALL_TAC] THEN
 572   DISCH_THEN(MP_TAC o SPEC
 573    `CONS (Cx(&1)) (APPEND (REPLICATE (k - 1) (Cx(&0))) [a])`) THEN
 574   ANTS_TAC THENL
 575    [CONJ_TAC THENL
 576      [REWRITE_TAC[LENGTH; LENGTH_APPEND; LENGTH_REPLICATE] THEN
 577       UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 578     REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN
 579     REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
 580     DISCH_THEN(MP_TAC o SPECL [`Cx(&0)`; `Cx(&1)`]) THEN
 581     REWRITE_TAC[COMPLEX_MUL_LID; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID] THEN
 582     ASM_REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_POW_ONE; SIMPLE_COMPLEX_ARITH
 583                   `(a = a + b) <=> (b = Cx(&0))`] THEN
 584     REWRITE_TAC[CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN
 585   REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN
 586   REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
 587   ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c = (a * b) * c`] THEN
 588   REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN
 589   ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> (SUC(k - 1) = k)`] THEN
 590   DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN
 591   MP_TAC(SPECL [`s:complex list`; `norm(w)`] POLY_BOUND_EXISTS) THEN
 592   DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
 593   SUBGOAL_THEN `~(w = Cx(&0))` ASSUME_TAC THENL
 594    [UNDISCH_TAC `Cx(&1) + w pow k * a = Cx(&0)` THEN
 595     ONCE_REWRITE_TAC[TAUT `a ==> ~b <=> b ==> ~a`] THEN
 596     DISCH_THEN SUBST1_TAC THEN
 597     UNDISCH_TAC `~(k = 0)` THEN SPEC_TAC(`k:num`,`k:num`) THEN
 598     INDUCT_TAC THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_LZERO] THEN
 599     REWRITE_TAC[COMPLEX_ADD_RID; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ];
 600     ALL_TAC] THEN
 601   MP_TAC(SPECL [`&1`; `inv(norm(w) pow (k + 1) * m)`] REAL_DOWN2) THEN
 602   ASM_SIMP_TAC[REAL_LT_01; REAL_LT_INV_EQ; REAL_LT_MUL; REAL_POW_LT;
 603                COMPLEX_NORM_NZ] THEN
 604   DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
 605   EXISTS_TAC `Cx(t) * w` THEN REWRITE_TAC[COMPLEX_POW_MUL] THEN
 606   REWRITE_TAC[COMPLEX_ADD_LDISTRIB; GSYM COMPLEX_MUL_ASSOC] THEN
 607   FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SIMPLE_COMPLEX_ARITH
 608    `(a + w = Cx(&0)) ==> (w = --a)`)) THEN
 609   REWRITE_TAC[GSYM CX_NEG; GSYM CX_POW; GSYM CX_MUL] THEN
 610   REWRITE_TAC[COMPLEX_ADD_ASSOC; GSYM CX_ADD] THEN
 611   MATCH_MP_TAC REAL_LET_TRANS THEN
 612   EXISTS_TAC `norm(Cx(&1 + t pow k * -- &1)) +
 613               norm(Cx(t pow k) * w pow k * Cx t * w * poly s (Cx t * w))` THEN
 614   REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
 615   MATCH_MP_TAC(REAL_ARITH
 616    `&0 <= x /\ x < t /\ t <= &1 ==> abs(&1 + t * --(&1)) + x < &1`) THEN
 617   REWRITE_TAC[COMPLEX_NORM_POS] THEN
 618   ASM_SIMP_TAC[REAL_POW_1_LE; REAL_LT_IMP_LE] THEN
 619   ONCE_REWRITE_TAC[COMPLEX_NORM_MUL] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
 620   ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_POW_LE] THEN
 621   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
 622   MATCH_MP_TAC REAL_LT_LMUL THEN ASM_SIMP_TAC[REAL_POW_LT] THEN
 623   ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c * d = b * (c * a) * d`] THEN
 624   REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN
 625   REWRITE_TAC[COMPLEX_NORM_MUL; ADD1; COMPLEX_NORM_CX] THEN
 626   MATCH_MP_TAC REAL_LET_TRANS THEN
 627   EXISTS_TAC `abs t * norm(w pow (k + 1)) * m` THEN CONJ_TAC THENL
 628    [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
 629     MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN
 630     FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
 631     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
 632     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN
 633     ASM_SIMP_TAC[COMPLEX_NORM_CX; REAL_ARITH
 634       `&0 < t /\ t < &1 ==> abs(t) <= &1`]; ALL_TAC] THEN
 635   ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_MUL; COMPLEX_NORM_POW;
 636                REAL_POW_LT; COMPLEX_NORM_NZ] THEN
 637   ASM_SIMP_TAC[real_div; REAL_MUL_LID;
 638                REAL_ARITH `&0 < t /\ t < x ==> abs(t) < x`]);;
 639
 640 (* ------------------------------------------------------------------------- *)
 641 (* Alternative version with a syntactic notion of constant polynomial.       *)
 642 (* ------------------------------------------------------------------------- *)
 643
 644 let FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT = prove
 645  (`!p. ~(?a l. ~(a = Cx(&0)) /\ ALL (\b. b = Cx(&0)) l /\ (p = CONS a l))
 646        ==> ?z. poly p z = Cx(&0)`,
 647   LIST_INDUCT_TAC THEN REWRITE_TAC[poly; CONS_11] THEN
 648   POP_ASSUM_LIST(K ALL_TAC) THEN
 649   ONCE_REWRITE_TAC[AC CONJ_ACI `a /\ b /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
 650   REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 651   ASM_CASES_TAC `h = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_ADD_LID] THENL
 652    [EXISTS_TAC `Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO]; ALL_TAC] THEN
 653   DISCH_TAC THEN REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN
 654   MATCH_MP_TAC FUNDAMENTAL_THEOREM_OF_ALGEBRA THEN
 655   UNDISCH_TAC `~ALL (\b. b = Cx (&0)) t` THEN
 656   REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN POP_ASSUM(K ALL_TAC) THEN
 657   REWRITE_TAC[constant; poly; REAL_EQ_LADD] THEN
 658   DISCH_THEN(MP_TAC o SPEC `Cx(&0)` o ONCE_REWRITE_RULE[SWAP_FORALL_THM]) THEN
 659   REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_EQ_ADD_LCANCEL] THEN
 660   REWRITE_TAC[COMPLEX_ENTIRE; TAUT `a \/ b <=> ~a ==> b`] THEN
 661   SPEC_TAC(`t:complex list`,`p:complex list`) THEN
 662   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL] THEN
 663   ASM_CASES_TAC `h = Cx(&0)` THEN
 664   ASM_SIMP_TAC[poly; COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN
 665   MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN
 666   DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
 667   MP_TAC(SPECL [`norm(h) / m`; `&1`] REAL_DOWN2) THEN
 668   ASM_SIMP_TAC[REAL_LT_01; REAL_LT_DIV; COMPLEX_NORM_NZ] THEN
 669   DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN
 670   DISCH_THEN(MP_TAC o SPEC `Cx(x)`) THEN
 671   ASM_SIMP_TAC[CX_INJ; REAL_LT_IMP_NZ] THEN
 672   REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(x + y = Cx(&0)) <=> (y = --x)`] THEN
 673   DISCH_THEN(MP_TAC o AP_TERM `norm`) THEN REWRITE_TAC[COMPLEX_NORM_NEG] THEN
 674   MATCH_MP_TAC(REAL_ARITH `abs(a) < abs(b) ==> ~(a = b)`) THEN
 675   REWRITE_TAC[real_abs; COMPLEX_NORM_POS] THEN
 676   REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
 677   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `norm(h) / m * m` THEN
 678   CONJ_TAC THENL
 679    [ALL_TAC; ASM_SIMP_TAC[REAL_LE_REFL; REAL_DIV_RMUL; REAL_LT_IMP_NZ]] THEN
 680   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(x) * m` THEN
 681   ASM_SIMP_TAC[REAL_LT_RMUL; REAL_ARITH `&0 < x /\ x < a ==> abs(x) < a`] THEN
 682   ASM_MESON_TAC[REAL_LE_LMUL; REAL_ABS_POS; COMPLEX_NORM_CX;
 683                 REAL_ARITH `&0 < x /\ x < &1 ==> abs(x) <= &1`]);;