Complex/complexnumbers.ml

   1 (* ========================================================================= *)
   2 (* Basic definitions and properties of complex numbers.                      *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/transc.ml";;
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Definition of complex number type.                                        *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let complex_tybij_raw =
  14   new_type_definition "complex" ("complex","coords")
  15    (prove(`?x:real#real. T`,REWRITE_TAC[]));;
  16
  17 let complex_tybij = REWRITE_RULE [] complex_tybij_raw;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Real and imaginary parts of a number.                                     *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let RE_DEF = new_definition
  24   `Re(z) = FST(coords(z))`;;
  25
  26 let IM_DEF = new_definition
  27   `Im(z) = SND(coords(z))`;;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Set up overloading.                                                       *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 do_list overload_interface
  34  ["+",`complex_add:complex->complex->complex`;
  35   "-",`complex_sub:complex->complex->complex`;
  36   "*",`complex_mul:complex->complex->complex`;
  37   "/",`complex_div:complex->complex->complex`;
  38   "--",`complex_neg:complex->complex`;
  39   "pow",`complex_pow:complex->num->complex`;
  40   "inv",`complex_inv:complex->complex`];;
  41
  42 let prioritize_complex() = prioritize_overload(mk_type("complex",[]));;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (* Complex absolute value (modulus).                                         *)
  46 (* ------------------------------------------------------------------------- *)
  47
  48 make_overloadable "norm" `:A->real`;;
  49 overload_interface("norm",`complex_norm:complex->real`);;
  50
  51 let complex_norm = new_definition
  52   `norm(z) = sqrt(Re(z) pow 2 + Im(z) pow 2)`;;
  53
  54 (* ------------------------------------------------------------------------- *)
  55 (* Imaginary unit (too inconvenient to use "i"!)                             *)
  56 (* ------------------------------------------------------------------------- *)
  57
  58 let ii = new_definition
  59   `ii = complex(&0,&1)`;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Injection from reals.                                                     *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let CX_DEF = new_definition
  66   `Cx(a) = complex(a,&0)`;;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Arithmetic operations.                                                    *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 let complex_neg = new_definition
  73   `--z = complex(--(Re(z)),--(Im(z)))`;;
  74
  75 let complex_add = new_definition
  76   `w + z = complex(Re(w) + Re(z),Im(w) + Im(z))`;;
  77
  78 let complex_sub = new_definition
  79   `w - z = w + --z`;;
  80
  81 let complex_mul = new_definition
  82   `w * z = complex(Re(w) * Re(z) - Im(w) * Im(z),
  83                    Re(w) * Im(z) + Im(w) * Re(z))`;;
  84
  85 let complex_inv = new_definition
  86   `inv(z) = complex(Re(z) / (Re(z) pow 2 + Im(z) pow 2),
  87                     --(Im(z)) / (Re(z) pow 2 + Im(z) pow 2))`;;
  88
  89 let complex_div = new_definition
  90   `w / z = w * inv(z)`;;
  91
  92 let complex_pow = new_recursive_definition num_RECURSION
  93   `(x pow 0 = Cx(&1)) /\
  94    (!n. x pow (SUC n) = x * x pow n)`;;
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* Various handy rewrites.                                                   *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let RE = prove
 101  (`(Re(complex(x,y)) = x)`,
 102   REWRITE_TAC[RE_DEF; complex_tybij]);;
 103
 104 let IM = prove
 105  (`Im(complex(x,y)) = y`,
 106   REWRITE_TAC[IM_DEF; complex_tybij]);;
 107
 108 let COMPLEX = prove
 109  (`complex(Re(z),Im(z)) = z`,
 110   REWRITE_TAC[IM_DEF; RE_DEF; complex_tybij]);;
 111
 112 let COMPLEX_EQ = prove
 113  (`!w z. (w = z) <=> (Re(w) = Re(z)) /\ (Im(w) = Im(z))`,
 114   REWRITE_TAC[RE_DEF; IM_DEF; GSYM PAIR_EQ] THEN MESON_TAC[complex_tybij]);;
 115
 116 (* ------------------------------------------------------------------------- *)
 117 (* Crude tactic to automate very simple algebraic equivalences.              *)
 118 (* ------------------------------------------------------------------------- *)
 119
 120 let SIMPLE_COMPLEX_ARITH_TAC =
 121   REWRITE_TAC[COMPLEX_EQ; RE; IM; CX_DEF;
 122               complex_add; complex_neg; complex_sub; complex_mul] THEN
 123   REAL_ARITH_TAC;;
 124
 125 let SIMPLE_COMPLEX_ARITH tm = prove(tm,SIMPLE_COMPLEX_ARITH_TAC);;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Basic algebraic properties that can be proved automatically by this.      *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 let COMPLEX_ADD_SYM = prove
 132  (`!x y. x + y = y + x`,
 133   SIMPLE_COMPLEX_ARITH_TAC);;
 134
 135 let COMPLEX_ADD_ASSOC = prove
 136  (`!x y z. x + y + z = (x + y) + z`,
 137   SIMPLE_COMPLEX_ARITH_TAC);;
 138
 139 let COMPLEX_ADD_LID = prove
 140  (`!x. Cx(&0) + x = x`,
 141   SIMPLE_COMPLEX_ARITH_TAC);;
 142
 143 let COMPLEX_ADD_LINV = prove
 144  (`!x. --x + x = Cx(&0)`,
 145   SIMPLE_COMPLEX_ARITH_TAC);;
 146
 147 let COMPLEX_MUL_SYM = prove
 148  (`!x y. x * y = y * x`,
 149   SIMPLE_COMPLEX_ARITH_TAC);;
 150
 151 let COMPLEX_MUL_ASSOC = prove
 152  (`!x y z. x * y * z = (x * y) * z`,
 153   SIMPLE_COMPLEX_ARITH_TAC);;
 154
 155 let COMPLEX_MUL_LID = prove
 156  (`!x. Cx(&1) * x = x`,
 157   SIMPLE_COMPLEX_ARITH_TAC);;
 158
 159 let COMPLEX_ADD_LDISTRIB = prove
 160  (`!x y z. x * (y + z) = x * y + x * z`,
 161   SIMPLE_COMPLEX_ARITH_TAC);;
 162
 163 let COMPLEX_ADD_AC = prove
 164  (`(m + n = n + m) /\ ((m + n) + p = m + n + p) /\ (m + n + p = n + m + p)`,
 165   SIMPLE_COMPLEX_ARITH_TAC);;
 166
 167 let COMPLEX_MUL_AC = prove
 168  (`(m * n = n * m) /\ ((m * n) * p = m * n * p) /\ (m * n * p = n * m * p)`,
 169   SIMPLE_COMPLEX_ARITH_TAC);;
 170
 171 let COMPLEX_ADD_RID = prove
 172  (`!x. x + Cx(&0) = x`,
 173   SIMPLE_COMPLEX_ARITH_TAC);;
 174
 175 let COMPLEX_MUL_RID = prove
 176  (`!x. x * Cx(&1) = x`,
 177   SIMPLE_COMPLEX_ARITH_TAC);;
 178
 179 let COMPLEX_ADD_RINV = prove
 180  (`!x. x + --x = Cx(&0)`,
 181   SIMPLE_COMPLEX_ARITH_TAC);;
 182
 183 let COMPLEX_ADD_RDISTRIB = prove
 184  (`!x y z. (x + y) * z = x * z + y * z`,
 185   SIMPLE_COMPLEX_ARITH_TAC);;
 186
 187 let COMPLEX_EQ_ADD_LCANCEL = prove
 188  (`!x y z. (x + y = x + z) <=> (y = z)`,
 189   SIMPLE_COMPLEX_ARITH_TAC);;
 190
 191 let COMPLEX_EQ_ADD_RCANCEL = prove
 192  (`!x y z. (x + z = y + z) <=> (x = y)`,
 193   SIMPLE_COMPLEX_ARITH_TAC);;
 194
 195 let COMPLEX_MUL_RZERO = prove
 196  (`!x. x * Cx(&0) = Cx(&0)`,
 197   SIMPLE_COMPLEX_ARITH_TAC);;
 198
 199 let COMPLEX_MUL_LZERO = prove
 200  (`!x. Cx(&0) * x = Cx(&0)`,
 201   SIMPLE_COMPLEX_ARITH_TAC);;
 202
 203 let COMPLEX_NEG_NEG = prove
 204  (`!x. --(--x) = x`,
 205   SIMPLE_COMPLEX_ARITH_TAC);;
 206
 207 let COMPLEX_MUL_RNEG = prove
 208  (`!x y. x * --y = --(x * y)`,
 209   SIMPLE_COMPLEX_ARITH_TAC);;
 210
 211 let COMPLEX_MUL_LNEG = prove
 212  (`!x y. --x * y = --(x * y)`,
 213   SIMPLE_COMPLEX_ARITH_TAC);;
 214
 215 let COMPLEX_NEG_ADD = prove
 216  (`!x y. --(x + y) = --x + --y`,
 217   SIMPLE_COMPLEX_ARITH_TAC);;
 218
 219 let COMPLEX_NEG_0 = prove
 220  (`--Cx(&0) = Cx(&0)`,
 221   SIMPLE_COMPLEX_ARITH_TAC);;
 222
 223 let COMPLEX_EQ_ADD_LCANCEL_0 = prove
 224  (`!x y. (x + y = x) <=> (y = Cx(&0))`,
 225   SIMPLE_COMPLEX_ARITH_TAC);;
 226
 227 let COMPLEX_EQ_ADD_RCANCEL_0 = prove
 228  (`!x y. (x + y = y) <=> (x = Cx(&0))`,
 229   SIMPLE_COMPLEX_ARITH_TAC);;
 230
 231 let COMPLEX_LNEG_UNIQ = prove
 232  (`!x y. (x + y = Cx(&0)) <=> (x = --y)`,
 233   SIMPLE_COMPLEX_ARITH_TAC);;
 234
 235 let COMPLEX_RNEG_UNIQ = prove
 236  (`!x y. (x + y = Cx(&0)) <=> (y = --x)`,
 237   SIMPLE_COMPLEX_ARITH_TAC);;
 238
 239 let COMPLEX_NEG_LMUL = prove
 240  (`!x y. --(x * y) = --x * y`,
 241   SIMPLE_COMPLEX_ARITH_TAC);;
 242
 243 let COMPLEX_NEG_RMUL = prove
 244  (`!x y. --(x * y) = x * --y`,
 245   SIMPLE_COMPLEX_ARITH_TAC);;
 246
 247 let COMPLEX_NEG_MUL2 = prove
 248  (`!x y. --x * --y = x * y`,
 249   SIMPLE_COMPLEX_ARITH_TAC);;
 250
 251 let COMPLEX_SUB_ADD = prove
 252  (`!x y. x - y + y = x`,
 253   SIMPLE_COMPLEX_ARITH_TAC);;
 254
 255 let COMPLEX_SUB_ADD2 = prove
 256  (`!x y. y + x - y = x`,
 257   SIMPLE_COMPLEX_ARITH_TAC);;
 258
 259 let COMPLEX_SUB_REFL = prove
 260  (`!x. x - x = Cx(&0)`,
 261   SIMPLE_COMPLEX_ARITH_TAC);;
 262
 263 let COMPLEX_SUB_0 = prove
 264  (`!x y. (x - y = Cx(&0)) <=> (x = y)`,
 265   SIMPLE_COMPLEX_ARITH_TAC);;
 266
 267 let COMPLEX_NEG_EQ_0 = prove
 268  (`!x. (--x = Cx(&0)) <=> (x = Cx(&0))`,
 269   SIMPLE_COMPLEX_ARITH_TAC);;
 270
 271 let COMPLEX_NEG_SUB = prove
 272  (`!x y. --(x - y) = y - x`,
 273   SIMPLE_COMPLEX_ARITH_TAC);;
 274
 275 let COMPLEX_ADD_SUB = prove
 276  (`!x y. (x + y) - x = y`,
 277   SIMPLE_COMPLEX_ARITH_TAC);;
 278
 279 let COMPLEX_NEG_EQ = prove
 280  (`!x y. (--x = y) <=> (x = --y)`,
 281   SIMPLE_COMPLEX_ARITH_TAC);;
 282
 283 let COMPLEX_NEG_MINUS1 = prove
 284  (`!x. --x = --Cx(&1) * x`,
 285   SIMPLE_COMPLEX_ARITH_TAC);;
 286
 287 let COMPLEX_SUB_SUB = prove
 288  (`!x y. x - y - x = --y`,
 289   SIMPLE_COMPLEX_ARITH_TAC);;
 290
 291 let COMPLEX_ADD2_SUB2 = prove
 292  (`!a b c d. (a + b) - (c + d) = a - c + b - d`,
 293   SIMPLE_COMPLEX_ARITH_TAC);;
 294
 295 let COMPLEX_SUB_LZERO = prove
 296  (`!x. Cx(&0) - x = --x`,
 297   SIMPLE_COMPLEX_ARITH_TAC);;
 298
 299 let COMPLEX_SUB_RZERO = prove
 300  (`!x. x - Cx(&0) = x`,
 301   SIMPLE_COMPLEX_ARITH_TAC);;
 302
 303 let COMPLEX_SUB_LNEG = prove
 304  (`!x y. --x - y = --(x + y)`,
 305   SIMPLE_COMPLEX_ARITH_TAC);;
 306
 307 let COMPLEX_SUB_RNEG = prove
 308  (`!x y. x - --y = x + y`,
 309   SIMPLE_COMPLEX_ARITH_TAC);;
 310
 311 let COMPLEX_SUB_NEG2 = prove
 312  (`!x y. --x - --y = y - x`,
 313   SIMPLE_COMPLEX_ARITH_TAC);;
 314
 315 let COMPLEX_SUB_TRIANGLE = prove
 316  (`!a b c. a - b + b - c = a - c`,
 317   SIMPLE_COMPLEX_ARITH_TAC);;
 318
 319 let COMPLEX_EQ_SUB_LADD = prove
 320  (`!x y z. (x = y - z) <=> (x + z = y)`,
 321   SIMPLE_COMPLEX_ARITH_TAC);;
 322
 323 let COMPLEX_EQ_SUB_RADD = prove
 324  (`!x y z. (x - y = z) <=> (x = z + y)`,
 325   SIMPLE_COMPLEX_ARITH_TAC);;
 326
 327 let COMPLEX_SUB_SUB2 = prove
 328  (`!x y. x - (x - y) = y`,
 329   SIMPLE_COMPLEX_ARITH_TAC);;
 330
 331 let COMPLEX_ADD_SUB2 = prove
 332  (`!x y. x - (x + y) = --y`,
 333   SIMPLE_COMPLEX_ARITH_TAC);;
 334
 335 let COMPLEX_DIFFSQ = prove
 336  (`!x y. (x + y) * (x - y) = x * x - y * y`,
 337   SIMPLE_COMPLEX_ARITH_TAC);;
 338
 339 let COMPLEX_EQ_NEG2 = prove
 340  (`!x y. (--x = --y) <=> (x = y)`,
 341   SIMPLE_COMPLEX_ARITH_TAC);;
 342
 343 let COMPLEX_SUB_LDISTRIB = prove
 344  (`!x y z. x * (y - z) = x * y - x * z`,
 345   SIMPLE_COMPLEX_ARITH_TAC);;
 346
 347 let COMPLEX_SUB_RDISTRIB = prove
 348  (`!x y z. (x - y) * z = x * z - y * z`,
 349   SIMPLE_COMPLEX_ARITH_TAC);;
 350
 351 let COMPLEX_MUL_2 = prove
 352  (`!x. &2 * x = x + x`,
 353   SIMPLE_COMPLEX_ARITH_TAC);;
 354
 355 (* ------------------------------------------------------------------------- *)
 356 (* Homomorphic embedding properties for Cx mapping.                          *)
 357 (* ------------------------------------------------------------------------- *)
 358
 359 let CX_INJ = prove
 360  (`!x y. (Cx(x) = Cx(y)) <=> (x = y)`,
 361   REWRITE_TAC[CX_DEF; COMPLEX_EQ; RE; IM]);;
 362
 363 let CX_NEG = prove
 364  (`!x. Cx(--x) = --(Cx(x))`,
 365   REWRITE_TAC[CX_DEF; complex_neg; RE; IM; REAL_NEG_0]);;
 366
 367 let CX_INV = prove
 368  (`!x. Cx(inv x) = inv(Cx x)`,
 369   GEN_TAC THEN
 370   REWRITE_TAC[CX_DEF; complex_inv; RE; IM] THEN
 371   REWRITE_TAC[real_div; REAL_NEG_0; REAL_MUL_LZERO] THEN
 372   REWRITE_TAC[COMPLEX_EQ; REAL_POW_2; REAL_MUL_RZERO; RE; IM] THEN
 373   REWRITE_TAC[REAL_ADD_RID; REAL_INV_MUL] THEN
 374   ASM_CASES_TAC `x = &0` THEN
 375   ASM_REWRITE_TAC[REAL_INV_0; REAL_MUL_LZERO] THEN
 376   REWRITE_TAC[REAL_MUL_ASSOC] THEN
 377   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
 378   AP_THM_TAC THEN AP_TERM_TAC THEN ASM_MESON_TAC[REAL_MUL_RINV]);;
 379
 380 let CX_ADD = prove
 381  (`!x y. Cx(x + y) = Cx(x) + Cx(y)`,
 382   REWRITE_TAC[CX_DEF; complex_add; RE; IM; REAL_ADD_LID]);;
 383
 384 let CX_SUB = prove
 385  (`!x y. Cx(x - y) = Cx(x) - Cx(y)`,
 386   REWRITE_TAC[complex_sub; real_sub; CX_ADD; CX_NEG]);;
 387
 388 let CX_MUL = prove
 389  (`!x y. Cx(x * y) = Cx(x) * Cx(y)`,
 390   REWRITE_TAC[CX_DEF; complex_mul; RE; IM; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN
 391   REWRITE_TAC[REAL_SUB_RZERO; REAL_ADD_RID]);;
 392
 393 let CX_DIV = prove
 394  (`!x y. Cx(x / y) = Cx(x) / Cx(y)`,
 395   REWRITE_TAC[complex_div; real_div; CX_MUL; CX_INV]);;
 396
 397 let CX_POW = prove
 398  (`!x n. Cx(x pow n) = Cx(x) pow n`,
 399   GEN_TAC THEN INDUCT_TAC THEN
 400   ASM_REWRITE_TAC[complex_pow; real_pow; CX_MUL]);;
 401
 402 let CX_ABS = prove
 403  (`!x. Cx(abs x) = Cx(norm(Cx(x)))`,
 404   REWRITE_TAC[CX_DEF; complex_norm; COMPLEX_EQ; RE; IM] THEN
 405   REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 406   REWRITE_TAC[GSYM REAL_POW_2; POW_2_SQRT_ABS]);;
 407
 408 let COMPLEX_NORM_CX = prove
 409  (`!x. norm(Cx(x)) = abs(x)`,
 410   REWRITE_TAC[GSYM CX_INJ; CX_ABS]);;
 411
 412 (* ------------------------------------------------------------------------- *)
 413 (* A convenient lemma that we need a few times below.                        *)
 414 (* ------------------------------------------------------------------------- *)
 415
 416 let COMPLEX_ENTIRE = prove
 417  (`!x y. (x * y = Cx(&0)) <=> (x = Cx(&0)) \/ (y = Cx(&0))`,
 418   REWRITE_TAC[COMPLEX_EQ; complex_mul; RE; IM; CX_DEF; GSYM REAL_SOS_EQ_0] THEN
 419   CONV_TAC REAL_RING);;
 420
 421 (* ------------------------------------------------------------------------- *)
 422 (* Powers.                                                                   *)
 423 (* ------------------------------------------------------------------------- *)
 424
 425 let COMPLEX_POW_ADD = prove
 426  (`!x m n. x pow (m + n) = x pow m * x pow n`,
 427   GEN_TAC THEN INDUCT_TAC THEN
 428   ASM_REWRITE_TAC[ADD_CLAUSES; complex_pow;
 429                   COMPLEX_MUL_LID; COMPLEX_MUL_ASSOC]);;
 430
 431 let COMPLEX_POW_POW = prove
 432  (`!x m n. (x pow m) pow n = x pow (m * n)`,
 433   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 434   ASM_REWRITE_TAC[complex_pow; MULT_CLAUSES; COMPLEX_POW_ADD]);;
 435
 436 let COMPLEX_POW_1 = prove
 437  (`!x. x pow 1 = x`,
 438   REWRITE_TAC[num_CONV `1`] THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_RID]);;
 439
 440 let COMPLEX_POW_2 = prove
 441  (`!x. x pow 2 = x * x`,
 442   REWRITE_TAC[num_CONV `2`] THEN REWRITE_TAC[complex_pow; COMPLEX_POW_1]);;
 443
 444 let COMPLEX_POW_NEG = prove
 445  (`!x n. (--x) pow n = if EVEN n then x pow n else --(x pow n)`,
 446   GEN_TAC THEN INDUCT_TAC THEN
 447   ASM_REWRITE_TAC[complex_pow; EVEN] THEN
 448   ASM_CASES_TAC `EVEN n` THEN
 449   ASM_REWRITE_TAC[COMPLEX_MUL_RNEG; COMPLEX_MUL_LNEG; COMPLEX_NEG_NEG]);;
 450
 451 let COMPLEX_POW_ONE = prove
 452  (`!n. Cx(&1) pow n = Cx(&1)`,
 453   INDUCT_TAC THEN ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID]);;
 454
 455 let COMPLEX_POW_MUL = prove
 456  (`!x y n. (x * y) pow n = (x pow n) * (y pow n)`,
 457   GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
 458   ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID; COMPLEX_MUL_AC]);;
 459
 460 let COMPLEX_POW_II_2 = prove
 461  (`ii pow 2 = --Cx(&1)`,
 462   REWRITE_TAC[ii; COMPLEX_POW_2; complex_mul; CX_DEF; RE; IM; complex_neg] THEN
 463   CONV_TAC REAL_RAT_REDUCE_CONV);;
 464
 465 let COMPLEX_POW_EQ_0 = prove
 466  (`!x n. (x pow n = Cx(&0)) <=> (x = Cx(&0)) /\ ~(n = 0)`,
 467   GEN_TAC THEN INDUCT_TAC THEN
 468   ASM_REWRITE_TAC[NOT_SUC; complex_pow; COMPLEX_ENTIRE] THENL
 469    [SIMPLE_COMPLEX_ARITH_TAC; CONV_TAC TAUT]);;
 470
 471 (* ------------------------------------------------------------------------- *)
 472 (* Norms (aka "moduli").                                                     *)
 473 (* ------------------------------------------------------------------------- *)
 474
 475 let COMPLEX_NORM_CX = prove
 476  (`!x. norm(Cx x) = abs(x)`,
 477   GEN_TAC THEN REWRITE_TAC[complex_norm; CX_DEF; RE; IM] THEN
 478   REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 479   REWRITE_TAC[GSYM REAL_POW_2; POW_2_SQRT_ABS]);;
 480
 481 let COMPLEX_NORM_POS = prove
 482  (`!z. &0 <= norm(z)`,
 483   SIMP_TAC[complex_norm; SQRT_POS_LE; REAL_POW_2;
 484            REAL_LE_SQUARE; REAL_LE_ADD]);;
 485
 486 let COMPLEX_ABS_NORM = prove
 487  (`!z. abs(norm z) = norm z`,
 488   REWRITE_TAC[real_abs; COMPLEX_NORM_POS]);;
 489
 490 let COMPLEX_NORM_ZERO = prove
 491  (`!z. (norm z = &0) <=> (z = Cx(&0))`,
 492   GEN_TAC THEN REWRITE_TAC[complex_norm] THEN
 493   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_0] THEN
 494   SIMP_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_LE_ADD; REAL_POS; SQRT_INJ] THEN
 495   REWRITE_TAC[COMPLEX_EQ; RE; IM; CX_DEF] THEN
 496   SIMP_TAC[REAL_LE_SQUARE; REAL_ARITH
 497    `&0 <= x /\ &0 <= y ==> ((x + y = &0) <=> (x = &0) /\ (y = &0))`] THEN
 498   REWRITE_TAC[REAL_ENTIRE]);;
 499
 500 let COMPLEX_NORM_NUM = prove
 501  (`norm(Cx(&n)) = &n`,
 502   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM]);;
 503
 504 let COMPLEX_NORM_0 = prove
 505  (`norm(Cx(&0)) = &0`,
 506   MESON_TAC[COMPLEX_NORM_ZERO]);;
 507
 508 let COMPLEX_NORM_NZ = prove
 509  (`!z. &0 < norm(z) <=> ~(z = Cx(&0))`,
 510   MESON_TAC[COMPLEX_NORM_ZERO; COMPLEX_ABS_NORM; REAL_ABS_NZ]);;
 511
 512 let COMPLEX_NORM_NEG = prove
 513  (`!z. norm(--z) = norm(z)`,
 514   REWRITE_TAC[complex_neg; complex_norm; REAL_POW_2; RE; IM] THEN
 515   GEN_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC);;
 516
 517 let COMPLEX_NORM_MUL = prove
 518  (`!w z. norm(w * z) = norm(w) * norm(z)`,
 519   REPEAT GEN_TAC THEN
 520   REWRITE_TAC[complex_norm; complex_mul; RE; IM] THEN
 521   SIMP_TAC[GSYM SQRT_MUL; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
 522   AP_TERM_TAC THEN REAL_ARITH_TAC);;
 523
 524 let COMPLEX_NORM_POW = prove
 525  (`!z n. norm(z pow n) = norm(z) pow n`,
 526   GEN_TAC THEN INDUCT_TAC THEN
 527   ASM_REWRITE_TAC[complex_pow; real_pow; COMPLEX_NORM_NUM; COMPLEX_NORM_MUL]);;
 528
 529 let COMPLEX_NORM_INV = prove
 530  (`!z. norm(inv z) = inv(norm z)`,
 531   GEN_TAC THEN REWRITE_TAC[complex_norm; complex_inv; RE; IM] THEN
 532   REWRITE_TAC[REAL_POW_2; real_div] THEN
 533   REWRITE_TAC[REAL_ARITH `(r * d) * r * d + (--i * d) * --i * d =
 534                           (r * r + i * i) * d * d:real`] THEN
 535   ASM_CASES_TAC `Re z * Re z + Im z * Im z = &0` THENL
 536    [ASM_REWRITE_TAC[REAL_INV_0; SQRT_0; REAL_MUL_LZERO]; ALL_TAC] THEN
 537   CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN
 538   SIMP_TAC[GSYM SQRT_MUL; REAL_LE_MUL; REAL_LE_INV_EQ; REAL_LE_ADD;
 539            REAL_LE_SQUARE] THEN
 540   ONCE_REWRITE_TAC[AC REAL_MUL_AC
 541    `a * a * b * b:real = (a * b) * (a * b)`] THEN
 542   ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; SQRT_1]);;
 543
 544 let COMPLEX_NORM_DIV = prove
 545  (`!w z. norm(w / z) = norm(w) / norm(z)`,
 546   REWRITE_TAC[complex_div; real_div; COMPLEX_NORM_INV; COMPLEX_NORM_MUL]);;
 547
 548 let COMPLEX_NORM_TRIANGLE = prove
 549  (`!w z. norm(w + z) <= norm(w) + norm(z)`,
 550   REPEAT GEN_TAC THEN REWRITE_TAC[complex_norm; complex_add; RE; IM] THEN
 551   MATCH_MP_TAC(REAL_ARITH `&0 <= y /\ abs(x) <= abs(y) ==> x <= y`) THEN
 552   SIMP_TAC[SQRT_POS_LE; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE;
 553            REAL_LE_SQUARE_ABS; SQRT_POW_2] THEN
 554   GEN_REWRITE_TAC RAND_CONV[REAL_ARITH
 555     `(a + b) * (a + b) = a * a + b * b + &2 * a * b`] THEN
 556   REWRITE_TAC[GSYM REAL_POW_2] THEN
 557   SIMP_TAC[SQRT_POW_2; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
 558   REWRITE_TAC[REAL_ARITH
 559    `(rw + rz) * (rw + rz) + (iw + iz) * (iw + iz) <=
 560     (rw * rw + iw * iw) + (rz * rz + iz * iz) + &2 * other <=>
 561     rw * rz + iw * iz <= other`] THEN
 562   SIMP_TAC[GSYM SQRT_MUL; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
 563   MATCH_MP_TAC(REAL_ARITH `&0 <= y /\ abs(x) <= abs(y) ==> x <= y`) THEN
 564   SIMP_TAC[SQRT_POS_LE; REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE;
 565            REAL_LE_SQUARE_ABS; SQRT_POW_2; REAL_LE_MUL] THEN
 566   REWRITE_TAC[REAL_ARITH
 567    `(rw * rz + iw * iz) * (rw * rz + iw * iz) <=
 568     (rw * rw + iw * iw) * (rz * rz + iz * iz) <=>
 569     &0 <= (rw * iz - rz * iw) * (rw * iz - rz * iw)`] THEN
 570   REWRITE_TAC[REAL_LE_SQUARE]);;
 571
 572 let COMPLEX_NORM_TRIANGLE_SUB = prove
 573  (`!w z. norm(w) <= norm(w + z) + norm(z)`,
 574   MESON_TAC[COMPLEX_NORM_TRIANGLE; COMPLEX_NORM_NEG; COMPLEX_ADD_ASSOC;
 575             COMPLEX_ADD_RINV; COMPLEX_ADD_RID]);;
 576
 577 let COMPLEX_NORM_ABS_NORM = prove
 578  (`!w z. abs(norm w - norm z) <= norm(w - z)`,
 579   REPEAT GEN_TAC THEN
 580   MATCH_MP_TAC(REAL_ARITH
 581    `a - b <= x /\ b - a <= x ==> abs(a - b) <= x:real`) THEN
 582   MESON_TAC[COMPLEX_NEG_SUB; COMPLEX_NORM_NEG; REAL_LE_SUB_RADD; complex_sub;
 583             COMPLEX_NORM_TRIANGLE_SUB]);;
 584
 585 (* ------------------------------------------------------------------------- *)
 586 (* Complex conjugate.                                                        *)
 587 (* ------------------------------------------------------------------------- *)
 588
 589 let cnj = new_definition
 590   `cnj(z) = complex(Re(z),--(Im(z)))`;;
 591
 592 (* ------------------------------------------------------------------------- *)
 593 (* Conjugation is an automorphism.                                           *)
 594 (* ------------------------------------------------------------------------- *)
 595
 596 let CNJ_INJ = prove
 597  (`!w z. (cnj(w) = cnj(z)) <=> (w = z)`,
 598   REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_EQ_NEG2]);;
 599
 600 let CNJ_CNJ = prove
 601  (`!z. cnj(cnj z) = z`,
 602   REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_NEG_NEG]);;
 603
 604 let CNJ_CX = prove
 605  (`!x. cnj(Cx x) = Cx x`,
 606   REWRITE_TAC[cnj; COMPLEX_EQ; CX_DEF; REAL_NEG_0; RE; IM]);;
 607
 608 let COMPLEX_NORM_CNJ = prove
 609  (`!z. norm(cnj z) = norm(z)`,
 610   REWRITE_TAC[complex_norm; cnj; REAL_POW_2] THEN
 611   REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; RE; IM; REAL_NEG_NEG]);;
 612
 613 let CNJ_NEG = prove
 614  (`!z. cnj(--z) = --(cnj z)`,
 615   REWRITE_TAC[cnj; complex_neg; COMPLEX_EQ; RE; IM]);;
 616
 617 let CNJ_INV = prove
 618  (`!z. cnj(inv z) = inv(cnj z)`,
 619   REWRITE_TAC[cnj; complex_inv; COMPLEX_EQ; RE; IM] THEN
 620   REWRITE_TAC[real_div; REAL_NEG_NEG; REAL_POW_2;
 621               REAL_MUL_LNEG; REAL_MUL_RNEG]);;
 622
 623 let CNJ_ADD = prove
 624  (`!w z. cnj(w + z) = cnj(w) + cnj(z)`,
 625   REWRITE_TAC[cnj; complex_add; COMPLEX_EQ; RE; IM] THEN
 626   REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
 627
 628 let CNJ_SUB = prove
 629  (`!w z. cnj(w - z) = cnj(w) - cnj(z)`,
 630   REWRITE_TAC[complex_sub; CNJ_ADD; CNJ_NEG]);;
 631
 632 let CNJ_MUL = prove
 633  (`!w z. cnj(w * z) = cnj(w) * cnj(z)`,
 634   REWRITE_TAC[cnj; complex_mul; COMPLEX_EQ; RE; IM] THEN
 635   REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
 636
 637 let CNJ_DIV = prove
 638  (`!w z. cnj(w / z) = cnj(w) / cnj(z)`,
 639   REWRITE_TAC[complex_div; CNJ_MUL; CNJ_INV]);;
 640
 641 let CNJ_POW = prove
 642  (`!z n. cnj(z pow n) = cnj(z) pow n`,
 643   GEN_TAC THEN INDUCT_TAC THEN
 644   ASM_REWRITE_TAC[complex_pow; CNJ_MUL; CNJ_CX]);;
 645
 646 (* ------------------------------------------------------------------------- *)
 647 (* Conversion of (complex-type) rational constant to ML rational number.     *)
 648 (* ------------------------------------------------------------------------- *)
 649
 650 let is_complex_const =
 651   let cx_tm = `Cx` in
 652   fun tm ->
 653     is_comb tm &
 654     let l,r = dest_comb tm in l = cx_tm & is_ratconst r;;
 655
 656 let dest_complex_const =
 657   let cx_tm = `Cx` in
 658   fun tm ->
 659     let l,r = dest_comb tm in
 660     if l = cx_tm then rat_of_term r
 661     else failwith "dest_complex_const";;
 662
 663 let mk_complex_const =
 664   let cx_tm = `Cx` in
 665   fun r ->
 666     mk_comb(cx_tm,term_of_rat r);;
 667
 668 (* ------------------------------------------------------------------------- *)
 669 (* Conversions to perform operations if coefficients are rational constants. *)
 670 (* ------------------------------------------------------------------------- *)
 671
 672 let COMPLEX_RAT_MUL_CONV =
 673   GEN_REWRITE_CONV I [GSYM CX_MUL] THENC RAND_CONV REAL_RAT_MUL_CONV;;
 674
 675 let COMPLEX_RAT_ADD_CONV =
 676   GEN_REWRITE_CONV I [GSYM CX_ADD] THENC RAND_CONV REAL_RAT_ADD_CONV;;
 677
 678 let COMPLEX_RAT_EQ_CONV =
 679   GEN_REWRITE_CONV I [CX_INJ] THENC REAL_RAT_EQ_CONV;;
 680
 681 let COMPLEX_RAT_POW_CONV =
 682   let x_tm = `x:real`
 683   and n_tm = `n:num` in
 684   let pth = SYM(SPECL [x_tm; n_tm] CX_POW) in
 685   fun tm ->
 686     let lop,r = dest_comb tm in
 687     let op,bod = dest_comb lop in
 688     let th1 = INST [rand bod,x_tm; r,n_tm] pth in
 689     let tm1,tm2 = dest_comb(concl th1) in
 690     if rand tm1 <> tm then failwith "COMPLEX_RAT_POW_CONV" else
 691     let tm3,tm4 = dest_comb tm2 in
 692     TRANS th1 (AP_TERM tm3 (REAL_RAT_REDUCE_CONV tm4));;
 693
 694 (* ------------------------------------------------------------------------- *)
 695 (* Instantiate polynomial normalizer.                                        *)
 696 (* ------------------------------------------------------------------------- *)
 697
 698 let COMPLEX_POLY_CLAUSES = prove
 699  (`(!x y z. x + (y + z) = (x + y) + z) /\
 700    (!x y. x + y = y + x) /\
 701    (!x. Cx(&0) + x = x) /\
 702    (!x y z. x * (y * z) = (x * y) * z) /\
 703    (!x y. x * y = y * x) /\
 704    (!x. Cx(&1) * x = x) /\
 705    (!x. Cx(&0) * x = Cx(&0)) /\
 706    (!x y z. x * (y + z) = x * y + x * z) /\
 707    (!x. x pow 0 = Cx(&1)) /\
 708    (!x n. x pow (SUC n) = x * x pow n)`,
 709   REWRITE_TAC[complex_pow] THEN SIMPLE_COMPLEX_ARITH_TAC)
 710 and COMPLEX_POLY_NEG_CLAUSES = prove
 711  (`(!x. --x = Cx(-- &1) * x) /\
 712    (!x y. x - y = x + Cx(-- &1) * y)`,
 713   SIMPLE_COMPLEX_ARITH_TAC);;
 714
 715 let COMPLEX_POLY_NEG_CONV,COMPLEX_POLY_ADD_CONV,COMPLEX_POLY_SUB_CONV,
 716     COMPLEX_POLY_MUL_CONV,COMPLEX_POLY_POW_CONV,COMPLEX_POLY_CONV =
 717   SEMIRING_NORMALIZERS_CONV COMPLEX_POLY_CLAUSES COMPLEX_POLY_NEG_CLAUSES
 718    (is_complex_const,
 719     COMPLEX_RAT_ADD_CONV,COMPLEX_RAT_MUL_CONV,COMPLEX_RAT_POW_CONV)
 720    (<);;
 721
 722 let COMPLEX_RAT_INV_CONV =
 723   GEN_REWRITE_CONV I [GSYM CX_INV] THENC RAND_CONV REAL_RAT_INV_CONV;;
 724
 725 let COMPLEX_POLY_CONV =
 726   let neg_tm = `(--):complex->complex`
 727   and inv_tm = `inv:complex->complex`
 728   and add_tm = `(+):complex->complex->complex`
 729   and sub_tm = `(-):complex->complex->complex`
 730   and mul_tm = `(*):complex->complex->complex`
 731   and div_tm = `(/):complex->complex->complex`
 732   and pow_tm = `(pow):complex->num->complex`
 733   and div_conv = REWR_CONV complex_div in
 734   let rec COMPLEX_POLY_CONV tm =
 735     if not(is_comb tm) or is_complex_const tm then REFL tm else
 736     let lop,r = dest_comb tm in
 737     if lop = neg_tm then
 738       let th1 = AP_TERM lop (COMPLEX_POLY_CONV r) in
 739       TRANS th1 (COMPLEX_POLY_NEG_CONV (rand(concl th1)))
 740     else if lop = inv_tm then
 741       let th1 = AP_TERM lop (COMPLEX_POLY_CONV r) in
 742       TRANS th1 (TRY_CONV COMPLEX_RAT_INV_CONV (rand(concl th1)))
 743     else if not(is_comb lop) then REFL tm else
 744     let op,l = dest_comb lop in
 745     if op = pow_tm then
 746       let th1 = AP_THM (AP_TERM op (COMPLEX_POLY_CONV l)) r in
 747       TRANS th1 (TRY_CONV COMPLEX_POLY_POW_CONV (rand(concl th1)))
 748     else if op = add_tm or op = mul_tm or op = sub_tm then
 749       let th1 = MK_COMB(AP_TERM op (COMPLEX_POLY_CONV l),
 750                         COMPLEX_POLY_CONV r) in
 751       let fn = if op = add_tm then COMPLEX_POLY_ADD_CONV
 752                else if op = mul_tm then COMPLEX_POLY_MUL_CONV
 753                else COMPLEX_POLY_SUB_CONV in
 754       TRANS th1 (fn (rand(concl th1)))
 755     else if op = div_tm then
 756       let th1 = div_conv tm in
 757       TRANS th1 (COMPLEX_POLY_CONV (rand(concl th1)))
 758     else REFL tm in
 759   COMPLEX_POLY_CONV;;
 760
 761 (* ------------------------------------------------------------------------- *)
 762 (* Complex number version of usual ring procedure.                           *)
 763 (* ------------------------------------------------------------------------- *)
 764
 765 let COMPLEX_MUL_LINV = prove
 766  (`!z. ~(z = Cx(&0)) ==> (inv(z) * z = Cx(&1))`,
 767   REWRITE_TAC[complex_mul; complex_inv; RE; IM; COMPLEX_EQ; CX_DEF] THEN
 768   REWRITE_TAC[GSYM REAL_SOS_EQ_0] THEN CONV_TAC REAL_FIELD);;
 769
 770 let COMPLEX_MUL_RINV = prove
 771  (`!z. ~(z = Cx(&0)) ==> (z * inv(z) = Cx(&1))`,
 772   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN REWRITE_TAC[COMPLEX_MUL_LINV]);;
 773
 774 let COMPLEX_RING,complex_ideal_cofactors =
 775   let ring_pow_tm = `(pow):complex->num->complex`
 776   and COMPLEX_INTEGRAL = prove
 777    (`(!x. Cx(&0) * x = Cx(&0)) /\
 778      (!x y z. (x + y = x + z) <=> (y = z)) /\
 779      (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
 780     REWRITE_TAC[COMPLEX_ENTIRE; SIMPLE_COMPLEX_ARITH
 781      `(w * y + x * z = w * z + x * y) <=>
 782       (w - x) * (y - z) = Cx(&0)`] THEN
 783     SIMPLE_COMPLEX_ARITH_TAC)
 784   and COMPLEX_RABINOWITSCH = prove
 785    (`!x y:complex. ~(x = y) <=> ?z. (x - y) * z = Cx(&1)`,
 786     REPEAT GEN_TAC THEN
 787     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM COMPLEX_SUB_0] THEN
 788     MESON_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_LZERO;
 789               SIMPLE_COMPLEX_ARITH `~(Cx(&1) = Cx(&0))`])
 790   and init = ALL_CONV in
 791   let pure,ideal =
 792     RING_AND_IDEAL_CONV
 793         (dest_complex_const,mk_complex_const,COMPLEX_RAT_EQ_CONV,
 794          `(--):complex->complex`,`(+):complex->complex->complex`,
 795          `(-):complex->complex->complex`,`(inv):complex->complex`,
 796          `(*):complex->complex->complex`,`(/):complex->complex->complex`,
 797          `(pow):complex->num->complex`,
 798          COMPLEX_INTEGRAL,COMPLEX_RABINOWITSCH,COMPLEX_POLY_CONV) in
 799   (fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)))),
 800   ideal;;
 801
 802 (* ------------------------------------------------------------------------- *)
 803 (* Most basic properties of inverses.                                        *)
 804 (* ------------------------------------------------------------------------- *)
 805
 806 let COMPLEX_INV_0 = prove
 807  (`inv(Cx(&0)) = Cx(&0)`,
 808   REWRITE_TAC[complex_inv; CX_DEF; RE; IM; real_div; REAL_MUL_LZERO;
 809               REAL_NEG_0]);;
 810
 811 let COMPLEX_INV_MUL = prove
 812  (`!w z. inv(w * z) = inv(w) * inv(z)`,
 813   REPEAT GEN_TAC THEN
 814   MAP_EVERY ASM_CASES_TAC [`w = Cx(&0)`; `z = Cx(&0)`] THEN
 815   ASM_REWRITE_TAC[COMPLEX_INV_0; COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO] THEN
 816   REPEAT(POP_ASSUM MP_TAC) THEN
 817   REWRITE_TAC[complex_mul; complex_inv; RE; IM; COMPLEX_EQ; CX_DEF] THEN
 818   REWRITE_TAC[GSYM REAL_SOS_EQ_0] THEN CONV_TAC REAL_FIELD);;
 819
 820 let COMPLEX_INV_1 = prove
 821  (`inv(Cx(&1)) = Cx(&1)`,
 822   REWRITE_TAC[complex_inv; CX_DEF; RE; IM] THEN
 823   CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_DIV_1]);;
 824
 825 let COMPLEX_POW_INV = prove
 826  (`!x n. (inv x) pow n = inv(x pow n)`,
 827   GEN_TAC THEN INDUCT_TAC THEN
 828   ASM_REWRITE_TAC[complex_pow; COMPLEX_INV_1; COMPLEX_INV_MUL]);;
 829
 830 let COMPLEX_INV_INV = prove
 831  (`!x:complex. inv(inv x) = x`,
 832   GEN_TAC THEN ASM_CASES_TAC `x = Cx(&0)` THEN
 833   ASM_REWRITE_TAC[COMPLEX_INV_0] THEN
 834   POP_ASSUM MP_TAC THEN
 835   MAP_EVERY (fun t -> MP_TAC(SPEC t COMPLEX_MUL_RINV))
 836    [`x:complex`; `inv(x):complex`] THEN
 837   CONV_TAC COMPLEX_RING);;
 838
 839 (* ------------------------------------------------------------------------- *)
 840 (* And also field procedure.                                                 *)
 841 (* ------------------------------------------------------------------------- *)
 842
 843 let COMPLEX_FIELD =
 844   let prenex_conv =
 845     TOP_DEPTH_CONV BETA_CONV THENC
 846     PURE_REWRITE_CONV[FORALL_SIMP; EXISTS_SIMP; complex_div;
 847                       COMPLEX_INV_INV; COMPLEX_INV_MUL; GSYM REAL_POW_INV] THENC
 848     NNFC_CONV THENC DEPTH_BINOP_CONV `(/\)` CONDS_CELIM_CONV THENC
 849     PRENEX_CONV
 850   and setup_conv = NNF_CONV THENC WEAK_CNF_CONV THENC CONJ_CANON_CONV
 851   and is_inv =
 852     let inv_tm = `inv:complex->complex`
 853     and is_div = is_binop `(/):complex->complex->complex` in
 854     fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) &
 855               not(is_complex_const(rand tm))
 856   and lemma_inv = MESON[COMPLEX_MUL_RINV]
 857     `!x. x = Cx(&0) \/ x * inv(x) = Cx(&1)`
 858   and dcases = MATCH_MP(TAUT `(p \/ q) /\ (r \/ s) ==> (p \/ r) \/ q /\ s`) in
 859   let cases_rule th1 th2 = dcases (CONJ th1 th2) in
 860   let BASIC_COMPLEX_FIELD tm =
 861     let is_freeinv t = is_inv t & free_in t tm in
 862     let itms = setify(map rand (find_terms is_freeinv tm)) in
 863     let dth = if itms = [] then TRUTH
 864               else end_itlist cases_rule (map (C SPEC lemma_inv) itms) in
 865     let tm' = mk_imp(concl dth,tm) in
 866     let th1 = setup_conv tm' in
 867     let ths = map COMPLEX_RING (conjuncts(rand(concl th1))) in
 868     let th2 = EQ_MP (SYM th1) (end_itlist CONJ ths) in
 869     MP (EQ_MP (SYM th1) (end_itlist CONJ ths)) dth in
 870   fun tm ->
 871     let th0 = prenex_conv tm in
 872     let tm0 = rand(concl th0) in
 873     let avs,bod = strip_forall tm0 in
 874     let th1 = setup_conv bod in
 875     let ths = map BASIC_COMPLEX_FIELD (conjuncts(rand(concl th1))) in
 876     EQ_MP (SYM th0) (GENL avs (EQ_MP (SYM th1) (end_itlist CONJ ths)));;
 877
 878 (* ------------------------------------------------------------------------- *)
 879 (* Properties of inverses, divisions are now mostly automatic.               *)
 880 (* ------------------------------------------------------------------------- *)
 881
 882 let COMPLEX_POW_DIV = prove
 883  (`!x y n. (x / y) pow n = (x pow n) / (y pow n)`,
 884   REWRITE_TAC[complex_div; COMPLEX_POW_MUL; COMPLEX_POW_INV]);;
 885
 886 let COMPLEX_DIV_REFL = prove
 887  (`!x. ~(x = Cx(&0)) ==> (x / x = Cx(&1))`,
 888   CONV_TAC COMPLEX_FIELD);;
 889
 890 let COMPLEX_EQ_MUL_LCANCEL = prove
 891  (`!x y z. (x * y = x * z) <=> (x = Cx(&0)) \/ (y = z)`,
 892   CONV_TAC COMPLEX_FIELD);;
 893
 894 let COMPLEX_EQ_MUL_RCANCEL = prove
 895  (`!x y z. (x * z = y * z) <=> (x = y) \/ (z = Cx(&0))`,
 896   CONV_TAC COMPLEX_FIELD);;
 897
 898 let COMPLEX_MUL_RINV_UNIQ = prove
 899  (`!w z. w * z = Cx(&1) ==> inv w = z`,
 900   CONV_TAC COMPLEX_FIELD);;
 901
 902 let COMPLEX_MUL_LINV_UNIQ = prove
 903  (`!w z. w * z = Cx(&1) ==> inv z = w`,
 904   CONV_TAC COMPLEX_FIELD);;
 905
 906 let COMPLEX_DIV_LMUL = prove
 907  (`!w z. ~(z = Cx(&0)) ==> z * w / z = w`,
 908   CONV_TAC COMPLEX_FIELD);;
 909
 910 let COMPLEX_DIV_RMUL = prove
 911  (`!w z. ~(z = Cx(&0)) ==> w / z * z = w`,
 912   CONV_TAC COMPLEX_FIELD);;