Complex/cpoly.ml

   1 (* ========================================================================= *)
   2 (* Properties of complex polynomials (not canonically represented).          *)
   3 (* ========================================================================= *)
   4
   5 needs "Complex/complexnumbers.ml";;
   6
   7 prioritize_complex();;
   8
   9 parse_as_infix("++",(16,"right"));;
  10 parse_as_infix("**",(20,"right"));;
  11 parse_as_infix("##",(20,"right"));;
  12 parse_as_infix("divides",(14,"right"));;
  13 parse_as_infix("exp",(22,"right"));;
  14
  15 do_list override_interface
  16   ["++",`poly_add:complex list->complex list->complex list`;
  17    "**",`poly_mul:complex list->complex list->complex list`;
  18    "##",`poly_cmul:complex->complex list->complex list`;
  19    "neg",`poly_neg:complex list->complex list`;
  20    "divides",`poly_divides:complex list->complex list->bool`;
  21    "exp",`poly_exp:complex list -> num -> complex list`;
  22    "diff",`poly_diff:complex list->complex list`];;
  23
  24 let SIMPLE_COMPLEX_ARITH tm = prove(tm,SIMPLE_COMPLEX_ARITH_TAC);;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Polynomials.                                                              *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let poly = new_recursive_definition list_RECURSION
  31   `(poly [] x = Cx(&0)) /\
  32    (poly (CONS h t) x = h + x * poly t x)`;;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Arithmetic operations on polynomials.                                     *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let poly_add = new_recursive_definition list_RECURSION
  39   `([] ++ l2 = l2) /\
  40    ((CONS h t) ++ l2 =
  41         (if l2 = [] then CONS h t
  42                     else CONS (h + HD l2) (t ++ TL l2)))`;;
  43
  44 let poly_cmul = new_recursive_definition list_RECURSION
  45   `(c ## [] = []) /\
  46    (c ## (CONS h t) = CONS (c * h) (c ## t))`;;
  47
  48 let poly_neg = new_definition
  49   `neg = (##) (--(Cx(&1)))`;;
  50
  51 let poly_mul = new_recursive_definition list_RECURSION
  52   `([] ** l2 = []) /\
  53    ((CONS h t) ** l2 =
  54         if t = [] then h ## l2
  55         else (h ## l2) ++ CONS (Cx(&0)) (t ** l2))`;;
  56
  57 let poly_exp = new_recursive_definition num_RECURSION
  58   `(p exp 0 = [Cx(&1)]) /\
  59    (p exp (SUC n) = p ** p exp n)`;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Useful clausifications.                                                   *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let POLY_ADD_CLAUSES = prove
  66  (`([] ++ p2 = p2) /\
  67    (p1 ++ [] = p1) /\
  68    ((CONS h1 t1) ++ (CONS h2 t2) = CONS (h1 + h2) (t1 ++ t2))`,
  69   REWRITE_TAC[poly_add; NOT_CONS_NIL; HD; TL] THEN
  70   SPEC_TAC(`p1:complex list`,`p1:complex list`) THEN
  71   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly_add]);;
  72
  73 let POLY_CMUL_CLAUSES = prove
  74  (`(c ## [] = []) /\
  75    (c ## (CONS h t) = CONS (c * h) (c ## t))`,
  76   REWRITE_TAC[poly_cmul]);;
  77
  78 let POLY_NEG_CLAUSES = prove
  79  (`(neg [] = []) /\
  80    (neg (CONS h t) = CONS (--h) (neg t))`,
  81   REWRITE_TAC[poly_neg; POLY_CMUL_CLAUSES;
  82               COMPLEX_MUL_LNEG; COMPLEX_MUL_LID]);;
  83
  84 let POLY_MUL_CLAUSES = prove
  85  (`([] ** p2 = []) /\
  86    ([h1] ** p2 = h1 ## p2) /\
  87    ((CONS h1 (CONS k1 t1)) ** p2 =
  88         h1 ## p2 ++ CONS (Cx(&0)) (CONS k1 t1 ** p2))`,
  89   REWRITE_TAC[poly_mul; NOT_CONS_NIL]);;
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* Various natural consequences of syntactic definitions.                    *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 let POLY_ADD = prove
  96  (`!p1 p2 x. poly (p1 ++ p2) x = poly p1 x + poly p2 x`,
  97   LIST_INDUCT_TAC THEN REWRITE_TAC[poly_add; poly; COMPLEX_ADD_LID] THEN
  98   LIST_INDUCT_TAC THEN
  99   ASM_REWRITE_TAC[NOT_CONS_NIL; HD; TL; poly; COMPLEX_ADD_RID] THEN
 100   SIMPLE_COMPLEX_ARITH_TAC);;
 101
 102 let POLY_CMUL = prove
 103  (`!p c x. poly (c ## p) x = c * poly p x`,
 104   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly; poly_cmul] THEN
 105   SIMPLE_COMPLEX_ARITH_TAC);;
 106
 107 let POLY_NEG = prove
 108  (`!p x. poly (neg p) x = --(poly p x)`,
 109   REWRITE_TAC[poly_neg; POLY_CMUL] THEN
 110   SIMPLE_COMPLEX_ARITH_TAC);;
 111
 112 let POLY_MUL = prove
 113  (`!x p1 p2. poly (p1 ** p2) x = poly p1 x * poly p2 x`,
 114   GEN_TAC THEN LIST_INDUCT_TAC THEN
 115   REWRITE_TAC[poly_mul; poly; COMPLEX_MUL_LZERO; POLY_CMUL; POLY_ADD] THEN
 116   SPEC_TAC(`h:complex`,`h:complex`) THEN
 117   SPEC_TAC(`t:complex list`,`t:complex list`) THEN
 118   LIST_INDUCT_TAC THEN
 119   REWRITE_TAC[poly_mul; POLY_CMUL; POLY_ADD; poly; POLY_CMUL;
 120     COMPLEX_MUL_RZERO; COMPLEX_ADD_RID; NOT_CONS_NIL] THEN
 121   ASM_REWRITE_TAC[POLY_ADD; POLY_CMUL; poly] THEN
 122   SIMPLE_COMPLEX_ARITH_TAC);;
 123
 124 let POLY_EXP = prove
 125  (`!p n x. poly (p exp n) x = (poly p x) pow n`,
 126   GEN_TAC THEN INDUCT_TAC THEN
 127   ASM_REWRITE_TAC[poly_exp; complex_pow; POLY_MUL] THEN
 128   REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 129
 130 (* ------------------------------------------------------------------------- *)
 131 (* Lemmas.                                                                   *)
 132 (* ------------------------------------------------------------------------- *)
 133
 134 let POLY_ADD_RZERO = prove
 135  (`!p. poly (p ++ []) = poly p`,
 136   REWRITE_TAC[FUN_EQ_THM; POLY_ADD; poly; COMPLEX_ADD_RID]);;
 137
 138 let POLY_MUL_ASSOC = prove
 139  (`!p q r. poly (p ** (q ** r)) = poly ((p ** q) ** r)`,
 140   REWRITE_TAC[FUN_EQ_THM; POLY_MUL; COMPLEX_MUL_ASSOC]);;
 141
 142 let POLY_EXP_ADD = prove
 143  (`!d n p. poly(p exp (n + d)) = poly(p exp n ** p exp d)`,
 144   REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
 145   INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_MUL; ADD_CLAUSES; poly_exp; poly] THEN
 146   SIMPLE_COMPLEX_ARITH_TAC);;
 147
 148 (* ------------------------------------------------------------------------- *)
 149 (* Key property that f(a) = 0 ==> (x - a) divides p(x). Very delicate!       *)
 150 (* ------------------------------------------------------------------------- *)
 151
 152 let POLY_LINEAR_REM = prove
 153  (`!t h. ?q r. CONS h t = [r] ++ [--a; Cx(&1)] ** q`,
 154   LIST_INDUCT_TAC THEN REWRITE_TAC[] THENL
 155    [GEN_TAC THEN EXISTS_TAC `[]:complex list` THEN
 156     EXISTS_TAC `h:complex` THEN
 157     REWRITE_TAC[poly_add; poly_mul; poly_cmul; NOT_CONS_NIL] THEN
 158     REWRITE_TAC[HD; TL; COMPLEX_ADD_RID];
 159     X_GEN_TAC `k:complex` THEN
 160     POP_ASSUM(STRIP_ASSUME_TAC o SPEC `h:complex`) THEN
 161     EXISTS_TAC `CONS (r:complex) q` THEN EXISTS_TAC `r * a + k` THEN
 162     ASM_REWRITE_TAC[POLY_ADD_CLAUSES; POLY_MUL_CLAUSES; poly_cmul] THEN
 163     REWRITE_TAC[CONS_11] THEN CONJ_TAC THENL
 164      [SIMPLE_COMPLEX_ARITH_TAC; ALL_TAC] THEN
 165     SPEC_TAC(`q:complex list`,`q:complex list`) THEN
 166     LIST_INDUCT_TAC THEN
 167     REWRITE_TAC[POLY_ADD_CLAUSES; POLY_MUL_CLAUSES; poly_cmul] THEN
 168     REWRITE_TAC[COMPLEX_ADD_RID; COMPLEX_MUL_LID] THEN
 169     REWRITE_TAC[COMPLEX_ADD_AC]]);;
 170
 171 let POLY_LINEAR_DIVIDES = prove
 172  (`!a p. (poly p a = Cx(&0)) <=> (p = []) \/ ?q. p = [--a; Cx(&1)] ** q`,
 173   GEN_TAC THEN LIST_INDUCT_TAC THENL
 174    [REWRITE_TAC[poly]; ALL_TAC] THEN
 175   EQ_TAC THEN STRIP_TAC THENL
 176    [DISJ2_TAC THEN STRIP_ASSUME_TAC(SPEC_ALL POLY_LINEAR_REM) THEN
 177     EXISTS_TAC `q:complex list` THEN ASM_REWRITE_TAC[] THEN
 178     SUBGOAL_THEN `r = Cx(&0)` SUBST_ALL_TAC THENL
 179      [UNDISCH_TAC `poly (CONS h t) a = Cx(&0)` THEN
 180       ASM_REWRITE_TAC[] THEN REWRITE_TAC[POLY_ADD; POLY_MUL] THEN
 181       REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID;
 182                   COMPLEX_MUL_RID] THEN
 183       REWRITE_TAC[COMPLEX_ADD_LINV] THEN SIMPLE_COMPLEX_ARITH_TAC;
 184       REWRITE_TAC[poly_mul] THEN REWRITE_TAC[NOT_CONS_NIL] THEN
 185       SPEC_TAC(`q:complex list`,`q:complex list`) THEN LIST_INDUCT_TAC THENL
 186        [REWRITE_TAC[poly_cmul; poly_add; NOT_CONS_NIL;
 187                     HD; TL; COMPLEX_ADD_LID];
 188         REWRITE_TAC[poly_cmul; poly_add; NOT_CONS_NIL;
 189                     HD; TL; COMPLEX_ADD_LID]]];
 190     ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly];
 191     ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly] THEN
 192     REWRITE_TAC[POLY_MUL] THEN REWRITE_TAC[poly] THEN
 193     REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID; COMPLEX_MUL_RID] THEN
 194     REWRITE_TAC[COMPLEX_ADD_LINV] THEN SIMPLE_COMPLEX_ARITH_TAC]);;
 195
 196 (* ------------------------------------------------------------------------- *)
 197 (* Thanks to the finesse of the above, we can use length rather than degree. *)
 198 (* ------------------------------------------------------------------------- *)
 199
 200 let POLY_LENGTH_MUL = prove
 201  (`!q. LENGTH([--a; Cx(&1)] ** q) = SUC(LENGTH q)`,
 202   let lemma = prove
 203    (`!p h k a. LENGTH (k ## p ++ CONS h (a ## p)) = SUC(LENGTH p)`,
 204     LIST_INDUCT_TAC THEN
 205     ASM_REWRITE_TAC[poly_cmul; POLY_ADD_CLAUSES; LENGTH]) in
 206   REWRITE_TAC[poly_mul; NOT_CONS_NIL; lemma]);;
 207
 208 (* ------------------------------------------------------------------------- *)
 209 (* Thus a nontrivial polynomial of degree n has no more than n roots.        *)
 210 (* ------------------------------------------------------------------------- *)
 211
 212 let POLY_ROOTS_INDEX_LEMMA = prove
 213  (`!n. !p. ~(poly p = poly []) /\ (LENGTH p = n)
 214            ==> ?i. !x. (poly p x = Cx(&0)) ==> ?m. m <= n /\ (x = i m)`,
 215   INDUCT_TAC THENL
 216    [REWRITE_TAC[LENGTH_EQ_NIL] THEN MESON_TAC[];
 217     REPEAT STRIP_TAC THEN ASM_CASES_TAC `?a. poly p a = Cx(&0)` THENL
 218      [UNDISCH_TAC `?a. poly p a = Cx(&0)` THEN
 219       DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
 220       GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN
 221       DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 222       DISCH_THEN(X_CHOOSE_THEN `q:complex list` SUBST_ALL_TAC) THEN
 223       FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 224       UNDISCH_TAC `~(poly ([-- a; Cx(&1)] ** q) = poly [])` THEN
 225       POP_ASSUM MP_TAC THEN REWRITE_TAC[POLY_LENGTH_MUL; SUC_INJ] THEN
 226       DISCH_TAC THEN ASM_CASES_TAC `poly q = poly []` THENL
 227        [ASM_REWRITE_TAC[POLY_MUL; poly; COMPLEX_MUL_RZERO; FUN_EQ_THM];
 228         DISCH_THEN(K ALL_TAC)] THEN
 229       DISCH_THEN(MP_TAC o SPEC `q:complex list`) THEN ASM_REWRITE_TAC[] THEN
 230       DISCH_THEN(X_CHOOSE_TAC `i:num->complex`) THEN
 231       EXISTS_TAC `\m. if m = SUC n then a:complex else i m` THEN
 232       REWRITE_TAC[POLY_MUL; LE; COMPLEX_ENTIRE] THEN
 233       X_GEN_TAC `x:complex` THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
 234        [DISCH_THEN(fun th -> EXISTS_TAC `SUC n` THEN MP_TAC th) THEN
 235         REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC;
 236         DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 237         DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
 238         EXISTS_TAC `m:num` THEN ASM_REWRITE_TAC[] THEN
 239         COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 240         UNDISCH_TAC `m:num <= n` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC];
 241       UNDISCH_TAC `~(?a. poly p a = Cx(&0))` THEN
 242       REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]]]);;
 243
 244 let POLY_ROOTS_INDEX_LENGTH = prove
 245  (`!p. ~(poly p = poly [])
 246        ==> ?i. !x. (poly p(x) = Cx(&0)) ==> ?n. n <= LENGTH p /\ (x = i n)`,
 247   MESON_TAC[POLY_ROOTS_INDEX_LEMMA]);;
 248
 249 let POLY_ROOTS_FINITE_LEMMA = prove
 250  (`!p. ~(poly p = poly [])
 251        ==> ?N i. !x. (poly p(x) = Cx(&0)) ==> ?n:num. n < N /\ (x = i n)`,
 252   MESON_TAC[POLY_ROOTS_INDEX_LENGTH; LT_SUC_LE]);;
 253
 254 let FINITE_LEMMA = prove
 255  (`!i N P. (!x. P x ==> ?n:num. n < N /\ (x = i n))
 256            ==> ?a. !x. P x ==> norm(x) < a`,
 257   GEN_TAC THEN ONCE_REWRITE_TAC[RIGHT_IMP_EXISTS_THM] THEN INDUCT_TAC THENL
 258    [REWRITE_TAC[LT] THEN MESON_TAC[]; ALL_TAC] THEN
 259   X_GEN_TAC `P:complex->bool` THEN
 260   POP_ASSUM(MP_TAC o SPEC `\z. P z /\ ~(z = (i:num->complex) N)`) THEN
 261   DISCH_THEN(X_CHOOSE_TAC `a:real`) THEN
 262   EXISTS_TAC `abs(a) + norm(i(N:num)) + &1` THEN
 263   POP_ASSUM MP_TAC THEN REWRITE_TAC[LT] THEN
 264   SUBGOAL_THEN `(!x. norm(x) < abs(a) + norm(x) + &1) /\
 265                 (!x y. norm(x) < a ==> norm(x) < abs(a) + norm(y) + &1)`
 266    (fun th -> MP_TAC th THEN MESON_TAC[]) THEN
 267   CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 268   REPEAT GEN_TAC THEN MP_TAC(SPEC `y:complex` COMPLEX_NORM_POS) THEN
 269   REAL_ARITH_TAC);;
 270
 271 let POLY_ROOTS_FINITE = prove
 272  (`!p. ~(poly p = poly []) <=>
 273        ?N i. !x. (poly p(x) = Cx(&0)) ==> ?n:num. n < N /\ (x = i n)`,
 274   GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE_LEMMA] THEN
 275   REWRITE_TAC[FUN_EQ_THM; LEFT_IMP_EXISTS_THM; NOT_FORALL_THM; poly] THEN
 276   MP_TAC(GENL [`i:num->complex`; `N:num`]
 277    (SPECL [`i:num->complex`; `N:num`; `\x. poly p x = Cx(&0)`]
 278          FINITE_LEMMA)) THEN
 279   REWRITE_TAC[] THEN MESON_TAC[REAL_ARITH `~(abs(x) < x)`; COMPLEX_NORM_CX]);;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Hence get entirety and cancellation for polynomials.                      *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 let POLY_ENTIRE_LEMMA = prove
 286  (`!p q. ~(poly p = poly []) /\ ~(poly q = poly [])
 287          ==> ~(poly (p ** q) = poly [])`,
 288   REPEAT GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
 289   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 290   DISCH_THEN(X_CHOOSE_THEN `N2:num` (X_CHOOSE_TAC `i2:num->complex`)) THEN
 291   DISCH_THEN(X_CHOOSE_THEN `N1:num` (X_CHOOSE_TAC `i1:num->complex`)) THEN
 292   EXISTS_TAC `N1 + N2:num` THEN
 293   EXISTS_TAC `\n:num. if n < N1 then i1(n):complex else i2(n - N1)` THEN
 294   X_GEN_TAC `x:complex` THEN REWRITE_TAC[COMPLEX_ENTIRE; POLY_MUL] THEN
 295   DISCH_THEN(DISJ_CASES_THEN (ANTE_RES_THEN (X_CHOOSE_TAC `n:num`))) THENL
 296    [EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 297     FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN ARITH_TAC;
 298     EXISTS_TAC `N1 + n:num` THEN ASM_REWRITE_TAC[LT_ADD_LCANCEL] THEN
 299     REWRITE_TAC[ARITH_RULE `~(m + n < m:num)`] THEN
 300     AP_TERM_TAC THEN ARITH_TAC]);;
 301
 302 let POLY_ENTIRE = prove
 303  (`!p q. (poly (p ** q) = poly []) <=>
 304          (poly p = poly []) \/ (poly q = poly [])`,
 305   REPEAT GEN_TAC THEN EQ_TAC THENL
 306    [MESON_TAC[POLY_ENTIRE_LEMMA];
 307     REWRITE_TAC[FUN_EQ_THM; POLY_MUL] THEN
 308     STRIP_TAC THEN
 309     ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_MUL_LZERO; poly]]);;
 310
 311 let POLY_MUL_LCANCEL = prove
 312  (`!p q r. (poly (p ** q) = poly (p ** r)) <=>
 313            (poly p = poly []) \/ (poly q = poly r)`,
 314   let lemma1 = prove
 315    (`!p q. (poly (p ++ neg q) = poly []) <=> (poly p = poly q)`,
 316     REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_NEG; poly] THEN
 317     REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(p + --q = Cx(&0)) <=> (p = q)`]) in
 318   let lemma2 = prove
 319    (`!p q r. poly (p ** q ++ neg(p ** r)) = poly (p ** (q ++ neg(r)))`,
 320     REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_NEG; POLY_MUL] THEN
 321     SIMPLE_COMPLEX_ARITH_TAC) in
 322   ONCE_REWRITE_TAC[GSYM lemma1] THEN
 323   REWRITE_TAC[lemma2; POLY_ENTIRE] THEN
 324   REWRITE_TAC[lemma1]);;
 325
 326 let POLY_EXP_EQ_0 = prove
 327  (`!p n. (poly (p exp n) = poly []) <=> (poly p = poly []) /\ ~(n = 0)`,
 328   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 329   REWRITE_TAC[LEFT_AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
 330   SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 331   REWRITE_TAC[poly_exp; poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID;
 332     CX_INJ; REAL_OF_NUM_EQ; ARITH; NOT_SUC] THEN
 333   ASM_REWRITE_TAC[POLY_MUL; poly; COMPLEX_ENTIRE] THEN
 334   CONV_TAC TAUT);;
 335
 336 let POLY_PRIME_EQ_0 = prove
 337  (`!a. ~(poly [a ; Cx(&1)] = poly [])`,
 338   GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 339   DISCH_THEN(MP_TAC o SPEC `Cx(&1) - a`) THEN
 340   SIMPLE_COMPLEX_ARITH_TAC);;
 341
 342 let POLY_EXP_PRIME_EQ_0 = prove
 343  (`!a n. ~(poly ([a ; Cx(&1)] exp n) = poly [])`,
 344   MESON_TAC[POLY_EXP_EQ_0; POLY_PRIME_EQ_0]);;
 345
 346 (* ------------------------------------------------------------------------- *)
 347 (* Can also prove a more "constructive" notion of polynomial being trivial.  *)
 348 (* ------------------------------------------------------------------------- *)
 349
 350 let POLY_ZERO_LEMMA = prove
 351  (`!h t. (poly (CONS h t) = poly []) ==> (h = Cx(&0)) /\ (poly t = poly [])`,
 352   let lemma = REWRITE_RULE[FUN_EQ_THM; poly] POLY_ROOTS_FINITE in
 353   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; poly] THEN
 354   ASM_CASES_TAC `h = Cx(&0)` THEN ASM_REWRITE_TAC[] THENL
 355    [REWRITE_TAC[COMPLEX_ADD_LID];
 356     DISCH_THEN(MP_TAC o SPEC `Cx(&0)`) THEN
 357     POP_ASSUM MP_TAC THEN SIMPLE_COMPLEX_ARITH_TAC] THEN
 358   CONV_TAC CONTRAPOS_CONV THEN
 359   DISCH_THEN(MP_TAC o REWRITE_RULE[lemma]) THEN
 360   DISCH_THEN(X_CHOOSE_THEN `N:num` (X_CHOOSE_TAC `i:num->complex`)) THEN
 361   MP_TAC(SPECL
 362     [`i:num->complex`; `N:num`; `\x. poly t x = Cx(&0)`] FINITE_LEMMA) THEN
 363   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `a:real`) THEN
 364   DISCH_THEN(MP_TAC o SPEC `Cx(abs(a) + &1)`) THEN
 365   REWRITE_TAC[COMPLEX_ENTIRE; DE_MORGAN_THM] THEN CONJ_TAC THENL
 366    [REWRITE_TAC[CX_INJ] THEN REAL_ARITH_TAC;
 367     DISCH_THEN(MP_TAC o MATCH_MP
 368      (ASSUME `!x. (poly t x = Cx(&0)) ==> norm(x) < a`)) THEN
 369     REWRITE_TAC[COMPLEX_NORM_CX] THEN REAL_ARITH_TAC]);;
 370
 371 let POLY_ZERO = prove
 372  (`!p. (poly p = poly []) <=> ALL (\c. c = Cx(&0)) p`,
 373   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL] THEN EQ_TAC THENL
 374    [DISCH_THEN(MP_TAC o MATCH_MP POLY_ZERO_LEMMA) THEN ASM_REWRITE_TAC[];
 375     POP_ASSUM(SUBST1_TAC o SYM) THEN STRIP_TAC THEN
 376     ASM_REWRITE_TAC[FUN_EQ_THM; poly] THEN SIMPLE_COMPLEX_ARITH_TAC]);;
 377
 378 (* ------------------------------------------------------------------------- *)
 379 (* Basics of divisibility.                                                   *)
 380 (* ------------------------------------------------------------------------- *)
 381
 382 let divides = new_definition
 383   `p1 divides p2 <=> ?q. poly p2 = poly (p1 ** q)`;;
 384
 385 let POLY_PRIMES = prove
 386  (`!a p q. [a; Cx(&1)] divides (p ** q) <=>
 387            [a; Cx(&1)] divides p \/ [a; Cx(&1)] divides q`,
 388   REPEAT GEN_TAC THEN REWRITE_TAC[divides; POLY_MUL; FUN_EQ_THM; poly] THEN
 389   REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID; COMPLEX_MUL_RID] THEN
 390   EQ_TAC THENL
 391    [DISCH_THEN(X_CHOOSE_THEN `r:complex list` (MP_TAC o SPEC `--a`)) THEN
 392     REWRITE_TAC[COMPLEX_ENTIRE; GSYM complex_sub;
 393                 COMPLEX_SUB_REFL; COMPLEX_MUL_LZERO] THEN
 394     DISCH_THEN DISJ_CASES_TAC THENL [DISJ1_TAC; DISJ2_TAC] THEN
 395     (POP_ASSUM(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 396      REWRITE_TAC[COMPLEX_NEG_NEG] THEN
 397      DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC
 398         (X_CHOOSE_THEN `s:complex list` SUBST_ALL_TAC)) THENL
 399       [EXISTS_TAC `[]:complex list` THEN REWRITE_TAC[poly; COMPLEX_MUL_RZERO];
 400        EXISTS_TAC `s:complex list` THEN GEN_TAC THEN
 401        REWRITE_TAC[POLY_MUL; poly] THEN SIMPLE_COMPLEX_ARITH_TAC]);
 402     DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_TAC `s:complex list`)) THEN
 403     ASM_REWRITE_TAC[] THENL
 404      [EXISTS_TAC `s ** q`; EXISTS_TAC `p ** s`] THEN
 405     GEN_TAC THEN REWRITE_TAC[POLY_MUL] THEN SIMPLE_COMPLEX_ARITH_TAC]);;
 406
 407 let POLY_DIVIDES_REFL = prove
 408  (`!p. p divides p`,
 409   GEN_TAC THEN REWRITE_TAC[divides] THEN EXISTS_TAC `[Cx(&1)]` THEN
 410   REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 411
 412 let POLY_DIVIDES_TRANS = prove
 413  (`!p q r. p divides q /\ q divides r ==> p divides r`,
 414   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 415   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 416   DISCH_THEN(X_CHOOSE_THEN `s:complex list` ASSUME_TAC) THEN
 417   DISCH_THEN(X_CHOOSE_THEN `t:complex list` ASSUME_TAC) THEN
 418   EXISTS_TAC `t ** s` THEN
 419   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; COMPLEX_MUL_ASSOC]);;
 420
 421 let POLY_DIVIDES_EXP = prove
 422  (`!p m n. m <= n ==> (p exp m) divides (p exp n)`,
 423   REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
 424   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
 425   SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
 426   REWRITE_TAC[ADD_CLAUSES; POLY_DIVIDES_REFL] THEN
 427   MATCH_MP_TAC POLY_DIVIDES_TRANS THEN
 428   EXISTS_TAC `p exp (m + d)` THEN ASM_REWRITE_TAC[] THEN
 429   REWRITE_TAC[divides] THEN EXISTS_TAC `p:complex list` THEN
 430   REWRITE_TAC[poly_exp; FUN_EQ_THM; POLY_MUL] THEN
 431   SIMPLE_COMPLEX_ARITH_TAC);;
 432
 433 let POLY_EXP_DIVIDES = prove
 434  (`!p q m n. (p exp n) divides q /\ m <= n ==> (p exp m) divides q`,
 435   MESON_TAC[POLY_DIVIDES_TRANS; POLY_DIVIDES_EXP]);;
 436
 437 let POLY_DIVIDES_ADD = prove
 438  (`!p q r. p divides q /\ p divides r ==> p divides (q ++ r)`,
 439   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 440   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 441   DISCH_THEN(X_CHOOSE_THEN `s:complex list` ASSUME_TAC) THEN
 442   DISCH_THEN(X_CHOOSE_THEN `t:complex list` ASSUME_TAC) THEN
 443   EXISTS_TAC `t ++ s` THEN
 444   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_MUL] THEN
 445   SIMPLE_COMPLEX_ARITH_TAC);;
 446
 447 let POLY_DIVIDES_SUB = prove
 448  (`!p q r. p divides q /\ p divides (q ++ r) ==> p divides r`,
 449   REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
 450   DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
 451   DISCH_THEN(X_CHOOSE_THEN `s:complex list` ASSUME_TAC) THEN
 452   DISCH_THEN(X_CHOOSE_THEN `t:complex list` ASSUME_TAC) THEN
 453   EXISTS_TAC `s ++ neg(t)` THEN
 454   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
 455   REWRITE_TAC[FUN_EQ_THM; POLY_ADD; POLY_MUL; POLY_NEG] THEN
 456   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 457   REWRITE_TAC[COMPLEX_ADD_LDISTRIB; COMPLEX_MUL_RNEG] THEN
 458   ASM_REWRITE_TAC[] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 459
 460 let POLY_DIVIDES_SUB2 = prove
 461  (`!p q r. p divides r /\ p divides (q ++ r) ==> p divides q`,
 462   REPEAT STRIP_TAC THEN MATCH_MP_TAC POLY_DIVIDES_SUB THEN
 463   EXISTS_TAC `r:complex list` THEN ASM_REWRITE_TAC[] THEN
 464   UNDISCH_TAC `p divides (q ++ r)` THEN
 465   REWRITE_TAC[divides; POLY_ADD; FUN_EQ_THM; POLY_MUL] THEN
 466   DISCH_THEN(X_CHOOSE_TAC `s:complex list`) THEN
 467   EXISTS_TAC `s:complex list` THEN
 468   X_GEN_TAC `x:complex` THEN POP_ASSUM(MP_TAC o SPEC `x:complex`) THEN
 469   SIMPLE_COMPLEX_ARITH_TAC);;
 470
 471 let POLY_DIVIDES_ZERO = prove
 472  (`!p q. (poly p = poly []) ==> q divides p`,
 473   REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[divides] THEN
 474   EXISTS_TAC `[]:complex list` THEN
 475   ASM_REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO]);;
 476
 477 (* ------------------------------------------------------------------------- *)
 478 (* At last, we can consider the order of a root.                             *)
 479 (* ------------------------------------------------------------------------- *)
 480
 481 let POLY_ORDER_EXISTS = prove
 482  (`!a d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
 483              ==> ?n. ([--a; Cx(&1)] exp n) divides p /\
 484                      ~(([--a; Cx(&1)] exp (SUC n)) divides p)`,
 485   GEN_TAC THEN
 486   (STRIP_ASSUME_TAC o prove_recursive_functions_exist num_RECURSION)
 487     `(!p q. mulexp 0 p q = q) /\
 488      (!p q n. mulexp (SUC n) p q = p ** (mulexp n p q))` THEN
 489   SUBGOAL_THEN
 490    `!d. !p. (LENGTH p = d) /\ ~(poly p = poly [])
 491            ==> ?n q. (p = mulexp (n:num) [--a; Cx(&1)] q) /\
 492                      ~(poly q a = Cx(&0))`
 493   MP_TAC THENL
 494    [INDUCT_TAC THENL
 495      [REWRITE_TAC[LENGTH_EQ_NIL] THEN MESON_TAC[]; ALL_TAC] THEN
 496     X_GEN_TAC `p:complex list` THEN
 497     ASM_CASES_TAC `poly p a = Cx(&0)` THENL
 498      [STRIP_TAC THEN UNDISCH_TAC `poly p a = Cx(&0)` THEN
 499       DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 500       DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 501       DISCH_THEN(X_CHOOSE_THEN `q:complex list` SUBST_ALL_TAC) THEN
 502       UNDISCH_TAC
 503        `!p. (LENGTH p = d) /\ ~(poly p = poly [])
 504             ==> ?n q. (p = mulexp (n:num) [--a; Cx(&1)] q) /\
 505                       ~(poly q a = Cx(&0))` THEN
 506       DISCH_THEN(MP_TAC o SPEC `q:complex list`) THEN
 507       RULE_ASSUM_TAC(REWRITE_RULE[POLY_LENGTH_MUL; POLY_ENTIRE;
 508         DE_MORGAN_THM; SUC_INJ]) THEN
 509       ASM_REWRITE_TAC[] THEN
 510       DISCH_THEN(X_CHOOSE_THEN `n:num`
 511        (X_CHOOSE_THEN `s:complex list` STRIP_ASSUME_TAC)) THEN
 512       EXISTS_TAC `SUC n` THEN EXISTS_TAC `s:complex list` THEN
 513       ASM_REWRITE_TAC[];
 514       STRIP_TAC THEN EXISTS_TAC `0` THEN EXISTS_TAC `p:complex list` THEN
 515       ASM_REWRITE_TAC[]];
 516     DISCH_TAC THEN REPEAT GEN_TAC THEN
 517     DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
 518     DISCH_THEN(X_CHOOSE_THEN `n:num`
 519        (X_CHOOSE_THEN `s:complex list` STRIP_ASSUME_TAC)) THEN
 520     EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 521     REWRITE_TAC[divides] THEN CONJ_TAC THENL
 522      [EXISTS_TAC `s:complex list` THEN
 523       SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 524       ASM_REWRITE_TAC[poly_exp; FUN_EQ_THM; POLY_MUL; poly] THEN
 525       SIMPLE_COMPLEX_ARITH_TAC;
 526       DISCH_THEN(X_CHOOSE_THEN `r:complex list` MP_TAC) THEN
 527       SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 528       ASM_REWRITE_TAC[] THENL
 529        [UNDISCH_TAC `~(poly s a = Cx(&0))` THEN CONV_TAC CONTRAPOS_CONV THEN
 530         REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
 531         REWRITE_TAC[poly; poly_exp; POLY_MUL] THEN SIMPLE_COMPLEX_ARITH_TAC;
 532         REWRITE_TAC[] THEN ONCE_ASM_REWRITE_TAC[] THEN
 533         ONCE_REWRITE_TAC[poly_exp] THEN
 534         REWRITE_TAC[GSYM POLY_MUL_ASSOC; POLY_MUL_LCANCEL] THEN
 535         REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THENL
 536          [REWRITE_TAC[FUN_EQ_THM] THEN
 537           DISCH_THEN(MP_TAC o SPEC `a + Cx(&1)`) THEN
 538           REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC;
 539           DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[]]]]]);;
 540
 541 let POLY_ORDER = prove
 542  (`!p a. ~(poly p = poly [])
 543          ==> ?!n. ([--a; Cx(&1)] exp n) divides p /\
 544                       ~(([--a; Cx(&1)] exp (SUC n)) divides p)`,
 545   MESON_TAC[POLY_ORDER_EXISTS; POLY_EXP_DIVIDES; LE_SUC_LT; LT_CASES]);;
 546
 547 (* ------------------------------------------------------------------------- *)
 548 (* Definition of order.                                                      *)
 549 (* ------------------------------------------------------------------------- *)
 550
 551 let order = new_definition
 552   `order a p = @n. ([--a; Cx(&1)] exp n) divides p /\
 553                    ~(([--a; Cx(&1)] exp (SUC n)) divides p)`;;
 554
 555 let ORDER = prove
 556  (`!p a n. ([--a; Cx(&1)] exp n) divides p /\
 557            ~(([--a; Cx(&1)] exp (SUC n)) divides p) <=>
 558            (n = order a p) /\
 559            ~(poly p = poly [])`,
 560   REPEAT GEN_TAC THEN REWRITE_TAC[order] THEN
 561   EQ_TAC THEN STRIP_TAC THENL
 562    [SUBGOAL_THEN `~(poly p = poly [])` ASSUME_TAC THENL
 563      [FIRST_ASSUM(UNDISCH_TAC o check is_neg o concl) THEN
 564       CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[divides] THEN
 565       DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `[]:complex list` THEN
 566       REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO];
 567       ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN
 568       MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[]];
 569     ONCE_ASM_REWRITE_TAC[] THEN CONV_TAC SELECT_CONV] THEN
 570   ASM_MESON_TAC[POLY_ORDER]);;
 571
 572 let ORDER_THM = prove
 573  (`!p a. ~(poly p = poly [])
 574          ==> ([--a; Cx(&1)] exp (order a p)) divides p /\
 575              ~(([--a; Cx(&1)] exp (SUC(order a p))) divides p)`,
 576   MESON_TAC[ORDER]);;
 577
 578 let ORDER_UNIQUE = prove
 579  (`!p a n. ~(poly p = poly []) /\
 580            ([--a; Cx(&1)] exp n) divides p /\
 581            ~(([--a; Cx(&1)] exp (SUC n)) divides p)
 582            ==> (n = order a p)`,
 583   MESON_TAC[ORDER]);;
 584
 585 let ORDER_POLY = prove
 586  (`!p q a. (poly p = poly q) ==> (order a p = order a q)`,
 587   REPEAT STRIP_TAC THEN
 588   ASM_REWRITE_TAC[order; divides; FUN_EQ_THM; POLY_MUL]);;
 589
 590 let ORDER_ROOT = prove
 591  (`!p a. (poly p a = Cx(&0)) <=> (poly p = poly []) \/ ~(order a p = 0)`,
 592   REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN
 593   ASM_REWRITE_TAC[poly] THEN EQ_TAC THENL
 594    [DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN
 595     ASM_CASES_TAC `p:complex list = []` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 596     ASM_REWRITE_TAC[] THEN
 597     DISCH_THEN(X_CHOOSE_THEN `q:complex list` SUBST_ALL_TAC) THEN DISCH_TAC THEN
 598     FIRST_ASSUM(MP_TAC o SPEC `a:complex` o MATCH_MP ORDER_THM) THEN
 599     ASM_REWRITE_TAC[poly_exp; DE_MORGAN_THM] THEN DISJ2_TAC THEN
 600     REWRITE_TAC[divides] THEN EXISTS_TAC `q:complex list` THEN
 601     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly] THEN SIMPLE_COMPLEX_ARITH_TAC;
 602     DISCH_TAC THEN
 603     FIRST_ASSUM(MP_TAC o SPEC `a:complex` o MATCH_MP ORDER_THM) THEN
 604     UNDISCH_TAC `~(order a p = 0)` THEN
 605     SPEC_TAC(`order a p`,`n:num`) THEN
 606     INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp; NOT_SUC] THEN
 607     DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[divides] THEN
 608     DISCH_THEN(X_CHOOSE_THEN `s:complex list` SUBST1_TAC) THEN
 609     REWRITE_TAC[POLY_MUL; poly] THEN SIMPLE_COMPLEX_ARITH_TAC]);;
 610
 611 let ORDER_DIVIDES = prove
 612  (`!p a n. ([--a; Cx(&1)] exp n) divides p <=>
 613            (poly p = poly []) \/ n <= order a p`,
 614   REPEAT GEN_TAC THEN ASM_CASES_TAC `poly p = poly []` THEN
 615   ASM_REWRITE_TAC[] THENL
 616    [ASM_REWRITE_TAC[divides] THEN EXISTS_TAC `[]:complex list` THEN
 617     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO];
 618     ASM_MESON_TAC[ORDER_THM; POLY_EXP_DIVIDES; NOT_LE; LE_SUC_LT]]);;
 619
 620 let ORDER_DECOMP = prove
 621  (`!p a. ~(poly p = poly [])
 622          ==> ?q. (poly p = poly (([--a; Cx(&1)] exp (order a p)) ** q)) /\
 623                  ~([--a; Cx(&1)] divides q)`,
 624   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_THM) THEN
 625   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC o SPEC `a:complex`) THEN
 626   DISCH_THEN(X_CHOOSE_TAC `q:complex list` o REWRITE_RULE[divides]) THEN
 627   EXISTS_TAC `q:complex list` THEN ASM_REWRITE_TAC[] THEN
 628   DISCH_THEN(X_CHOOSE_TAC `r: complex list` o REWRITE_RULE[divides]) THEN
 629   UNDISCH_TAC `~([-- a; Cx(&1)] exp SUC (order a p) divides p)` THEN
 630   ASM_REWRITE_TAC[] THEN REWRITE_TAC[divides] THEN
 631   EXISTS_TAC `r:complex list` THEN
 632   ASM_REWRITE_TAC[POLY_MUL; FUN_EQ_THM; poly_exp] THEN
 633   SIMPLE_COMPLEX_ARITH_TAC);;
 634
 635 (* ------------------------------------------------------------------------- *)
 636 (* Important composition properties of orders.                               *)
 637 (* ------------------------------------------------------------------------- *)
 638
 639 let ORDER_MUL = prove
 640  (`!a p q. ~(poly (p ** q) = poly []) ==>
 641            (order a (p ** q) = order a p + order a q)`,
 642   REPEAT GEN_TAC THEN
 643   DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
 644   REWRITE_TAC[POLY_ENTIRE; DE_MORGAN_THM] THEN STRIP_TAC THEN
 645   SUBGOAL_THEN `(order a p + order a q = order a (p ** q)) /\
 646                 ~(poly (p ** q) = poly [])`
 647   MP_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 648   REWRITE_TAC[GSYM ORDER] THEN CONJ_TAC THENL
 649    [MP_TAC(CONJUNCT1 (SPEC `a:complex`
 650       (MATCH_MP ORDER_THM (ASSUME `~(poly p = poly [])`)))) THEN
 651     DISCH_THEN(X_CHOOSE_TAC `r: complex list` o REWRITE_RULE[divides]) THEN
 652     MP_TAC(CONJUNCT1 (SPEC `a:complex`
 653       (MATCH_MP ORDER_THM (ASSUME `~(poly q = poly [])`)))) THEN
 654     DISCH_THEN(X_CHOOSE_TAC `s: complex list` o REWRITE_RULE[divides]) THEN
 655     REWRITE_TAC[divides; FUN_EQ_THM] THEN EXISTS_TAC `s ** r` THEN
 656     ASM_REWRITE_TAC[POLY_MUL; POLY_EXP_ADD] THEN SIMPLE_COMPLEX_ARITH_TAC;
 657     X_CHOOSE_THEN `r: complex list` STRIP_ASSUME_TAC
 658     (SPEC `a:complex` (MATCH_MP ORDER_DECOMP
 659        (ASSUME `~(poly p = poly [])`))) THEN
 660     X_CHOOSE_THEN `s: complex list` STRIP_ASSUME_TAC
 661     (SPEC `a:complex` (MATCH_MP ORDER_DECOMP
 662        (ASSUME `~(poly q = poly [])`))) THEN
 663     ASM_REWRITE_TAC[divides; FUN_EQ_THM; POLY_EXP_ADD; POLY_MUL; poly_exp] THEN
 664     DISCH_THEN(X_CHOOSE_THEN `t:complex list` STRIP_ASSUME_TAC) THEN
 665     SUBGOAL_THEN `[--a; Cx(&1)] divides (r ** s)` MP_TAC THENL
 666      [ALL_TAC; ASM_REWRITE_TAC[POLY_PRIMES]] THEN
 667     REWRITE_TAC[divides] THEN EXISTS_TAC `t:complex list` THEN
 668     SUBGOAL_THEN `poly ([-- a; Cx(&1)] exp (order a p) ** r ** s) =
 669                   poly ([-- a; Cx(&1)] exp (order a p) **
 670                        ([-- a; Cx(&1)] ** t))`
 671     MP_TAC THENL
 672      [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN
 673     SUBGOAL_THEN `poly ([-- a; Cx(&1)] exp (order a q) **
 674                         [-- a; Cx(&1)] exp (order a p) ** r ** s) =
 675                   poly ([-- a; Cx(&1)] exp (order a q) **
 676                         [-- a; Cx(&1)] exp (order a p) **
 677                         [-- a; Cx(&1)] ** t)`
 678     MP_TAC THENL
 679      [ALL_TAC; MESON_TAC[POLY_MUL_LCANCEL; POLY_EXP_PRIME_EQ_0]] THEN
 680     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_ADD] THEN
 681     FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 682     REWRITE_TAC[COMPLEX_MUL_AC]]);;
 683
 684 (* ------------------------------------------------------------------------- *)
 685 (* Normalization of a polynomial.                                            *)
 686 (* ------------------------------------------------------------------------- *)
 687
 688 let normalize = new_recursive_definition list_RECURSION
 689   `(normalize [] = []) /\
 690    (normalize (CONS h t) =
 691         if normalize t = [] then if h = Cx(&0) then [] else [h]
 692         else CONS h (normalize t))`;;
 693
 694 let POLY_NORMALIZE = prove
 695  (`!p. poly (normalize p) = poly p`,
 696   LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; poly] THEN
 697   ASM_CASES_TAC `h = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
 698   COND_CASES_TAC THEN ASM_REWRITE_TAC[poly; FUN_EQ_THM] THEN
 699   UNDISCH_TAC `poly (normalize t) = poly t` THEN
 700   DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN
 701   REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_LID]);;
 702
 703 let LENGTH_NORMALIZE_LE = prove
 704  (`!p. LENGTH(normalize p) <= LENGTH p`,
 705   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; normalize; LE_REFL] THEN
 706   COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; LE_SUC] THEN
 707   COND_CASES_TAC THEN REWRITE_TAC[LENGTH] THEN ARITH_TAC);;
 708
 709 (* ------------------------------------------------------------------------- *)
 710 (* The degree of a polynomial.                                               *)
 711 (* ------------------------------------------------------------------------- *)
 712
 713 let degree = new_definition
 714   `degree p = PRE(LENGTH(normalize p))`;;
 715
 716 let DEGREE_ZERO = prove
 717  (`!p. (poly p = poly []) ==> (degree p = 0)`,
 718   REPEAT STRIP_TAC THEN REWRITE_TAC[degree] THEN
 719   SUBGOAL_THEN `normalize p = []` SUBST1_TAC THENL
 720    [POP_ASSUM MP_TAC THEN SPEC_TAC(`p:complex list`,`p:complex list`) THEN
 721     REWRITE_TAC[POLY_ZERO] THEN
 722     LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; ALL] THEN
 723     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 724     SUBGOAL_THEN `normalize t = []` (fun th -> REWRITE_TAC[th]) THEN
 725     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 726     REWRITE_TAC[LENGTH; PRE]]);;
 727
 728 (* ------------------------------------------------------------------------- *)
 729 (* Show that the degree is welldefined.                                      *)
 730 (* ------------------------------------------------------------------------- *)
 731
 732 let POLY_CONS_EQ = prove
 733  (`(poly (CONS h1 t1) = poly (CONS h2 t2)) <=>
 734    (h1 = h2) /\ (poly t1 = poly t2)`,
 735   REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL [ALL_TAC; SIMP_TAC[poly]] THEN
 736   ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(a = b) <=> (a + --b = Cx(&0))`] THEN
 737   REWRITE_TAC[GSYM POLY_NEG; GSYM POLY_ADD] THEN DISCH_TAC THEN
 738   SUBGOAL_THEN `poly (CONS h1 t1 ++ neg(CONS h2 t2)) = poly []` MP_TAC THENL
 739    [ASM_REWRITE_TAC[poly; FUN_EQ_THM]; ALL_TAC] THEN
 740   REWRITE_TAC[poly_neg; poly_cmul; poly_add; NOT_CONS_NIL; HD; TL] THEN
 741   DISCH_THEN(MP_TAC o MATCH_MP POLY_ZERO_LEMMA) THEN
 742   SIMP_TAC[poly; COMPLEX_MUL_LNEG; COMPLEX_MUL_LID]);;
 743
 744 let POLY_NORMALIZE_ZERO = prove
 745  (`!p. (poly p = poly []) <=> (normalize p = [])`,
 746   REWRITE_TAC[POLY_ZERO] THEN
 747   LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; normalize] THEN
 748   ASM_CASES_TAC `normalize t = []` THEN ASM_REWRITE_TAC[] THEN
 749   REWRITE_TAC[NOT_CONS_NIL] THEN
 750   COND_CASES_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL]);;
 751
 752 let POLY_NORMALIZE_EQ_LEMMA = prove
 753  (`!p q. (poly p = poly q) ==> (normalize p = normalize q)`,
 754   LIST_INDUCT_TAC THENL
 755    [MESON_TAC[POLY_NORMALIZE_ZERO]; ALL_TAC] THEN
 756   LIST_INDUCT_TAC THENL
 757    [MESON_TAC[POLY_NORMALIZE_ZERO]; ALL_TAC] THEN
 758   REWRITE_TAC[POLY_CONS_EQ] THEN
 759   STRIP_TAC THEN ASM_REWRITE_TAC[normalize] THEN
 760   FIRST_X_ASSUM(MP_TAC o SPEC `t':complex list`) THEN ASM_REWRITE_TAC[] THEN
 761   DISCH_THEN SUBST1_TAC THEN REFL_TAC);;
 762
 763 let POLY_NORMALIZE_EQ = prove
 764  (`!p q. (poly p = poly q) <=> (normalize p = normalize q)`,
 765   MESON_TAC[POLY_NORMALIZE_EQ_LEMMA; POLY_NORMALIZE]);;
 766
 767 let DEGREE_WELLDEF = prove
 768  (`!p q. (poly p = poly q) ==> (degree p = degree q)`,
 769   SIMP_TAC[degree; POLY_NORMALIZE_EQ]);;
 770
 771 (* ------------------------------------------------------------------------- *)
 772 (* Degree of a product with a power of linear terms.                         *)
 773 (* ------------------------------------------------------------------------- *)
 774
 775 let NORMALIZE_EQ = prove
 776  (`!p. ~(LAST p = Cx(&0)) ==> (normalize p = p)`,
 777   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[NOT_CONS_NIL] THEN
 778   REWRITE_TAC[normalize; LAST] THEN REPEAT GEN_TAC THEN
 779   REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[normalize]));;
 780
 781 let NORMAL_DEGREE = prove
 782  (`!p. ~(LAST p = Cx(&0)) ==> (degree p = LENGTH p - 1)`,
 783   SIMP_TAC[degree; NORMALIZE_EQ] THEN REPEAT STRIP_TAC THEN ARITH_TAC);;
 784
 785 let LAST_LINEAR_MUL_LEMMA = prove
 786  (`!p a b x.
 787      LAST(a ## p ++ CONS x (b ## p)) = if p = [] then x else b * LAST(p)`,
 788   LIST_INDUCT_TAC THEN
 789   REWRITE_TAC[poly_cmul; poly_add; LAST; HD; TL; NOT_CONS_NIL] THEN
 790   REPEAT GEN_TAC THEN
 791   SUBGOAL_THEN `~(a ## t ++ CONS (b * h) (b ## t) = [])`
 792   ASSUME_TAC THENL
 793    [SPEC_TAC(`t:complex list`,`t:complex list`) THEN
 794     LIST_INDUCT_TAC THEN REWRITE_TAC[poly_cmul; poly_add; NOT_CONS_NIL];
 795     ALL_TAC] THEN
 796   ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
 797
 798 let LAST_LINEAR_MUL = prove
 799  (`!p. ~(p = []) ==> (LAST([a; Cx(&1)] ** p) = LAST p)`,
 800   SIMP_TAC[poly_mul; NOT_CONS_NIL; LAST_LINEAR_MUL_LEMMA; COMPLEX_MUL_LID]);;
 801
 802 let NORMAL_NORMALIZE = prove
 803  (`!p. ~(normalize p = []) ==> ~(LAST(normalize p) = Cx(&0))`,
 804   LIST_INDUCT_TAC THEN REWRITE_TAC[normalize] THEN
 805   POP_ASSUM MP_TAC THEN ASM_CASES_TAC `normalize t = []` THEN
 806   ASM_REWRITE_TAC[LAST; NOT_CONS_NIL] THEN
 807   COND_CASES_TAC THEN ASM_REWRITE_TAC[LAST]);;
 808
 809 let LINEAR_MUL_DEGREE = prove
 810  (`!p a. ~(poly p = poly []) ==> (degree([a; Cx(&1)] ** p) = degree(p) + 1)`,
 811   REPEAT STRIP_TAC THEN
 812   SUBGOAL_THEN `degree([a; Cx(&1)] ** normalize p) = degree(normalize p) + 1`
 813   MP_TAC THENL
 814    [FIRST_ASSUM(ASSUME_TAC o
 815       GEN_REWRITE_RULE RAND_CONV [POLY_NORMALIZE_ZERO]) THEN
 816     FIRST_ASSUM(MP_TAC o MATCH_MP NORMAL_NORMALIZE) THEN
 817     FIRST_ASSUM(MP_TAC o MATCH_MP LAST_LINEAR_MUL) THEN
 818     SIMP_TAC[NORMAL_DEGREE] THEN REPEAT STRIP_TAC THEN
 819     SUBST1_TAC(SYM(SPEC `a:complex` COMPLEX_NEG_NEG)) THEN
 820     REWRITE_TAC[POLY_LENGTH_MUL] THEN
 821     UNDISCH_TAC `~(normalize p = [])` THEN
 822     SPEC_TAC(`normalize p`,`p:complex list`) THEN
 823     LIST_INDUCT_TAC THEN REWRITE_TAC[NOT_CONS_NIL; LENGTH] THEN ARITH_TAC;
 824     MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THEN
 825     TRY(AP_THM_TAC THEN AP_TERM_TAC) THEN MATCH_MP_TAC DEGREE_WELLDEF THEN
 826     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; POLY_NORMALIZE]]);;
 827
 828 let LINEAR_POW_MUL_DEGREE = prove
 829  (`!n a p. degree([a; Cx(&1)] exp n ** p) =
 830                 if poly p = poly [] then 0 else degree p + n`,
 831   INDUCT_TAC THEN REWRITE_TAC[poly_exp] THENL
 832    [GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 833      [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `degree(p)` THEN CONJ_TAC THENL
 834        [MATCH_MP_TAC DEGREE_WELLDEF THEN
 835         REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO;
 836                     COMPLEX_ADD_RID; COMPLEX_MUL_LID];
 837         MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `degree []` THEN CONJ_TAC THENL
 838          [MATCH_MP_TAC DEGREE_WELLDEF THEN ASM_REWRITE_TAC[];
 839           REWRITE_TAC[degree; LENGTH; normalize; ARITH]]];
 840       REWRITE_TAC[ADD_CLAUSES] THEN MATCH_MP_TAC DEGREE_WELLDEF THEN
 841       REWRITE_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO;
 842                   COMPLEX_ADD_RID; COMPLEX_MUL_LID]];
 843     ALL_TAC] THEN
 844   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 845   EXISTS_TAC `degree([a; Cx (&1)] exp n ** ([a; Cx (&1)] ** p))` THEN
 846   CONJ_TAC THENL
 847    [MATCH_MP_TAC DEGREE_WELLDEF THEN
 848     REWRITE_TAC[FUN_EQ_THM; POLY_MUL; COMPLEX_MUL_AC]; ALL_TAC] THEN
 849   ASM_REWRITE_TAC[POLY_ENTIRE] THEN
 850   ASM_CASES_TAC `poly p = poly []` THEN ASM_REWRITE_TAC[] THEN
 851   ASM_SIMP_TAC[LINEAR_MUL_DEGREE] THEN
 852   SUBGOAL_THEN `~(poly [a; Cx (&1)] = poly [])`
 853    (fun th -> REWRITE_TAC[th] THEN ARITH_TAC) THEN
 854   REWRITE_TAC[POLY_NORMALIZE_EQ] THEN
 855   REWRITE_TAC[normalize; CX_INJ; REAL_OF_NUM_EQ; ARITH; NOT_CONS_NIL]);;
 856
 857 (* ------------------------------------------------------------------------- *)
 858 (* Show that the order of a root (or nonroot!) is bounded by degree.         *)
 859 (* ------------------------------------------------------------------------- *)
 860
 861 let ORDER_DEGREE = prove
 862  (`!a p. ~(poly p = poly []) ==> order a p <= degree p`,
 863   REPEAT STRIP_TAC THEN
 864   FIRST_ASSUM(MP_TAC o SPEC `a:complex` o MATCH_MP ORDER_THM) THEN
 865   DISCH_THEN(MP_TAC o REWRITE_RULE[divides] o CONJUNCT1) THEN
 866   DISCH_THEN(X_CHOOSE_THEN `q:complex list` ASSUME_TAC) THEN
 867   FIRST_ASSUM(SUBST1_TAC o MATCH_MP DEGREE_WELLDEF) THEN
 868   ASM_REWRITE_TAC[LINEAR_POW_MUL_DEGREE] THEN
 869   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
 870   COND_CASES_TAC THEN ASM_REWRITE_TAC[POLY_MUL] THENL
 871    [UNDISCH_TAC `~(poly p = poly [])` THEN
 872     SIMP_TAC[FUN_EQ_THM; POLY_MUL; poly; COMPLEX_MUL_RZERO];
 873     DISCH_TAC THEN ARITH_TAC]);;
 874
 875 (* ------------------------------------------------------------------------- *)
 876 (* Tidier versions of finiteness of roots.                                   *)
 877 (* ------------------------------------------------------------------------- *)
 878
 879 let POLY_ROOTS_FINITE_SET = prove
 880  (`!p. ~(poly p = poly []) ==> FINITE { x | poly p x = Cx(&0)}`,
 881   GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN
 882   DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC) THEN
 883   DISCH_THEN(X_CHOOSE_THEN `i:num->complex` ASSUME_TAC) THEN
 884   MATCH_MP_TAC FINITE_SUBSET THEN
 885   EXISTS_TAC `{x:complex | ?n:num. n < N /\ (x = i n)}` THEN
 886   CONJ_TAC THENL
 887    [SPEC_TAC(`N:num`,`N:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 888     INDUCT_TAC THENL
 889      [SUBGOAL_THEN `{x:complex | ?n. n < 0 /\ (x = i n)} = {}`
 890       (fun th -> REWRITE_TAC[th; FINITE_RULES]) THEN
 891       REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY; LT];
 892       SUBGOAL_THEN `{x:complex | ?n. n < SUC N /\ (x = i n)} =
 893                     (i N) INSERT {x:complex | ?n. n < N /\ (x = i n)}`
 894       SUBST1_TAC THENL
 895        [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; LT] THEN MESON_TAC[];
 896         MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN ASM_REWRITE_TAC[]]];
 897     ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM]]);;
 898
 899 (* ------------------------------------------------------------------------- *)
 900 (* Conversions to perform operations if coefficients are rational constants. *)
 901 (* ------------------------------------------------------------------------- *)
 902
 903 let COMPLEX_RAT_MUL_CONV =
 904   GEN_REWRITE_CONV I [GSYM CX_MUL] THENC RAND_CONV REAL_RAT_MUL_CONV;;
 905
 906 let COMPLEX_RAT_ADD_CONV =
 907   GEN_REWRITE_CONV I [GSYM CX_ADD] THENC RAND_CONV REAL_RAT_ADD_CONV;;
 908
 909 let COMPLEX_RAT_EQ_CONV =
 910   GEN_REWRITE_CONV I [CX_INJ] THENC REAL_RAT_EQ_CONV;;
 911
 912 let POLY_CMUL_CONV =
 913   let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul]
 914   and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul] in
 915   let rec POLY_CMUL_CONV tm =
 916    (cmul_conv0 ORELSEC
 917     (cmul_conv1 THENC
 918      LAND_CONV COMPLEX_RAT_MUL_CONV THENC
 919      RAND_CONV POLY_CMUL_CONV)) tm in
 920   POLY_CMUL_CONV;;
 921
 922 let POLY_ADD_CONV =
 923   let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES))
 924   and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)] in
 925   let rec POLY_ADD_CONV tm =
 926    (add_conv0 ORELSEC
 927     (add_conv1 THENC
 928      LAND_CONV COMPLEX_RAT_ADD_CONV THENC
 929      RAND_CONV POLY_ADD_CONV)) tm in
 930   POLY_ADD_CONV;;
 931
 932 let POLY_MUL_CONV =
 933   let mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES]
 934   and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)]
 935   and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)] in
 936   let rec POLY_MUL_CONV tm =
 937    (mul_conv0 ORELSEC
 938     (mul_conv1 THENC POLY_CMUL_CONV) ORELSEC
 939     (mul_conv2 THENC
 940      LAND_CONV POLY_CMUL_CONV THENC
 941      RAND_CONV(RAND_CONV POLY_MUL_CONV) THENC
 942      POLY_ADD_CONV)) tm in
 943   POLY_MUL_CONV;;
 944
 945 let POLY_NORMALIZE_CONV =
 946   let pth = prove
 947    (`normalize (CONS h t) =
 948       (\n. if n = [] then if h = Cx(&0) then [] else [h] else CONS h n)
 949       (normalize t)`,
 950     REWRITE_TAC[normalize]) in
 951   let norm_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 normalize]
 952   and norm_conv1 = GEN_REWRITE_CONV I [pth]
 953   and norm_conv2 = GEN_REWRITE_CONV DEPTH_CONV
 954    [COND_CLAUSES; NOT_CONS_NIL; EQT_INTRO(SPEC_ALL EQ_REFL)] in
 955   let rec POLY_NORMALIZE_CONV tm =
 956    (norm_conv0 ORELSEC
 957     (norm_conv1 THENC
 958      RAND_CONV POLY_NORMALIZE_CONV THENC
 959      BETA_CONV THENC
 960      RATOR_CONV(RAND_CONV(RATOR_CONV(LAND_CONV COMPLEX_RAT_EQ_CONV))) THENC
 961      norm_conv2)) tm in
 962   POLY_NORMALIZE_CONV;;
 963
 964 (* ------------------------------------------------------------------------- *)
 965 (* Now we're finished with polynomials...                                    *)
 966 (* ------------------------------------------------------------------------- *)
 967
 968 (************** keep this for now
 969
 970 do_list reduce_interface
 971  ["divides",`poly_divides:complex list->complex list->bool`;
 972   "exp",`poly_exp:complex list -> num -> complex list`;
 973   "diff",`poly_diff:complex list->complex list`];;
 974
 975 unparse_as_infix "exp";;
 976
 977  ****************)