Multivariate/complexes.ml

   1 (* ========================================================================= *)
   2 (* The type "real^2" regarded as the complex numbers.                        *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2008                       *)
   5 (*              (c) Copyright, Valentina Bruno 2010                          *)
   6 (* ========================================================================= *)
   7
   8 needs "Multivariate/integration.ml";;
   9
  10 new_type_abbrev("complex",`:real^2`);;
  11
  12 let prioritize_complex() =
  13   overload_interface("--",`vector_neg:complex->complex`);
  14   overload_interface("+",`vector_add:complex->complex->complex`);
  15   overload_interface("-",`vector_sub:complex->complex->complex`);
  16   overload_interface("*",`complex_mul:complex->complex->complex`);
  17   overload_interface("/",`complex_div:complex->complex->complex`);
  18   overload_interface("pow",`complex_pow:complex->num->complex`);
  19   overload_interface("inv",`complex_inv:complex->complex`);;
  20
  21 prioritize_complex();;
  22
  23 (* ------------------------------------------------------------------------- *)
  24 (* Real and imaginary parts of a number.                                     *)
  25 (* ------------------------------------------------------------------------- *)
  26
  27 let RE_DEF = new_definition
  28   `Re(z:complex) = z$1`;;
  29
  30 let IM_DEF = new_definition
  31   `Im(z:complex) = z$2`;;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Real injection and imaginary unit.                                        *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let complex = new_definition
  38  `complex(x,y) = vector[x;y]:complex`;;
  39
  40 let CX_DEF = new_definition
  41  `Cx(a) = complex(a,&0)`;;
  42
  43 let ii = new_definition
  44   `ii = complex(&0,&1)`;;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Complex multiplication.                                                   *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let complex_mul = new_definition
  51   `w * z = complex(Re(w) * Re(z) - Im(w) * Im(z),
  52                    Re(w) * Im(z) + Im(w) * Re(z))`;;
  53
  54 let complex_inv = new_definition
  55   `inv(z) = complex(Re(z) / (Re(z) pow 2 + Im(z) pow 2),
  56                     --(Im(z)) / (Re(z) pow 2 + Im(z) pow 2))`;;
  57
  58 let complex_div = new_definition
  59   `w / z = w * inv(z)`;;
  60
  61 let complex_pow = define
  62   `(x pow 0 = Cx(&1)) /\
  63    (!n. x pow (SUC n) = x * x pow n)`;;
  64
  65 (* ------------------------------------------------------------------------- *)
  66 (* Various handy rewrites.                                                   *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let RE = prove
  70  (`(Re(complex(x,y)) = x)`,
  71   REWRITE_TAC[RE_DEF; complex; VECTOR_2]);;
  72
  73 let IM = prove
  74  (`Im(complex(x,y)) = y`,
  75   REWRITE_TAC[IM_DEF; complex; VECTOR_2]);;
  76
  77 let COMPLEX_EQ = prove
  78  (`!w z. (w = z) <=> (Re(w) = Re(z)) /\ (Im(w) = Im(z))`,
  79   SIMP_TAC[CART_EQ; FORALL_2; DIMINDEX_2; RE_DEF; IM_DEF]);;
  80
  81 let COMPLEX = prove
  82  (`!z. complex(Re(z),Im(z)) = z`,
  83   REWRITE_TAC[COMPLEX_EQ; RE; IM]);;
  84
  85 let COMPLEX_EQ_0 = prove
  86  (`z = Cx(&0) <=> Re(z) pow 2 + Im(z) pow 2 = &0`,
  87   REWRITE_TAC[COMPLEX_EQ; CX_DEF; RE; IM] THEN
  88   EQ_TAC THEN SIMP_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  89   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
  90    `!x y:real. x + y = &0 ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN
  91   REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_ENTIRE]);;
  92
  93 let FORALL_COMPLEX = prove
  94  (`(!z. P z) <=> (!x y. P(complex(x,y)))`,
  95   MESON_TAC[COMPLEX]);;
  96
  97 let EXISTS_COMPLEX = prove
  98  (`(?z. P z) <=> (?x y. P(complex(x,y)))`,
  99   MESON_TAC[COMPLEX]);;
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Pseudo-definitions of other general vector concepts over R^2.             *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105 let complex_neg = prove
 106  (`--z = complex(--(Re(z)),--(Im(z)))`,
 107   REWRITE_TAC[COMPLEX_EQ; RE; IM] THEN REWRITE_TAC[RE_DEF; IM_DEF] THEN
 108   SIMP_TAC[VECTOR_NEG_COMPONENT; DIMINDEX_2; ARITH]);;
 109
 110 let complex_add = prove
 111  (`w + z = complex(Re(w) + Re(z),Im(w) + Im(z))`,
 112   REWRITE_TAC[COMPLEX_EQ; RE; IM] THEN REWRITE_TAC[RE_DEF; IM_DEF] THEN
 113   SIMP_TAC[VECTOR_ADD_COMPONENT; DIMINDEX_2; ARITH]);;
 114
 115 let complex_sub = VECTOR_ARITH `(w:complex) - z = w + --z`;;
 116
 117 let complex_norm = prove
 118  (`norm(z) = sqrt(Re(z) pow 2 + Im(z) pow 2)`,
 119   REWRITE_TAC[vector_norm; dot; RE_DEF; IM_DEF; SUM_2; DIMINDEX_2] THEN
 120   AP_TERM_TAC THEN REAL_ARITH_TAC);;
 121
 122 let COMPLEX_SQNORM = prove
 123  (`norm(z) pow 2 = Re(z) pow 2 + Im(z) pow 2`,
 124   REWRITE_TAC[NORM_POW_2; dot; RE_DEF; IM_DEF; SUM_2; DIMINDEX_2] THEN
 125   REAL_ARITH_TAC);;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Crude tactic to automate very simple algebraic equivalences.              *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 let SIMPLE_COMPLEX_ARITH_TAC =
 132   REWRITE_TAC[COMPLEX_EQ; RE; IM; CX_DEF;
 133               complex_add; complex_neg; complex_sub; complex_mul;
 134               complex_inv; complex_div] THEN
 135   CONV_TAC REAL_FIELD;;
 136
 137 let SIMPLE_COMPLEX_ARITH tm = prove(tm,SIMPLE_COMPLEX_ARITH_TAC);;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Basic algebraic properties that can be proved automatically by this.      *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let COMPLEX_ADD_SYM = prove
 144  (`!x y. x + y = y + x`,
 145   SIMPLE_COMPLEX_ARITH_TAC);;
 146
 147 let COMPLEX_ADD_ASSOC = prove
 148  (`!x y z. x + y + z = (x + y) + z`,
 149   SIMPLE_COMPLEX_ARITH_TAC);;
 150
 151 let COMPLEX_ADD_LID = prove
 152  (`!x. Cx(&0) + x = x`,
 153   SIMPLE_COMPLEX_ARITH_TAC);;
 154
 155 let COMPLEX_ADD_LINV = prove
 156  (`!x. --x + x = Cx(&0)`,
 157   SIMPLE_COMPLEX_ARITH_TAC);;
 158
 159 let COMPLEX_MUL_SYM = prove
 160  (`!x y. x * y = y * x`,
 161   SIMPLE_COMPLEX_ARITH_TAC);;
 162
 163 let COMPLEX_MUL_ASSOC = prove
 164  (`!x y z. x * y * z = (x * y) * z`,
 165   SIMPLE_COMPLEX_ARITH_TAC);;
 166
 167 let COMPLEX_MUL_LID = prove
 168  (`!x. Cx(&1) * x = x`,
 169   SIMPLE_COMPLEX_ARITH_TAC);;
 170
 171 let COMPLEX_ADD_LDISTRIB = prove
 172  (`!x y z. x * (y + z) = x * y + x * z`,
 173   SIMPLE_COMPLEX_ARITH_TAC);;
 174
 175 let COMPLEX_ADD_AC = prove
 176  (`(m + n = n + m) /\ ((m + n) + p = m + n + p) /\ (m + n + p = n + m + p)`,
 177   SIMPLE_COMPLEX_ARITH_TAC);;
 178
 179 let COMPLEX_MUL_AC = prove
 180  (`(m * n = n * m) /\ ((m * n) * p = m * n * p) /\ (m * n * p = n * m * p)`,
 181   SIMPLE_COMPLEX_ARITH_TAC);;
 182
 183 let COMPLEX_ADD_RID = prove
 184  (`!x. x + Cx(&0) = x`,
 185   SIMPLE_COMPLEX_ARITH_TAC);;
 186
 187 let COMPLEX_MUL_RID = prove
 188  (`!x. x * Cx(&1) = x`,
 189   SIMPLE_COMPLEX_ARITH_TAC);;
 190
 191 let COMPLEX_ADD_RINV = prove
 192  (`!x. x + --x = Cx(&0)`,
 193   SIMPLE_COMPLEX_ARITH_TAC);;
 194
 195 let COMPLEX_ADD_RDISTRIB = prove
 196  (`!x y z. (x + y) * z = x * z + y * z`,
 197   SIMPLE_COMPLEX_ARITH_TAC);;
 198
 199 let COMPLEX_EQ_ADD_LCANCEL = prove
 200  (`!x y z. (x + y = x + z) <=> (y = z)`,
 201   SIMPLE_COMPLEX_ARITH_TAC);;
 202
 203 let COMPLEX_EQ_ADD_RCANCEL = prove
 204  (`!x y z. (x + z = y + z) <=> (x = y)`,
 205   SIMPLE_COMPLEX_ARITH_TAC);;
 206
 207 let COMPLEX_MUL_RZERO = prove
 208  (`!x. x * Cx(&0) = Cx(&0)`,
 209   SIMPLE_COMPLEX_ARITH_TAC);;
 210
 211 let COMPLEX_MUL_LZERO = prove
 212  (`!x. Cx(&0) * x = Cx(&0)`,
 213   SIMPLE_COMPLEX_ARITH_TAC);;
 214
 215 let COMPLEX_NEG_NEG = prove
 216  (`!x. --(--x) = x`,
 217   SIMPLE_COMPLEX_ARITH_TAC);;
 218
 219 let COMPLEX_MUL_RNEG = prove
 220  (`!x y. x * --y = --(x * y)`,
 221   SIMPLE_COMPLEX_ARITH_TAC);;
 222
 223 let COMPLEX_MUL_LNEG = prove
 224  (`!x y. --x * y = --(x * y)`,
 225   SIMPLE_COMPLEX_ARITH_TAC);;
 226
 227 let COMPLEX_NEG_ADD = prove
 228  (`!x y. --(x + y) = --x + --y`,
 229   SIMPLE_COMPLEX_ARITH_TAC);;
 230
 231 let COMPLEX_NEG_0 = prove
 232  (`--Cx(&0) = Cx(&0)`,
 233   SIMPLE_COMPLEX_ARITH_TAC);;
 234
 235 let COMPLEX_EQ_ADD_LCANCEL_0 = prove
 236  (`!x y. (x + y = x) <=> (y = Cx(&0))`,
 237   SIMPLE_COMPLEX_ARITH_TAC);;
 238
 239 let COMPLEX_EQ_ADD_RCANCEL_0 = prove
 240  (`!x y. (x + y = y) <=> (x = Cx(&0))`,
 241   SIMPLE_COMPLEX_ARITH_TAC);;
 242
 243 let COMPLEX_LNEG_UNIQ = prove
 244  (`!x y. (x + y = Cx(&0)) <=> (x = --y)`,
 245   SIMPLE_COMPLEX_ARITH_TAC);;
 246
 247 let COMPLEX_RNEG_UNIQ = prove
 248  (`!x y. (x + y = Cx(&0)) <=> (y = --x)`,
 249   SIMPLE_COMPLEX_ARITH_TAC);;
 250
 251 let COMPLEX_NEG_LMUL = prove
 252  (`!x y. --(x * y) = --x * y`,
 253   SIMPLE_COMPLEX_ARITH_TAC);;
 254
 255 let COMPLEX_NEG_RMUL = prove
 256  (`!x y. --(x * y) = x * --y`,
 257   SIMPLE_COMPLEX_ARITH_TAC);;
 258
 259 let COMPLEX_NEG_MUL2 = prove
 260  (`!x y. --x * --y = x * y`,
 261   SIMPLE_COMPLEX_ARITH_TAC);;
 262
 263 let COMPLEX_SUB_ADD = prove
 264  (`!x y. x - y + y = x`,
 265   SIMPLE_COMPLEX_ARITH_TAC);;
 266
 267 let COMPLEX_SUB_ADD2 = prove
 268  (`!x y. y + x - y = x`,
 269   SIMPLE_COMPLEX_ARITH_TAC);;
 270
 271 let COMPLEX_SUB_REFL = prove
 272  (`!x. x - x = Cx(&0)`,
 273   SIMPLE_COMPLEX_ARITH_TAC);;
 274
 275 let COMPLEX_SUB_0 = prove
 276  (`!x y. (x - y = Cx(&0)) <=> (x = y)`,
 277   SIMPLE_COMPLEX_ARITH_TAC);;
 278
 279 let COMPLEX_NEG_EQ_0 = prove
 280  (`!x. (--x = Cx(&0)) <=> (x = Cx(&0))`,
 281   SIMPLE_COMPLEX_ARITH_TAC);;
 282
 283 let COMPLEX_NEG_SUB = prove
 284  (`!x y. --(x - y) = y - x`,
 285   SIMPLE_COMPLEX_ARITH_TAC);;
 286
 287 let COMPLEX_ADD_SUB = prove
 288  (`!x y. (x + y) - x = y`,
 289   SIMPLE_COMPLEX_ARITH_TAC);;
 290
 291 let COMPLEX_NEG_EQ = prove
 292  (`!x y. (--x = y) <=> (x = --y)`,
 293   SIMPLE_COMPLEX_ARITH_TAC);;
 294
 295 let COMPLEX_NEG_MINUS1 = prove
 296  (`!x. --x = --Cx(&1) * x`,
 297   SIMPLE_COMPLEX_ARITH_TAC);;
 298
 299 let COMPLEX_SUB_SUB = prove
 300  (`!x y. x - y - x = --y`,
 301   SIMPLE_COMPLEX_ARITH_TAC);;
 302
 303 let COMPLEX_ADD2_SUB2 = prove
 304  (`!a b c d. (a + b) - (c + d) = a - c + b - d`,
 305   SIMPLE_COMPLEX_ARITH_TAC);;
 306
 307 let COMPLEX_SUB_LZERO = prove
 308  (`!x. Cx(&0) - x = --x`,
 309   SIMPLE_COMPLEX_ARITH_TAC);;
 310
 311 let COMPLEX_SUB_RZERO = prove
 312  (`!x. x - Cx(&0) = x`,
 313   SIMPLE_COMPLEX_ARITH_TAC);;
 314
 315 let COMPLEX_SUB_LNEG = prove
 316  (`!x y. --x - y = --(x + y)`,
 317   SIMPLE_COMPLEX_ARITH_TAC);;
 318
 319 let COMPLEX_SUB_RNEG = prove
 320  (`!x y. x - --y = x + y`,
 321   SIMPLE_COMPLEX_ARITH_TAC);;
 322
 323 let COMPLEX_SUB_NEG2 = prove
 324  (`!x y. --x - --y = y - x`,
 325   SIMPLE_COMPLEX_ARITH_TAC);;
 326
 327 let COMPLEX_SUB_TRIANGLE = prove
 328  (`!a b c. a - b + b - c = a - c`,
 329   SIMPLE_COMPLEX_ARITH_TAC);;
 330
 331 let COMPLEX_EQ_SUB_LADD = prove
 332  (`!x y z. (x = y - z) <=> (x + z = y)`,
 333   SIMPLE_COMPLEX_ARITH_TAC);;
 334
 335 let COMPLEX_EQ_SUB_RADD = prove
 336  (`!x y z. (x - y = z) <=> (x = z + y)`,
 337   SIMPLE_COMPLEX_ARITH_TAC);;
 338
 339 let COMPLEX_SUB_SUB2 = prove
 340  (`!x y. x - (x - y) = y`,
 341   SIMPLE_COMPLEX_ARITH_TAC);;
 342
 343 let COMPLEX_ADD_SUB2 = prove
 344  (`!x y. x - (x + y) = --y`,
 345   SIMPLE_COMPLEX_ARITH_TAC);;
 346
 347 let COMPLEX_DIFFSQ = prove
 348  (`!x y. (x + y) * (x - y) = x * x - y * y`,
 349   SIMPLE_COMPLEX_ARITH_TAC);;
 350
 351 let COMPLEX_EQ_NEG2 = prove
 352  (`!x y. (--x = --y) <=> (x = y)`,
 353   SIMPLE_COMPLEX_ARITH_TAC);;
 354
 355 let COMPLEX_SUB_LDISTRIB = prove
 356  (`!x y z. x * (y - z) = x * y - x * z`,
 357   SIMPLE_COMPLEX_ARITH_TAC);;
 358
 359 let COMPLEX_SUB_RDISTRIB = prove
 360  (`!x y z. (x - y) * z = x * z - y * z`,
 361   SIMPLE_COMPLEX_ARITH_TAC);;
 362
 363 let COMPLEX_MUL_2 = prove
 364  (`!x. Cx(&2) * x = x + x`,
 365   SIMPLE_COMPLEX_ARITH_TAC);;
 366
 367 (* ------------------------------------------------------------------------- *)
 368 (* Sometimes here we need to tweak non-zeroness assertions.                  *)
 369 (* ------------------------------------------------------------------------- *)
 370
 371 let II_NZ = prove
 372  (`~(ii = Cx(&0))`,
 373   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 374
 375 let COMPLEX_MUL_LINV = prove
 376  (`!z. ~(z = Cx(&0)) ==> (inv(z) * z = Cx(&1))`,
 377   REWRITE_TAC[COMPLEX_EQ_0] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 378
 379 let COMPLEX_ENTIRE = prove
 380  (`!x y. (x * y = Cx(&0)) <=> (x = Cx(&0)) \/ (y = Cx(&0))`,
 381   REWRITE_TAC[COMPLEX_EQ_0] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 382
 383 let COMPLEX_MUL_RINV = prove
 384  (`!z. ~(z = Cx(&0)) ==> (z * inv(z) = Cx(&1))`,
 385   REWRITE_TAC[COMPLEX_EQ_0] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 386
 387 let COMPLEX_DIV_REFL = prove
 388  (`!x. ~(x = Cx(&0)) ==> (x / x = Cx(&1))`,
 389   REWRITE_TAC[COMPLEX_EQ_0] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 390
 391 (* ------------------------------------------------------------------------- *)
 392 (* Homomorphic embedding properties for Cx mapping.                          *)
 393 (* ------------------------------------------------------------------------- *)
 394
 395 let CX_INJ = prove
 396  (`!x y. (Cx(x) = Cx(y)) <=> (x = y)`,
 397   REWRITE_TAC[CX_DEF; COMPLEX_EQ; RE; IM]);;
 398
 399 let CX_NEG = prove
 400  (`!x. Cx(--x) = --(Cx(x))`,
 401   REWRITE_TAC[CX_DEF; complex_neg; RE; IM; REAL_NEG_0]);;
 402
 403 let CX_ADD = prove
 404  (`!x y. Cx(x + y) = Cx(x) + Cx(y)`,
 405   REWRITE_TAC[CX_DEF; complex_add; RE; IM; REAL_ADD_LID]);;
 406
 407 let CX_SUB = prove
 408  (`!x y. Cx(x - y) = Cx(x) - Cx(y)`,
 409   REWRITE_TAC[complex_sub; real_sub; CX_ADD; CX_NEG]);;
 410
 411 let CX_INV = prove
 412  (`!x. Cx(inv x) = inv(Cx x)`,
 413   GEN_TAC THEN REWRITE_TAC[CX_DEF; complex_inv; RE; IM; COMPLEX_EQ] THEN
 414   ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
 415   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 416   POP_ASSUM MP_TAC THEN CONV_TAC REAL_FIELD);;
 417
 418 let CX_MUL = prove
 419  (`!x y. Cx(x * y) = Cx(x) * Cx(y)`,
 420   REWRITE_TAC[CX_DEF; complex_mul; RE; IM; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
 421   REWRITE_TAC[REAL_SUB_RZERO; REAL_ADD_RID]);;
 422
 423 let CX_POW = prove
 424  (`!x n. Cx(x pow n) = Cx(x) pow n`,
 425   GEN_TAC THEN INDUCT_TAC THEN
 426   ASM_REWRITE_TAC[complex_pow; real_pow; CX_MUL]);;
 427
 428 let CX_DIV = prove
 429  (`!x y. Cx(x / y) = Cx(x) / Cx(y)`,
 430   REWRITE_TAC[complex_div; real_div; CX_MUL; CX_INV]);;
 431
 432 let CX_ABS = prove
 433  (`!x. Cx(abs x) = Cx(norm(Cx(x)))`,
 434   REWRITE_TAC[CX_DEF; complex_norm; COMPLEX_EQ; RE; IM] THEN
 435   REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 436   REWRITE_TAC[GSYM REAL_POW_2; POW_2_SQRT_ABS]);;
 437
 438 let COMPLEX_NORM_CX = prove
 439  (`!x. norm(Cx(x)) = abs(x)`,
 440   REWRITE_TAC[GSYM CX_INJ; CX_ABS]);;
 441
 442 let DIST_CX = prove
 443  (`!x y. dist(Cx x,Cx y) = abs(x - y)`,
 444   REWRITE_TAC[dist; GSYM CX_SUB; COMPLEX_NORM_CX]);;
 445
 446 (* ------------------------------------------------------------------------- *)
 447 (* Some "linear" things hold for Re and Im too.                              *)
 448 (* ------------------------------------------------------------------------- *)
 449
 450 let RE_CX = prove
 451  (`!x. Re(Cx x) = x`,
 452   REWRITE_TAC[RE; CX_DEF]);;
 453
 454 let RE_NEG = prove
 455  (`!x. Re(--x) = --Re(x)`,
 456   REWRITE_TAC[complex_neg; RE]);;
 457
 458 let RE_ADD = prove
 459  (`!x y. Re(x + y) = Re(x) + Re(y)`,
 460   REWRITE_TAC[complex_add; RE]);;
 461
 462 let RE_SUB = prove
 463  (`!x y. Re(x - y) = Re(x) - Re(y)`,
 464   REWRITE_TAC[complex_sub; real_sub; RE_ADD; RE_NEG]);;
 465
 466 let IM_CX = prove
 467  (`!x. Im(Cx x) = &0`,
 468   REWRITE_TAC[IM; CX_DEF]);;
 469
 470 let IM_NEG = prove
 471  (`!x. Im(--x) = --Im(x)`,
 472   REWRITE_TAC[complex_neg; IM]);;
 473
 474 let IM_ADD = prove
 475  (`!x y. Im(x + y) = Im(x) + Im(y)`,
 476   REWRITE_TAC[complex_add; IM]);;
 477
 478 let IM_SUB = prove
 479  (`!x y. Im(x - y) = Im(x) - Im(y)`,
 480   REWRITE_TAC[complex_sub; real_sub; IM_ADD; IM_NEG]);;
 481
 482 (* ------------------------------------------------------------------------- *)
 483 (* An "expansion" theorem into the traditional notation.                     *)
 484 (* ------------------------------------------------------------------------- *)
 485
 486 let COMPLEX_EXPAND = prove
 487  (`!z. z = Cx(Re z) + ii * Cx(Im z)`,
 488   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 489
 490 let COMPLEX_TRAD = prove
 491  (`!x y. complex(x,y) = Cx(x) + ii * Cx(y)`,
 492   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 493
 494 (* ------------------------------------------------------------------------- *)
 495 (* Real and complex parts of ii and multiples.                               *)
 496 (* ------------------------------------------------------------------------- *)
 497
 498 let RE_II = prove
 499  (`Re ii = &0`,
 500   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 501
 502 let IM_II = prove
 503  (`Im ii = &1`,
 504   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 505
 506 let RE_MUL_II = prove
 507  (`!z. Re(z * ii) = --(Im z) /\ Re(ii * z) = --(Im z)`,
 508   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 509
 510 let IM_MUL_II = prove
 511  (`!z. Im(z * ii) = Re z /\ Im(ii * z) = Re z`,
 512   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
 513
 514 let COMPLEX_NORM_II = prove
 515  (`norm ii = &1`,
 516   REWRITE_TAC[complex_norm; RE_II; IM_II] THEN
 517   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[SQRT_1]);;
 518
 519 (* ------------------------------------------------------------------------- *)
 520 (* Limited "multiplicative" theorems for Re and Im.                          *)
 521 (* ------------------------------------------------------------------------- *)
 522
 523 let RE_CMUL = prove
 524  (`!a z. Re(a % z) = a * Re z`,
 525   SIMP_TAC[RE_DEF; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH]);;
 526
 527 let IM_CMUL = prove
 528  (`!a z. Im(a % z) = a * Im z`,
 529   SIMP_TAC[IM_DEF; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH]);;
 530
 531 let RE_MUL_CX = prove
 532  (`!x z. Re(Cx(x) * z) = x * Re z /\
 533          Re(z * Cx(x)) = Re z * x`,
 534   SIMPLE_COMPLEX_ARITH_TAC);;
 535
 536 let IM_MUL_CX = prove
 537  (`!x z. Im(Cx(x) * z) = x * Im z /\
 538          Im(z * Cx(x)) = Im z * x`,
 539   SIMPLE_COMPLEX_ARITH_TAC);;
 540
 541 let RE_DIV_CX = prove
 542  (`!z x. Re(z / Cx(x)) = Re(z) / x`,
 543   REWRITE_TAC[complex_div; real_div; GSYM CX_INV; RE_MUL_CX]);;
 544
 545 let IM_DIV_CX = prove
 546  (`!z x. Im(z / Cx(x)) = Im(z) / x`,
 547   REWRITE_TAC[complex_div; real_div; GSYM CX_INV; IM_MUL_CX]);;
 548
 549 (* ------------------------------------------------------------------------- *)
 550 (* Syntax constructors etc. for complex constants.                           *)
 551 (* ------------------------------------------------------------------------- *)
 552
 553 let is_complex_const =
 554   let cx_tm = `Cx` in
 555   fun tm ->
 556     is_comb tm &
 557     let l,r = dest_comb tm in l = cx_tm & is_ratconst r;;
 558
 559 let dest_complex_const =
 560   let cx_tm = `Cx` in
 561   fun tm ->
 562     let l,r = dest_comb tm in
 563     if l = cx_tm then rat_of_term r
 564     else failwith "dest_complex_const";;
 565
 566 let mk_complex_const =
 567   let cx_tm = `Cx` in
 568   fun r ->
 569     mk_comb(cx_tm,term_of_rat r);;
 570
 571 (* ------------------------------------------------------------------------- *)
 572 (* Conversions for arithmetic on complex constants.                          *)
 573 (* ------------------------------------------------------------------------- *)
 574
 575 let COMPLEX_RAT_EQ_CONV =
 576   GEN_REWRITE_CONV I [CX_INJ] THENC REAL_RAT_EQ_CONV;;
 577
 578 let COMPLEX_RAT_MUL_CONV =
 579   GEN_REWRITE_CONV I [GSYM CX_MUL] THENC RAND_CONV REAL_RAT_MUL_CONV;;
 580
 581 let COMPLEX_RAT_ADD_CONV =
 582   GEN_REWRITE_CONV I [GSYM CX_ADD] THENC RAND_CONV REAL_RAT_ADD_CONV;;
 583
 584 let COMPLEX_RAT_POW_CONV =
 585   let x_tm = `x:real`
 586   and n_tm = `n:num` in
 587   let pth = SYM(SPECL [x_tm; n_tm] CX_POW) in
 588   fun tm ->
 589     let lop,r = dest_comb tm in
 590     let op,bod = dest_comb lop in
 591     let th1 = INST [rand bod,x_tm; r,n_tm] pth in
 592     let tm1,tm2 = dest_comb(concl th1) in
 593     if rand tm1 <> tm then failwith "COMPLEX_RAT_POW_CONV" else
 594     let tm3,tm4 = dest_comb tm2 in
 595     TRANS th1 (AP_TERM tm3 (REAL_RAT_REDUCE_CONV tm4));;
 596
 597 (* ------------------------------------------------------------------------- *)
 598 (* Complex polynomial normalizer.                                            *)
 599 (* ------------------------------------------------------------------------- *)
 600
 601 let COMPLEX_POLY_CLAUSES = prove
 602  (`(!x y z. x + (y + z) = (x + y) + z) /\
 603    (!x y. x + y = y + x) /\
 604    (!x. Cx(&0) + x = x) /\
 605    (!x y z. x * (y * z) = (x * y) * z) /\
 606    (!x y. x * y = y * x) /\
 607    (!x. Cx(&1) * x = x) /\
 608    (!x. Cx(&0) * x = Cx(&0)) /\
 609    (!x y z. x * (y + z) = x * y + x * z) /\
 610    (!x. x pow 0 = Cx(&1)) /\
 611    (!x n. x pow (SUC n) = x * x pow n)`,
 612   REWRITE_TAC[complex_pow] THEN SIMPLE_COMPLEX_ARITH_TAC)
 613 and COMPLEX_POLY_NEG_CLAUSES = prove
 614  (`(!x. --x = Cx(-- &1) * x) /\
 615    (!x y. x - y = x + Cx(-- &1) * y)`,
 616   SIMPLE_COMPLEX_ARITH_TAC);;
 617
 618 let COMPLEX_POLY_NEG_CONV,COMPLEX_POLY_ADD_CONV,COMPLEX_POLY_SUB_CONV,
 619     COMPLEX_POLY_MUL_CONV,COMPLEX_POLY_POW_CONV,COMPLEX_POLY_CONV =
 620   SEMIRING_NORMALIZERS_CONV COMPLEX_POLY_CLAUSES COMPLEX_POLY_NEG_CLAUSES
 621    (is_complex_const,
 622     COMPLEX_RAT_ADD_CONV,COMPLEX_RAT_MUL_CONV,COMPLEX_RAT_POW_CONV)
 623    (<);;
 624
 625 (* ------------------------------------------------------------------------- *)
 626 (* Extend it to handle "inv" and division, by constants after normalization. *)
 627 (* ------------------------------------------------------------------------- *)
 628
 629 let COMPLEX_RAT_INV_CONV =
 630   REWR_CONV(GSYM CX_INV) THENC RAND_CONV REAL_RAT_INV_CONV;;
 631
 632 let COMPLEX_POLY_CONV =
 633   let neg_tm = `(--):complex->complex`
 634   and inv_tm = `inv:complex->complex`
 635   and add_tm = `(+):complex->complex->complex`
 636   and sub_tm = `(-):complex->complex->complex`
 637   and mul_tm = `(*):complex->complex->complex`
 638   and div_tm = `(/):complex->complex->complex`
 639   and pow_tm = `(pow):complex->num->complex`
 640   and div_conv = REWR_CONV complex_div in
 641   let rec COMPLEX_POLY_CONV tm =
 642     if not(is_comb tm) or is_ratconst tm then REFL tm else
 643     let lop,r = dest_comb tm in
 644     if lop = neg_tm then
 645       let th1 = AP_TERM lop (COMPLEX_POLY_CONV r) in
 646       TRANS th1 (COMPLEX_POLY_NEG_CONV (rand(concl th1)))
 647     else if lop = inv_tm then
 648       let th1 = AP_TERM lop (COMPLEX_POLY_CONV r) in
 649       TRANS th1 (TRY_CONV COMPLEX_RAT_INV_CONV (rand(concl th1)))
 650     else if not(is_comb lop) then REFL tm else
 651     let op,l = dest_comb lop in
 652     if op = pow_tm then
 653       let th1 = AP_THM (AP_TERM op (COMPLEX_POLY_CONV l)) r in
 654       TRANS th1 (TRY_CONV COMPLEX_POLY_POW_CONV (rand(concl th1)))
 655     else if op = add_tm or op = mul_tm or op = sub_tm then
 656       let th1 = MK_COMB(AP_TERM op (COMPLEX_POLY_CONV l),
 657                         COMPLEX_POLY_CONV r) in
 658       let fn = if op = add_tm then COMPLEX_POLY_ADD_CONV
 659                else if op = mul_tm then COMPLEX_POLY_MUL_CONV
 660                else COMPLEX_POLY_SUB_CONV in
 661       TRANS th1 (fn (rand(concl th1)))
 662     else if op = div_tm then
 663       let th1 = div_conv tm in
 664       TRANS th1 (COMPLEX_POLY_CONV (rand(concl th1)))
 665     else REFL tm in
 666   COMPLEX_POLY_CONV;;
 667
 668 (* ------------------------------------------------------------------------- *)
 669 (* Complex number version of usual ring procedure.                           *)
 670 (* ------------------------------------------------------------------------- *)
 671
 672 let COMPLEX_RING,complex_ideal_cofactors =
 673   let COMPLEX_INTEGRAL = prove
 674    (`(!x. Cx(&0) * x = Cx(&0)) /\
 675      (!x y z. (x + y = x + z) <=> (y = z)) /\
 676      (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
 677     REWRITE_TAC[COMPLEX_ENTIRE; SIMPLE_COMPLEX_ARITH
 678      `(w * y + x * z = w * z + x * y) <=>
 679       (w - x) * (y - z) = Cx(&0)`] THEN
 680     SIMPLE_COMPLEX_ARITH_TAC)
 681   and COMPLEX_RABINOWITSCH = prove
 682    (`!x y:complex. ~(x = y) <=> ?z. (x - y) * z = Cx(&1)`,
 683     REPEAT GEN_TAC THEN
 684     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM COMPLEX_SUB_0] THEN
 685     MESON_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_LZERO;
 686               SIMPLE_COMPLEX_ARITH `~(Cx(&1) = Cx(&0))`])
 687   and COMPLEX_IIII = prove
 688    (`ii * ii + Cx(&1) = Cx(&0)`,
 689     REWRITE_TAC[ii; CX_DEF; complex_mul; complex_add; RE; IM] THEN
 690     AP_TERM_TAC THEN BINOP_TAC THEN REAL_ARITH_TAC) in
 691   let ring,ideal =
 692     RING_AND_IDEAL_CONV
 693         (dest_complex_const,mk_complex_const,COMPLEX_RAT_EQ_CONV,
 694          `(--):complex->complex`,`(+):complex->complex->complex`,
 695          `(-):complex->complex->complex`,`(inv):complex->complex`,
 696          `(*):complex->complex->complex`,`(/):complex->complex->complex`,
 697          `(pow):complex->num->complex`,
 698          COMPLEX_INTEGRAL,COMPLEX_RABINOWITSCH,COMPLEX_POLY_CONV)
 699   and ii_tm = `ii` and iiii_tm = concl COMPLEX_IIII in
 700   (fun tm -> if free_in ii_tm tm then
 701              MP (ring (mk_imp(iiii_tm,tm))) COMPLEX_IIII
 702              else ring tm),
 703   ideal;;
 704
 705 (* ------------------------------------------------------------------------- *)
 706 (* Most basic properties of inverses.                                        *)
 707 (* ------------------------------------------------------------------------- *)
 708
 709 let COMPLEX_INV_0 = prove
 710  (`inv(Cx(&0)) = Cx(&0)`,
 711   SIMPLE_COMPLEX_ARITH_TAC);;
 712
 713 let COMPLEX_INV_1 = prove
 714  (`inv(Cx(&1)) = Cx(&1)`,
 715   SIMPLE_COMPLEX_ARITH_TAC);;
 716
 717 let COMPLEX_INV_MUL = prove
 718  (`!w z. inv(w * z) = inv(w) * inv(z)`,
 719   REPEAT GEN_TAC THEN
 720   MAP_EVERY ASM_CASES_TAC [`w = Cx(&0)`; `z = Cx(&0)`] THEN
 721   ASM_REWRITE_TAC[COMPLEX_INV_0; COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THEN
 722   REPEAT(POP_ASSUM MP_TAC) THEN
 723   REWRITE_TAC[complex_mul; complex_inv; RE; IM; COMPLEX_EQ; CX_DEF] THEN
 724   REWRITE_TAC[GSYM REAL_SOS_EQ_0] THEN CONV_TAC REAL_FIELD);;
 725
 726 let COMPLEX_POW_INV = prove
 727  (`!x n. (inv x) pow n = inv(x pow n)`,
 728   GEN_TAC THEN INDUCT_TAC THEN
 729   ASM_REWRITE_TAC[complex_pow; COMPLEX_INV_1; COMPLEX_INV_MUL]);;
 730
 731 let COMPLEX_INV_INV = prove
 732  (`!x:complex. inv(inv x) = x`,
 733   GEN_TAC THEN ASM_CASES_TAC `x = Cx(&0)` THEN
 734   ASM_REWRITE_TAC[COMPLEX_INV_0] THEN
 735   POP_ASSUM MP_TAC THEN
 736   MAP_EVERY (fun t -> MP_TAC(SPEC t COMPLEX_MUL_RINV))
 737    [`x:complex`; `inv(x):complex`] THEN
 738   CONV_TAC COMPLEX_RING);;
 739
 740 let COMPLEX_INV_DIV = prove
 741  (`!w z:complex. inv(w / z) = z / w`,
 742   REWRITE_TAC[complex_div; COMPLEX_INV_MUL; COMPLEX_INV_INV] THEN
 743   REWRITE_TAC[COMPLEX_MUL_AC]);;
 744
 745 (* ------------------------------------------------------------------------- *)
 746 (* And also field procedure.                                                 *)
 747 (* ------------------------------------------------------------------------- *)
 748
 749 let COMPLEX_EQ_MUL_LCANCEL = prove
 750  (`!x y z. (x * y = x * z) <=> (x = Cx(&0)) \/ (y = z)`,
 751   CONV_TAC COMPLEX_RING);;
 752
 753 let COMPLEX_EQ_MUL_RCANCEL = prove
 754  (`!x y z. (x * z = y * z) <=> (x = y) \/ (z = Cx(&0))`,
 755   CONV_TAC COMPLEX_RING);;
 756
 757 let COMPLEX_FIELD =
 758   let prenex_conv =
 759     TOP_DEPTH_CONV BETA_CONV THENC
 760     PURE_REWRITE_CONV[FORALL_SIMP; EXISTS_SIMP; complex_div;
 761                COMPLEX_INV_INV; COMPLEX_INV_MUL; GSYM COMPLEX_POW_INV] THENC
 762     NNFC_CONV THENC DEPTH_BINOP_CONV `(/\)` CONDS_CELIM_CONV THENC
 763     PRENEX_CONV
 764   and setup_conv = NNF_CONV THENC WEAK_CNF_CONV THENC CONJ_CANON_CONV
 765   and is_inv =
 766     let inv_tm = `inv:complex->complex`
 767     and is_div = is_binop `(/):complex->complex->complex` in
 768     fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) &
 769               not(is_ratconst(rand tm)) in
 770   let BASIC_COMPLEX_FIELD tm =
 771     let is_freeinv t = is_inv t & free_in t tm in
 772     let itms = setify(map rand (find_terms is_freeinv tm)) in
 773     let hyps = map (fun t -> SPEC t COMPLEX_MUL_RINV) itms in
 774     let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in
 775     let th1 = setup_conv tm' in
 776     let cjs = conjuncts(rand(concl th1)) in
 777     let ths = map COMPLEX_RING cjs in
 778     let th2 = EQ_MP (SYM th1) (end_itlist CONJ ths) in
 779     rev_itlist (C MP) hyps th2 in
 780   fun tm ->
 781     let th0 = prenex_conv tm in
 782     let tm0 = rand(concl th0) in
 783     let avs,bod = strip_forall tm0 in
 784     let th1 = setup_conv bod in
 785     let ths = map BASIC_COMPLEX_FIELD (conjuncts(rand(concl th1))) in
 786     EQ_MP (SYM th0) (GENL avs (EQ_MP (SYM th1) (end_itlist CONJ ths)));;
 787
 788 (* ------------------------------------------------------------------------- *)
 789 (* More trivial lemmas.                                                      *)
 790 (* ------------------------------------------------------------------------- *)
 791
 792 let COMPLEX_DIV_1 = prove
 793  (`!z. z / Cx(&1) = z`,
 794   CONV_TAC COMPLEX_FIELD);;
 795
 796 let COMPLEX_DIV_LMUL = prove
 797  (`!x y. ~(y = Cx(&0)) ==> y * x / y = x`,
 798   CONV_TAC COMPLEX_FIELD);;
 799
 800 let COMPLEX_DIV_RMUL = prove
 801  (`!x y. ~(y = Cx(&0)) ==> x / y * y = x`,
 802   CONV_TAC COMPLEX_FIELD);;
 803
 804 let COMPLEX_INV_EQ_0 = prove
 805  (`!x. inv x = Cx(&0) <=> x = Cx(&0)`,
 806   GEN_TAC THEN ASM_CASES_TAC `x = Cx(&0)` THEN
 807   ASM_REWRITE_TAC[COMPLEX_INV_0] THEN POP_ASSUM MP_TAC THEN
 808   CONV_TAC COMPLEX_FIELD);;
 809
 810 let COMPLEX_INV_NEG = prove
 811  (`!x:complex. inv(--x) = --(inv x)`,
 812   GEN_TAC THEN ASM_CASES_TAC `x = Cx(&0)` THEN
 813   ASM_REWRITE_TAC[COMPLEX_INV_0; COMPLEX_NEG_0] THEN
 814   POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD);;
 815
 816 let COMPLEX_NEG_INV = prove
 817  (`!x:complex. --(inv x) = inv(--x)`,
 818   REWRITE_TAC[COMPLEX_INV_NEG]);;
 819
 820 let COMPLEX_INV_EQ_1 = prove
 821  (`!x. inv x = Cx(&1) <=> x = Cx(&1)`,
 822   GEN_TAC THEN ASM_CASES_TAC `x = Cx(&0)` THEN
 823   ASM_REWRITE_TAC[COMPLEX_INV_0] THEN POP_ASSUM MP_TAC THEN
 824   CONV_TAC COMPLEX_FIELD);;
 825
 826 let COMPLEX_DIV_EQ_0 = prove
 827  (`!w z. w / z = Cx(&0) <=> w = Cx(&0) \/ z = Cx(&0)`,
 828   REWRITE_TAC[complex_div; COMPLEX_INV_EQ_0; COMPLEX_ENTIRE]);;
 829
 830 (* ------------------------------------------------------------------------- *)
 831 (* Powers.                                                                   *)
 832 (* ------------------------------------------------------------------------- *)
 833
 834 let COMPLEX_POW_ADD = prove
 835  (`!x m n. x pow (m + n) = x pow m * x pow n`,
 836   GEN_TAC THEN INDUCT_TAC THEN
 837   ASM_REWRITE_TAC[ADD_CLAUSES; complex_pow;
 838                   COMPLEX_MUL_LID; COMPLEX_MUL_ASSOC]);;
 839
 840 let COMPLEX_POW_POW = prove
 841  (`!x m n. (x pow m) pow n = x pow (m * n)`,
 842   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 843   ASM_REWRITE_TAC[complex_pow; MULT_CLAUSES; COMPLEX_POW_ADD]);;
 844
 845 let COMPLEX_POW_1 = prove
 846  (`!x. x pow 1 = x`,
 847   REWRITE_TAC[num_CONV `1`] THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_RID]);;
 848
 849 let COMPLEX_POW_2 = prove
 850  (`!x. x pow 2 = x * x`,
 851   REWRITE_TAC[num_CONV `2`] THEN REWRITE_TAC[complex_pow; COMPLEX_POW_1]);;
 852
 853 let COMPLEX_POW_NEG = prove
 854  (`!x n. (--x) pow n = if EVEN n then x pow n else --(x pow n)`,
 855   GEN_TAC THEN INDUCT_TAC THEN
 856   ASM_REWRITE_TAC[complex_pow; EVEN] THEN
 857   ASM_CASES_TAC `EVEN n` THEN
 858   ASM_REWRITE_TAC[COMPLEX_MUL_RNEG; COMPLEX_MUL_LNEG; COMPLEX_NEG_NEG]);;
 859
 860 let COMPLEX_POW_ONE = prove
 861  (`!n. Cx(&1) pow n = Cx(&1)`,
 862   INDUCT_TAC THEN ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID]);;
 863
 864 let COMPLEX_POW_MUL = prove
 865  (`!x y n. (x * y) pow n = (x pow n) * (y pow n)`,
 866   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 867   ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID; COMPLEX_MUL_AC]);;
 868
 869 let COMPLEX_POW_DIV = prove
 870  (`!x y n. (x / y) pow n = (x pow n) / (y pow n)`,
 871   REWRITE_TAC[complex_div; COMPLEX_POW_MUL; COMPLEX_POW_INV]);;
 872
 873 let COMPLEX_POW_II_2 = prove
 874  (`ii pow 2 = --Cx(&1)`,
 875   REWRITE_TAC[ii; COMPLEX_POW_2; complex_mul; CX_DEF; RE; IM; complex_neg] THEN
 876   CONV_TAC REAL_RAT_REDUCE_CONV);;
 877
 878 let COMPLEX_POW_EQ_0 = prove
 879  (`!x n. (x pow n = Cx(&0)) <=> (x = Cx(&0)) /\ ~(n = 0)`,
 880   GEN_TAC THEN INDUCT_TAC THEN
 881   ASM_REWRITE_TAC[NOT_SUC; complex_pow; COMPLEX_ENTIRE] THENL
 882    [SIMPLE_COMPLEX_ARITH_TAC; CONV_TAC TAUT]);;
 883
 884 let COMPLEX_POW_ZERO = prove
 885  (`!n. Cx(&0) pow n = if n = 0 then Cx(&1) else Cx(&0)`,
 886   INDUCT_TAC THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_LZERO; NOT_SUC]);;
 887
 888 let COMPLEX_INV_II = prove
 889  (`inv ii = --ii`,
 890   CONV_TAC COMPLEX_FIELD);;
 891
 892 let COMPLEX_DIV_POW = prove
 893  (`!x:complex n k:num.
 894       ~(x= Cx(&0)) /\ k <= n /\ ~(k = 0)
 895       ==> x pow (n - k) = x pow n / x pow k`,
 896   REPEAT STRIP_TAC THEN SUBGOAL_THEN `x:complex pow (n - k) * x pow k =
 897   x pow n / x pow k * x pow k` (fun th-> ASM_MESON_TAC
 898   [th;COMPLEX_POW_EQ_0;COMPLEX_EQ_MUL_RCANCEL])
 899   THEN ASM_SIMP_TAC[GSYM COMPLEX_POW_ADD;SUB_ADD] THEN
 900   MP_TAC (MESON [COMPLEX_POW_EQ_0;ASSUME `~(k = 0)`; ASSUME `~(x = Cx(&0))`]
 901   `~(x pow k = Cx(&0))`) THEN ASM_SIMP_TAC[COMPLEX_DIV_RMUL]);;
 902
 903 let COMPLEX_DIV_POW2 = prove
 904  (`!z m n. ~(z = Cx(&0))
 905            ==> z pow m / z pow n =
 906                if n <= m then z pow (m - n) else inv(z pow (n - m))`,
 907   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
 908   ASM_SIMP_TAC[COMPLEX_POW_EQ_0; COMPLEX_FIELD
 909     `~(b = Cx(&0)) /\ ~(c = Cx(&0))
 910      ==> (a / b = inv c <=> a * c = b)`] THEN
 911   ASM_SIMP_TAC[COMPLEX_POW_EQ_0; COMPLEX_FIELD
 912    `~(b = Cx(&0)) ==> (a / b = c <=> b * c = a)`] THEN
 913   REWRITE_TAC[GSYM COMPLEX_POW_ADD] THEN AP_TERM_TAC THEN ASM_ARITH_TAC);;
 914
 915 (* ------------------------------------------------------------------------- *)
 916 (* Norms (aka "moduli").                                                     *)
 917 (* ------------------------------------------------------------------------- *)
 918
 919 let COMPLEX_VEC_0 = prove
 920  (`vec 0 = Cx(&0)`,
 921   SIMP_TAC[CART_EQ; VEC_COMPONENT; CX_DEF; complex;
 922            DIMINDEX_2; FORALL_2; VECTOR_2]);;
 923
 924 let COMPLEX_NORM_ZERO = prove
 925  (`!z. (norm z = &0) <=> (z = Cx(&0))`,
 926   REWRITE_TAC[NORM_EQ_0; COMPLEX_VEC_0]);;
 927
 928 let COMPLEX_NORM_NUM = prove
 929  (`!n. norm(Cx(&n)) = &n`,
 930   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM]);;
 931
 932 let COMPLEX_NORM_0 = prove
 933  (`norm(Cx(&0)) = &0`,
 934   MESON_TAC[COMPLEX_NORM_ZERO]);;
 935
 936 let COMPLEX_NORM_NZ = prove
 937  (`!z. &0 < norm(z) <=> ~(z = Cx(&0))`,
 938   REWRITE_TAC[NORM_POS_LT; COMPLEX_VEC_0]);;
 939
 940 let COMPLEX_NORM_MUL = prove
 941  (`!w z. norm(w * z) = norm(w) * norm(z)`,
 942   REPEAT GEN_TAC THEN REWRITE_TAC[complex_norm; complex_mul; RE; IM] THEN
 943   SIMP_TAC[GSYM SQRT_MUL; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
 944   AP_TERM_TAC THEN REAL_ARITH_TAC);;
 945
 946 let COMPLEX_NORM_POW = prove
 947  (`!z n. norm(z pow n) = norm(z) pow n`,
 948   GEN_TAC THEN INDUCT_TAC THEN
 949   ASM_REWRITE_TAC[complex_pow; real_pow; COMPLEX_NORM_NUM; COMPLEX_NORM_MUL]);;
 950
 951 let COMPLEX_NORM_INV = prove
 952  (`!z. norm(inv z) = inv(norm z)`,
 953   GEN_TAC THEN REWRITE_TAC[complex_norm; complex_inv; RE; IM] THEN
 954   REWRITE_TAC[REAL_POW_2; real_div] THEN
 955   REWRITE_TAC[REAL_ARITH `(r * d) * r * d + (--i * d) * --i * d =
 956                           (r * r + i * i) * d * d:real`] THEN
 957   ASM_CASES_TAC `Re z * Re z + Im z * Im z = &0` THENL
 958    [ASM_REWRITE_TAC[REAL_INV_0; SQRT_0; REAL_MUL_LZERO]; ALL_TAC] THEN
 959   CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN
 960   SIMP_TAC[GSYM SQRT_MUL; REAL_LE_MUL; REAL_LE_INV_EQ; REAL_LE_ADD;
 961            REAL_LE_SQUARE] THEN
 962   ONCE_REWRITE_TAC[AC REAL_MUL_AC
 963    `a * a * b * b:real = (a * b) * (a * b)`] THEN
 964   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; SQRT_1]);;
 965
 966 let COMPLEX_NORM_DIV = prove
 967  (`!w z. norm(w / z) = norm(w) / norm(z)`,
 968   REWRITE_TAC[complex_div; real_div; COMPLEX_NORM_INV; COMPLEX_NORM_MUL]);;
 969
 970 let COMPLEX_NORM_TRIANGLE_SUB = prove
 971  (`!w z. norm(w) <= norm(w + z) + norm(z)`,
 972   MESON_TAC[NORM_TRIANGLE; NORM_NEG; COMPLEX_ADD_ASSOC;
 973             COMPLEX_ADD_RINV; COMPLEX_ADD_RID]);;
 974
 975 let COMPLEX_NORM_ABS_NORM = prove
 976  (`!w z. abs(norm w - norm z) <= norm(w - z)`,
 977   REPEAT GEN_TAC THEN
 978   MATCH_MP_TAC(REAL_ARITH
 979    `a - b <= x /\ b - a <= x ==> abs(a - b) <= x:real`) THEN
 980   MESON_TAC[COMPLEX_NEG_SUB; NORM_NEG; REAL_LE_SUB_RADD; complex_sub;
 981             COMPLEX_NORM_TRIANGLE_SUB]);;
 982
 983 let COMPLEX_POW_EQ_1 = prove
 984  (`!z n. z pow n = Cx(&1) ==> norm(z) = &1 \/ n = 0`,
 985   REPEAT GEN_TAC THEN
 986   DISCH_THEN(MP_TAC o AP_TERM `norm:complex->real`) THEN
 987   SIMP_TAC[COMPLEX_NORM_POW; COMPLEX_NORM_CX; REAL_POW_EQ_1; REAL_ABS_NUM] THEN
 988   SIMP_TAC[REAL_ABS_NORM] THEN CONV_TAC TAUT);;
 989
 990 (* ------------------------------------------------------------------------- *)
 991 (* Complex conjugate.                                                        *)
 992 (* ------------------------------------------------------------------------- *)
 993
 994 let cnj = new_definition
 995   `cnj(z) = complex(Re(z),--(Im(z)))`;;
 996
 997 (* ------------------------------------------------------------------------- *)
 998 (* Conjugation is an automorphism.                                           *)
 999 (* ------------------------------------------------------------------------- *)
1000
1001 let CNJ_INJ = prove
1002  (`!w z. (cnj(w) = cnj(z)) <=> (w = z)`,
1003   REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_EQ_NEG2]);;
1004
1005 let CNJ_CNJ = prove
1006  (`!z. cnj(cnj z) = z`,
1007   REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_NEG_NEG]);;
1008
1009 let CNJ_CX = prove
1010  (`!x. cnj(Cx x) = Cx x`,
1011   REWRITE_TAC[cnj; COMPLEX_EQ; CX_DEF; REAL_NEG_0; RE; IM]);;
1012
1013 let COMPLEX_NORM_CNJ = prove
1014  (`!z. norm(cnj z) = norm(z)`,
1015   REWRITE_TAC[complex_norm; cnj; REAL_POW_2] THEN
1016   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; RE; IM; REAL_NEG_NEG]);;
1017
1018 let CNJ_NEG = prove
1019  (`!z. cnj(--z) = --(cnj z)`,
1020   REWRITE_TAC[cnj; complex_neg; COMPLEX_EQ; RE; IM]);;
1021
1022 let CNJ_INV = prove
1023  (`!z. cnj(inv z) = inv(cnj z)`,
1024   REWRITE_TAC[cnj; complex_inv; COMPLEX_EQ; RE; IM] THEN
1025   REWRITE_TAC[real_div; REAL_NEG_NEG; REAL_POW_2;
1026               REAL_MUL_LNEG; REAL_MUL_RNEG]);;
1027
1028 let CNJ_ADD = prove
1029  (`!w z. cnj(w + z) = cnj(w) + cnj(z)`,
1030   REWRITE_TAC[cnj; complex_add; COMPLEX_EQ; RE; IM] THEN
1031   REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
1032
1033 let CNJ_SUB = prove
1034  (`!w z. cnj(w - z) = cnj(w) - cnj(z)`,
1035   REWRITE_TAC[complex_sub; CNJ_ADD; CNJ_NEG]);;
1036
1037 let CNJ_MUL = prove
1038  (`!w z. cnj(w * z) = cnj(w) * cnj(z)`,
1039   REWRITE_TAC[cnj; complex_mul; COMPLEX_EQ; RE; IM] THEN
1040   REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
1041
1042 let CNJ_DIV = prove
1043  (`!w z. cnj(w / z) = cnj(w) / cnj(z)`,
1044   REWRITE_TAC[complex_div; CNJ_MUL; CNJ_INV]);;
1045
1046 let CNJ_POW = prove
1047  (`!z n. cnj(z pow n) = cnj(z) pow n`,
1048   GEN_TAC THEN INDUCT_TAC THEN
1049   ASM_REWRITE_TAC[complex_pow; CNJ_MUL; CNJ_CX]);;
1050
1051 let RE_CNJ = prove
1052  (`!z. Re(cnj z) = Re z`,
1053   REWRITE_TAC[cnj; RE]);;
1054
1055 let IM_CNJ = prove
1056  (`!z. Im(cnj z) = --Im z`,
1057   REWRITE_TAC[cnj; IM]);;
1058
1059 let CNJ_EQ_CX = prove
1060  (`!x z. cnj z = Cx x <=> z = Cx x`,
1061   REWRITE_TAC[COMPLEX_EQ; RE_CNJ; IM_CNJ; RE_CX; IM_CX] THEN
1062   CONV_TAC REAL_RING);;
1063
1064 let CNJ_EQ_0 = prove
1065  (`!z. cnj z = Cx(&0) <=> z = Cx(&0)`,
1066   REWRITE_TAC[CNJ_EQ_CX]);;
1067
1068 let COMPLEX_ADD_CNJ = prove
1069  (`(!z. z + cnj z = Cx(&2 * Re z)) /\ (!z. cnj z + z = Cx(&2 * Re z))`,
1070   REWRITE_TAC[COMPLEX_EQ; RE_CX; IM_CX; RE_ADD; IM_ADD; RE_CNJ; IM_CNJ] THEN
1071   REAL_ARITH_TAC);;
1072
1073 let CNJ_II = prove
1074  (`cnj ii = --ii`,
1075   REWRITE_TAC[cnj; ii; RE; IM; complex_neg; REAL_NEG_0]);;
1076
1077 let CX_RE_CNJ = prove
1078  (`!z. Cx(Re z) = (z + cnj z) / Cx(&2)`,
1079   REWRITE_TAC[COMPLEX_EQ; RE_DIV_CX; IM_DIV_CX; RE_CX; IM_CX] THEN
1080   REWRITE_TAC[RE_ADD; IM_ADD; RE_CNJ; IM_CNJ] THEN REAL_ARITH_TAC);;
1081
1082 let CX_IM_CNJ = prove
1083  (`!z. Cx(Im z) = --ii * (z - cnj z) / Cx(&2)`,
1084   REWRITE_TAC[COMPLEX_EQ; RE_DIV_CX; IM_DIV_CX; RE_CX; IM_CX;
1085               COMPLEX_MUL_LNEG; RE_NEG; IM_NEG; RE_MUL_II; IM_MUL_II] THEN
1086   REWRITE_TAC[RE_SUB; IM_SUB; RE_CNJ; IM_CNJ] THEN REAL_ARITH_TAC);;
1087
1088 let FORALL_CNJ = prove
1089  (`(!z. P(cnj z)) <=> (!z. P z)`,
1090   MESON_TAC[CNJ_CNJ]);;
1091
1092 let EXISTS_CNJ = prove
1093  (`(?z. P(cnj z)) <=> (?z. P z)`,
1094   MESON_TAC[CNJ_CNJ]);;
1095
1096 (* ------------------------------------------------------------------------- *)
1097 (* Slightly ad hoc theorems relating multiplication, inverse and conjugation *)
1098 (* ------------------------------------------------------------------------- *)
1099
1100 let COMPLEX_NORM_POW_2 = prove
1101  (`!z. Cx(norm z) pow 2 = z * cnj z`,
1102   GEN_TAC THEN REWRITE_TAC [GSYM CX_POW; COMPLEX_SQNORM] THEN
1103   REWRITE_TAC [cnj; complex_mul; CX_DEF; RE; IM; COMPLEX_EQ] THEN
1104   CONV_TAC REAL_RING);;
1105
1106 let COMPLEX_MUL_CNJ = prove
1107  (`!z. cnj z * z = Cx(norm(z)) pow 2 /\ z * cnj z = Cx(norm(z)) pow 2`,
1108   GEN_TAC THEN REWRITE_TAC[COMPLEX_MUL_SYM] THEN
1109   REWRITE_TAC[cnj; complex_mul; RE; IM; GSYM CX_POW; COMPLEX_SQNORM] THEN
1110   REWRITE_TAC[CX_DEF] THEN AP_TERM_TAC THEN BINOP_TAC THEN
1111   CONV_TAC REAL_RING);;
1112
1113 let COMPLEX_INV_CNJ = prove
1114  (`!z. inv z = cnj z / Cx(norm z) pow 2`,
1115   GEN_TAC THEN ASM_CASES_TAC `z = Cx(&0)` THENL
1116    [ASM_REWRITE_TAC[CNJ_CX; complex_div; COMPLEX_INV_0; COMPLEX_MUL_LZERO];
1117     MATCH_MP_TAC(COMPLEX_FIELD
1118      `x * y = z /\ ~(x = Cx(&0)) /\ ~(z = Cx(&0)) ==> inv x = y / z`) THEN
1119     ASM_REWRITE_TAC[COMPLEX_MUL_CNJ; GSYM CX_POW; CX_INJ; REAL_POW_EQ_0] THEN
1120     ASM_REWRITE_TAC[COMPLEX_NORM_ZERO; ARITH]]);;
1121
1122 let COMPLEX_DIV_CNJ = prove
1123  (`!a b. a / b = (a * cnj b) / Cx(norm b) pow 2`,
1124   REPEAT GEN_TAC THEN REWRITE_TAC[complex_div; GSYM COMPLEX_MUL_ASSOC] THEN
1125   AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [COMPLEX_INV_CNJ] THEN
1126   REWRITE_TAC[complex_div]);;
1127
1128 let RE_COMPLEX_DIV_EQ_0 = prove
1129  (`!a b. Re(a / b) = &0 <=> Re(a * cnj b) = &0`,
1130   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
1131   REWRITE_TAC[complex_div; GSYM CX_POW; GSYM CX_INV] THEN
1132   REWRITE_TAC[RE_MUL_CX; REAL_INV_EQ_0; REAL_POW_EQ_0; ARITH;
1133               REAL_ENTIRE; COMPLEX_NORM_ZERO] THEN
1134   ASM_CASES_TAC `b = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
1135   REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; RE_CX]);;
1136
1137 let IM_COMPLEX_DIV_EQ_0 = prove
1138  (`!a b. Im(a / b) = &0 <=> Im(a * cnj b) = &0`,
1139   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
1140   REWRITE_TAC[complex_div; GSYM CX_POW; GSYM CX_INV] THEN
1141   REWRITE_TAC[IM_MUL_CX; REAL_INV_EQ_0; REAL_POW_EQ_0; ARITH;
1142               REAL_ENTIRE; COMPLEX_NORM_ZERO] THEN
1143   ASM_CASES_TAC `b = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
1144   REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; IM_CX]);;
1145
1146 let RE_COMPLEX_DIV_GT_0 = prove
1147  (`!a b. &0 < Re(a / b) <=> &0 < Re(a * cnj b)`,
1148   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
1149   REWRITE_TAC[complex_div; GSYM CX_POW; GSYM CX_INV] THEN
1150   REWRITE_TAC[RE_MUL_CX; REAL_INV_EQ_0; REAL_POW_EQ_0; ARITH;
1151               REAL_ENTIRE; COMPLEX_NORM_ZERO] THEN
1152   ASM_CASES_TAC `b = Cx(&0)` THEN
1153   ASM_REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; RE_CX; REAL_MUL_LZERO] THEN
1154   REWRITE_TAC[REAL_ARITH `&0 < a * x <=> &0 * x < a * x`] THEN
1155   ASM_SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_INV_EQ; REAL_POW_LT; ARITH;
1156                COMPLEX_NORM_NZ]);;
1157
1158 let IM_COMPLEX_DIV_GT_0 = prove
1159  (`!a b. &0 < Im(a / b) <=> &0 < Im(a * cnj b)`,
1160   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_DIV_CNJ] THEN
1161   REWRITE_TAC[complex_div; GSYM CX_POW; GSYM CX_INV] THEN
1162   REWRITE_TAC[IM_MUL_CX; REAL_INV_EQ_0; REAL_POW_EQ_0; ARITH;
1163               REAL_ENTIRE; COMPLEX_NORM_ZERO] THEN
1164   ASM_CASES_TAC `b = Cx(&0)` THEN
1165   ASM_REWRITE_TAC[CNJ_CX; COMPLEX_MUL_RZERO; IM_CX; REAL_MUL_LZERO] THEN
1166   REWRITE_TAC[REAL_ARITH `&0 < a * x <=> &0 * x < a * x`] THEN
1167   ASM_SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_INV_EQ; REAL_POW_LT; ARITH;
1168                COMPLEX_NORM_NZ]);;
1169
1170 let RE_COMPLEX_DIV_GE_0 = prove
1171  (`!a b. &0 <= Re(a / b) <=> &0 <= Re(a * cnj b)`,
1172   REWRITE_TAC[REAL_ARITH `&0 <= x <=> &0 < x \/ x = &0`] THEN
1173   REWRITE_TAC[RE_COMPLEX_DIV_GT_0; RE_COMPLEX_DIV_EQ_0]);;
1174
1175 let IM_COMPLEX_DIV_GE_0 = prove
1176  (`!a b. &0 <= Im(a / b) <=> &0 <= Im(a * cnj b)`,
1177   REWRITE_TAC[REAL_ARITH `&0 <= x <=> &0 < x \/ x = &0`] THEN
1178   REWRITE_TAC[IM_COMPLEX_DIV_GT_0; IM_COMPLEX_DIV_EQ_0]);;
1179
1180 let RE_COMPLEX_DIV_LE_0 = prove
1181  (`!a b. Re(a / b) <= &0 <=> Re(a * cnj b) <= &0`,
1182   REWRITE_TAC[GSYM REAL_NOT_LT; RE_COMPLEX_DIV_GT_0]);;
1183
1184 let IM_COMPLEX_DIV_LE_0 = prove
1185  (`!a b. Im(a / b) <= &0 <=> Im(a * cnj b) <= &0`,
1186   REWRITE_TAC[GSYM REAL_NOT_LT; IM_COMPLEX_DIV_GT_0]);;
1187
1188 let RE_COMPLEX_DIV_LT_0 = prove
1189  (`!a b. Re(a / b) < &0 <=> Re(a * cnj b) < &0`,
1190   REWRITE_TAC[GSYM REAL_NOT_LE; RE_COMPLEX_DIV_GE_0]);;
1191
1192 let IM_COMPLEX_DIV_LT_0 = prove
1193  (`!a b. Im(a / b) < &0 <=> Im(a * cnj b) < &0`,
1194   REWRITE_TAC[GSYM REAL_NOT_LE; IM_COMPLEX_DIV_GE_0]);;
1195
1196 let IM_COMPLEX_INV_GE_0 = prove
1197  (`!z. &0 <= Im(inv z) <=> Im(z) <= &0`,
1198   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `z:complex`] IM_COMPLEX_DIV_GE_0) THEN
1199   REWRITE_TAC[complex_div; COMPLEX_MUL_LID; IM_CNJ] THEN REAL_ARITH_TAC);;
1200
1201 let IM_COMPLEX_INV_LE_0 = prove
1202  (`!z. Im(inv z) <= &0 <=> &0 <= Im(z)`,
1203   MESON_TAC[IM_COMPLEX_INV_GE_0; COMPLEX_INV_INV]);;
1204
1205 let IM_COMPLEX_INV_GT_0 = prove
1206  (`!z. &0 < Im(inv z) <=> Im(z) < &0`,
1207   REWRITE_TAC[REAL_ARITH `&0 < a <=> ~(a <= &0)`; IM_COMPLEX_INV_LE_0] THEN
1208   REAL_ARITH_TAC);;
1209
1210 let IM_COMPLEX_INV_LT_0 = prove
1211  (`!z. Im(inv z) < &0 <=> &0 < Im(z)`,
1212   REWRITE_TAC[REAL_ARITH `a < &0 <=> ~(&0 <= a)`; IM_COMPLEX_INV_GE_0] THEN
1213   REAL_ARITH_TAC);;
1214
1215 let IM_COMPLEX_INV_EQ_0 = prove
1216  (`!z. Im(inv z) = &0 <=> Im(z) = &0`,
1217   SIMP_TAC[GSYM REAL_LE_ANTISYM; IM_COMPLEX_INV_LE_0; IM_COMPLEX_INV_GE_0] THEN
1218   REAL_ARITH_TAC);;
1219
1220 let REAL_SGN_RE_COMPLEX_DIV = prove
1221  (`!w z. real_sgn(Re(w / z)) = real_sgn(Re(w * cnj z))`,
1222   REWRITE_TAC[real_sgn; RE_COMPLEX_DIV_GT_0; RE_COMPLEX_DIV_GE_0;
1223               REAL_ARITH `x < &0 <=> ~(&0 <= x)`]);;
1224
1225 let REAL_SGN_IM_COMPLEX_DIV = prove
1226  (`!w z. real_sgn(Im(w / z)) = real_sgn(Im(w * cnj z))`,
1227   REWRITE_TAC[real_sgn; IM_COMPLEX_DIV_GT_0; IM_COMPLEX_DIV_GE_0;
1228               REAL_ARITH `x < &0 <=> ~(&0 <= x)`]);;
1229
1230 (* ------------------------------------------------------------------------- *)
1231 (* Norm versus components for complex numbers.                               *)
1232 (* ------------------------------------------------------------------------- *)
1233
1234 let COMPLEX_NORM_GE_RE_IM = prove
1235  (`!z. abs(Re(z)) <= norm(z) /\ abs(Im(z)) <= norm(z)`,
1236   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN
1237   REWRITE_TAC[complex_norm] THEN
1238   CONJ_TAC THEN
1239   MATCH_MP_TAC SQRT_MONO_LE THEN
1240   ASM_SIMP_TAC[REAL_LE_ADDR; REAL_LE_ADDL; REAL_POW_2; REAL_LE_SQUARE]);;
1241
1242 let COMPLEX_NORM_LE_RE_IM = prove
1243  (`!z. norm(z) <= abs(Re z) + abs(Im z)`,
1244   GEN_TAC THEN MP_TAC(ISPEC `z:complex` NORM_LE_L1) THEN
1245   REWRITE_TAC[DIMINDEX_2; SUM_2; RE_DEF; IM_DEF]);;
1246
1247 let COMPLEX_L1_LE_NORM = prove
1248  (`!z. sqrt(&2) / &2 * (abs(Re z) + abs(Im z)) <= norm z`,
1249   GEN_TAC THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `sqrt(&2)` THEN
1250   SIMP_TAC[REAL_ARITH `x * x / &2 * y = (x pow 2) / &2 * y`;
1251            SQRT_POW_2; REAL_POS; SQRT_POS_LT; REAL_OF_NUM_LT; ARITH] THEN
1252   MP_TAC(ISPEC `z:complex` L1_LE_NORM) THEN
1253   REWRITE_TAC[DIMINDEX_2; SUM_2; RE_DEF; IM_DEF] THEN REAL_ARITH_TAC);;
1254
1255 (* ------------------------------------------------------------------------- *)
1256 (* Complex square roots.                                                     *)
1257 (* ------------------------------------------------------------------------- *)
1258
1259 let csqrt = new_definition
1260   `csqrt(z) = if Im(z) = &0 then
1261                 if &0 <= Re(z) then complex(sqrt(Re(z)),&0)
1262                 else complex(&0,sqrt(--Re(z)))
1263               else complex(sqrt((norm(z) + Re(z)) / &2),
1264                            (Im(z) / abs(Im(z))) *
1265                            sqrt((norm(z) - Re(z)) / &2))`;;
1266
1267
1268 let CSQRT = prove
1269  (`!z. csqrt(z) pow 2 = z`,
1270   GEN_TAC THEN REWRITE_TAC[COMPLEX_POW_2; csqrt] THEN COND_CASES_TAC THENL
1271    [COND_CASES_TAC THEN
1272     ASM_REWRITE_TAC[CX_DEF; complex_mul; RE; IM; REAL_MUL_RZERO; REAL_MUL_LZERO;
1273       REAL_SUB_LZERO; REAL_SUB_RZERO; REAL_ADD_LID; COMPLEX_EQ] THEN
1274     REWRITE_TAC[REAL_NEG_EQ; GSYM REAL_POW_2] THEN
1275     ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `~(&0 <= x) ==> &0 <= --x`];
1276     ALL_TAC] THEN
1277   REWRITE_TAC[complex_mul; RE; IM] THEN
1278   ONCE_REWRITE_TAC[REAL_ARITH
1279    `(s * s - (i * s') * (i * s') = s * s - (i * i) * (s' * s')) /\
1280     (s * i * s' + (i * s')* s = &2 * i * s * s')`] THEN
1281   REWRITE_TAC[GSYM REAL_POW_2] THEN
1282   SUBGOAL_THEN `&0 <= norm(z) + Re(z) /\ &0 <= norm(z) - Re(z)`
1283   STRIP_ASSUME_TAC THENL
1284    [MP_TAC(SPEC `z:complex` COMPLEX_NORM_GE_RE_IM) THEN REAL_ARITH_TAC;
1285     ALL_TAC] THEN
1286   ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; GSYM SQRT_MUL; SQRT_POW_2] THEN
1287   REWRITE_TAC[COMPLEX_EQ; RE; IM] THEN CONJ_TAC THENL
1288    [ASM_SIMP_TAC[REAL_POW_DIV; REAL_POW2_ABS;
1289                  REAL_POW_EQ_0; REAL_DIV_REFL] THEN
1290     REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_SUB_RDISTRIB] THEN
1291     REWRITE_TAC[REAL_ARITH `(m + r) - (m - r) = r * &2`] THEN
1292     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1293     REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN
1294   REWRITE_TAC[real_div] THEN
1295   ONCE_REWRITE_TAC[AC REAL_MUL_AC
1296     `(a * b) * a' * b = (a * a') * (b * b:real)`] THEN
1297   REWRITE_TAC[REAL_DIFFSQ] THEN
1298   REWRITE_TAC[complex_norm; GSYM REAL_POW_2] THEN
1299   SIMP_TAC[SQRT_POW_2; REAL_LE_ADD;
1300            REWRITE_RULE[GSYM REAL_POW_2] REAL_LE_SQUARE] THEN
1301   REWRITE_TAC[REAL_ADD_SUB; GSYM REAL_POW_MUL] THEN
1302   REWRITE_TAC[POW_2_SQRT_ABS] THEN
1303   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_INV; REAL_ABS_NUM] THEN
1304   ONCE_REWRITE_TAC[AC REAL_MUL_AC
1305     `&2 * (i * a') * a * h = i * (&2 * h) * a * a'`] THEN
1306   CONV_TAC REAL_RAT_REDUCE_CONV THEN
1307   REWRITE_TAC[REAL_MUL_LID; GSYM real_div] THEN
1308   ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ABS_ZERO; REAL_MUL_RID]);;
1309
1310 let CX_SQRT = prove
1311  (`!x. &0 <= x ==> Cx(sqrt x) = csqrt(Cx x)`,
1312   SIMP_TAC[csqrt; IM_CX; RE_CX; COMPLEX_EQ; RE; IM]);;
1313
1314 let CSQRT_CX = prove
1315  (`!x. &0 <= x ==> csqrt(Cx x) = Cx(sqrt x)`,
1316   SIMP_TAC[CX_SQRT]);;
1317
1318 let CSQRT_0 = prove
1319  (`csqrt(Cx(&0)) = Cx(&0)`,
1320   SIMP_TAC[CSQRT_CX; REAL_POS; SQRT_0]);;
1321
1322 let CSQRT_1 = prove
1323  (`csqrt(Cx(&1)) = Cx(&1)`,
1324   SIMP_TAC[CSQRT_CX; REAL_POS; SQRT_1]);;
1325
1326 let CSQRT_PRINCIPAL = prove
1327  (`!z. &0 < Re(csqrt(z)) \/ Re(csqrt(z)) = &0 /\ &0 <= Im(csqrt(z))`,
1328   GEN_TAC THEN REWRITE_TAC[csqrt] THEN
1329   REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[RE; IM]) THENL
1330    [FIRST_ASSUM(MP_TAC o MATCH_MP SQRT_POS_LE) THEN REAL_ARITH_TAC;
1331     DISJ2_TAC THEN REWRITE_TAC[real_ge] THEN MATCH_MP_TAC SQRT_POS_LE THEN
1332     ASM_REAL_ARITH_TAC;
1333     DISJ1_TAC THEN MATCH_MP_TAC SQRT_POS_LT THEN
1334     MATCH_MP_TAC(REAL_ARITH `abs(y) < x ==> &0 < (x + y) / &2`) THEN
1335     REWRITE_TAC[complex_norm] THEN REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN
1336     MATCH_MP_TAC SQRT_MONO_LT THEN
1337     REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_LT_ADDR] THEN
1338     REWRITE_TAC[REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN
1339     ASM_REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]]);;
1340
1341 let RE_CSQRT = prove
1342  (`!z. &0 <= Re(csqrt z)`,
1343   MP_TAC CSQRT_PRINCIPAL THEN MATCH_MP_TAC MONO_FORALL THEN REAL_ARITH_TAC);;
1344
1345 let CSQRT_UNIQUE = prove
1346  (`!s z. s pow 2 = z /\ (&0 < Re s \/ Re s = &0 /\ &0 <= Im s)
1347          ==> csqrt z = s`,
1348   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
1349   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
1350   MP_TAC(SPEC `(s:complex) pow 2` CSQRT) THEN
1351   SIMP_TAC[COMPLEX_RING `a pow 2 = b pow 2 <=> a = b \/ a = --b:complex`] THEN
1352   STRIP_TAC THEN ASM_REWRITE_TAC[COMPLEX_RING `--z = z <=> z = Cx(&0)`] THEN
1353   FIRST_ASSUM(MP_TAC o AP_TERM `Re`) THEN
1354   FIRST_X_ASSUM(MP_TAC o AP_TERM `Im`) THEN
1355   REWRITE_TAC[RE_NEG; IM_NEG; COMPLEX_EQ; RE_CX; IM_CX] THEN
1356   MP_TAC(SPEC `(s:complex) pow 2` CSQRT_PRINCIPAL) THEN
1357   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
1358
1359 let POW_2_CSQRT = prove
1360  (`!z. &0 < Re z \/ Re(z) = &0 /\ &0 <= Im(z) ==> csqrt(z pow 2) = z`,
1361   MESON_TAC[CSQRT_UNIQUE]);;
1362
1363 let CSQRT_EQ_0 = prove
1364  (`!z. csqrt z = Cx(&0) <=> z = Cx(&0)`,
1365   GEN_TAC THEN MP_TAC (SPEC `z:complex` CSQRT) THEN CONV_TAC COMPLEX_RING);;
1366
1367 (* ------------------------------------------------------------------------- *)
1368 (* A few more complex-specific cases of vector notions.                      *)
1369 (* ------------------------------------------------------------------------- *)
1370
1371 let COMPLEX_CMUL = prove
1372  (`!c x. c % x = Cx(c) * x`,
1373   SIMP_TAC[CART_EQ; VECTOR_MUL_COMPONENT; CX_DEF; complex;
1374            complex_mul; DIMINDEX_2; FORALL_2; IM_DEF; RE_DEF; VECTOR_2] THEN
1375   REAL_ARITH_TAC);;
1376
1377 let LINEAR_COMPLEX_MUL = prove
1378  (`!c. linear (\x. c * x)`,
1379    REWRITE_TAC[linear; COMPLEX_CMUL] THEN CONV_TAC COMPLEX_RING);;
1380
1381 let BILINEAR_COMPLEX_MUL = prove
1382  (`bilinear( * )`,
1383   REWRITE_TAC[bilinear; linear; COMPLEX_CMUL] THEN  CONV_TAC COMPLEX_RING);;
1384
1385 let LINEAR_CNJ = prove
1386  (`linear cnj`,
1387   REWRITE_TAC[linear; COMPLEX_CMUL; CNJ_ADD; CNJ_MUL; CNJ_CX]);;
1388
1389 (* ------------------------------------------------------------------------- *)
1390 (* Complex-specific theorems about sums.                                     *)
1391 (* ------------------------------------------------------------------------- *)
1392
1393 let RE_VSUM = prove
1394  (`!f s. FINITE s ==> Re(vsum s f) = sum s (\x. Re(f x))`,
1395   SIMP_TAC[RE_DEF; VSUM_COMPONENT; DIMINDEX_2; ARITH]);;
1396
1397 let IM_VSUM = prove
1398  (`!f s. FINITE s ==> Im(vsum s f) = sum s (\x. Im(f x))`,
1399   SIMP_TAC[IM_DEF; VSUM_COMPONENT; DIMINDEX_2; ARITH]);;
1400
1401 let VSUM_COMPLEX_LMUL = prove
1402  (`!c f s. FINITE(s) ==> vsum s (\x. c * f x) = c * vsum s f`,
1403   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1404   SIMP_TAC[VSUM_CLAUSES; COMPLEX_VEC_0; COMPLEX_MUL_RZERO] THEN
1405   SIMPLE_COMPLEX_ARITH_TAC);;
1406
1407 let VSUM_COMPLEX_RMUL = prove
1408  (`!c f s. FINITE(s) ==> vsum s (\x. f x * c) = vsum s f * c`,
1409   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN REWRITE_TAC[VSUM_COMPLEX_LMUL]);;
1410
1411 let VSUM_CX = prove
1412  (`!f:A->real s. vsum s (\a. Cx(f a)) = Cx(sum s f)`,
1413   SIMP_TAC[CART_EQ; VSUM_COMPONENT] THEN
1414   REWRITE_TAC[DIMINDEX_2; FORALL_2; GSYM RE_DEF; GSYM IM_DEF] THEN
1415   REWRITE_TAC[IM_CX; SUM_0; RE_CX; ETA_AX]);;
1416
1417 let CNJ_VSUM = prove
1418  (`!f s. FINITE s ==> cnj(vsum s f) = vsum s (\x. cnj(f x))`,
1419   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1420   SIMP_TAC[VSUM_CLAUSES; CNJ_ADD; CNJ_CX; COMPLEX_VEC_0]);;
1421
1422 let VSUM_CX_NUMSEG = prove
1423  (`!f m n. vsum (m..n) (\a. Cx(f a)) = Cx(sum (m..n) f)`,
1424   SIMP_TAC[VSUM_CX; FINITE_NUMSEG]);;
1425
1426 let COMPLEX_SUB_POW = prove
1427  (`!x y n.
1428         1 <= n ==> x pow n - y pow n =
1429                    (x - y) * vsum(0..n-1) (\i. x pow i * y pow (n - 1 - i))`,
1430   SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; FINITE_NUMSEG] THEN
1431   REWRITE_TAC[COMPLEX_RING
1432    `(x - y) * (a * b):complex = (x * a) * b - a * (y * b)`] THEN
1433   SIMP_TAC[GSYM complex_pow; ADD1; ARITH_RULE
1434     `1 <= n /\ x <= n - 1
1435      ==> n - 1 - x = n - (x + 1) /\ SUC(n - 1 - x) = n - x`] THEN
1436   REWRITE_TAC[VSUM_DIFFS_ALT; LE_0] THEN
1437   SIMP_TAC[SUB_0; SUB_ADD; SUB_REFL;
1438            complex_pow; COMPLEX_MUL_LID; COMPLEX_MUL_RID]);;
1439
1440 let COMPLEX_SUB_POW_R1 = prove
1441  (`!x n. 1 <= n
1442          ==> x pow n - Cx(&1) = (x - Cx(&1)) * vsum(0..n-1) (\i. x pow i)`,
1443   REPEAT GEN_TAC THEN
1444   DISCH_THEN(MP_TAC o SPECL [`x:complex`; `Cx(&1)`] o
1445     MATCH_MP COMPLEX_SUB_POW) THEN
1446   REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_MUL_RID]);;
1447
1448 let COMPLEX_SUB_POW_L1 = prove
1449  (`!x n. 1 <= n
1450          ==> Cx(&1) - x pow n = (Cx(&1) - x) * vsum(0..n-1) (\i. x pow i)`,
1451   ONCE_REWRITE_TAC[GSYM COMPLEX_NEG_SUB] THEN
1452   SIMP_TAC[COMPLEX_SUB_POW_R1] THEN REWRITE_TAC[COMPLEX_MUL_LNEG]);;
1453
1454 (* ------------------------------------------------------------------------- *)
1455 (* The complex numbers that are real (zero imaginary part).                  *)
1456 (* ------------------------------------------------------------------------- *)
1457
1458 let real = new_definition
1459  `real z <=> Im z = &0`;;
1460
1461 let REAL = prove
1462  (`!z. real z <=> Cx(Re z) = z`,
1463   REWRITE_TAC[COMPLEX_EQ; real; CX_DEF; RE; IM] THEN REAL_ARITH_TAC);;
1464
1465 let REAL_CNJ = prove
1466  (`!z. real z <=> cnj z = z`,
1467   REWRITE_TAC[real; cnj; COMPLEX_EQ; RE; IM] THEN REAL_ARITH_TAC);;
1468
1469 let REAL_IMP_CNJ = prove
1470  (`!z. real z ==> cnj z = z`,
1471   REWRITE_TAC[REAL_CNJ]);;
1472
1473 let REAL_EXISTS = prove
1474  (`!z. real z <=> ?x. z = Cx x`,
1475   MESON_TAC[REAL; real; IM_CX]);;
1476
1477 let FORALL_REAL = prove
1478  (`(!z. real z ==> P z) <=> (!x. P(Cx x))`,
1479   MESON_TAC[REAL_EXISTS]);;
1480
1481 let EXISTS_REAL = prove
1482  (`(?z. real z /\ P z) <=> (?x. P(Cx x))`,
1483   MESON_TAC[REAL_EXISTS]);;
1484
1485 let REAL_CX = prove
1486  (`!x. real(Cx x)`,
1487   REWRITE_TAC[REAL_CNJ; CNJ_CX]);;
1488
1489 let REAL_MUL_CX = prove
1490  (`!x z. real(Cx x * z) <=> x = &0 \/ real z`,
1491   REWRITE_TAC[real; IM_MUL_CX; REAL_ENTIRE]);;
1492
1493 let REAL_ADD = prove
1494  (`!w z. real w /\ real z ==> real(w + z)`,
1495   SIMP_TAC[REAL_CNJ; CNJ_ADD]);;
1496
1497 let REAL_NEG = prove
1498  (`!z. real z ==> real(--z)`,
1499   SIMP_TAC[REAL_CNJ; CNJ_NEG]);;
1500
1501 let REAL_SUB = prove
1502  (`!w z. real w /\ real z ==> real(w - z)`,
1503   SIMP_TAC[REAL_CNJ; CNJ_SUB]);;
1504
1505 let REAL_MUL = prove
1506  (`!w z. real w /\ real z ==> real(w * z)`,
1507   SIMP_TAC[REAL_CNJ; CNJ_MUL]);;
1508
1509 let REAL_POW = prove
1510  (`!z n. real z ==> real(z pow n)`,
1511   SIMP_TAC[REAL_CNJ; CNJ_POW]);;
1512
1513 let REAL_INV = prove
1514  (`!z. real z ==> real(inv z)`,
1515   SIMP_TAC[REAL_CNJ; CNJ_INV]);;
1516
1517 let REAL_INV_EQ = prove
1518  (`!z. real(inv z) = real z`,
1519   MESON_TAC[REAL_INV; COMPLEX_INV_INV]);;
1520
1521 let REAL_DIV = prove
1522  (`!w z. real w /\ real z ==> real(w / z)`,
1523   SIMP_TAC[REAL_CNJ; CNJ_DIV]);;
1524
1525 let REAL_VSUM = prove
1526  (`!f s. FINITE s /\ (!a. a IN s ==> real(f a)) ==> real(vsum s f)`,
1527   SIMP_TAC[CNJ_VSUM; REAL_CNJ]);;
1528
1529 let REAL_MUL_CNJ = prove
1530  (`(!z. real(z * cnj z)) /\ (!z. real(cnj z * z))`,
1531   REWRITE_TAC[COMPLEX_MUL_CNJ; GSYM CX_POW; REAL_CX]);;
1532
1533 let REAL_SEGMENT = prove
1534  (`!a b x. x IN segment[a,b] /\ real a /\ real b ==> real x`,
1535   SIMP_TAC[segment; IN_ELIM_THM; real; COMPLEX_EQ; LEFT_AND_EXISTS_THM;
1536            LEFT_IMP_EXISTS_THM; IM_ADD; IM_CMUL] THEN
1537   REAL_ARITH_TAC);;
1538
1539 let IN_SEGMENT_CX = prove
1540  (`!a b x. Cx(x) IN segment[Cx(a),Cx(b)] <=>
1541                 a <= x /\ x <= b \/ b <= x /\ x <= a`,
1542   REPEAT STRIP_TAC THEN REWRITE_TAC[segment; IN_ELIM_THM] THEN
1543   REWRITE_TAC[COMPLEX_CMUL; GSYM CX_ADD; CX_INJ; GSYM CX_MUL] THEN
1544   ASM_CASES_TAC `a:real = b` THENL
1545    [ASM_REWRITE_TAC[REAL_ARITH `(&1 - u) * b + u * b = b`] THEN
1546     ASM_CASES_TAC `x:real = b` THEN ASM_REWRITE_TAC[REAL_LE_ANTISYM] THEN
1547     EXISTS_TAC `&0` THEN REWRITE_TAC[REAL_POS];
1548     ALL_TAC] THEN
1549   EQ_TAC THENL
1550    [DISCH_THEN(X_CHOOSE_THEN `u:real`
1551      (CONJUNCTS_THEN2 STRIP_ASSUME_TAC SUBST1_TAC)) THEN
1552     REWRITE_TAC[REAL_ARITH `a <= (&1 - u) * a + u * b <=> &0 <= u * (b - a)`;
1553       REAL_ARITH `b <= (&1 - u) * a + u * b <=> &0 <= (&1 - u) * (a - b)`;
1554       REAL_ARITH `(&1 - u) * a + u * b <= a <=> &0 <= u * (a - b)`;
1555       REAL_ARITH `(&1 - u) * a + u * b <= b <=> &0 <= (&1 - u) * (b - a)`] THEN
1556     DISJ_CASES_TAC(REAL_ARITH `a <= b \/ b <= a`) THENL
1557      [DISJ1_TAC; DISJ2_TAC] THEN
1558     CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN
1559     ASM_REAL_ARITH_TAC;
1560     ALL_TAC] THEN
1561   STRIP_TAC THENL
1562    [SUBGOAL_THEN `&0 < b - a` ASSUME_TAC THENL
1563      [ASM_REAL_ARITH_TAC;
1564       EXISTS_TAC `(x - a:real) / (b - a)`];
1565     SUBGOAL_THEN `&0 < a - b` ASSUME_TAC THENL
1566      [ASM_REAL_ARITH_TAC;
1567       EXISTS_TAC `(a - x:real) / (a - b)`]] THEN
1568   (CONJ_TAC THENL
1569     [ALL_TAC; UNDISCH_TAC `~(a:real = b)` THEN CONV_TAC REAL_FIELD]) THEN
1570   ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
1571   ASM_REAL_ARITH_TAC);;
1572
1573 let IN_SEGMENT_CX_GEN = prove
1574  (`!a b x.
1575         x IN segment[Cx a,Cx b] <=>
1576         Im(x) = &0 /\ (a <= Re x /\ Re x <= b \/ b <= Re x /\ Re x <= a)`,
1577   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM real] THEN
1578   ASM_CASES_TAC `real x` THENL
1579    [FIRST_X_ASSUM(SUBST1_TAC o SYM o REWRITE_RULE[REAL]) THEN
1580     REWRITE_TAC[IN_SEGMENT_CX; REAL_CX; RE_CX] THEN REAL_ARITH_TAC;
1581     ASM_MESON_TAC[REAL_SEGMENT; REAL_CX]]);;
1582
1583 let RE_POS_SEGMENT = prove
1584  (`!a b x. x IN segment[a,b] /\ &0 < Re a /\ &0 < Re b ==> &0 < Re x`,
1585   SIMP_TAC[segment; IN_ELIM_THM; real; COMPLEX_EQ; LEFT_AND_EXISTS_THM;
1586            LEFT_IMP_EXISTS_THM; RE_ADD; RE_CMUL] THEN
1587   REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH
1588     `&0 <= x /\ &0 <= y /\ ~(x = &0 /\ y = &0) ==> &0 < x + y`) THEN
1589   ASM_SIMP_TAC[REAL_LE_MUL; REAL_SUB_LE; REAL_LT_IMP_LE; REAL_ENTIRE] THEN
1590   ASM_REAL_ARITH_TAC);;
1591
1592 let CONVEX_REAL = prove
1593  (`convex real`,
1594   REWRITE_TAC[convex; IN; COMPLEX_CMUL] THEN
1595   SIMP_TAC[REAL_ADD; REAL_MUL; REAL_CX]);;
1596
1597 let IMAGE_CX = prove
1598  (`!s. IMAGE Cx s = {z | real z /\ Re(z) IN s}`,
1599   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN MESON_TAC[RE_CX; REAL]);;
1600
1601 (* ------------------------------------------------------------------------- *)
1602 (* Useful bound-type theorems for real quantities.                           *)
1603 (* ------------------------------------------------------------------------- *)
1604
1605 let REAL_NORM = prove
1606  (`!z. real z ==> norm(z) = abs(Re z)`,
1607   SIMP_TAC[real; complex_norm] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1608   REWRITE_TAC[POW_2_SQRT_ABS; REAL_ADD_RID]);;
1609
1610 let REAL_NORM_POS = prove
1611  (`!z. real z /\ &0 <= Re z ==> norm(z) = Re(z)`,
1612   SIMP_TAC[REAL_NORM] THEN REAL_ARITH_TAC);;
1613
1614 let COMPLEX_NORM_VSUM_SUM_RE = prove
1615  (`!f s. FINITE s /\ (!x. x IN s ==> real(f x) /\ &0 <= Re(f x))
1616          ==> norm(vsum s f) = sum s (\x. Re(f x))`,
1617   SIMP_TAC[GSYM RE_VSUM] THEN REPEAT STRIP_TAC THEN
1618   MATCH_MP_TAC REAL_NORM_POS THEN
1619   ASM_SIMP_TAC[REAL_VSUM; RE_VSUM; SUM_POS_LE]);;
1620
1621 let COMPLEX_NORM_VSUM_BOUND = prove
1622  (`!s f:A->complex g:A->complex.
1623         FINITE s /\ (!x. x IN s ==> real(g x) /\ norm(f x) <= Re(g x))
1624         ==> norm(vsum s f) <= norm(vsum s g)`,
1625   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1626   EXISTS_TAC `sum s (\x. norm((f:A->complex) x))` THEN
1627   ASM_SIMP_TAC[VSUM_NORM] THEN
1628   MATCH_MP_TAC REAL_LE_TRANS THEN
1629   EXISTS_TAC `sum s (\x. Re((g:A->complex) x))` THEN
1630   ASM_SIMP_TAC[SUM_LE] THEN
1631   MATCH_MP_TAC(REAL_ARITH `x:real = y ==> y <= x`) THEN
1632   MATCH_MP_TAC COMPLEX_NORM_VSUM_SUM_RE THEN
1633   ASM_MESON_TAC[REAL_LE_TRANS; NORM_POS_LE]);;
1634
1635 let COMPLEX_NORM_VSUM_BOUND_SUBSET = prove
1636  (`!f:A->complex g:A->complex s t.
1637         FINITE s /\ t SUBSET s /\
1638         (!x. x IN s ==> real(g x) /\ norm(f x) <= Re(g x))
1639         ==> norm(vsum t f) <= norm(vsum s g)`,
1640   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1641   EXISTS_TAC `norm(vsum t (g:A->complex))` THEN CONJ_TAC THENL
1642    [ASM_MESON_TAC[COMPLEX_NORM_VSUM_BOUND; SUBSET; FINITE_SUBSET];ALL_TAC] THEN
1643   SUBGOAL_THEN
1644    `norm(vsum t (g:A->complex)) = sum t (\x. Re(g x)) /\
1645     norm(vsum s g) = sum s (\x. Re(g x))`
1646    (CONJUNCTS_THEN SUBST1_TAC)
1647   THENL
1648    [CONJ_TAC THEN MATCH_MP_TAC COMPLEX_NORM_VSUM_SUM_RE;
1649     MATCH_MP_TAC SUM_SUBSET THEN REWRITE_TAC[IN_DIFF]] THEN
1650   ASM_MESON_TAC[REAL_LE_TRANS; NORM_POS_LE; FINITE_SUBSET; SUBSET]);;
1651
1652 (* ------------------------------------------------------------------------- *)
1653 (* Geometric progression.                                                    *)
1654 (* ------------------------------------------------------------------------- *)
1655
1656 let VSUM_GP_BASIC = prove
1657  (`!x n. (Cx(&1) - x) * vsum(0..n) (\i. x pow i) = Cx(&1) - x pow (SUC n)`,
1658   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[VSUM_CLAUSES_NUMSEG] THEN
1659   REWRITE_TAC[complex_pow; COMPLEX_MUL_RID; LE_0] THEN
1660   ASM_REWRITE_TAC[COMPLEX_ADD_LDISTRIB; complex_pow] THEN
1661   SIMPLE_COMPLEX_ARITH_TAC);;
1662
1663 let VSUM_GP_MULTIPLIED = prove
1664  (`!x m n. m <= n
1665            ==> ((Cx(&1) - x) * vsum(m..n) (\i. x pow i) =
1666                 x pow m - x pow (SUC n))`,
1667   REPEAT STRIP_TAC THEN
1668   ASM_SIMP_TAC[VSUM_OFFSET_0; COMPLEX_POW_ADD; FINITE_NUMSEG;
1669                COMPLEX_MUL_ASSOC; VSUM_GP_BASIC; VSUM_COMPLEX_RMUL] THEN
1670   REWRITE_TAC[COMPLEX_SUB_RDISTRIB; GSYM COMPLEX_POW_ADD; COMPLEX_MUL_LID] THEN
1671   ASM_SIMP_TAC[ARITH_RULE `m <= n ==> (SUC(n - m) + m = SUC n)`]);;
1672
1673 let VSUM_GP = prove
1674  (`!x m n.
1675         vsum(m..n) (\i. x pow i) =
1676                 if n < m then Cx(&0)
1677                 else if x = Cx(&1) then Cx(&((n + 1) - m))
1678                 else (x pow m - x pow (SUC n)) / (Cx(&1) - x)`,
1679   REPEAT GEN_TAC THEN
1680   DISJ_CASES_TAC(ARITH_RULE `n < m \/ ~(n < m) /\ m <= n:num`) THEN
1681   ASM_SIMP_TAC[VSUM_TRIV_NUMSEG; COMPLEX_VEC_0] THEN COND_CASES_TAC THENL
1682    [ASM_REWRITE_TAC[COMPLEX_POW_ONE; VSUM_CONST_NUMSEG; COMPLEX_MUL_RID];
1683     ALL_TAC] THEN
1684   REWRITE_TAC[COMPLEX_CMUL; COMPLEX_MUL_RID] THEN
1685   MATCH_MP_TAC(COMPLEX_FIELD
1686    `~(z = Cx(&1)) /\ (Cx(&1) - z) * x = y ==> x = y / (Cx(&1) - z)`) THEN
1687   ASM_SIMP_TAC[COMPLEX_DIV_LMUL; COMPLEX_SUB_0; VSUM_GP_MULTIPLIED]);;
1688
1689 let VSUM_GP_OFFSET = prove
1690  (`!x m n. vsum(m..m+n) (\i. x pow i) =
1691                 if x = Cx(&1) then Cx(&n) + Cx(&1)
1692                 else x pow m * (Cx(&1) - x pow (SUC n)) / (Cx(&1) - x)`,
1693   REPEAT GEN_TAC THEN REWRITE_TAC[VSUM_GP; ARITH_RULE `~(m + n < m:num)`] THEN
1694   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
1695    [REWRITE_TAC[REAL_OF_NUM_ADD; GSYM CX_ADD] THEN
1696     AP_TERM_TAC THEN AP_TERM_TAC THEN ARITH_TAC;
1697     REWRITE_TAC[complex_div; complex_pow; COMPLEX_POW_ADD] THEN
1698     SIMPLE_COMPLEX_ARITH_TAC]);;
1699
1700 (* ------------------------------------------------------------------------- *)
1701 (* Basics about polynomial functions: extremal behaviour and root counts.    *)
1702 (* ------------------------------------------------------------------------- *)
1703
1704 let COMPLEX_SUB_POLYFUN = prove
1705  (`!a x y n.
1706    1 <= n
1707    ==> vsum(0..n) (\i. a i * x pow i) - vsum(0..n) (\i. a i * y pow i) =
1708        (x - y) *
1709        vsum(0..n-1) (\j. vsum(j+1..n) (\i. a i * y pow (i - j - 1)) * x pow j)`,
1710   REPEAT STRIP_TAC THEN
1711   REWRITE_TAC[GSYM VSUM_SUB_NUMSEG; GSYM COMPLEX_SUB_LDISTRIB] THEN
1712   GEN_REWRITE_TAC LAND_CONV [MATCH_MP VSUM_CLAUSES_LEFT (SPEC_ALL LE_0)] THEN
1713   REWRITE_TAC[COMPLEX_SUB_REFL; complex_pow; COMPLEX_MUL_RZERO;
1714       COMPLEX_ADD_LID] THEN
1715   SIMP_TAC[COMPLEX_SUB_POW; ADD_CLAUSES] THEN
1716   ONCE_REWRITE_TAC[COMPLEX_RING `a * x * s:complex = x * a * s`] THEN
1717   SIMP_TAC[VSUM_COMPLEX_LMUL; FINITE_NUMSEG] THEN AP_TERM_TAC THEN
1718   SIMP_TAC[GSYM VSUM_COMPLEX_LMUL; GSYM VSUM_COMPLEX_RMUL; FINITE_NUMSEG;
1719            VSUM_VSUM_PRODUCT; FINITE_NUMSEG] THEN
1720   MATCH_MP_TAC VSUM_EQ_GENERAL_INVERSES THEN
1721   REPEAT(EXISTS_TAC `\(x:num,y:num). (y,x)`) THEN
1722   REWRITE_TAC[FORALL_IN_GSPEC; IN_ELIM_PAIR_THM; IN_NUMSEG] THEN
1723   REWRITE_TAC[ARITH_RULE `a - b - c:num = a - (b + c)`; ADD_SYM] THEN
1724   REWRITE_TAC[COMPLEX_MUL_AC] THEN ARITH_TAC);;
1725
1726 let COMPLEX_SUB_POLYFUN_ALT = prove
1727  (`!a x y n.
1728     1 <= n
1729     ==> vsum(0..n) (\i. a i * x pow i) - vsum(0..n) (\i. a i * y pow i) =
1730         (x - y) *
1731         vsum(0..n-1) (\j. vsum(0..n-j-1) (\k. a(j+k+1) * y pow k) * x pow j)`,
1732   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[COMPLEX_SUB_POLYFUN] THEN AP_TERM_TAC THEN
1733   MATCH_MP_TAC VSUM_EQ_NUMSEG THEN X_GEN_TAC `j:num` THEN REPEAT STRIP_TAC THEN
1734   REWRITE_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1735   MATCH_MP_TAC VSUM_EQ_GENERAL_INVERSES THEN
1736   MAP_EVERY EXISTS_TAC
1737    [`\i. i - (j + 1)`; `\k. j + k + 1`] THEN
1738   REWRITE_TAC[IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
1739   TRY(BINOP_TAC THEN AP_TERM_TAC) THEN ASM_ARITH_TAC);;
1740
1741 let COMPLEX_POLYFUN_LINEAR_FACTOR = prove
1742  (`!a c n. ?b. !z. vsum(0..n) (\i. c(i) * z pow i) =
1743                    (z - a) * vsum(0..n-1) (\i. b(i) * z pow i) +
1744                     vsum(0..n) (\i. c(i) * a pow i)`,
1745   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM COMPLEX_EQ_SUB_RADD] THEN
1746   ASM_CASES_TAC `n = 0` THENL
1747    [EXISTS_TAC `\i:num. Cx(&0)` THEN
1748     ASM_SIMP_TAC[VSUM_SING; NUMSEG_SING; complex_pow; COMPLEX_MUL_LZERO] THEN
1749     REWRITE_TAC[COMPLEX_SUB_REFL; GSYM COMPLEX_VEC_0; VSUM_0] THEN
1750     REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_MUL_RZERO];
1751     ASM_SIMP_TAC[COMPLEX_SUB_POLYFUN; LE_1] THEN
1752     EXISTS_TAC `\j. vsum (j + 1..n) (\i. c i * a pow (i - j - 1))` THEN
1753     REWRITE_TAC[]]);;
1754
1755 let COMPLEX_POLYFUN_LINEAR_FACTOR_ROOT = prove
1756  (`!a c n. vsum(0..n) (\i. c(i) * a pow i) = Cx(&0)
1757            ==> ?b. !z. vsum(0..n) (\i. c(i) * z pow i) =
1758                       (z - a) * vsum(0..n-1) (\i. b(i) * z pow i)`,
1759   MESON_TAC[COMPLEX_POLYFUN_LINEAR_FACTOR; COMPLEX_ADD_RID]);;
1760
1761 let COMPLEX_POLYFUN_EXTREMAL_LEMMA = prove
1762  (`!c n e. &0 < e
1763            ==> ?M. !z. M <= norm(z)
1764                        ==> norm(vsum(0..n) (\i. c(i) * z pow i))
1765                                <= e * norm(z) pow (n + 1)`,
1766   GEN_TAC THEN INDUCT_TAC THEN SIMP_TAC[VSUM_CLAUSES_NUMSEG; LE_0] THEN
1767   REPEAT STRIP_TAC THENL
1768    [REWRITE_TAC[ADD_CLAUSES; complex_pow; REAL_POW_1; COMPLEX_MUL_RID] THEN
1769     EXISTS_TAC `norm(c 0:complex) / e` THEN ASM_SIMP_TAC[REAL_LE_LDIV_EQ] THEN
1770     REWRITE_TAC[REAL_MUL_AC];
1771     ALL_TAC] THEN
1772   FIRST_X_ASSUM(MP_TAC o C MATCH_MP (REAL_ARITH `&0 < &1 / &2`)) THEN
1773   DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN
1774   EXISTS_TAC `max M ((&1 / &2 + norm(c(n+1):complex)) / e)` THEN
1775   X_GEN_TAC `z:complex` THEN REWRITE_TAC[REAL_MAX_LE] THEN STRIP_TAC THEN
1776   FIRST_X_ASSUM(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
1777   MATCH_MP_TAC(NORM_ARITH
1778    `a + norm(y) <= b ==> norm(x) <= a ==> norm(x + y) <= b`) THEN
1779   SIMP_TAC[ADD1; COMPLEX_NORM_MUL; COMPLEX_NORM_POW;
1780            GSYM REAL_ADD_RDISTRIB; ARITH_RULE `(n + 1) + 1 = 1 + n + 1`] THEN
1781   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_POW_ADD] THEN
1782   REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
1783   ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1784   ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; REAL_POW_LE; NORM_POS_LE; REAL_POW_1]);;
1785
1786 let COMPLEX_POLYFUN_EXTREMAL = prove
1787  (`!c n. (!k. k IN 1..n ==> c(k) = Cx(&0)) \/
1788          !B. eventually (\z. norm(vsum(0..n) (\i. c(i) * z pow i)) >= B)
1789                         at_infinity`,
1790   GEN_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
1791   ASM_CASES_TAC `n = 0` THEN
1792   ASM_REWRITE_TAC[NUMSEG_CLAUSES; ARITH; NOT_IN_EMPTY] THEN
1793   MP_TAC(ARITH_RULE `0 <= n`) THEN SIMP_TAC[GSYM NUMSEG_RREC] THEN
1794   DISCH_THEN(K ALL_TAC) THEN ASM_CASES_TAC `c(n:num) = Cx(&0)` THENL
1795    [FIRST_X_ASSUM(MP_TAC o SPEC `n - 1`) THEN
1796     ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1797     ASM_SIMP_TAC[GSYM NUMSEG_RREC; LE_1] THEN
1798     SIMP_TAC[IN_INSERT; VSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1799     ASM_REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_ADD_LID; COND_ID] THEN
1800     ASM_MESON_TAC[];
1801     DISJ2_TAC THEN MP_TAC(ISPECL
1802       [`c:num->complex`; `n - 1`; `norm(c(n:num):complex) / &2`]
1803       COMPLEX_POLYFUN_EXTREMAL_LEMMA) THEN ASM_SIMP_TAC[SUB_ADD; LE_1] THEN
1804     ASM_SIMP_TAC[COMPLEX_NORM_NZ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1805     SIMP_TAC[IN_INSERT; VSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1806     ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> ~(n <= n - 1)`] THEN
1807     DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN X_GEN_TAC `B:real` THEN
1808     REWRITE_TAC[EVENTUALLY_AT_INFINITY] THEN EXISTS_TAC
1809      `max M (max (&1) ((abs B + &1) / (norm(c(n:num):complex) / &2)))` THEN
1810     X_GEN_TAC `z:complex` THEN REWRITE_TAC[real_ge; REAL_MAX_LE] THEN
1811     STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `z:complex`) THEN
1812     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NORM_ARITH
1813      `abs b + &1 <= norm(y) - a ==> norm(x) <= a ==> b <= norm(y + x)`) THEN
1814     REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
1815     REWRITE_TAC[REAL_ARITH `c * x - c / &2 * x = x * c / &2`] THEN
1816     ASM_SIMP_TAC[GSYM REAL_LE_LDIV_EQ; COMPLEX_NORM_NZ; REAL_LT_DIV;
1817                  REAL_OF_NUM_LT; ARITH] THEN
1818     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `norm(z:complex) pow 1` THEN
1819     CONJ_TAC THENL [ASM_REWRITE_TAC[REAL_POW_1]; ALL_TAC] THEN
1820     MATCH_MP_TAC REAL_POW_MONO THEN ASM_SIMP_TAC[LE_1]]);;
1821
1822 let COMPLEX_POLYFUN_ROOTBOUND = prove
1823  (`!n c. ~(!i. i IN 0..n ==> c(i) = Cx(&0))
1824          ==> FINITE {z | vsum(0..n) (\i. c(i) * z pow i) = Cx(&0)} /\
1825              CARD {z | vsum(0..n) (\i. c(i) * z pow i) = Cx(&0)} <= n`,
1826   REWRITE_TAC[TAUT `~a ==> b <=> a \/ b`] THEN INDUCT_TAC THEN GEN_TAC THENL
1827    [SIMP_TAC[NUMSEG_SING; VSUM_SING; IN_SING; complex_pow] THEN
1828     ASM_CASES_TAC `c 0 = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_RID] THEN
1829     REWRITE_TAC[EMPTY_GSPEC; FINITE_RULES; CARD_CLAUSES; LE_REFL];
1830     ALL_TAC] THEN
1831   ASM_CASES_TAC `{z | vsum(0..SUC n) (\i. c(i) * z pow i) = Cx(&0)} = {}` THEN
1832   ASM_REWRITE_TAC[FINITE_RULES; CARD_CLAUSES; LE_0] THEN
1833   FIRST_X_ASSUM(X_CHOOSE_THEN `a:complex` MP_TAC o
1834     GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
1835   REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
1836   FIRST_ASSUM(MP_TAC o MATCH_MP COMPLEX_POLYFUN_LINEAR_FACTOR_ROOT) THEN
1837   DISCH_THEN(X_CHOOSE_TAC `b:num->complex`) THEN
1838   ASM_REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_SUB_0; SUC_SUB1; SET_RULE
1839    `{z | z = a \/ P z} = a INSERT {z | P z}`] THEN
1840   FIRST_X_ASSUM(MP_TAC o SPEC `b:num->complex`) THEN
1841   STRIP_TAC THEN ASM_SIMP_TAC[CARD_CLAUSES; FINITE_RULES] THENL
1842    [DISJ1_TAC; ASM_ARITH_TAC] THEN
1843   MP_TAC(SPECL [`c:num->complex`; `SUC n`] COMPLEX_POLYFUN_EXTREMAL) THEN
1844   ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN
1845   ASM_SIMP_TAC[SUC_SUB1; COMPLEX_MUL_LZERO] THEN
1846   SIMP_TAC[COMPLEX_POW_ZERO; COND_RAND; COMPLEX_MUL_RZERO] THEN
1847   ASM_SIMP_TAC[VSUM_0; GSYM COMPLEX_VEC_0; VSUM_DELTA; IN_NUMSEG; LE_0] THEN
1848   REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_MUL_RZERO; COMPLEX_NORM_NUM] THEN
1849   REWRITE_TAC[COMPLEX_MUL_RID; real_ge; EVENTUALLY_AT_INFINITY] THEN
1850   REPEAT STRIP_TAC THENL [ASM_MESON_TAC[LE_1]; ALL_TAC] THEN
1851   FIRST_X_ASSUM(MP_TAC o SPEC `&1`) THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1852   MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1853   REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM] THEN X_GEN_TAC `b:real` THEN
1854   MP_TAC(SPEC `b:real` (INST_TYPE [`:2`,`:N`] VECTOR_CHOOSE_SIZE)) THEN
1855   ASM_MESON_TAC[NORM_POS_LE; REAL_LE_TOTAL; REAL_LE_TRANS]);;
1856
1857 let COMPLEX_POLYFUN_FINITE_ROOTS = prove
1858  (`!n c. FINITE {x | vsum(0..n) (\i. c i * x pow i) = Cx(&0)} <=>
1859          ?i. i IN 0..n /\ ~(c i = Cx(&0))`,
1860   REPEAT GEN_TAC THEN REWRITE_TAC[TAUT `a /\ ~b <=> ~(a ==> b)`] THEN
1861   REWRITE_TAC[GSYM NOT_FORALL_THM] THEN EQ_TAC THEN
1862   SIMP_TAC[COMPLEX_POLYFUN_ROOTBOUND] THEN
1863   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1864   SIMP_TAC[COMPLEX_MUL_LZERO] THEN SIMP_TAC[GSYM COMPLEX_VEC_0; VSUM_0] THEN
1865   REWRITE_TAC[SET_RULE `{x | T} = (:complex)`; GSYM INFINITE;
1866               EUCLIDEAN_SPACE_INFINITE]);;
1867
1868 let COMPLEX_POLYFUN_EQ_0 = prove
1869  (`!n c. (!z. vsum(0..n) (\i. c i * z pow i) = Cx(&0)) <=>
1870          (!i. i IN 0..n ==> c i = Cx(&0))`,
1871   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
1872    [GEN_REWRITE_TAC I [TAUT `p <=> ~ ~p`] THEN DISCH_THEN(MP_TAC o MATCH_MP
1873      COMPLEX_POLYFUN_ROOTBOUND) THEN
1874     ASM_REWRITE_TAC[EUCLIDEAN_SPACE_INFINITE; GSYM INFINITE; DE_MORGAN_THM;
1875                     SET_RULE `{x | T} = (:complex)`];
1876     ASM_SIMP_TAC[IN_NUMSEG; LE_0; COMPLEX_MUL_LZERO] THEN
1877     REWRITE_TAC[GSYM COMPLEX_VEC_0; VSUM_0]]);;
1878
1879 let COMPLEX_POLYFUN_EQ_CONST = prove
1880  (`!n c k. (!z. vsum(0..n) (\i. c i * z pow i) = k) <=>
1881            c 0 = k /\ (!i. i IN 1..n ==> c i = Cx(&0))`,
1882   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1883    `!x. vsum(0..n) (\i. (if i = 0 then c 0 - k else c i) * x pow i) =
1884         Cx(&0)` THEN
1885   CONJ_TAC THENL
1886    [SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0; complex_pow; COMPLEX_MUL_RID] THEN
1887     REWRITE_TAC[COMPLEX_RING `(c - k) + s = Cx(&0) <=> c + s = k`] THEN
1888     AP_TERM_TAC THEN ABS_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1889     AP_TERM_TAC THEN MATCH_MP_TAC VSUM_EQ THEN GEN_TAC THEN
1890     REWRITE_TAC[IN_NUMSEG] THEN
1891     COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH];
1892     REWRITE_TAC[COMPLEX_POLYFUN_EQ_0; IN_NUMSEG; LE_0] THEN
1893     GEN_REWRITE_TAC LAND_CONV [MESON[]
1894      `(!n. P n) <=> P 0 /\ (!n. ~(n = 0) ==> P n)`] THEN
1895     SIMP_TAC[LE_0; COMPLEX_SUB_0] THEN MESON_TAC[LE_1]]);;
1896
1897 (* ------------------------------------------------------------------------- *)
1898 (* Complex products.                                                         *)
1899 (* ------------------------------------------------------------------------- *)
1900
1901 let cproduct = new_definition
1902   `cproduct = iterate (( * ):complex->complex->complex)`;;
1903
1904 let NEUTRAL_COMPLEX_MUL = prove
1905  (`neutral(( * ):complex->complex->complex) = Cx(&1)`,
1906   REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1907   MESON_TAC[COMPLEX_MUL_LID; COMPLEX_MUL_RID]);;
1908
1909 let MONOIDAL_COMPLEX_MUL = prove
1910  (`monoidal(( * ):complex->complex->complex)`,
1911   REWRITE_TAC[monoidal; NEUTRAL_COMPLEX_MUL] THEN SIMPLE_COMPLEX_ARITH_TAC);;
1912
1913 let CPRODUCT_CLAUSES = prove
1914  (`(!f. cproduct {} f = Cx(&1)) /\
1915    (!x f s. FINITE(s)
1916             ==> (cproduct (x INSERT s) f =
1917                  if x IN s then cproduct s f else f(x) * cproduct s f))`,
1918   REWRITE_TAC[cproduct; GSYM NEUTRAL_COMPLEX_MUL] THEN
1919   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
1920   MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_COMPLEX_MUL]);;
1921
1922 let CPRODUCT_EQ_0 = prove
1923  (`!f s. FINITE s ==> (cproduct s f = Cx(&0) <=> ?x. x IN s /\ f(x) = Cx(&0))`,
1924   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1925   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_ENTIRE; IN_INSERT; CX_INJ; REAL_OF_NUM_EQ;
1926            ARITH; NOT_IN_EMPTY] THEN
1927   MESON_TAC[]);;
1928
1929 let CPRODUCT_INV = prove
1930  (`!f s. FINITE s ==> cproduct s (\x. inv(f x)) = inv(cproduct s f)`,
1931   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1932   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_INV_1; COMPLEX_INV_MUL]);;
1933
1934 let CPRODUCT_MUL = prove
1935  (`!f g s. FINITE s
1936            ==> cproduct s (\x. f x * g x) = cproduct s f * cproduct s g`,
1937   GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1938   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_MUL_AC; COMPLEX_MUL_LID]);;
1939
1940 let CPRODUCT_EQ_1 = prove
1941  (`!f s. (!x:A. x IN s ==> (f(x) = Cx(&1))) ==> (cproduct s f = Cx(&1))`,
1942   REWRITE_TAC[cproduct; GSYM NEUTRAL_COMPLEX_MUL] THEN
1943   SIMP_TAC[ITERATE_EQ_NEUTRAL; MONOIDAL_COMPLEX_MUL]);;
1944
1945 let CPRODUCT_1 = prove
1946  (`!s. cproduct s (\n. Cx(&1)) = Cx(&1)`,
1947   SIMP_TAC[CPRODUCT_EQ_1]);;
1948
1949 let CPRODUCT_POW = prove
1950  (`!f s n. FINITE s
1951            ==> cproduct s (\x. f x pow n) = (cproduct s f) pow n`,
1952   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1953   DISCH_TAC THEN INDUCT_TAC THEN
1954   ASM_SIMP_TAC[complex_pow; CPRODUCT_MUL; CPRODUCT_1]);;
1955
1956 let NORM_CPRODUCT = prove
1957  (`!f s. FINITE s ==> norm(cproduct s f) = product s (\x. norm(f x))`,
1958   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1959   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_NORM_CX; REAL_ABS_NUM;
1960            CPRODUCT_MUL; PRODUCT_CLAUSES; COMPLEX_NORM_MUL]);;
1961
1962 let CPRODUCT_EQ = prove
1963  (`!f g s. (!x. x IN s ==> (f x = g x)) ==> cproduct s f = cproduct s g`,
1964   REWRITE_TAC[cproduct] THEN MATCH_MP_TAC ITERATE_EQ THEN
1965   REWRITE_TAC[MONOIDAL_COMPLEX_MUL]);;
1966
1967 let CPRODUCT_SING = prove
1968  (`!f x. cproduct {x} f = f(x)`,
1969   SIMP_TAC[CPRODUCT_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; COMPLEX_MUL_RID]);;
1970
1971 let CPRODUCT_CLAUSES_NUMSEG = prove
1972  (`(!m. cproduct(m..0) f = if m = 0 then f(0) else Cx(&1)) /\
1973    (!m n. cproduct(m..SUC n) f = if m <= SUC n then cproduct(m..n) f * f(SUC n)
1974                                  else cproduct(m..n) f)`,
1975   REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
1976   COND_CASES_TAC THEN
1977   ASM_SIMP_TAC[CPRODUCT_SING; CPRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1978   REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`; COMPLEX_MUL_AC]);;
1979
1980 let CPRODUCT_CLAUSES_RIGHT = prove
1981  (`!f m n. 0 < n /\ m <= n ==> cproduct(m..n) f = cproduct(m..n-1) f * (f n)`,
1982   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1983   SIMP_TAC[LT_REFL; CPRODUCT_CLAUSES_NUMSEG; SUC_SUB1]);;
1984
1985 let CPRODUCT_CLAUSES_LEFT = prove
1986  (`!f m n. m <= n ==> cproduct(m..n) f = f m * cproduct(m + 1..n) f`,
1987   SIMP_TAC[GSYM NUMSEG_LREC; CPRODUCT_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
1988   ARITH_TAC);;
1989
1990 let CPRODUCT_IMAGE = prove
1991  (`!f g s. (!x y. x IN s /\ y IN s /\ f x = f y ==> (x = y))
1992            ==> (cproduct (IMAGE f s) g = cproduct s (g o f))`,
1993   REWRITE_TAC[cproduct; GSYM NEUTRAL_COMPLEX_MUL] THEN
1994   MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_COMPLEX_MUL]);;
1995
1996 let CPRODUCT_OFFSET = prove
1997  (`!f m p. cproduct(m+p..n+p) f = cproduct(m..n) (\i. f(i + p))`,
1998   SIMP_TAC[NUMSEG_OFFSET_IMAGE; CPRODUCT_IMAGE;
1999            EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
2000   REWRITE_TAC[o_DEF]);;
2001
2002 let CPRODUCT_CONST = prove
2003  (`!c s. FINITE s ==> cproduct s (\x. c) = c pow (CARD s)`,
2004   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2005   SIMP_TAC[CPRODUCT_CLAUSES; CARD_CLAUSES; complex_pow]);;
2006
2007 let CPRODUCT_CONST_NUMSEG = prove
2008  (`!c m n. cproduct (m..n) (\x. c) = c pow ((n + 1) - m)`,
2009   SIMP_TAC[CPRODUCT_CONST; CARD_NUMSEG; FINITE_NUMSEG]);;
2010
2011 let CPRODUCT_PAIR = prove
2012  (`!f m n. cproduct(2*m..2*n+1) f = cproduct(m..n) (\i. f(2*i) * f(2*i+1))`,
2013   MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_COMPLEX_MUL) THEN
2014   REWRITE_TAC[cproduct; NEUTRAL_COMPLEX_MUL]);;
2015
2016 let CNJ_CPRODUCT = prove
2017  (`!f s. FINITE s ==> cnj(cproduct s f) = cproduct s (\i. cnj(f i))`,
2018   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2019   SIMP_TAC[CPRODUCT_CLAUSES; CNJ_MUL; CNJ_CX]);;
2020
2021 let CX_PRODUCT = prove
2022  (`!f s. FINITE s ==> Cx(product s f) = cproduct s (\i. Cx(f i))`,
2023   GEN_TAC THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
2024   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2025   SIMP_TAC[CPRODUCT_CLAUSES; PRODUCT_CLAUSES; GSYM CX_MUL]);;
2026
2027 let th = prove
2028  (`(!f g s.   (!x. x IN s ==> f(x) = g(x))
2029               ==> cproduct s (\i. f(i)) = cproduct s g) /\
2030    (!f g a b. (!i. a <= i /\ i <= b ==> f(i) = g(i))
2031               ==> cproduct(a..b) (\i. f(i)) = cproduct(a..b) g) /\
2032    (!f g p.   (!x. p x ==> f x = g x)
2033               ==> cproduct {y | p y} (\i. f(i)) = cproduct {y | p y} g)`,
2034   REPEAT STRIP_TAC THEN MATCH_MP_TAC CPRODUCT_EQ THEN
2035   ASM_SIMP_TAC[IN_ELIM_THM; IN_NUMSEG]) in
2036   extend_basic_congs (map SPEC_ALL (CONJUNCTS th));;