complexScript.sml
1(* ==================================================================
2 TITLE: Developing the theory of complex number
3
4 DESCRIPTION : Definitions and properties of the complex data type
5 and arithmetic operations of complex numbers, and many
6 properties organized in terms of group, field and R-module.
7 Moreover, definitions and properties of complex conjugate,
8 modulus and argument principal value of complex, the operation
9 of nature numbers power of complex numbers, the polar form and
10 exponential form of complex numbers.
11
12 AUTHORS : (Copyright) Yong Guan, Liming Li, Minhua Wu and
13 Zhiping Shi
14 Beijing Engineering Research Center of High Reliable
15 Emmbedded System, Capital Normal University, China
16 DATE : 2011.04.23
17 REFERENCES : John Harrison, realScript.sml, complex.ml and [1]
18 ================================================================== *)
19Theory complex
20Ancestors
21 arithmetic pair real transc
22Libs
23 numLib realLib tautLib AC boolSimps complexPP[qualified]
24
25
26val _ = ParseExtras.temp_loose_equality()
27
28(* ------------------------------------------------------------------ *)
29(* Definition of complex number type. *)
30(* ------------------------------------------------------------------ *)
31
32Type complex = ``: real # real``
33
34(*--------------------------------------------------------------------*)
35(* Now prove 2 lemmas. *)
36(*--------------------------------------------------------------------*)
37
38Theorem COMPLEX_LEMMA1:
39 !a:real b:real c:real d:real.
40 (a * c- b * d) pow 2 + (a * d + b * c) pow 2 =
41 (a pow 2 + b pow 2) * (c pow 2 + d pow 2)
42Proof
43 REWRITE_TAC[POW_2] THEN REAL_ARITH_TAC
44QED
45
46Theorem COMPLEX_LEMMA2:
47 !x y : real. abs x <= sqrt (x pow 2 + y pow 2)
48Proof
49 REPEAT GEN_TAC THEN `0 <= abs x` by PROVE_TAC[ABS_POS] THEN
50 `abs x = sqrt (abs x pow 2)` by PROVE_TAC[POW_2_SQRT] THEN
51 ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_POW2_ABS] THEN
52 `0 <= x pow 2 /\ 0 <= y pow 2` by PROVE_TAC[REAL_LE_POW2] THEN
53 ` x pow 2 <= x pow 2 + y pow 2` by PROVE_TAC[REAL_LE_ADDR] THEN
54 PROVE_TAC[SQRT_MONO_LE]
55QED
56
57(*--------------------------------------------------------------------*)
58(* Now define real part and imaginary part of complex number. *)
59(*--------------------------------------------------------------------*)
60
61Definition RE[nocompute]:RE (z:complex) = FST z
62End
63
64Definition IM[nocompute]:IM (z:complex) = SND z
65End
66
67Theorem COMPLEX:
68 !z:complex. (RE z,IM z) = z
69Proof
70 REWRITE_TAC[RE,IM]
71QED
72
73Theorem COMPLEX_RE_IM_EQ:
74 !z:complex w:complex. (z = w) = (RE z = RE w) /\ (IM z = IM w)
75Proof
76 REWRITE_TAC[RE,IM, PAIR_FST_SND_EQ]
77QED
78
79
80
81(*--------------------------------------------------------------------*)
82(* Now define the inclusion homomorphism: real->complex *)
83(* : num->complex *)
84(*--------------------------------------------------------------------*)
85
86Definition complex_of_real[nocompute]:
87 complex_of_real (x:real) = (x,&0)
88End
89
90Theorem RE_COMPLEX_OF_REAL:
91 !x:real. RE (complex_of_real x) = x
92Proof
93 REWRITE_TAC [complex_of_real,RE]
94QED
95
96Theorem IM_COMPLEX_OF_REAL:
97 !x:real. IM (complex_of_real x) = &0
98Proof
99 REWRITE_TAC [complex_of_real, IM]
100QED
101
102Definition complex_of_num[nocompute]:
103 complex_of_num (n:num) = complex_of_real (real_of_num n)
104End
105
106val _ = add_numeral_form(#"c", SOME "complex_of_num");
107
108Theorem COMPLEX_0:
109 0 = complex_of_real &0
110Proof
111 REWRITE_TAC[complex_of_num]
112QED
113
114Theorem COMPLEX_1:
115 1 = complex_of_real 1
116Proof
117 REWRITE_TAC[complex_of_num]
118QED
119
120Theorem COMPLEX_10:
121 ~(1 = 0)
122Proof
123 REWRITE_TAC[complex_of_num, complex_of_real, COMPLEX_RE_IM_EQ, RE, IM,
124 REAL_10]
125QED
126
127Theorem COMPLEX_0_THM:
128 !z:complex. (z = 0) = (RE z pow 2 + IM z pow 2 = &0)
129Proof
130 REWRITE_TAC [complex_of_num, complex_of_real,RE, IM, PAIR_FST_SND_EQ, POW_2,
131 REAL_SUMSQ]
132QED
133
134(* ------------------------------------------------------------------ *)
135(* Imaginary unit *)
136(* ------------------------------------------------------------------ *)
137
138Definition i[nocompute]: i = (0r,1r)
139End
140
141(* ------------------------------------------------------------------ *)
142(* Arithmetic operations. *)
143(* ------------------------------------------------------------------ *)
144
145Definition complex_add[nocompute]:
146complex_add (z:complex) (w:complex) = (RE z + RE w,IM z + IM w)
147End
148
149Definition complex_neg[nocompute]:
150 complex_neg (z:complex) = (-RE z, -IM z)
151End
152
153Definition complex_mul[nocompute]:
154 complex_mul (z:complex) (w:complex) =
155 (RE z * RE w - IM z * IM w, RE z * IM w + IM z * RE w)
156End
157
158Definition complex_inv[nocompute]:
159 complex_inv (z:complex) =
160 (RE z / ((RE z) pow 2 + (IM z) pow 2),
161 -IM z / ((RE z) pow 2 + (IM z) pow 2))
162End
163
164Overload "+" = Term`$complex_add`
165Overload "~" = Term`$complex_neg`
166Overload "*" = Term`$complex_mul`
167Overload inv = Term`$complex_inv`
168Overload numeric_negate = ``$~ : complex->complex``
169Overload "~" = “$~ : bool -> bool”
170Overload "¬" = “$~ : bool -> bool”
171
172Definition complex_sub[nocompute]:
173 complex_sub (z:complex) (w:complex) = z + ~w
174End
175
176Definition complex_div[nocompute]:
177 complex_div (z:complex) (w:complex) = z * inv w
178End
179
180Overload "-" = Term`$complex_sub`
181val _ = overload_on (GrammarSpecials.decimal_fraction_special, ``complex_div``)
182Overload "/" = Term`complex_div`
183
184val _ = add_ML_dependency "complexPP"
185val _ =
186 add_user_printer ("complex.decimalfractions",
187 ``&(NUMERAL x) : complex / &(NUMERAL y)``)
188
189
190(*--------------------------------------------------------------------*)
191(* Prove lots of field theorems *)
192(*--------------------------------------------------------------------*)
193
194Theorem COMPLEX_ADD_COMM:
195 !z:complex w:complex. z + w = w + z
196Proof
197 REWRITE_TAC [complex_add, RE, IM] THEN PROVE_TAC [REAL_ADD_COMM]
198QED
199
200Theorem COMPLEX_ADD_ASSOC:
201 !z:complex w:complex v:complex. z + (w + v) = z + w + v
202Proof
203 REWRITE_TAC [complex_add, RE, IM] THEN PROVE_TAC [REAL_ADD_ASSOC]
204QED
205
206Theorem COMPLEX_ADD_RID:
207 !z:complex. z + 0 = z
208Proof
209 REWRITE_TAC [complex_of_num,complex_of_real, complex_add, REAL_ADD_RID,
210 RE, IM]
211QED
212
213Theorem COMPLEX_ADD_LID:
214 !z:complex. 0 + z = z
215Proof
216 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_ADD_RID]
217QED
218
219Theorem COMPLEX_ADD_RINV:
220 !z:complex. z + -z = 0
221Proof
222 REWRITE_TAC [complex_of_num, complex_of_real, complex_add, complex_neg,
223 REAL_ADD_RINV, RE, IM]
224QED
225
226Theorem COMPLEX_ADD_LINV:
227 !z:complex. -z + z = 0
228Proof
229 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_ADD_RINV]
230QED
231
232Theorem COMPLEX_MUL_COMM:
233 !z:complex w:complex. z * w = w * z
234Proof
235 REPEAT GEN_TAC THEN REWRITE_TAC [complex_mul,RE,IM] THEN
236 PROVE_TAC[REAL_MUL_COMM,REAL_ADD_COMM]
237QED
238
239Theorem COMPLEX_MUL_ASSOC:
240 !z:complex w:complex v:complex. z * (w * v) = z * w * v
241Proof
242 REPEAT GEN_TAC THEN
243 REWRITE_TAC [complex_mul, RE, IM, REAL_SUB_LDISTRIB, REAL_ADD_LDISTRIB,
244 REAL_SUB_RDISTRIB, REAL_ADD_RDISTRIB, REAL_MUL_ASSOC] THEN
245 REWRITE_TAC [real_sub, REAL_NEG_ADD] THEN RW_TAC std_ss[] THEN
246 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))
247QED
248
249Theorem COMPLEX_MUL_RID:
250 !z:complex. z * 1 = z
251Proof
252 REPEAT GEN_TAC THEN
253 REWRITE_TAC [complex_of_num, complex_of_real, complex_mul, REAL_MUL_RZERO,
254 REAL_MUL_RID, REAL_SUB_RZERO, REAL_ADD_LID,RE,IM]
255QED
256
257Theorem COMPLEX_MUL_LID:
258 !z:complex. 1 * z = z
259Proof
260 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_MUL_RID]
261QED
262
263Theorem COMPLEX_MUL_RINV:
264 !z:complex. ~(z = 0) ==> (z * inv z = 1)
265Proof
266 REWRITE_TAC [complex_of_num, complex_of_real, COMPLEX_0_THM, complex_inv,
267 complex_mul, RE, IM, POW_2] THEN
268 RW_TAC std_ss[] THEN
269 `1 = (FST z * FST z + SND z * SND z) / (FST z * FST z + SND z * SND z)`
270 by RW_TAC real_ss[REAL_DIV_REFL] THEN
271 ASM_REWRITE_TAC[] THEN REWRITE_TAC [real_div] THEN REAL_ARITH_TAC
272QED
273
274Theorem COMPLEX_MUL_LINV:
275 !z:complex. ~(z = 0) ==> (inv z * z = 1)
276Proof
277 PROVE_TAC[COMPLEX_MUL_COMM,COMPLEX_MUL_RINV]
278QED
279
280Theorem COMPLEX_ADD_LDISTRIB:
281 !z:complex w:complex v:complex. z * (w + v) = z * w + z * v
282Proof
283 REWRITE_TAC [complex_mul,complex_add,RE,IM,REAL_ADD_LDISTRIB] THEN
284 REWRITE_TAC [real_sub, REAL_NEG_ADD] THEN RW_TAC std_ss[] THEN
285 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))
286QED
287
288Theorem COMPLEX_ADD_RDISTRIB:
289 !z:complex w:complex v:complex. (z + w) * v = z * v + w * v
290Proof
291 PROVE_TAC [COMPLEX_MUL_COMM,COMPLEX_ADD_LDISTRIB]
292QED
293
294Theorem COMPLEX_EQ_LADD:
295 !z:complex w:complex v:complex. (z + w = z + v) = (w = v)
296Proof
297 REWRITE_TAC[complex_add, PAIR_EQ, REAL_EQ_LADD, GSYM COMPLEX_RE_IM_EQ]
298QED
299
300Theorem COMPLEX_EQ_RADD:
301 !z:complex w:complex v:complex. (z + v = w + v) = (z = w)
302Proof
303 ONCE_REWRITE_TAC [COMPLEX_ADD_COMM] THEN REWRITE_TAC [COMPLEX_EQ_LADD]
304QED
305
306Theorem COMPLEX_ADD_RID_UNIQ:
307 !z:complex w:complex. (z + w = z) = (w = 0)
308Proof
309 REWRITE_TAC [complex_of_num, complex_of_real, complex_add, COMPLEX_RE_IM_EQ,
310 RE, IM, REAL_ADD_RID_UNIQ]
311QED
312
313Theorem COMPLEX_ADD_LID_UNIQ:
314 !z:complex w:complex. (z + w = w) = (z = 0)
315Proof
316 ONCE_REWRITE_TAC [COMPLEX_ADD_COMM] THEN
317 REWRITE_TAC [COMPLEX_ADD_RID_UNIQ]
318QED
319
320Theorem COMPLEX_NEGNEG:
321 !z:complex. --z = z
322Proof
323 REWRITE_TAC [complex_neg, RE, IM, REAL_NEGNEG]
324QED
325
326Theorem COMPLEX_NEG_EQ:
327 !z:complex w:complex. (-z = w) = (z = -w)
328Proof
329 REWRITE_TAC [complex_neg, COMPLEX_RE_IM_EQ, RE, IM, REAL_NEG_EQ]
330QED
331
332Theorem COMPLEX_EQ_NEG:
333 !z:complex w:complex. (-z = -w) = (z = w)
334Proof
335 REWRITE_TAC [COMPLEX_NEG_EQ, COMPLEX_NEGNEG]
336QED
337
338Theorem COMPLEX_RNEG_UNIQ:
339 !z:complex w:complex. (z + w = 0) = (w = -z)
340Proof
341 REWRITE_TAC [complex_of_num, complex_of_real, GSYM COMPLEX_ADD_RINV] THEN
342 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_EQ_LADD]
343QED
344
345Theorem COMPLEX_LNEG_UNIQ:
346 !z:complex w:complex. (z + w = 0) = (z = -w)
347Proof
348 PROVE_TAC[COMPLEX_RNEG_UNIQ,COMPLEX_NEG_EQ]
349QED
350
351Theorem COMPLEX_NEG_ADD:
352 !z:complex w:complex. -(z + w) = -z + -w
353Proof
354 REWRITE_TAC[complex_neg,complex_add ,RE,IM, REAL_NEG_ADD]
355QED
356
357Theorem COMPLEX_MUL_RZERO:
358 !z:complex. z * 0 = 0
359Proof
360 REWRITE_TAC [complex_of_num, complex_of_real, complex_mul, REAL_MUL_RZERO,
361 REAL_ADD_RID, REAL_SUB_RZERO, RE,IM]
362QED
363
364Theorem COMPLEX_MUL_LZERO:
365 !z:complex. 0 * z = 0
366Proof
367 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_MUL_RZERO]
368QED
369
370Theorem COMPLEX_NEG_LMUL:
371 !z:complex w:complex. -(z * w) = -z * w
372Proof
373 REWRITE_TAC [complex_neg, complex_mul, RE,IM, real_sub, REAL_NEG_ADD,
374 REAL_NEG_LMUL]
375QED
376
377Theorem COMPLEX_NEG_RMUL:
378 !z:complex w:complex. -(z * w) = z * -w
379Proof
380 PROVE_TAC [COMPLEX_NEG_LMUL, COMPLEX_MUL_COMM]
381QED
382
383Theorem COMPLEX_NEG_MUL2:
384 !z:complex w:complex. -z * -w = z * w
385Proof
386 REWRITE_TAC [GSYM COMPLEX_NEG_LMUL, GSYM COMPLEX_NEG_RMUL, COMPLEX_NEGNEG]
387QED
388
389Theorem COMPLEX_ENTIRE:
390 !z:complex w:complex.
391 (z * w = 0) = (z = 0) \/ (w = 0)
392Proof
393 REWRITE_TAC[complex_of_num, complex_of_real, COMPLEX_0_THM, complex_mul,
394 RE,IM,COMPLEX_LEMMA1,REAL_ENTIRE]
395QED
396
397Theorem COMPLEX_NEG_0:
398 -0 = 0
399Proof
400 REWRITE_TAC [complex_of_num, complex_of_real, complex_neg, RE, IM,
401 REAL_NEG_0]
402QED
403
404Theorem COMPLEX_NEG_EQ0:
405 !z:complex. (-z = 0) = (z = 0)
406Proof
407 REWRITE_TAC[COMPLEX_NEG_EQ,COMPLEX_NEG_0]
408QED
409
410Theorem COMPLEX_SUB_REFL:
411 !z:complex. z - z = 0
412Proof
413 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_ADD_RINV]
414QED
415
416Theorem COMPLEX_SUB_RZERO:
417 !z:complex. z - 0 = z
418Proof
419 REWRITE_TAC [complex_sub, COMPLEX_NEG_0, COMPLEX_ADD_RID]
420QED
421
422Theorem COMPLEX_SUB_LZERO:
423 !z:complex. 0 - z = -z
424Proof
425 REWRITE_TAC [complex_sub, COMPLEX_ADD_LID]
426QED
427
428Theorem COMPLEX_SUB_LNEG:
429 !z:complex w:complex. -z - w = -(z + w)
430Proof
431 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_NEG_ADD]
432QED
433
434Theorem COMPLEX_SUB_NEG2:
435 !z:complex w:complex. -z - -w = w - z
436Proof
437 REWRITE_TAC[complex_sub, COMPLEX_NEGNEG] THEN PROVE_TAC [COMPLEX_ADD_COMM]
438QED
439
440Theorem COMPLEX_NEG_SUB:
441 !z:complex w:complex. -(z - w) = w - z
442Proof
443 REWRITE_TAC[complex_sub, COMPLEX_NEG_ADD, COMPLEX_NEGNEG] THEN
444 PROVE_TAC [COMPLEX_ADD_COMM]
445QED
446
447Theorem COMPLEX_SUB_RNEG:
448 !z:complex w:complex. z - -w = z + w
449Proof
450 REPEAT GEN_TAC THEN REWRITE_TAC [complex_sub, COMPLEX_NEGNEG]
451QED
452
453Theorem COMPLEX_SUB_ADD:
454 !z:complex w:complex. (z - w) + w = z
455Proof
456 REWRITE_TAC [complex_sub, GSYM COMPLEX_ADD_ASSOC, COMPLEX_ADD_LINV,
457 COMPLEX_ADD_RID]
458QED
459
460Theorem COMPLEX_SUB_ADD2:
461 !z:complex w:complex. w + (z - w) = z
462Proof
463 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN
464 MATCH_ACCEPT_TAC COMPLEX_SUB_ADD
465QED
466
467Theorem COMPLEX_ADD_SUB:
468 !z:complex w:complex. (z + w) - z = w
469Proof
470 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN
471 REWRITE_TAC[complex_sub, GSYM COMPLEX_ADD_ASSOC, COMPLEX_ADD_RINV,
472 COMPLEX_ADD_RID]
473QED
474
475Theorem COMPLEX_SUB_SUB:
476 !z:complex w:complex. (z - w) - z = -w
477Proof
478 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub] THEN
479 REWRITE_TAC[GSYM COMPLEX_ADD_ASSOC] THEN
480 ONCE_REWRITE_TAC[COMPLEX_ADD_COMM] THEN
481 REWRITE_TAC[GSYM COMPLEX_ADD_ASSOC] THEN
482 REWRITE_TAC[COMPLEX_ADD_LINV, COMPLEX_ADD_RID]
483QED
484
485Theorem COMPLEX_SUB_SUB2:
486 !z:complex w:complex. z - (z - w) = w
487Proof
488 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM COMPLEX_NEGNEG] THEN
489 AP_TERM_TAC THEN REWRITE_TAC[COMPLEX_NEG_SUB, COMPLEX_SUB_SUB]
490QED
491
492Theorem COMPLEX_ADD_SUB2:
493 !z:complex w:complex. z - (z + w) = -w
494Proof
495 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM COMPLEX_NEG_SUB] THEN
496 AP_TERM_TAC THEN REWRITE_TAC[COMPLEX_ADD_SUB]
497QED
498
499Theorem COMPLEX_ADD2_SUB2:
500 !z:complex w:complex u:complex v:complex.
501(z + w) - (u + v) = (z - u) + (w - v)
502Proof
503 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub, COMPLEX_NEG_ADD] THEN
504 CONV_TAC(AC_CONV(COMPLEX_ADD_ASSOC,COMPLEX_ADD_COMM))
505QED
506
507Theorem COMPLEX_SUB_TRIANGLE:
508 !z:complex w:complex v:complex. (z - w) + (w - v) = z - v
509Proof
510 REPEAT GEN_TAC THEN REWRITE_TAC[complex_sub] THEN
511 ONCE_REWRITE_TAC[AC(COMPLEX_ADD_ASSOC,COMPLEX_ADD_COMM)
512 ``(a + b) + (c + d) = (b + c) + (a + d)``] THEN
513 REWRITE_TAC[COMPLEX_ADD_LINV, COMPLEX_ADD_LID]
514QED
515
516Theorem COMPLEX_SUB_0:
517 !z:complex w:complex. (z - w = 0) = (z = w)
518Proof
519 REWRITE_TAC [complex_sub, COMPLEX_LNEG_UNIQ , COMPLEX_NEGNEG]
520QED
521
522Theorem COMPLEX_EQ_SUB_LADD:
523 !z:complex w:complex v:complex. (z = w - v) = (z + v = w)
524Proof
525 REPEAT GEN_TAC THEN
526 Q.SPECL_THEN [`z`, `w-v`, `v`] (SUBST1_TAC o SYM) COMPLEX_EQ_RADD THEN
527 REWRITE_TAC[COMPLEX_SUB_ADD]
528QED
529
530Theorem COMPLEX_EQ_SUB_RADD:
531 !z:complex w:complex v:complex. (z - w = v) = (z = v + w)
532Proof
533 REPEAT GEN_TAC THEN
534 CONV_TAC(SUB_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
535 MATCH_ACCEPT_TAC COMPLEX_EQ_SUB_LADD
536QED
537
538Theorem COMPLEX_MUL_RNEG:
539 ! z:complex w:complex. z * -w = -(z * w)
540Proof
541 REWRITE_TAC[COMPLEX_NEG_RMUL]
542QED
543
544Theorem COMPLEX_MUL_LNEG:
545 ! z:complex w:complex. -z * w = -(z * w)
546Proof
547 REWRITE_TAC[COMPLEX_NEG_LMUL]
548QED
549
550Theorem COMPLEX_SUB_LDISTRIB:
551 !z:complex w:complex v:complex. z * (w - v) = z * w - z * v
552Proof
553 REWRITE_TAC [complex_sub, COMPLEX_ADD_LDISTRIB, GSYM COMPLEX_NEG_RMUL]
554QED
555
556Theorem COMPLEX_SUB_RDISTRIB:
557 !z:complex w:complex v:complex. (z - w) * v = z * v - w * v
558Proof
559 PROVE_TAC [COMPLEX_MUL_COMM,COMPLEX_SUB_LDISTRIB]
560QED
561
562Theorem COMPLEX_DIFFSQ:
563 !z:complex w:complex. (z + w) * (z - w) = z * z - w * w
564Proof
565 REWRITE_TAC[COMPLEX_ADD_RDISTRIB, COMPLEX_SUB_LDISTRIB, complex_sub,
566 GSYM COMPLEX_ADD_ASSOC, COMPLEX_EQ_LADD] THEN
567 REWRITE_TAC [COMPLEX_ADD_ASSOC, COMPLEX_ADD_LID_UNIQ] THEN
568 PROVE_TAC [COMPLEX_ADD_COMM, COMPLEX_MUL_COMM, COMPLEX_ADD_RINV]
569QED
570
571Theorem COMPLEX_EQ_LMUL:
572 !z:complex w:complex v:complex.
573 (z * w = z * v) = (z = 0) \/ (w = v)
574Proof
575 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN
576 REWRITE_TAC [GSYM COMPLEX_SUB_LDISTRIB, COMPLEX_ENTIRE, COMPLEX_SUB_RZERO]
577QED
578
579Theorem COMPLEX_EQ_RMUL:
580 !z:complex w:complex v:complex.
581 (z * v = w * v) = (v = 0) \/ (z = w)
582Proof
583 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_EQ_LMUL]
584QED
585
586Theorem COMPLEX_EQ_LMUL2:
587 !z:complex w:complex v:complex.
588 ~(z = 0) ==> ((w = v) = (z * w = z * v))
589Proof
590 REPEAT GEN_TAC THEN DISCH_TAC THEN
591 Q.SPECL_THEN [`z`, `w`, `v`] MP_TAC COMPLEX_EQ_LMUL THEN
592 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN REFL_TAC
593QED
594
595Theorem COMPLEX_EQ_RMUL_IMP:
596 !z:complex w:complex v:complex.
597 ~(z = 0) /\ (w * z = v * z)==> (w = v)
598Proof
599 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
600 ASM_REWRITE_TAC[COMPLEX_EQ_RMUL]
601QED
602
603Theorem COMPLEX_EQ_LMUL_IMP:
604 !z:complex w:complex v:complex.
605 ~(z = 0) /\ (z * w = z * v)==> (w = v)
606Proof
607 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
608 MATCH_ACCEPT_TAC COMPLEX_EQ_RMUL_IMP
609QED
610
611Theorem COMPLEX_NEG_INV:
612 !z: complex. ~(z = 0) ==> (inv (-z) = -(inv z))
613Proof
614 REWRITE_TAC [COMPLEX_0_THM,complex_inv,complex_neg,RE,IM,POW_2] THEN
615 RW_TAC real_ss[real_div]
616QED
617
618Theorem COMPLEX_INV_MUL:
619 !z:complex w:complex.
620 (z <> 0 /\ w <> 0) ==> (inv (z * w) = inv z * inv w)
621Proof
622 REWRITE_TAC [complex_inv,COMPLEX_0_THM, complex_mul, RE,IM] THEN
623 RW_TAC real_ss[real_div,COMPLEX_LEMMA1,REAL_INV_MUL] THEN REAL_ARITH_TAC
624QED
625
626Theorem COMPLEX_INVINV:
627 !z: complex. (z <> 0) ==> (inv (inv z) = z)
628Proof
629 REPEAT STRIP_TAC THEN
630 FIRST_ASSUM(MP_TAC o MATCH_MP COMPLEX_MUL_RINV) THEN
631 Q.ASM_CASES_TAC `inv z = 0` THENL[
632 ASM_REWRITE_TAC[COMPLEX_MUL_RZERO, GSYM COMPLEX_10],
633 Q.SPECL_THEN [`inv(inv z)`, `z`, `inv z`] MP_TAC COMPLEX_EQ_RMUL THEN
634 ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
635 DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC COMPLEX_MUL_LINV THEN
636 FIRST_ASSUM ACCEPT_TAC
637 ]
638QED
639
640Theorem COMPLEX_LINV_UNIQ:
641 !z:complex w:complex. (z * w = 1) ==> (z = inv w)
642Proof
643 REPEAT GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL [
644 ASM_REWRITE_TAC [COMPLEX_MUL_LZERO, GSYM COMPLEX_10],
645 DISCH_THEN(MP_TAC o AP_TERM (``$* (inv z:complex) ``)) THEN
646 REWRITE_TAC [COMPLEX_MUL_ASSOC] THEN
647 FIRST_ASSUM (fn th=> REWRITE_TAC [MATCH_MP COMPLEX_MUL_LINV th]) THEN
648 REWRITE_TAC [COMPLEX_MUL_LID, COMPLEX_MUL_RID] THEN
649 DISCH_THEN SUBST1_TAC THEN CONV_TAC SYM_CONV THEN
650 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC COMPLEX_INVINV
651 ]
652QED
653
654Theorem COMPLEX_RINV_UNIQ:
655 !z:complex w:complex. (z * w = 1) ==> (w = inv z)
656Proof
657 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
658 MATCH_ACCEPT_TAC COMPLEX_LINV_UNIQ
659QED
660
661Theorem COMPLEX_INV_0:
662 inv 0 = 0c
663Proof
664 RW_TAC real_ss [complex_of_num, complex_of_real, complex_inv, RE, IM,
665 POW_2, real_div, REAL_INV_0]
666QED
667
668Theorem COMPLEX_INV1:
669 inv 1c = 1
670Proof
671 RW_TAC real_ss [complex_of_num, complex_of_real, complex_inv, RE, IM,
672 POW_2, real_div, REAL_INV1]
673QED
674
675Theorem COMPLEX_INV_INV:
676 !z: complex. inv (inv z) = z
677Proof
678 GEN_TAC THEN Q.ASM_CASES_TAC `z = 0` THENL [
679 ASM_REWRITE_TAC [COMPLEX_INV_0],
680 MATCH_MP_TAC COMPLEX_INVINV THEN ASM_REWRITE_TAC[]
681 ]
682QED
683
684Theorem COMPLEX_INV_NEG:
685 !z: complex. inv (-z) = -inv z
686Proof
687 GEN_TAC THEN Q.ASM_CASES_TAC `z = 0` THEN
688 ASM_REWRITE_TAC [COMPLEX_INV_0, COMPLEX_NEG_0] THEN
689 MATCH_MP_TAC COMPLEX_NEG_INV THEN ASM_REWRITE_TAC[]
690QED
691
692Theorem COMPLEX_INV_EQ_0:
693 !z: complex. (inv z = 0) = (z = 0)
694Proof
695 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN
696 ASM_REWRITE_TAC[COMPLEX_INV_0] THEN
697 ONCE_REWRITE_TAC[GSYM COMPLEX_INV_INV] THEN
698 ASM_REWRITE_TAC[COMPLEX_INV_0]
699QED
700
701Theorem COMPLEX_INV_NZ:
702 !z:complex. z <> 0 ==> inv z <> 0
703Proof
704 REWRITE_TAC[COMPLEX_INV_EQ_0]
705QED
706
707Theorem COMPLEX_INV_INJ:
708 !z: complex w: complex. (inv z = inv w) = (z = w)
709Proof
710 PROVE_TAC[COMPLEX_INV_INV]
711QED
712
713Theorem COMPLEX_NEG_LDIV:
714 !z w : complex. -(z / w) = -z / w
715Proof
716 REWRITE_TAC[complex_div, COMPLEX_NEG_LMUL]
717QED
718
719Theorem COMPLEX_NEG_RDIV:
720 !z w : complex. -(z / w) = z / -w
721Proof
722 REWRITE_TAC[complex_div, COMPLEX_INV_NEG, COMPLEX_NEG_RMUL]
723QED
724
725Theorem COMPLEX_NEG_DIV2:
726 !z w : complex. -z / -w = z / w
727Proof
728 REWRITE_TAC[complex_div, COMPLEX_INV_NEG, COMPLEX_NEG_MUL2]
729QED
730
731Theorem COMPLEX_INV_1OVER:
732 !z: complex. inv z = 1 / z
733Proof
734 REWRITE_TAC[complex_div, COMPLEX_MUL_LID]
735QED
736
737Theorem COMPLEX_DIV1:
738 !z: complex. z / 1 = z
739Proof
740 REWRITE_TAC[complex_div, COMPLEX_INV1,COMPLEX_MUL_RID]
741QED
742
743Theorem COMPLEX_DIV_ADD:
744 !z w v :complex. z / v + w / v = (z + w) / v
745Proof
746 REWRITE_TAC[complex_div, GSYM COMPLEX_ADD_RDISTRIB]
747QED
748
749Theorem COMPLEX_DIV_SUB:
750 !z w v :complex. z / v - w / v = (z - w) / v
751Proof
752 REWRITE_TAC[complex_div, GSYM COMPLEX_SUB_RDISTRIB]
753QED
754
755Theorem COMPLEX_DIV_RMUL_CANCEL:
756 !v:complex z w. ~(v = 0) ==> ((z * v) / (w * v) = z / w)
757Proof
758 RW_TAC bool_ss [complex_div] THEN
759 Cases_on `w = 0` THEN
760 RW_TAC bool_ss [COMPLEX_MUL_LZERO, COMPLEX_INV_0, COMPLEX_INV_MUL,
761 COMPLEX_MUL_RZERO, COMPLEX_EQ_LMUL,
762 GSYM COMPLEX_MUL_ASSOC] THEN
763 DISJ2_TAC THEN ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN
764 ONCE_REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN
765 RW_TAC bool_ss [COMPLEX_MUL_LINV, COMPLEX_MUL_RID]
766QED
767
768Theorem COMPLEX_DIV_LMUL_CANCEL:
769 !v:complex z w. ~(v = 0) ==> ((v * z) / (v * w) = z / w)
770Proof
771 METIS_TAC [COMPLEX_DIV_RMUL_CANCEL, COMPLEX_MUL_COMM]
772QED
773
774Theorem COMPLEX_DIV_DENOM_CANCEL:
775 !z:complex w v. ~(z = 0) ==> ((w / z) / (v / z) = w / v)
776Proof
777 RW_TAC bool_ss [complex_div] THEN
778 Cases_on `w = 0` THEN1 RW_TAC bool_ss [COMPLEX_MUL_LZERO] THEN
779 Cases_on `v = 0`
780 THEN1 RW_TAC bool_ss [COMPLEX_INV_0, COMPLEX_MUL_RZERO,
781 COMPLEX_MUL_LZERO] THEN
782 RW_TAC bool_ss [COMPLEX_INV_MUL, COMPLEX_INV_EQ_0,
783 COMPLEX_INVINV] THEN
784 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN
785 RW_TAC bool_ss [COMPLEX_EQ_LMUL] THEN
786 ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN
787 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN
788 RW_TAC bool_ss [COMPLEX_MUL_RINV, COMPLEX_MUL_RID]
789QED
790
791Theorem COMPLEX_DIV_INNER_CANCEL:
792 !z:complex w v. ~(z = 0) ==> ((w / z) * (z / v) = w / v)
793Proof
794 RW_TAC bool_ss [complex_div] THEN
795 Cases_on `w = 0` THEN1 RW_TAC bool_ss [COMPLEX_MUL_LZERO] THEN
796 REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC] THEN
797 RW_TAC bool_ss [COMPLEX_EQ_LMUL] THEN
798 REWRITE_TAC[COMPLEX_MUL_ASSOC] THEN
799 RW_TAC bool_ss [COMPLEX_MUL_LINV, COMPLEX_MUL_LID]
800QED
801
802Theorem COMPLEX_DIV_OUTER_CANCEL:
803 !z:complex w v. ~(z = 0) ==> ((z /w) * (v / z) = v / w)
804Proof
805 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
806 REWRITE_TAC[COMPLEX_DIV_INNER_CANCEL]
807QED
808
809Theorem COMPLEX_DIV_MUL2:
810 !z:complex w.
811 ~(z = 0) /\ ~(w = 0) ==> !v. v / w = (z * v) / (z * w)
812Proof
813 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
814 RW_TAC bool_ss [COMPLEX_DIV_LMUL_CANCEL]
815QED
816
817Theorem COMPLEX_ADD_RAT:
818 !z:complex w u v.
819 ~(w = 0) /\ ~(v = 0) ==>
820 (z / w + u / v = (z * v + w * u) / (w * v))
821Proof
822 RW_TAC bool_ss [GSYM COMPLEX_DIV_ADD, COMPLEX_DIV_RMUL_CANCEL,
823 COMPLEX_DIV_LMUL_CANCEL]
824QED
825
826Theorem COMPLEX_SUB_RAT:
827 !z:complex w u v.
828 ~(w = 0) /\ ~(v = 0) ==>
829 (z / w - u / v = (z * v - w * u) / (w * v))
830Proof
831 RW_TAC bool_ss [complex_sub, COMPLEX_NEG_LDIV]
832 THEN METIS_TAC [COMPLEX_ADD_RAT, COMPLEX_NEG_LMUL, COMPLEX_NEG_RMUL]
833QED
834
835Theorem COMPLEX_DIV_LZERO:
836 !z:complex. 0 / z = 0
837Proof
838 REWRITE_TAC[complex_div, COMPLEX_MUL_LZERO]
839QED
840
841Theorem COMPLEX_DIV_REFL:
842 !z:complex. ~(z = 0) ==> (z / z = 1)
843Proof
844 REWRITE_TAC[complex_div, COMPLEX_MUL_RINV]
845QED
846
847Theorem COMPLEX_SUB_INV2:
848 !z:complex w.
849 (z <> 0 /\ w <> 0) ==>
850 (inv z - inv w = (w - z) / (z * w))
851Proof
852 REWRITE_TAC[complex_div] THEN REPEAT STRIP_TAC THEN
853 IMP_RES_TAC COMPLEX_INV_MUL THEN ASM_REWRITE_TAC[] THEN
854 REWRITE_TAC [COMPLEX_SUB_RDISTRIB, COMPLEX_MUL_ASSOC] THEN
855 IMP_RES_TAC COMPLEX_MUL_RINV THEN ASM_REWRITE_TAC[] THEN
856 REWRITE_TAC [COMPLEX_MUL_LID, GSYM COMPLEX_MUL_ASSOC] THEN
857 ONCE_REWRITE_TAC [COMPLEX_MUL_COMM] THEN
858 REWRITE_TAC [GSYM COMPLEX_MUL_ASSOC] THEN
859 FIRST_ASSUM (fn th=> REWRITE_TAC [MATCH_MP COMPLEX_MUL_LINV th]) THEN
860 REWRITE_TAC[COMPLEX_MUL_RID]
861QED
862
863Theorem COMPLEX_EQ_RDIV_EQ:
864 !z:complex w:complex v:complex.
865 ~(v = 0) ==> ((z = w / v) = (z * v= w))
866Proof
867 REPEAT GEN_TAC THEN REWRITE_TAC[complex_div] THEN
868 DISCH_TAC THEN EQ_TAC THENL [
869 DISCH_THEN(MP_TAC o AP_TERM ``$* (v:complex)``) THEN
870 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
871 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC,
872 COMPLEX_MUL_LINV, COMPLEX_MUL_RID],
873 DISCH_THEN(MP_TAC o AP_TERM ``$* (inv v:complex)``) THEN
874 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
875 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC,
876 COMPLEX_MUL_RINV, COMPLEX_MUL_RID]
877 ]
878QED
879
880Theorem COMPLEX_EQ_LDIV_EQ:
881 !z:complex w:complex v:complex.
882 ~(v = 0) ==> ((z / v = w) = (z = w * v))
883Proof
884 REPEAT GEN_TAC THEN REWRITE_TAC[complex_div] THEN
885 DISCH_TAC THEN EQ_TAC THENL [
886 DISCH_THEN(MP_TAC o AP_TERM (``$* (v:complex)``)) THEN
887 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
888 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC,
889 COMPLEX_MUL_LINV, COMPLEX_MUL_RID],
890 DISCH_THEN(MP_TAC o AP_TERM (``$* (inv v:complex)``)) THEN
891 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
892 RW_TAC bool_ss [COMPLEX_MUL_COMM, GSYM COMPLEX_MUL_ASSOC, COMPLEX_MUL_RINV,
893 COMPLEX_MUL_RID]
894 ]
895QED
896
897(* ------------------------------------------------------------------ *)
898(* Homomorphic embedding properties for complex_of_real mapping. *)
899(* ------------------------------------------------------------------ *)
900
901Theorem COMPLEX_OF_REAL_EQ:
902 !x:real y:real.
903 (complex_of_real x = complex_of_real y) = (x = y)
904Proof
905 REWRITE_TAC[complex_of_real, COMPLEX_RE_IM_EQ, RE, IM]
906QED
907
908Theorem COMPLEX_OF_REAL_ADD:
909 !x:real y:real.
910 complex_of_real x + complex_of_real y = complex_of_real (x + y)
911Proof
912 REWRITE_TAC [complex_of_real,complex_add,RE,IM,REAL_ADD_RID]
913QED
914
915Theorem COMPLEX_OF_REAL_NEG:
916 !x:real. -complex_of_real x = complex_of_real (-x)
917Proof
918 REWRITE_TAC [complex_of_real,complex_neg,RE,IM,REAL_NEG_0]
919QED
920
921Theorem COMPLEX_OF_REAL_MUL:
922 !x:real y:real.
923 complex_of_real x * complex_of_real y = complex_of_real (x * y)
924Proof
925 REWRITE_TAC [complex_of_real, complex_mul, RE, IM, REAL_MUL_RZERO,
926 REAL_MUL_LZERO, REAL_SUB_RZERO, REAL_ADD_RID]
927QED
928
929Theorem COMPLEX_OF_REAL_INV:
930 !x:real. inv (complex_of_real x) = complex_of_real (inv x)
931Proof
932 GEN_TAC THEN ASM_CASES_TAC (``x = 0r``) THEN
933 RW_TAC real_ss [complex_inv, complex_of_real, REAL_INV_0, RE, IM, POW_2,
934 REAL_MUL_RZERO, REAL_ADD_RID, real_div, REAL_MUL_LZERO,
935 REAL_NEG_0, REAL_INV_MUL, REAL_MUL_ASSOC, REAL_MUL_RINV,
936 REAL_MUL_LID]
937QED
938
939Theorem COMPLEX_OF_REAL_SUB:
940 !x:real y:real.
941 complex_of_real x - complex_of_real y = complex_of_real (x - y)
942Proof
943 REWRITE_TAC [real_sub, COMPLEX_OF_REAL_ADD, COMPLEX_OF_REAL_NEG,
944 complex_sub]
945QED
946
947Theorem COMPLEX_OF_REAL_DIV:
948 !x:real y:real.
949 complex_of_real x / complex_of_real y = complex_of_real (x / y)
950Proof
951 REWRITE_TAC [real_div, COMPLEX_OF_REAL_MUL, COMPLEX_OF_REAL_INV,
952 complex_div]
953QED
954
955(* ------------------------------------------------------------------ *)
956(* Homomorphic embedding properties for complex_of_num mapping. *)
957(* ------------------------------------------------------------------ *)
958
959Theorem COMPLEX_OF_NUM_EQ:
960 !m:num n:num. (complex_of_num m = complex_of_num n) = (m = n)
961Proof
962 REWRITE_TAC[complex_of_num, COMPLEX_OF_REAL_EQ,REAL_OF_NUM_EQ]
963QED
964
965Theorem COMPLEX_OF_NUM_ADD:
966 !m:num n:num.
967 complex_of_num m + complex_of_num n = complex_of_num (m + n)
968Proof
969 REWRITE_TAC [complex_of_num, REAL_OF_NUM_ADD, COMPLEX_OF_REAL_ADD]
970QED
971
972Theorem COMPLEX_OF_NUM_MUL:
973 !m:num n:num.
974 complex_of_num m * complex_of_num n = complex_of_num (m * n)
975Proof
976 REWRITE_TAC [complex_of_num, REAL_OF_NUM_MUL, COMPLEX_OF_REAL_MUL]
977QED
978
979(* ------------------------------------------------------------------ *)
980(* A tactical to automate very simple algebraic equivalences. *)
981(* ------------------------------------------------------------------ *)
982
983val SIMPLE_COMPLEX_ARITH_TAC =
984 REWRITE_TAC[COMPLEX_RE_IM_EQ, RE, IM, complex_of_real, complex_add,
985 complex_neg, complex_sub, complex_mul] THEN REAL_ARITH_TAC;
986
987(*--------------------------------------------------------------------*)
988(* Define the left scalar multiplication *)
989(* and right scalar multiplication *)
990(*--------------------------------------------------------------------*)
991
992Definition complex_scalar_lmul[nocompute]:
993complex_scalar_lmul (k:real) (z:complex) = (k * RE z,k * IM z)
994End
995
996Definition complex_scalar_rmul[nocompute]:
997complex_scalar_rmul (z:complex) (k:real) = (RE z * k,IM z * k)
998End
999
1000Overload "*" = Term`$complex_scalar_lmul`
1001Overload "*" = Term`$complex_scalar_rmul`
1002
1003(*--------------------------------------------------------------------*)
1004(* The properities of R-module *)
1005(*--------------------------------------------------------------------*)
1006
1007
1008Theorem COMPLEX_SCALAR_LMUL:
1009 !k:real l:real z:complex. k * (l * z) = k * l * z
1010Proof
1011 REWRITE_TAC[complex_scalar_lmul, RE,IM,REAL_MUL_ASSOC]
1012QED
1013
1014Theorem COMPLEX_SCALAR_LMUL_NEG:
1015 !k:real z:complex. -(k * z) = -k * z
1016Proof
1017 REWRITE_TAC[complex_scalar_lmul,complex_neg,RE,IM,REAL_NEG_LMUL]
1018QED
1019
1020Theorem COMPLEX_NEG_SCALAR_LMUL:
1021 !k:real z:complex. k * (-z) = -k * z
1022Proof
1023 REWRITE_TAC [complex_neg, complex_scalar_lmul, RE, IM, REAL_MUL_LNEG,
1024 REAL_MUL_RNEG]
1025QED
1026
1027Theorem COMPLEX_SCALAR_LMUL_ADD:
1028 !k:real l:real z:complex. (k + l) * z = k * z + l * z
1029Proof
1030 REWRITE_TAC[complex_add,complex_scalar_lmul,RE,IM,GSYM REAL_ADD_RDISTRIB]
1031QED
1032
1033Theorem COMPLEX_SCALAR_LMUL_SUB:
1034 !k:real l:real z:complex. (k - l) * z = k * z - l * z
1035Proof
1036 REWRITE_TAC [complex_sub, COMPLEX_SCALAR_LMUL_NEG,
1037 GSYM COMPLEX_SCALAR_LMUL_ADD, real_sub]
1038QED
1039
1040Theorem COMPLEX_ADD_SCALAR_LMUL:
1041 !k:real z:complex w:complex. k * (z + w) = k * z + k * w
1042Proof
1043 REWRITE_TAC[complex_add, complex_scalar_lmul, RE, IM,
1044 GSYM REAL_ADD_LDISTRIB]
1045QED
1046
1047Theorem COMPLEX_SUB_SCALAR_LMUL:
1048 !k:real z:complex w:complex. k * (z - w) = k * z - k * w
1049Proof
1050 REWRITE_TAC[complex_sub, COMPLEX_ADD_SCALAR_LMUL, COMPLEX_NEG_SCALAR_LMUL,
1051 COMPLEX_SCALAR_LMUL_NEG]
1052QED
1053
1054Theorem COMPLEX_MUL_SCALAR_LMUL2:
1055 !k:real l:real z:complex w:complex.
1056 (k * z) * (l * w) = (k * l) * (z * w)
1057Proof
1058 REWRITE_TAC [complex_mul, complex_scalar_lmul, RE, IM, PAIR_EQ] THEN
1059 REAL_ARITH_TAC
1060QED
1061
1062Theorem COMPLEX_LMUL_SCALAR_LMUL:
1063 !k:real z:complex w:complex. (k * z) * w = k * (z * w)
1064Proof
1065 REWRITE_TAC [complex_mul, complex_scalar_lmul, RE, IM, PAIR_EQ] THEN
1066 REAL_ARITH_TAC
1067QED
1068
1069Theorem COMPLEX_RMUL_SCALAR_LMUL:
1070 !k:real z:complex w:complex. z * (k * w) = k * (z * w)
1071Proof
1072 PROVE_TAC[COMPLEX_MUL_COMM, COMPLEX_LMUL_SCALAR_LMUL]
1073QED
1074
1075Theorem COMPLEX_SCALAR_LMUL_ZERO:
1076 !z:complex. 0r * z = 0
1077Proof
1078 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_lmul,
1079 REAL_MUL_LZERO]
1080QED
1081
1082Theorem COMPLEX_ZERO_SCALAR_LMUL:
1083 !k:real. k * 0c = 0
1084Proof
1085 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_lmul, RE, IM,
1086 REAL_MUL_RZERO]
1087QED
1088
1089Theorem COMPLEX_SCALAR_LMUL_ONE:
1090 !z:complex. 1r * z = z
1091Proof
1092 REWRITE_TAC[complex_scalar_lmul, REAL_MUL_LID,RE,IM]
1093QED
1094
1095Theorem COMPLEX_SCALAR_LMUL_NEG1:
1096 !z:complex. -1r * z = -z
1097Proof
1098 GEN_TAC THEN REWRITE_TAC[GSYM COMPLEX_SCALAR_LMUL_NEG] THEN
1099 REWRITE_TAC[COMPLEX_SCALAR_LMUL_ONE]
1100QED
1101
1102Theorem COMPLEX_DOUBLE:
1103 !z:complex. z + z = &2 * z
1104Proof
1105 GEN_TAC THEN REWRITE_TAC[num_CONV ``2:num``, REAL] THEN
1106 REWRITE_TAC[COMPLEX_SCALAR_LMUL_ADD, COMPLEX_SCALAR_LMUL_ONE]
1107QED
1108
1109Theorem COMPLEX_SCALAR_LMUL_ENTIRE:
1110 !k:real z:complex. (k * z = 0) = (k = 0) \/ (z = 0)
1111Proof
1112 REWRITE_TAC[COMPLEX_0_THM, complex_scalar_lmul, RE,IM, POW_2, REAL_SUMSQ,
1113 REAL_ENTIRE, GSYM LEFT_OR_OVER_AND]
1114QED
1115
1116Theorem COMPLEX_EQ_SCALAR_LMUL:
1117 !k:real z:complex w:complex. (k * z = k * w) = (k = 0) \/ (z = w)
1118Proof
1119 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN
1120 REWRITE_TAC [GSYM COMPLEX_SUB_SCALAR_LMUL, COMPLEX_SCALAR_LMUL_ENTIRE]
1121QED
1122
1123Theorem COMPLEX_SCALAR_LMUL_EQ:
1124 !k:real l:real z:complex.
1125 (k * z = l * z) = (k = l) \/ (z = 0)
1126Proof
1127 ONCE_REWRITE_TAC [GSYM COMPLEX_SUB_0] THEN
1128 REWRITE_TAC [GSYM COMPLEX_SCALAR_LMUL_SUB, COMPLEX_SCALAR_LMUL_ENTIRE,
1129 COMPLEX_SUB_RZERO, REAL_SUB_0]
1130QED
1131
1132Theorem COMPLEX_SCALAR_LMUL_EQ1:
1133 !k:real z:complex. (k * z = z) = (k = 1) \/ (z = 0)
1134Proof
1135 PROVE_TAC[COMPLEX_SCALAR_LMUL_ONE,COMPLEX_SCALAR_LMUL_EQ]
1136QED
1137
1138Theorem COMPLEX_INV_SCALAR_LMUL:
1139 !k:real z:complex.
1140 k <> 0 /\ z <> 0 ==> (inv (k * z) = inv k * inv z)
1141Proof
1142 REWRITE_TAC [COMPLEX_0_THM, complex_inv,complex_scalar_lmul,RE,IM, POW_MUL,
1143 GSYM REAL_ADD_LDISTRIB, real_div, REAL_INV_MUL] THEN
1144 REPEAT STRIP_TAC THEN
1145 `k pow 2 <> 0` by RW_TAC real_ss[POW_2, REAL_ENTIRE] THEN
1146 RW_TAC real_ss[REAL_INV_MUL] THEN
1147 `inv (k pow 2) = inv k * inv k` by RW_TAC real_ss[POW_2, REAL_INV_MUL] THEN
1148 ASM_REWRITE_TAC[REAL_MUL_ASSOC] THENL[
1149 `k * FST z * inv k * inv k = inv k * k * FST z * inv k` by REAL_ARITH_TAC,
1150 `k * SND z * inv k * inv k = inv k * k * SND z * inv k` by REAL_ARITH_TAC
1151 ] THEN
1152 ASM_REWRITE_TAC[] THEN RW_TAC real_ss[REAL_MUL_LINV,REAL_MUL_COMM]
1153QED
1154
1155Theorem COMPLEX_SCALAR_LMUL_DIV2:
1156 !k l :real z w :complex.
1157 (l <> 0 /\ w <> 0) ==> ((k * z) / (l * w) = (k / l) * (z / w))
1158Proof
1159 REWRITE_TAC [complex_div] THEN REPEAT STRIP_TAC THEN
1160 IMP_RES_TAC COMPLEX_INV_SCALAR_LMUL THEN ASM_REWRITE_TAC[] THEN
1161 REWRITE_TAC [COMPLEX_MUL_SCALAR_LMUL2, real_div]
1162QED
1163
1164Theorem COMPLEX_SCALAR_MUL_COMM:
1165 !k:real z:complex. k * z = z * k
1166Proof
1167 PROVE_TAC[complex_scalar_lmul, complex_scalar_rmul, REAL_MUL_COMM]
1168QED
1169
1170Theorem COMPLEX_SCALAR_RMUL:
1171 !k:real l:real z:complex. z * k * l = z * (k * l)
1172Proof
1173 RW_TAC bool_ss [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL,
1174 REAL_MUL_COMM]
1175QED
1176
1177Theorem COMPLEX_SCALAR_RMUL_NEG:
1178 !k:real z:complex. -(z * k) = z * -k
1179Proof
1180 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_NEG]
1181QED
1182
1183Theorem COMPLEX_NEG_SCALAR_RMUL:
1184 !k:real z:complex. (-z) * k = z * -k
1185Proof
1186 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_NEG_SCALAR_LMUL]
1187QED
1188
1189Theorem COMPLEX_SCALAR_RMUL_ADD:
1190 !k:real l:real z:complex. z * (k + l) = z * k + z * l
1191Proof
1192 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_ADD]
1193QED
1194
1195Theorem COMPLEX_RSCALAR_RMUL_SUB:
1196 !k: real l:real z:complex. z * (k - l) = z * k - z * l
1197Proof
1198 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_SUB]
1199QED
1200
1201Theorem COMPLEX_ADD_RSCALAR_RMUL:
1202 !k:real z:complex w:complex. (z + w) * k = z * k + w * k
1203Proof
1204 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_ADD_SCALAR_LMUL]
1205QED
1206
1207Theorem COMPLEX_SUB_SCALAR_RMUL:
1208 !k:real z:complex w:complex. (z - w) * k = z * k - w * k
1209Proof
1210 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SUB_SCALAR_LMUL]
1211QED
1212
1213Theorem COMPLEX_SCALAR_RMUL_ZERO:
1214 !z:complex. z * 0r = 0
1215Proof
1216 REWRITE_TAC[complex_of_num, complex_of_real, complex_scalar_rmul,
1217 REAL_MUL_RZERO]
1218QED
1219
1220Theorem COMPLEX_ZERO_SCALAR_RMUL:
1221 !k:real. 0 * k = 0
1222Proof
1223 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_ZERO_SCALAR_LMUL]
1224QED
1225
1226Theorem COMPLEX_SCALAR_RMUL_ONE:
1227 !z:complex. z * 1r = z
1228Proof
1229 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_ONE]
1230QED
1231
1232Theorem COMPLEX_SCALAR_RMUL_NEG1:
1233 !z:complex. z * -1r = -z
1234Proof
1235 REWRITE_TAC [GSYM COMPLEX_SCALAR_MUL_COMM, COMPLEX_SCALAR_LMUL_NEG1]
1236QED
1237
1238(*--------------------------------------------------------------------*)
1239(* Complex conjugate *)
1240(*--------------------------------------------------------------------*)
1241
1242Definition conj[nocompute]: conj (z:complex) = (RE z, -IM z)
1243End
1244
1245Theorem CONJ_REAL_REFL:
1246 !x:real. conj (complex_of_real x) = complex_of_real x
1247Proof
1248 REWRITE_TAC[complex_of_real,conj, RE,IM, REAL_NEG_0]
1249QED
1250
1251Theorem CONJ_NUM_REFL:
1252 !n:num. conj (complex_of_num n) = complex_of_num n
1253Proof
1254 REWRITE_TAC[complex_of_num,CONJ_REAL_REFL]
1255QED
1256
1257Theorem CONJ_ADD:
1258 !z:complex w:complex. conj (z + w) = conj z + conj w
1259Proof
1260 REWRITE_TAC [conj,complex_add,RE,IM,REAL_NEG_ADD]
1261QED
1262
1263Theorem CONJ_NEG:
1264 !z:complex. conj (-z) = -conj z
1265Proof
1266 REWRITE_TAC [complex_neg, conj,RE,IM]
1267QED
1268
1269Theorem CONJ_SUB:
1270 !z:complex w:complex. conj (z - w) = conj z - conj w
1271Proof
1272 REWRITE_TAC [complex_sub, CONJ_NEG, CONJ_ADD]
1273QED
1274
1275Theorem CONJ_MUL:
1276 !z:complex w:complex. conj (z * w) = conj z * conj w
1277Proof
1278 REWRITE_TAC [conj,complex_mul, RE,IM,REAL_NEG_ADD, REAL_NEG_MUL2,
1279 GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
1280QED
1281
1282Theorem CONJ_INV:
1283 !z: complex. conj (inv z) = inv (conj z)
1284Proof
1285 RW_TAC real_ss [conj, complex_inv, RE, IM, POW_2, real_div]
1286QED
1287
1288Theorem CONJ_DIV:
1289 !z:complex w. conj (z / w) = conj z / conj w
1290Proof
1291 REWRITE_TAC[complex_div, CONJ_MUL, CONJ_INV]
1292QED
1293
1294Theorem CONJ_SCALAR_LMUL:
1295 !k:real z:complex. conj (k * z) = k * conj z
1296Proof
1297 REWRITE_TAC [conj,complex_scalar_lmul, RE,IM,REAL_MUL_RNEG]
1298QED
1299
1300Theorem CONJ_CONJ:
1301 !z:complex. conj (conj z) = z
1302Proof
1303 REWRITE_TAC[conj, RE,IM,REAL_NEGNEG]
1304QED
1305
1306Theorem CONJ_EQ:
1307 !z:complex w:complex. (conj z = w) = (z = conj w)
1308Proof
1309 REWRITE_TAC [conj, COMPLEX_RE_IM_EQ, RE, IM, REAL_NEG_EQ]
1310QED
1311
1312Theorem CONJ_EQ2:
1313 !z:complex w:complex. (conj z = conj w) = (z = w)
1314Proof
1315 REWRITE_TAC [CONJ_EQ, CONJ_CONJ]
1316QED
1317
1318Theorem COMPLEX_MUL_RCONJ:
1319 !z:complex.
1320 z * conj z = complex_of_real ((RE z) pow 2 + (IM z) pow 2)
1321Proof
1322 REWRITE_TAC [complex_mul, conj, complex_of_real, RE, IM, REAL_MUL_RNEG,
1323 REAL_SUB_RNEG] THEN
1324 PROVE_TAC [POW_2, REAL_MUL_COMM, REAL_ADD_LINV]
1325QED
1326
1327Theorem COMPLEX_MUL_LCONJ:
1328 !z:complex.
1329 conj z * z = complex_of_real ((RE z) pow 2 + (IM z) pow 2)
1330Proof
1331 PROVE_TAC [COMPLEX_MUL_COMM, COMPLEX_MUL_RCONJ]
1332QED
1333
1334Theorem CONJ_ZERO:
1335 conj 0 = 0
1336Proof
1337 REWRITE_TAC [CONJ_NUM_REFL]
1338QED
1339
1340(*--------------------------------------------------------------------*)
1341(* Define modulus and argument principal value of complex *)
1342(*--------------------------------------------------------------------*)
1343
1344Definition modu[nocompute]:
1345 modu (z:complex) = sqrt( RE z pow 2 + IM z pow 2)
1346End
1347
1348Definition arg[nocompute]:
1349 arg z =
1350 if 0 <= IM z then acs (RE z / modu z)
1351 else -acs (RE z / modu z) + 2 * pi
1352End
1353
1354(*--------------------------------------------------------------------*)
1355(* The properities of modulus and argument principal value *)
1356(*--------------------------------------------------------------------*)
1357
1358Theorem MODU_POW2:
1359 !z:complex. modu z pow 2 = RE z pow 2 + IM z pow 2
1360Proof
1361 REWRITE_TAC[modu] THEN
1362 PROVE_TAC [REAL_LE_POW2, REAL_LE_ADD, SQRT_POW_2]
1363QED
1364
1365Theorem RE_IM_LE_MODU:
1366 !z:complex. abs (RE z) <= modu z /\ abs (IM z) <= modu z
1367Proof
1368 REWRITE_TAC [modu] THEN GEN_TAC THEN CONJ_TAC THENL
1369 [REWRITE_TAC [COMPLEX_LEMMA2],
1370 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN REWRITE_TAC [COMPLEX_LEMMA2]]
1371QED
1372
1373Theorem MODU_POS:
1374 !z:complex. 0 <= modu z
1375Proof
1376 GEN_TAC THEN REWRITE_TAC[modu] THEN MATCH_MP_TAC SQRT_POS_LE THEN
1377 MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_LE_POW2]
1378QED
1379
1380Theorem COMPLEX_MUL_RCONJ1:
1381 !z:complex. z * conj z = complex_of_real ((modu z) pow 2)
1382Proof
1383 REWRITE_TAC[COMPLEX_MUL_RCONJ, MODU_POW2]
1384QED
1385
1386Theorem COMPLEX_MUL_LCONJ1:
1387 !z:complex. conj z * z = complex_of_real ((modu z) pow 2)
1388Proof
1389 REWRITE_TAC[COMPLEX_MUL_LCONJ, MODU_POW2]
1390QED
1391
1392Theorem MODU_NEG:
1393 !z:complex. modu (-z) = modu z
1394Proof
1395 REWRITE_TAC[modu,complex_neg,RE,IM,POW_2,REAL_NEG_MUL2]
1396QED
1397
1398Theorem MODU_SUB:
1399 !z:complex w:complex. modu (z - w) = modu (w - z)
1400Proof
1401 REPEAT GEN_TAC THEN
1402 `w - z = -(z - w)` by REWRITE_TAC[COMPLEX_NEG_SUB] THEN
1403 ASM_REWRITE_TAC[] THEN REWRITE_TAC[MODU_NEG]
1404QED
1405
1406Theorem MODU_CONJ:
1407 !z:complex. modu (conj z) = modu z
1408Proof
1409 REWRITE_TAC[modu, conj,RE,IM,POW_2,REAL_NEG_MUL2]
1410QED
1411
1412Theorem MODU_MUL:
1413 !z:complex w:complex. modu (z * w) = modu z * modu w
1414Proof
1415 REWRITE_TAC [modu, complex_mul, RE, IM, COMPLEX_LEMMA1] THEN
1416 PROVE_TAC [REAL_LE_POW2, REAL_LE_ADD, SQRT_MUL]
1417QED
1418
1419Theorem MODU_0:
1420 modu 0 = 0
1421Proof
1422 REWRITE_TAC[complex_of_num,complex_of_real, modu, RE, IM, POW_2,
1423 REAL_MUL_RZERO, REAL_ADD_RID, SQRT_0]
1424QED
1425
1426Theorem MODU_1:
1427 modu 1 = 1
1428Proof
1429 REWRITE_TAC[complex_of_num,complex_of_real, modu, RE, IM, POW_2,
1430 REAL_MUL_RID, REAL_MUL_RZERO, REAL_ADD_RID, SQRT_1]
1431QED
1432
1433Theorem MODU_COMPLEX_INV:
1434 !z: complex. z <> 0 ==> (modu (inv z) = inv (modu z))
1435Proof
1436 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LINV_UNIQ THEN
1437 REWRITE_TAC[GSYM MODU_MUL] THEN
1438 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP COMPLEX_MUL_LINV th]) THEN
1439 REWRITE_TAC [MODU_1]
1440QED
1441
1442Theorem MODU_DIV:
1443 !z w : complex. (w <> 0) ==> (modu(z / w) = modu z / modu w)
1444Proof
1445 REWRITE_TAC[complex_div, MODU_MUL] THEN REPEAT STRIP_TAC THEN
1446 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP MODU_COMPLEX_INV th]) THEN
1447 REWRITE_TAC[real_div]
1448QED
1449
1450Theorem MODU_SCALAR_LMUL:
1451 !k:real z:complex. modu (k * z) = abs k * modu z
1452Proof
1453 REWRITE_TAC [modu, complex_scalar_lmul, RE, IM, POW_MUL,
1454 GSYM REAL_ADD_LDISTRIB] THEN
1455 ONCE_REWRITE_TAC [GSYM REAL_POW2_ABS] THEN
1456 PROVE_TAC[REAL_ABS_POS,REAL_LE_POW2,REAL_LE_ADD,SQRT_MUL,POW_2_SQRT]
1457QED
1458
1459Theorem MODU_REAL:
1460 !x:real. modu (complex_of_real x) = abs x
1461Proof
1462 REWRITE_TAC [complex_of_real, modu, RE, IM, POW_2, REAL_MUL_RZERO,
1463 REAL_ADD_RID] THEN
1464 REWRITE_TAC [GSYM POW_2] THEN
1465 ONCE_REWRITE_TAC [GSYM REAL_POW2_ABS] THEN GEN_TAC THEN
1466 `0 <= abs x` by PROVE_TAC [REAL_ABS_POS] THEN
1467 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP POW_2_SQRT th])
1468QED
1469
1470Theorem MODU_NUM:
1471 !n:num. modu (complex_of_num n) = &n
1472Proof
1473 REWRITE_TAC [complex_of_num, MODU_REAL, ABS_N]
1474QED
1475
1476Theorem MODU_ZERO:
1477 !z:complex. (z = 0) = (modu z = 0)
1478Proof
1479 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN
1480 ASM_REWRITE_TAC[MODU_0, COMPLEX_0_THM, GSYM MODU_POW2,
1481 num_CONV (``2:num``), POW_0]
1482QED
1483
1484Theorem MODU_NZ:
1485 !z:complex. (z <> 0) = 0 < modu z
1486Proof
1487 GEN_TAC THEN EQ_TAC THENL [
1488 REWRITE_TAC[MODU_ZERO] THEN
1489 DISCH_TAC THEN
1490 PROVE_TAC[REAL_LE_LT, MODU_POS],
1491 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
1492 DISCH_THEN SUBST1_TAC THEN
1493 REWRITE_TAC[MODU_0, REAL_LT_REFL]
1494 ]
1495QED
1496
1497Theorem MODU_CASES:
1498 !z:complex. (z = 0) \/ 0 < modu z
1499Proof
1500 GEN_TAC THEN REWRITE_TAC[GSYM MODU_NZ] THEN
1501 Cases_on `z = 0` THEN ASM_REWRITE_TAC[]
1502QED
1503
1504Theorem RE_DIV_MODU_BOUNDS:
1505 !z:complex.
1506 z <> 0 ==> (-1 <= RE z / modu z /\ RE z / modu z <= 1)
1507Proof
1508 GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL [
1509 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL [
1510 PROVE_TAC[MODU_NZ],
1511 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN
1512 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS]
1513 ],
1514 MATCH_MP_TAC REAL_LE_LDIV THEN CONJ_TAC THENL [
1515 PROVE_TAC[MODU_NZ],
1516 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN
1517 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS]
1518 ]
1519 ]
1520QED
1521
1522Theorem IM_DIV_MODU_BOUNDS:
1523 !z:complex.
1524 z <> 0 ==> (-1 <= IM z / modu z /\ IM z / modu z <= 1)
1525Proof
1526 GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THENL [
1527 MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL [
1528 PROVE_TAC[MODU_NZ],
1529 REWRITE_TAC[REAL_MUL_LNEG,REAL_MUL_LID] THEN
1530 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS]
1531 ],
1532 MATCH_MP_TAC REAL_LE_LDIV THEN CONJ_TAC THENL [
1533 PROVE_TAC[MODU_NZ],
1534 REWRITE_TAC[REAL_MUL_LID] THEN
1535 PROVE_TAC[RE_IM_LE_MODU,ABS_BOUNDS]
1536 ]
1537 ]
1538QED
1539
1540Theorem RE_DIV_MODU_ACS_BOUNDS:
1541 !z:complex.
1542 z <> 0 ==>
1543 (0 <=acs (RE z / modu z) /\ acs (RE z / modu z) <= pi)
1544Proof
1545 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ACS_BOUNDS THEN
1546 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC RE_DIV_MODU_BOUNDS
1547QED
1548
1549Theorem IM_DIV_MODU_ASN_BOUNDS:
1550 !z:complex.
1551 z <> 0 ==>
1552 (-(pi/2) <= asn (IM z / modu z) /\ asn (IM z / modu z) <= pi/2)
1553Proof
1554 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ASN_BOUNDS THEN
1555 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC IM_DIV_MODU_BOUNDS
1556QED
1557
1558Theorem RE_DIV_MODU_ACS_COS:
1559 !z:complex.
1560 z <> 0 ==> (cos ( acs (RE z / modu z)) = RE z / modu z)
1561Proof
1562 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ACS_COS THEN
1563 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC RE_DIV_MODU_BOUNDS
1564QED
1565
1566Theorem IM_DIV_MODU_ASN_SIN:
1567 !z:complex.
1568 z <> 0 ==> (sin ( asn (IM z / modu z)) = IM z / modu z)
1569Proof
1570 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC ASN_SIN THEN
1571 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC IM_DIV_MODU_BOUNDS
1572QED
1573
1574Theorem ARG_COS:
1575 !z:complex. z <> 0 ==> (cos (arg z) = RE z / modu z)
1576Proof
1577 GEN_TAC THEN DISCH_TAC THEN
1578 REWRITE_TAC[arg] THEN COND_CASES_TAC THEN
1579 REWRITE_TAC[COS_PERIODIC, COS_NEG] THEN
1580 MATCH_MP_TAC RE_DIV_MODU_ACS_COS THEN ASM_REWRITE_TAC[]
1581QED
1582
1583Theorem ARG_SIN:
1584 !z:complex. z <> 0 ==> (sin (arg z) = IM z / modu z)
1585Proof
1586 GEN_TAC THEN DISCH_TAC THEN
1587 REWRITE_TAC[arg] THEN COND_CASES_TAC THENL [
1588 Q.SUBGOAL_THEN
1589 `sin (acs (RE z / modu z)) = sqrt (1 - cos (acs (RE z / modu z)) pow 2)`
1590 ASSUME_TAC
1591 THENL [
1592 MATCH_MP_TAC SIN_COS_SQ THEN
1593 MATCH_MP_TAC RE_DIV_MODU_ACS_BOUNDS THEN
1594 ASM_REWRITE_TAC[],
1595 ASM_REWRITE_TAC[] THEN
1596 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP RE_DIV_MODU_ACS_COS th]) THEN
1597 Q.SUBGOAL_THEN `1 - (RE z / modu z) pow 2 = (IM z / modu z) pow 2 `
1598 ASSUME_TAC
1599 THENL [
1600 REWRITE_TAC[REAL_EQ_SUB_RADD, REAL_POW_DIV, REAL_DIV_ADD] THEN
1601 ONCE_REWRITE_TAC[REAL_ADD_COMM] THEN
1602 REWRITE_TAC[GSYM MODU_POW2] THEN CONV_TAC SYM_CONV THEN
1603 MATCH_MP_TAC REAL_DIV_REFL THEN
1604 ASM_REWRITE_TAC[MODU_POW2, GSYM COMPLEX_0_THM],
1605 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC POW_2_SQRT THEN
1606 MATCH_MP_TAC REAL_LE_DIV THEN ASM_REWRITE_TAC[MODU_POS]
1607 ]
1608 ],
1609 REWRITE_TAC[SIN_PERIODIC,SIN_NEG, REAL_NEG_EQ] THEN
1610 Q.SUBGOAL_THEN
1611 `sin (acs (RE z / modu z)) = sqrt (1 - cos (acs (RE z / modu z)) pow 2)`
1612 ASSUME_TAC
1613 THENL [
1614 MATCH_MP_TAC SIN_COS_SQ THEN
1615 MATCH_MP_TAC RE_DIV_MODU_ACS_BOUNDS THEN
1616 ASM_REWRITE_TAC[],
1617 ASM_REWRITE_TAC[] THEN
1618 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP RE_DIV_MODU_ACS_COS th]) THEN
1619 `1 - (RE z / modu z) pow 2 = (IM z / modu z) pow 2`
1620 by (REWRITE_TAC[REAL_EQ_SUB_RADD, REAL_POW_DIV, REAL_DIV_ADD] THEN
1621 ONCE_REWRITE_TAC[REAL_ADD_COMM] THEN
1622 REWRITE_TAC[GSYM MODU_POW2] THEN CONV_TAC SYM_CONV THEN
1623 MATCH_MP_TAC REAL_DIV_REFL THEN
1624 ASM_REWRITE_TAC[MODU_POW2, GSYM COMPLEX_0_THM]) THEN
1625 ASM_REWRITE_TAC[] THEN
1626 ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
1627 ONCE_REWRITE_TAC[GSYM ABS_NEG] THEN
1628 REWRITE_TAC[REAL_POW2_ABS] THEN
1629 MATCH_MP_TAC POW_2_SQRT THEN
1630 REWRITE_TAC[real_div, REAL_NEG_LMUL] THEN
1631 REWRITE_TAC[GSYM real_div] THEN
1632 MATCH_MP_TAC REAL_LE_DIV THEN
1633 PROVE_TAC [MODU_POS, REAL_NOT_LE, REAL_NEG_GT0, REAL_LT_IMP_LE]
1634 ]
1635 ]
1636QED
1637
1638Theorem RE_MODU_ARG:
1639 !z:complex. RE z = modu z * cos (arg z)
1640Proof
1641 GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL
1642 [ASM_REWRITE_TAC[MODU_0] THEN
1643 REWRITE_TAC[complex_of_num,complex_of_real,RE,REAL_MUL_LZERO],
1644 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP ARG_COS th]) THEN
1645 CONV_TAC SYM_CONV THEN
1646 MATCH_MP_TAC REAL_DIV_LMUL THEN
1647 ASM_REWRITE_TAC[GSYM MODU_ZERO]
1648 ]
1649QED
1650
1651Theorem IM_MODU_ARG:
1652 !z:complex. IM z = modu z * sin (arg z)
1653Proof
1654 GEN_TAC THEN ASM_CASES_TAC (``z = 0``) THENL [
1655 ASM_REWRITE_TAC[MODU_0] THEN
1656 REWRITE_TAC[complex_of_num,complex_of_real,IM,REAL_MUL_LZERO],
1657 FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP ARG_SIN th]) THEN
1658 CONV_TAC SYM_CONV THEN
1659 MATCH_MP_TAC REAL_DIV_LMUL THEN
1660 ASM_REWRITE_TAC[GSYM MODU_ZERO]
1661 ]
1662QED
1663
1664Theorem COMPLEX_TRIANGLE:
1665 !z:complex. modu z * (cos (arg z),sin (arg z)) = z
1666Proof
1667 REWRITE_TAC[complex_scalar_lmul, RE, IM, GSYM RE_MODU_ARG, GSYM IM_MODU_ARG]
1668QED
1669
1670Theorem COMPLEX_MODU_ARG_EQ:
1671 !z:complex w. (z = w) = ((modu z = modu w) /\ (arg z = arg w))
1672Proof
1673 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN
1674 ASM_REWRITE_TAC[COMPLEX_RE_IM_EQ,RE_MODU_ARG,IM_MODU_ARG]
1675QED
1676
1677Theorem MODU_UNIT:
1678 !x:real y. modu (cos x,sin x) = 1
1679Proof
1680 REWRITE_TAC [modu, RE, IM] THEN ONCE_REWRITE_TAC[REAL_ADD_COMM]
1681 THEN REWRITE_TAC[SIN_CIRCLE, SQRT_1]
1682QED
1683
1684Theorem COMPLEX_MUL_ARG:
1685 !x:real y:real.
1686 (cos x,sin x) * (cos y, sin y) = (cos (x + y),sin (x + y))
1687Proof
1688 REWRITE_TAC [complex_mul, RE, IM, SIN_ADD, COS_ADD] THEN
1689 PROVE_TAC [REAL_ADD_COMM]
1690QED
1691
1692Theorem COMPLEX_INV_ARG:
1693 !x:real. inv (cos x,sin x) = (cos (-x),sin (-x))
1694Proof
1695 REWRITE_TAC [complex_inv, RE, IM] THEN
1696 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN
1697 REWRITE_TAC[SIN_CIRCLE, real_div, REAL_INV1,REAL_MUL_RID, COS_NEG, SIN_NEG]
1698QED
1699
1700Theorem COMPLEX_DIV_ARG:
1701 !x:real y.
1702 (cos x,sin x) / (cos y, sin y) = (cos(x - y),sin(x - y))
1703Proof
1704 REWRITE_TAC[complex_div,COMPLEX_INV_ARG,COMPLEX_MUL_ARG,real_sub]
1705QED
1706
1707(*--------------------------------------------------------------------*)
1708(* The operation of nature numbers power of complex numbers *)
1709(*--------------------------------------------------------------------*)
1710
1711Definition complex_pow:
1712 (complex_pow (z:complex) 0 = 1) /\
1713 (complex_pow (z:complex) (SUC n) = z * (complex_pow z n))
1714End
1715
1716Overload pow = Term`$complex_pow`
1717
1718Theorem COMPLEX_POW_0:
1719 !n:num. 0 pow (SUC n) = 0
1720Proof
1721 INDUCT_TAC THEN REWRITE_TAC[complex_pow, COMPLEX_MUL_LZERO]
1722QED
1723
1724Theorem COMPLEX_POW_NZ:
1725 !z:complex n:num. (z <> 0) ==> (z pow n <> 0)
1726Proof
1727 REPEAT GEN_TAC THEN DISCH_TAC THEN
1728 SPEC_TAC((``n:num``),(``n:num``)) THEN INDUCT_TAC THEN
1729 ASM_REWRITE_TAC[complex_pow, COMPLEX_10, COMPLEX_ENTIRE]
1730QED
1731
1732Theorem COMPLEX_POWINV:
1733 !z:complex.
1734 ~(z = 0) ==> !n:num. (inv(z pow n) = (inv z) pow n)
1735Proof
1736 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN
1737 REWRITE_TAC[complex_pow, COMPLEX_INV1] THEN
1738 MP_TAC(SPECL [(``z:complex``), (``z pow n``)] COMPLEX_INV_MUL) THEN
1739 ASM_REWRITE_TAC[] THEN
1740 SUBGOAL_THEN (``~(z pow n = 0)``) ASSUME_TAC THENL
1741 [MATCH_MP_TAC COMPLEX_POW_NZ THEN ASM_REWRITE_TAC[], ALL_TAC]
1742 THEN ASM_REWRITE_TAC[]
1743QED
1744
1745Theorem MODU_COMPLEX_POW:
1746 !z:complex n:num. modu (z pow n) = modu z pow n
1747Proof
1748 GEN_TAC THEN INDUCT_TAC THEN
1749 ASM_REWRITE_TAC[complex_pow,pow, MODU_1, MODU_MUL]
1750QED
1751
1752Theorem COMPLEX_POW_ADD:
1753 !z:complex m:num n. z pow (m + n) = (z pow m) * (z pow n)
1754Proof
1755 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1756 ASM_REWRITE_TAC[complex_pow, ADD_CLAUSES, COMPLEX_MUL_RID] THEN
1757 CONV_TAC(AC_CONV(COMPLEX_MUL_ASSOC,COMPLEX_MUL_COMM))
1758QED
1759
1760Theorem COMPLEX_POW_1:
1761 !z:complex. z pow 1 = z
1762Proof
1763 GEN_TAC THEN REWRITE_TAC[num_CONV (``1:num``)] THEN
1764 REWRITE_TAC[complex_pow, COMPLEX_MUL_RID]
1765QED
1766
1767Theorem COMPLEX_POW_2:
1768 !z:complex. z pow 2 = z * z
1769Proof
1770 GEN_TAC THEN REWRITE_TAC[num_CONV ``2:num``] THEN
1771 REWRITE_TAC[complex_pow, COMPLEX_POW_1]
1772QED
1773
1774Theorem COMPLEX_POW_ONE:
1775 !n:num. 1 pow n = 1
1776Proof
1777 INDUCT_TAC THEN ASM_REWRITE_TAC[complex_pow, COMPLEX_MUL_LID]
1778QED
1779
1780Theorem COMPLEX_POW_MUL:
1781 !n:num z:complex w:complex. (z * w) pow n = (z pow n) * (w pow n)
1782Proof
1783 INDUCT_TAC THEN REWRITE_TAC[complex_pow, COMPLEX_MUL_LID] THEN
1784 REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN
1785 CONV_TAC(AC_CONV(COMPLEX_MUL_ASSOC,COMPLEX_MUL_COMM))
1786QED
1787
1788Theorem COMPLEX_POW_INV:
1789 !z:complex n:num. (inv z) pow n = inv (z pow n)
1790Proof
1791 Induct_on `n` THEN REWRITE_TAC [complex_pow] THENL
1792 [REWRITE_TAC [COMPLEX_INV1],
1793 GEN_TAC THEN Cases_on `z = 0` THENL
1794 [POP_ASSUM SUBST_ALL_TAC
1795 THEN REWRITE_TAC [COMPLEX_INV_0,COMPLEX_MUL_LZERO],
1796 `~(z pow n = 0)` by PROVE_TAC [COMPLEX_POW_NZ] THEN
1797 IMP_RES_TAC COMPLEX_INV_MUL THEN ASM_REWRITE_TAC []]]
1798QED
1799
1800Theorem COMPLEX_POW_DIV:
1801 !z:complex w:complex n:num. (z / w) pow n = (z pow n) / (w pow n)
1802Proof
1803 REWRITE_TAC[complex_div, COMPLEX_POW_MUL, COMPLEX_POW_INV]
1804QED
1805
1806Theorem COMPLEX_POW_L:
1807 !n:num k:real z:complex. (k * z) pow n = (k pow n) * (z pow n)
1808Proof
1809 INDUCT_TAC THEN
1810 REWRITE_TAC[complex_pow, pow, COMPLEX_SCALAR_LMUL_ONE] THEN
1811 REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN
1812 REWRITE_TAC[COMPLEX_MUL_SCALAR_LMUL2]
1813QED
1814
1815Theorem COMPLEX_POW_ZERO:
1816 !n:num z:complex. (z pow n = 0) ==> (z = 0)
1817Proof
1818 INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC[complex_pow] THEN
1819 REWRITE_TAC[COMPLEX_10, COMPLEX_ENTIRE] THEN
1820 DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC ASSUME_TAC) THEN
1821 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC
1822QED
1823
1824Theorem COMPLEX_POW_ZERO_EQ:
1825 !n:num z:complex. (z pow (SUC n) = 0) = (z = 0)
1826Proof
1827 REPEAT GEN_TAC THEN EQ_TAC THEN
1828 REWRITE_TAC[COMPLEX_POW_ZERO] THEN
1829 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[COMPLEX_POW_0]
1830QED
1831
1832Theorem COMPLEX_POW_POW:
1833 !z:complex m:num n:num. (z pow m) pow n = z pow (m * n)
1834Proof
1835 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
1836 ASM_REWRITE_TAC[complex_pow, MULT_CLAUSES, COMPLEX_POW_ADD]
1837QED
1838
1839Theorem DE_MOIVRE_LEMMA:
1840 !x:real n:num. (cos x, sin x) pow n = (cos (&n * x), sin(&n * x))
1841Proof
1842 GEN_TAC THEN INDUCT_TAC THEN
1843 ASM_REWRITE_TAC [complex_pow, REAL_MUL_LZERO, COS_0, SIN_0, complex_of_num,
1844 complex_of_real, COMPLEX_MUL_ARG] THEN
1845 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN
1846 REWRITE_TAC[REAL, REAL_ADD_RDISTRIB, REAL_MUL_LID]
1847QED
1848
1849Theorem DE_MOIVRE_THM:
1850 !z:complex n:num.
1851 (modu z * (cos (arg z),sin (arg z))) pow n =
1852 modu z pow n * (cos (&n * arg z),sin(&n * arg z))
1853Proof
1854 REWRITE_TAC[COMPLEX_POW_L, DE_MOIVRE_LEMMA]
1855QED
1856
1857(*--------------------------------------------------------------------*)
1858(*Exponential form of complex numbers *)
1859(*--------------------------------------------------------------------*)
1860
1861Definition complex_exp[nocompute]:
1862 complex_exp (z:complex) = exp(RE z) * (cos (IM z),sin (IM z))
1863End
1864
1865Overload exp = Term`$complex_exp`
1866
1867Theorem EXP_IMAGINARY:
1868 !x:real. exp (i * x) = (cos x,sin x)
1869Proof
1870 REWRITE_TAC[complex_exp, i, complex_scalar_rmul, RE, IM, REAL_MUL_LZERO,
1871 REAL_MUL_LID, EXP_0, COMPLEX_SCALAR_LMUL_ONE]
1872QED
1873
1874Theorem EULER_FORMULE:
1875 !z:complex. modu z * exp (i * arg z) = z
1876Proof
1877 REWRITE_TAC[complex_exp, i, complex_scalar_rmul, RE, IM, REAL_MUL_LZERO,
1878 REAL_MUL_LID, EXP_0, COMPLEX_SCALAR_LMUL_ONE, COMPLEX_TRIANGLE]
1879QED
1880
1881Theorem COMPLEX_EXP_ADD:
1882 !z:complex w:complex. exp (z + w) = exp z * exp w
1883Proof
1884 REWRITE_TAC[complex_exp, COMPLEX_MUL_SCALAR_LMUL2, GSYM EXP_ADD,
1885 COMPLEX_MUL_ARG, complex_add, RE, IM]
1886QED
1887
1888Theorem COMPLEX_EXP_NEG:
1889 !z:complex. exp (-z) = inv (exp z)
1890Proof
1891 GEN_TAC THEN
1892 REWRITE_TAC [complex_exp, complex_neg, RE, IM, EXP_NEG,
1893 GSYM COMPLEX_INV_ARG] THEN
1894 CONV_TAC SYM_CONV THEN MATCH_MP_TAC COMPLEX_INV_SCALAR_LMUL THEN
1895 REWRITE_TAC[EXP_NZ, MODU_NZ, MODU_UNIT, REAL_LT_01]
1896QED
1897
1898Theorem COMPLEX_EXP_SUB:
1899 !z:complex w:complex. exp (z - w) = exp z / exp w
1900Proof
1901 REWRITE_TAC[complex_sub,COMPLEX_EXP_ADD,COMPLEX_EXP_NEG,complex_div]
1902QED
1903
1904Theorem COMPLEX_EXP_N:
1905 !z:complex n:num. exp (&n : real * z) = exp z pow n
1906Proof
1907 REWRITE_TAC[complex_scalar_lmul] THEN
1908 REWRITE_TAC[complex_exp, RE, IM, EXP_N, GSYM DE_MOIVRE_LEMMA,
1909 COMPLEX_POW_L]
1910QED
1911
1912Theorem COMPLEX_EXP_N2:
1913 !z:complex n:num. exp (&n :complex * z) = exp z pow n
1914Proof
1915 REWRITE_TAC[complex_mul, complex_of_num, RE_COMPLEX_OF_REAL,
1916 IM_COMPLEX_OF_REAL, REAL_MUL_LZERO, REAL_ADD_RID,REAL_SUB_RZERO,
1917 GSYM complex_scalar_lmul, COMPLEX_EXP_N]
1918QED
1919
1920Theorem COMPLEX_EXP_0:
1921 exp 0c = 1
1922Proof
1923 REWRITE_TAC[complex_of_num, complex_of_real, complex_exp, RE, IM, EXP_0,
1924 COS_0, SIN_0, COMPLEX_SCALAR_LMUL_ONE]
1925QED
1926
1927Theorem COMPLEX_EXP_NZ:
1928 !z:complex. exp z <> 0
1929Proof
1930 REWRITE_TAC[complex_exp, COMPLEX_SCALAR_LMUL_ENTIRE] THEN
1931 REWRITE_TAC[EXP_NZ, MODU_NZ, MODU_UNIT, REAL_LT_01]
1932QED
1933
1934Theorem COMPLEX_EXP_ADD_MUL:
1935 !z:complex w:complex. exp (z + w) * exp (-z) = exp w
1936Proof
1937 REWRITE_TAC[GSYM COMPLEX_EXP_ADD, GSYM complex_sub, COMPLEX_ADD_SUB]
1938QED
1939
1940Theorem COMPLEX_EXP_NEG_MUL:
1941 !z:complex. exp z * exp (-z) = 1
1942Proof
1943 REWRITE_TAC[GSYM COMPLEX_EXP_ADD, COMPLEX_ADD_RINV, COMPLEX_EXP_0]
1944QED
1945
1946Theorem COMPLEX_EXP_NEG_MUL2:
1947 !z:complex. exp (-z) * exp z = 1
1948Proof
1949 ONCE_REWRITE_TAC[COMPLEX_MUL_COMM] THEN
1950 MATCH_ACCEPT_TAC COMPLEX_EXP_NEG_MUL
1951QED
1952
1953(* References:
1954
1955 [1] Shi, Z., Guan, Y., Li, X.: Formalization of Complex Analysis and Matrix
1956 Theory in HOL4. Appl. Math. Inf. Sci. 7, 279-286 (2013).
1957 *)