1 (* ========================================================================= *)
2 (* Basic definitions and properties of complex numbers. *)
3 (* ========================================================================= *)
5 needs "Library/transc.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Definition of complex number type. *)
11 (* ------------------------------------------------------------------------- *)
13 let complex_tybij_raw =
14 new_type_definition "complex" ("complex","coords")
15 (prove(`?x:real#real. T`,REWRITE_TAC[]));;
17 let complex_tybij = REWRITE_RULE [] complex_tybij_raw;;
19 (* ------------------------------------------------------------------------- *)
20 (* Real and imaginary parts of a number. *)
21 (* ------------------------------------------------------------------------- *)
23 let RE_DEF = new_definition
24 `Re(z) = FST(coords(z))`;;
26 let IM_DEF = new_definition
27 `Im(z) = SND(coords(z))`;;
29 (* ------------------------------------------------------------------------- *)
30 (* Set up overloading. *)
31 (* ------------------------------------------------------------------------- *)
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`];;
42 let prioritize_complex() = prioritize_overload(mk_type("complex",[]));;
44 (* ------------------------------------------------------------------------- *)
45 (* Complex absolute value (modulus). *)
46 (* ------------------------------------------------------------------------- *)
48 make_overloadable "norm" `:A->real`;;
49 overload_interface("norm",`complex_norm:complex->real`);;
51 let complex_norm = new_definition
52 `norm(z) = sqrt(Re(z) pow 2 + Im(z) pow 2)`;;
54 (* ------------------------------------------------------------------------- *)
55 (* Imaginary unit (too inconvenient to use "i"!) *)
56 (* ------------------------------------------------------------------------- *)
58 let ii = new_definition
59 `ii = complex(&0,&1)`;;
61 (* ------------------------------------------------------------------------- *)
62 (* Injection from reals. *)
63 (* ------------------------------------------------------------------------- *)
65 let CX_DEF = new_definition
66 `Cx(a) = complex(a,&0)`;;
68 (* ------------------------------------------------------------------------- *)
69 (* Arithmetic operations. *)
70 (* ------------------------------------------------------------------------- *)
72 let complex_neg = new_definition
73 `--z = complex(--(Re(z)),--(Im(z)))`;;
75 let complex_add = new_definition
76 `w + z = complex(Re(w) + Re(z),Im(w) + Im(z))`;;
78 let complex_sub = new_definition
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))`;;
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))`;;
89 let complex_div = new_definition
90 `w / z = w * inv(z)`;;
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)`;;
96 (* ------------------------------------------------------------------------- *)
97 (* Various handy rewrites. *)
98 (* ------------------------------------------------------------------------- *)
101 (`(Re(complex(x,y)) = x)`,
102 REWRITE_TAC[RE_DEF; complex_tybij]);;
105 (`Im(complex(x,y)) = y`,
106 REWRITE_TAC[IM_DEF; complex_tybij]);;
109 (`complex(Re(z),Im(z)) = z`,
110 REWRITE_TAC[IM_DEF; RE_DEF; complex_tybij]);;
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]);;
116 (* ------------------------------------------------------------------------- *)
117 (* Crude tactic to automate very simple algebraic equivalences. *)
118 (* ------------------------------------------------------------------------- *)
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
125 let SIMPLE_COMPLEX_ARITH tm = prove(tm,SIMPLE_COMPLEX_ARITH_TAC);;
127 (* ------------------------------------------------------------------------- *)
128 (* Basic algebraic properties that can be proved automatically by this. *)
129 (* ------------------------------------------------------------------------- *)
131 let COMPLEX_ADD_SYM = prove
132 (`!x y. x + y = y + x`,
133 SIMPLE_COMPLEX_ARITH_TAC);;
135 let COMPLEX_ADD_ASSOC = prove
136 (`!x y z. x + y + z = (x + y) + z`,
137 SIMPLE_COMPLEX_ARITH_TAC);;
139 let COMPLEX_ADD_LID = prove
140 (`!x. Cx(&0) + x = x`,
141 SIMPLE_COMPLEX_ARITH_TAC);;
143 let COMPLEX_ADD_LINV = prove
144 (`!x. --x + x = Cx(&0)`,
145 SIMPLE_COMPLEX_ARITH_TAC);;
147 let COMPLEX_MUL_SYM = prove
148 (`!x y. x * y = y * x`,
149 SIMPLE_COMPLEX_ARITH_TAC);;
151 let COMPLEX_MUL_ASSOC = prove
152 (`!x y z. x * y * z = (x * y) * z`,
153 SIMPLE_COMPLEX_ARITH_TAC);;
155 let COMPLEX_MUL_LID = prove
156 (`!x. Cx(&1) * x = x`,
157 SIMPLE_COMPLEX_ARITH_TAC);;
159 let COMPLEX_ADD_LDISTRIB = prove
160 (`!x y z. x * (y + z) = x * y + x * z`,
161 SIMPLE_COMPLEX_ARITH_TAC);;
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);;
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);;
171 let COMPLEX_ADD_RID = prove
172 (`!x. x + Cx(&0) = x`,
173 SIMPLE_COMPLEX_ARITH_TAC);;
175 let COMPLEX_MUL_RID = prove
176 (`!x. x * Cx(&1) = x`,
177 SIMPLE_COMPLEX_ARITH_TAC);;
179 let COMPLEX_ADD_RINV = prove
180 (`!x. x + --x = Cx(&0)`,
181 SIMPLE_COMPLEX_ARITH_TAC);;
183 let COMPLEX_ADD_RDISTRIB = prove
184 (`!x y z. (x + y) * z = x * z + y * z`,
185 SIMPLE_COMPLEX_ARITH_TAC);;
187 let COMPLEX_EQ_ADD_LCANCEL = prove
188 (`!x y z. (x + y = x + z) <=> (y = z)`,
189 SIMPLE_COMPLEX_ARITH_TAC);;
191 let COMPLEX_EQ_ADD_RCANCEL = prove
192 (`!x y z. (x + z = y + z) <=> (x = y)`,
193 SIMPLE_COMPLEX_ARITH_TAC);;
195 let COMPLEX_MUL_RZERO = prove
196 (`!x. x * Cx(&0) = Cx(&0)`,
197 SIMPLE_COMPLEX_ARITH_TAC);;
199 let COMPLEX_MUL_LZERO = prove
200 (`!x. Cx(&0) * x = Cx(&0)`,
201 SIMPLE_COMPLEX_ARITH_TAC);;
203 let COMPLEX_NEG_NEG = prove
205 SIMPLE_COMPLEX_ARITH_TAC);;
207 let COMPLEX_MUL_RNEG = prove
208 (`!x y. x * --y = --(x * y)`,
209 SIMPLE_COMPLEX_ARITH_TAC);;
211 let COMPLEX_MUL_LNEG = prove
212 (`!x y. --x * y = --(x * y)`,
213 SIMPLE_COMPLEX_ARITH_TAC);;
215 let COMPLEX_NEG_ADD = prove
216 (`!x y. --(x + y) = --x + --y`,
217 SIMPLE_COMPLEX_ARITH_TAC);;
219 let COMPLEX_NEG_0 = prove
220 (`--Cx(&0) = Cx(&0)`,
221 SIMPLE_COMPLEX_ARITH_TAC);;
223 let COMPLEX_EQ_ADD_LCANCEL_0 = prove
224 (`!x y. (x + y = x) <=> (y = Cx(&0))`,
225 SIMPLE_COMPLEX_ARITH_TAC);;
227 let COMPLEX_EQ_ADD_RCANCEL_0 = prove
228 (`!x y. (x + y = y) <=> (x = Cx(&0))`,
229 SIMPLE_COMPLEX_ARITH_TAC);;
231 let COMPLEX_LNEG_UNIQ = prove
232 (`!x y. (x + y = Cx(&0)) <=> (x = --y)`,
233 SIMPLE_COMPLEX_ARITH_TAC);;
235 let COMPLEX_RNEG_UNIQ = prove
236 (`!x y. (x + y = Cx(&0)) <=> (y = --x)`,
237 SIMPLE_COMPLEX_ARITH_TAC);;
239 let COMPLEX_NEG_LMUL = prove
240 (`!x y. --(x * y) = --x * y`,
241 SIMPLE_COMPLEX_ARITH_TAC);;
243 let COMPLEX_NEG_RMUL = prove
244 (`!x y. --(x * y) = x * --y`,
245 SIMPLE_COMPLEX_ARITH_TAC);;
247 let COMPLEX_NEG_MUL2 = prove
248 (`!x y. --x * --y = x * y`,
249 SIMPLE_COMPLEX_ARITH_TAC);;
251 let COMPLEX_SUB_ADD = prove
252 (`!x y. x - y + y = x`,
253 SIMPLE_COMPLEX_ARITH_TAC);;
255 let COMPLEX_SUB_ADD2 = prove
256 (`!x y. y + x - y = x`,
257 SIMPLE_COMPLEX_ARITH_TAC);;
259 let COMPLEX_SUB_REFL = prove
260 (`!x. x - x = Cx(&0)`,
261 SIMPLE_COMPLEX_ARITH_TAC);;
263 let COMPLEX_SUB_0 = prove
264 (`!x y. (x - y = Cx(&0)) <=> (x = y)`,
265 SIMPLE_COMPLEX_ARITH_TAC);;
267 let COMPLEX_NEG_EQ_0 = prove
268 (`!x. (--x = Cx(&0)) <=> (x = Cx(&0))`,
269 SIMPLE_COMPLEX_ARITH_TAC);;
271 let COMPLEX_NEG_SUB = prove
272 (`!x y. --(x - y) = y - x`,
273 SIMPLE_COMPLEX_ARITH_TAC);;
275 let COMPLEX_ADD_SUB = prove
276 (`!x y. (x + y) - x = y`,
277 SIMPLE_COMPLEX_ARITH_TAC);;
279 let COMPLEX_NEG_EQ = prove
280 (`!x y. (--x = y) <=> (x = --y)`,
281 SIMPLE_COMPLEX_ARITH_TAC);;
283 let COMPLEX_NEG_MINUS1 = prove
284 (`!x. --x = --Cx(&1) * x`,
285 SIMPLE_COMPLEX_ARITH_TAC);;
287 let COMPLEX_SUB_SUB = prove
288 (`!x y. x - y - x = --y`,
289 SIMPLE_COMPLEX_ARITH_TAC);;
291 let COMPLEX_ADD2_SUB2 = prove
292 (`!a b c d. (a + b) - (c + d) = a - c + b - d`,
293 SIMPLE_COMPLEX_ARITH_TAC);;
295 let COMPLEX_SUB_LZERO = prove
296 (`!x. Cx(&0) - x = --x`,
297 SIMPLE_COMPLEX_ARITH_TAC);;
299 let COMPLEX_SUB_RZERO = prove
300 (`!x. x - Cx(&0) = x`,
301 SIMPLE_COMPLEX_ARITH_TAC);;
303 let COMPLEX_SUB_LNEG = prove
304 (`!x y. --x - y = --(x + y)`,
305 SIMPLE_COMPLEX_ARITH_TAC);;
307 let COMPLEX_SUB_RNEG = prove
308 (`!x y. x - --y = x + y`,
309 SIMPLE_COMPLEX_ARITH_TAC);;
311 let COMPLEX_SUB_NEG2 = prove
312 (`!x y. --x - --y = y - x`,
313 SIMPLE_COMPLEX_ARITH_TAC);;
315 let COMPLEX_SUB_TRIANGLE = prove
316 (`!a b c. a - b + b - c = a - c`,
317 SIMPLE_COMPLEX_ARITH_TAC);;
319 let COMPLEX_EQ_SUB_LADD = prove
320 (`!x y z. (x = y - z) <=> (x + z = y)`,
321 SIMPLE_COMPLEX_ARITH_TAC);;
323 let COMPLEX_EQ_SUB_RADD = prove
324 (`!x y z. (x - y = z) <=> (x = z + y)`,
325 SIMPLE_COMPLEX_ARITH_TAC);;
327 let COMPLEX_SUB_SUB2 = prove
328 (`!x y. x - (x - y) = y`,
329 SIMPLE_COMPLEX_ARITH_TAC);;
331 let COMPLEX_ADD_SUB2 = prove
332 (`!x y. x - (x + y) = --y`,
333 SIMPLE_COMPLEX_ARITH_TAC);;
335 let COMPLEX_DIFFSQ = prove
336 (`!x y. (x + y) * (x - y) = x * x - y * y`,
337 SIMPLE_COMPLEX_ARITH_TAC);;
339 let COMPLEX_EQ_NEG2 = prove
340 (`!x y. (--x = --y) <=> (x = y)`,
341 SIMPLE_COMPLEX_ARITH_TAC);;
343 let COMPLEX_SUB_LDISTRIB = prove
344 (`!x y z. x * (y - z) = x * y - x * z`,
345 SIMPLE_COMPLEX_ARITH_TAC);;
347 let COMPLEX_SUB_RDISTRIB = prove
348 (`!x y z. (x - y) * z = x * z - y * z`,
349 SIMPLE_COMPLEX_ARITH_TAC);;
351 let COMPLEX_MUL_2 = prove
352 (`!x. &2 * x = x + x`,
353 SIMPLE_COMPLEX_ARITH_TAC);;
355 (* ------------------------------------------------------------------------- *)
356 (* Homomorphic embedding properties for Cx mapping. *)
357 (* ------------------------------------------------------------------------- *)
360 (`!x y. (Cx(x) = Cx(y)) <=> (x = y)`,
361 REWRITE_TAC[CX_DEF; COMPLEX_EQ; RE; IM]);;
364 (`!x. Cx(--x) = --(Cx(x))`,
365 REWRITE_TAC[CX_DEF; complex_neg; RE; IM; REAL_NEG_0]);;
368 (`!x. Cx(inv x) = inv(Cx x)`,
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]);;
381 (`!x y. Cx(x + y) = Cx(x) + Cx(y)`,
382 REWRITE_TAC[CX_DEF; complex_add; RE; IM; REAL_ADD_LID]);;
385 (`!x y. Cx(x - y) = Cx(x) - Cx(y)`,
386 REWRITE_TAC[complex_sub; real_sub; CX_ADD; CX_NEG]);;
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]);;
394 (`!x y. Cx(x / y) = Cx(x) / Cx(y)`,
395 REWRITE_TAC[complex_div; real_div; CX_MUL; CX_INV]);;
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]);;
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]);;
408 let COMPLEX_NORM_CX = prove
409 (`!x. norm(Cx(x)) = abs(x)`,
410 REWRITE_TAC[GSYM CX_INJ; CX_ABS]);;
412 (* ------------------------------------------------------------------------- *)
413 (* A convenient lemma that we need a few times below. *)
414 (* ------------------------------------------------------------------------- *)
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);;
421 (* ------------------------------------------------------------------------- *)
423 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
436 let COMPLEX_POW_1 = prove
438 REWRITE_TAC[num_CONV `1`] THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_RID]);;
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]);;
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]);;
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]);;
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]);;
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);;
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]);;
471 (* ------------------------------------------------------------------------- *)
472 (* Norms (aka "moduli"). *)
473 (* ------------------------------------------------------------------------- *)
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]);;
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]);;
486 let COMPLEX_ABS_NORM = prove
487 (`!z. abs(norm z) = norm z`,
488 REWRITE_TAC[real_abs; COMPLEX_NORM_POS]);;
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]);;
500 let COMPLEX_NORM_NUM = prove
501 (`norm(Cx(&n)) = &n`,
502 REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM]);;
504 let COMPLEX_NORM_0 = prove
505 (`norm(Cx(&0)) = &0`,
506 MESON_TAC[COMPLEX_NORM_ZERO]);;
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]);;
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);;
517 let COMPLEX_NORM_MUL = prove
518 (`!w z. norm(w * z) = norm(w) * norm(z)`,
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);;
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]);;
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;
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]);;
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]);;
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]);;
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]);;
577 let COMPLEX_NORM_ABS_NORM = prove
578 (`!w z. abs(norm w - norm z) <= norm(w - z)`,
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]);;
585 (* ------------------------------------------------------------------------- *)
586 (* Complex conjugate. *)
587 (* ------------------------------------------------------------------------- *)
589 let cnj = new_definition
590 `cnj(z) = complex(Re(z),--(Im(z)))`;;
592 (* ------------------------------------------------------------------------- *)
593 (* Conjugation is an automorphism. *)
594 (* ------------------------------------------------------------------------- *)
597 (`!w z. (cnj(w) = cnj(z)) <=> (w = z)`,
598 REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_EQ_NEG2]);;
601 (`!z. cnj(cnj z) = z`,
602 REWRITE_TAC[cnj; COMPLEX_EQ; RE; IM; REAL_NEG_NEG]);;
605 (`!x. cnj(Cx x) = Cx x`,
606 REWRITE_TAC[cnj; COMPLEX_EQ; CX_DEF; REAL_NEG_0; RE; IM]);;
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]);;
614 (`!z. cnj(--z) = --(cnj z)`,
615 REWRITE_TAC[cnj; complex_neg; COMPLEX_EQ; RE; IM]);;
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]);;
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]);;
629 (`!w z. cnj(w - z) = cnj(w) - cnj(z)`,
630 REWRITE_TAC[complex_sub; CNJ_ADD; CNJ_NEG]);;
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]);;
638 (`!w z. cnj(w / z) = cnj(w) / cnj(z)`,
639 REWRITE_TAC[complex_div; CNJ_MUL; CNJ_INV]);;
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]);;
646 (* ------------------------------------------------------------------------- *)
647 (* Conversion of (complex-type) rational constant to ML rational number. *)
648 (* ------------------------------------------------------------------------- *)
650 let is_complex_const =
654 let l,r = dest_comb tm in l = cx_tm & is_ratconst r;;
656 let dest_complex_const =
659 let l,r = dest_comb tm in
660 if l = cx_tm then rat_of_term r
661 else failwith "dest_complex_const";;
663 let mk_complex_const =
666 mk_comb(cx_tm,term_of_rat r);;
668 (* ------------------------------------------------------------------------- *)
669 (* Conversions to perform operations if coefficients are rational constants. *)
670 (* ------------------------------------------------------------------------- *)
672 let COMPLEX_RAT_MUL_CONV =
673 GEN_REWRITE_CONV I [GSYM CX_MUL] THENC RAND_CONV REAL_RAT_MUL_CONV;;
675 let COMPLEX_RAT_ADD_CONV =
676 GEN_REWRITE_CONV I [GSYM CX_ADD] THENC RAND_CONV REAL_RAT_ADD_CONV;;
678 let COMPLEX_RAT_EQ_CONV =
679 GEN_REWRITE_CONV I [CX_INJ] THENC REAL_RAT_EQ_CONV;;
681 let COMPLEX_RAT_POW_CONV =
683 and n_tm = `n:num` in
684 let pth = SYM(SPECL [x_tm; n_tm] CX_POW) in
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));;
694 (* ------------------------------------------------------------------------- *)
695 (* Instantiate polynomial normalizer. *)
696 (* ------------------------------------------------------------------------- *)
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);;
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
719 COMPLEX_RAT_ADD_CONV,COMPLEX_RAT_MUL_CONV,COMPLEX_RAT_POW_CONV)
722 let COMPLEX_RAT_INV_CONV =
723 GEN_REWRITE_CONV I [GSYM CX_INV] THENC RAND_CONV REAL_RAT_INV_CONV;;
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
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
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)))
761 (* ------------------------------------------------------------------------- *)
762 (* Complex number version of usual ring procedure. *)
763 (* ------------------------------------------------------------------------- *)
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);;
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]);;
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)`,
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
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)))),
802 (* ------------------------------------------------------------------------- *)
803 (* Most basic properties of inverses. *)
804 (* ------------------------------------------------------------------------- *)
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;
811 let COMPLEX_INV_MUL = prove
812 (`!w z. inv(w * z) = inv(w) * inv(z)`,
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);;
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]);;
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]);;
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);;
839 (* ------------------------------------------------------------------------- *)
840 (* And also field procedure. *)
841 (* ------------------------------------------------------------------------- *)
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
850 and setup_conv = NNF_CONV THENC WEAK_CNF_CONV THENC CONJ_CANON_CONV
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
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)));;
878 (* ------------------------------------------------------------------------- *)
879 (* Properties of inverses, divisions are now mostly automatic. *)
880 (* ------------------------------------------------------------------------- *)
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]);;
886 let COMPLEX_DIV_REFL = prove
887 (`!x. ~(x = Cx(&0)) ==> (x / x = Cx(&1))`,
888 CONV_TAC COMPLEX_FIELD);;
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);;
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);;
898 let COMPLEX_MUL_RINV_UNIQ = prove
899 (`!w z. w * z = Cx(&1) ==> inv w = z`,
900 CONV_TAC COMPLEX_FIELD);;
902 let COMPLEX_MUL_LINV_UNIQ = prove
903 (`!w z. w * z = Cx(&1) ==> inv z = w`,
904 CONV_TAC COMPLEX_FIELD);;
906 let COMPLEX_DIV_LMUL = prove
907 (`!w z. ~(z = Cx(&0)) ==> z * w / z = w`,
908 CONV_TAC COMPLEX_FIELD);;
910 let COMPLEX_DIV_RMUL = prove
911 (`!w z. ~(z = Cx(&0)) ==> w / z * z = w`,
912 CONV_TAC COMPLEX_FIELD);;