157 by (simp add: complex_inverse_def) |
157 by (simp add: complex_inverse_def) |
158 |
158 |
159 lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" |
159 lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" |
160 apply (induct z) |
160 apply (induct z) |
161 apply (rename_tac x y) |
161 apply (rename_tac x y) |
162 apply (auto simp add: times_divide_eq complex_mult complex_inverse |
162 apply (auto simp add: |
163 complex_one_def complex_zero_def add_divide_distrib [symmetric] |
163 complex_one_def complex_zero_def add_divide_distrib [symmetric] |
164 power2_eq_square mult_ac) |
164 power2_eq_square mult_ac) |
165 apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) |
165 apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) |
166 done |
166 done |
167 |
167 |
267 by (simp add: i_def complex_of_real_def) |
267 by (simp add: i_def complex_of_real_def) |
268 |
268 |
269 lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" |
269 lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" |
270 by (simp add: i_def complex_of_real_def) |
270 by (simp add: i_def complex_of_real_def) |
271 |
271 |
272 (* TODO: generalize and move to Real/RealVector.thy *) |
272 lemma complex_of_real_inverse: |
273 lemma complex_of_real_inverse [simp]: |
|
274 "complex_of_real(inverse x) = inverse(complex_of_real x)" |
273 "complex_of_real(inverse x) = inverse(complex_of_real x)" |
275 apply (case_tac "x=0", simp) |
274 by (rule of_real_inverse) |
276 apply (simp add: complex_of_real_def divide_inverse power2_eq_square) |
275 |
277 done |
276 lemma complex_of_real_divide: |
278 |
|
279 (* TODO: generalize and move to Real/RealVector.thy *) |
|
280 lemma complex_of_real_divide [simp]: |
|
281 "complex_of_real(x/y) = complex_of_real x / complex_of_real y" |
277 "complex_of_real(x/y) = complex_of_real x / complex_of_real y" |
282 apply (simp add: complex_divide_def) |
278 by (rule of_real_divide) |
283 apply (case_tac "y=0", simp) |
|
284 apply (simp add: divide_inverse) |
|
285 done |
|
286 |
279 |
287 |
280 |
288 subsection{*The Functions @{term Re} and @{term Im}*} |
281 subsection{*The Functions @{term Re} and @{term Im}*} |
289 |
282 |
290 lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z" |
283 lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z" |
291 by (induct z, induct w, simp add: complex_mult) |
284 by (induct z, induct w, simp) |
292 |
285 |
293 lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z" |
286 lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z" |
294 by (induct z, induct w, simp add: complex_mult) |
287 by (induct z, induct w, simp) |
295 |
288 |
296 lemma Re_i_times [simp]: "Re(ii * z) = - Im z" |
289 lemma Re_i_times [simp]: "Re(ii * z) = - Im z" |
297 by (simp add: complex_Re_mult_eq) |
290 by (simp add: complex_Re_mult_eq) |
298 |
291 |
299 lemma Re_times_i [simp]: "Re(z * ii) = - Im z" |
292 lemma Re_times_i [simp]: "Re(z * ii) = - Im z" |
300 by (simp add: complex_Re_mult_eq) |
293 by (simp add: complex_Re_mult_eq) |
301 |
294 |
302 lemma Im_i_times [simp]: "Im(ii * z) = Re z" |
295 lemma Im_i_times [simp]: "Im(ii * z) = Re z" |
303 by (simp add: complex_Im_mult_eq) |
296 by (simp add: complex_Im_mult_eq) |
304 |
297 |
305 lemma Im_times_i [simp]: "Im(z * ii) = Re z" |
298 lemma Im_times_i [simp]: "Im(z * ii) = Re z" |
306 by (simp add: complex_Im_mult_eq) |
299 by (simp add: complex_Im_mult_eq) |
307 |
300 |
308 lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" |
301 lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" |
309 by (simp add: complex_Re_mult_eq) |
302 by (simp add: complex_Re_mult_eq) |
310 |
303 |
311 lemma complex_Re_mult_complex_of_real [simp]: |
304 lemma complex_Re_mult_complex_of_real [simp]: |
343 lemma complex_cnj_complex_of_real [simp]: |
336 lemma complex_cnj_complex_of_real [simp]: |
344 "cnj (complex_of_real x) = complex_of_real x" |
337 "cnj (complex_of_real x) = complex_of_real x" |
345 by (simp add: complex_of_real_def complex_cnj) |
338 by (simp add: complex_of_real_def complex_cnj) |
346 |
339 |
347 lemma complex_cnj_minus: "cnj (-z) = - cnj z" |
340 lemma complex_cnj_minus: "cnj (-z) = - cnj z" |
348 by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus) |
341 by (simp add: cnj_def) |
349 |
342 |
350 lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)" |
343 lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)" |
351 by (induct z, simp add: complex_cnj complex_inverse power2_eq_square) |
344 by (induct z, simp add: complex_cnj power2_eq_square) |
352 |
345 |
353 lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)" |
346 lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)" |
354 by (induct w, induct z, simp add: complex_cnj complex_add) |
347 by (induct w, induct z, simp add: complex_cnj) |
355 |
348 |
356 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)" |
349 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)" |
357 by (simp add: diff_minus complex_cnj_add complex_cnj_minus) |
350 by (simp add: diff_minus complex_cnj_add complex_cnj_minus) |
358 |
351 |
359 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)" |
352 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)" |
360 by (induct w, induct z, simp add: complex_cnj complex_mult) |
353 by (induct w, induct z, simp add: complex_cnj) |
361 |
354 |
362 lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)" |
355 lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)" |
363 by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) |
356 by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) |
364 |
357 |
365 lemma complex_cnj_one [simp]: "cnj 1 = 1" |
358 lemma complex_cnj_one [simp]: "cnj 1 = 1" |
366 by (simp add: cnj_def complex_one_def) |
359 by (simp add: cnj_def complex_one_def) |
367 |
360 |
368 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" |
361 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" |
369 by (induct z, simp add: complex_add complex_cnj complex_of_real_def) |
362 by (induct z, simp add: complex_cnj complex_of_real_def) |
370 |
363 |
371 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii" |
364 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii" |
372 apply (induct z) |
365 apply (induct z) |
373 apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus |
366 apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus |
374 complex_minus i_def complex_mult) |
367 complex_minus i_def complex_mult) |
379 |
372 |
380 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" |
373 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" |
381 by (induct z, simp add: complex_zero_def complex_cnj) |
374 by (induct z, simp add: complex_zero_def complex_cnj) |
382 |
375 |
383 lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" |
376 lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" |
384 by (induct z, |
377 by (induct z, simp add: complex_cnj complex_of_real_def power2_eq_square) |
385 simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) |
|
386 |
378 |
387 |
379 |
388 subsection{*Modulus*} |
380 subsection{*Modulus*} |
389 |
381 |
390 instance complex :: norm .. |
382 instance complex :: norm .. |
406 |
398 |
407 lemma complex_mod_one [simp]: "cmod(1) = 1" |
399 lemma complex_mod_one [simp]: "cmod(1) = 1" |
408 by (simp add: cmod_def power2_eq_square) |
400 by (simp add: cmod_def power2_eq_square) |
409 |
401 |
410 lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" |
402 lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" |
411 by (simp add: complex_of_real_def power2_eq_square complex_mod) |
403 by (simp add: complex_of_real_def power2_eq_square) |
412 |
404 |
413 lemma complex_of_real_abs: |
405 lemma complex_of_real_abs: |
414 "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" |
406 "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" |
415 by simp |
407 by simp |
416 |
408 |
424 lemma complex_mod_complex_of_real_of_nat [simp]: |
416 lemma complex_mod_complex_of_real_of_nat [simp]: |
425 "cmod (complex_of_real(real (n::nat))) = real n" |
417 "cmod (complex_of_real(real (n::nat))) = real n" |
426 by simp |
418 by simp |
427 |
419 |
428 lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)" |
420 lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)" |
429 by (induct x, simp add: complex_mod complex_minus power2_eq_square) |
421 by (induct x, simp add: power2_eq_square) |
430 |
422 |
431 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" |
423 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" |
432 by (induct z, simp add: complex_cnj complex_mod power2_eq_square) |
424 by (induct z, simp add: complex_cnj power2_eq_square) |
433 |
425 |
434 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" |
426 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" |
435 apply (induct z, simp add: complex_mod complex_cnj complex_mult) |
427 apply (induct z, simp add: complex_mod complex_cnj complex_mult) |
436 apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) |
428 apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) |
437 done |
429 done |
462 by (simp only: cmod_unit_one complex_mod_mult, simp) |
454 by (simp only: cmod_unit_one complex_mod_mult, simp) |
463 |
455 |
464 lemma complex_mod_add_squared_eq: |
456 lemma complex_mod_add_squared_eq: |
465 "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" |
457 "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" |
466 apply (induct x, induct y) |
458 apply (induct x, induct y) |
467 apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc) |
459 apply (auto simp add: complex_mod_squared complex_cnj real_diff_def simp del: realpow_Suc) |
468 apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) |
460 apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) |
469 done |
461 done |
470 |
462 |
471 lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)" |
463 lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)" |
472 apply (induct x, induct y) |
464 apply (induct x, induct y) |
473 apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc) |
465 apply (auto simp add: complex_mod complex_cnj diff_def simp del: realpow_Suc) |
474 done |
466 done |
475 |
467 |
476 lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \<le> cmod(x * y)" |
468 lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \<le> cmod(x * y)" |
477 by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult) |
469 by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult) |
478 |
470 |
522 lemma complex_mod_mult_less: |
514 lemma complex_mod_mult_less: |
523 "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" |
515 "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" |
524 by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) |
516 by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) |
525 |
517 |
526 lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \<le> cmod(a + b)" |
518 lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \<le> cmod(a + b)" |
527 apply (rule linorder_cases [of "cmod(a)" "cmod (b)"]) |
519 proof - |
528 apply auto |
520 have "cmod a - cmod b = cmod a - cmod (- b)" by simp |
529 apply (rule order_trans [of _ 0], rule order_less_imp_le) |
521 also have "\<dots> \<le> cmod (a - - b)" by (rule norm_triangle_ineq2) |
530 apply (simp add: compare_rls, simp) |
522 also have "\<dots> = cmod (a + b)" by simp |
531 apply (simp add: compare_rls) |
523 finally show ?thesis . |
532 apply (rule complex_mod_minus [THEN subst]) |
524 qed |
533 apply (rule order_trans) |
|
534 apply (rule_tac [2] complex_mod_triangle_ineq) |
|
535 apply (auto simp add: add_ac) |
|
536 done |
|
537 |
525 |
538 lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z" |
526 lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z" |
539 by (induct z, simp add: complex_mod del: realpow_Suc) |
527 by (induct z, simp) |
540 |
528 |
541 lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" |
529 lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" |
542 by (rule zero_less_norm_iff [THEN iffD2]) |
530 by (rule zero_less_norm_iff [THEN iffD2]) |
543 |
531 |
544 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)" |
532 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)" |
545 by (rule norm_inverse) |
533 by (rule norm_inverse) |
546 |
534 |
547 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" |
535 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" |
548 by (simp add: divide_inverse norm_mult norm_inverse) |
536 by (rule norm_divide) |
549 |
537 |
550 |
538 |
551 subsection{*Exponentiation*} |
539 subsection{*Exponentiation*} |
552 |
540 |
553 primrec |
541 primrec |
563 show "z^(Suc n) = z * (z^n)" by simp |
551 show "z^(Suc n) = z * (z^n)" by simp |
564 qed |
552 qed |
565 |
553 |
566 |
554 |
567 lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n" |
555 lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n" |
568 apply (induct_tac "n") |
556 by (rule of_real_power) |
569 apply (auto simp add: of_real_mult [symmetric]) |
|
570 done |
|
571 |
557 |
572 lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n" |
558 lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n" |
573 apply (induct_tac "n") |
559 apply (induct_tac "n") |
574 apply (auto simp add: complex_cnj_mult) |
560 apply (auto simp add: complex_cnj_mult) |
575 done |
561 done |
576 |
562 |
577 lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n" |
563 lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n" |
578 apply (induct_tac "n") |
564 by (rule norm_power) |
579 apply (auto simp add: complex_mod_mult) |
|
580 done |
|
581 |
565 |
582 lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)" |
566 lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)" |
583 by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2) |
567 by (simp add: i_def complex_one_def numeral_2_eq_2) |
584 |
568 |
585 lemma complex_i_not_zero [simp]: "ii \<noteq> 0" |
569 lemma complex_i_not_zero [simp]: "ii \<noteq> 0" |
586 by (simp add: i_def complex_zero_def) |
570 by (simp add: i_def complex_zero_def) |
587 |
571 |
588 |
572 |
608 |
592 |
609 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" |
593 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" |
610 by (simp add: sgn_def) |
594 by (simp add: sgn_def) |
611 |
595 |
612 lemma i_mult_eq: "ii * ii = complex_of_real (-1)" |
596 lemma i_mult_eq: "ii * ii = complex_of_real (-1)" |
613 by (simp add: i_def complex_of_real_def complex_mult complex_add) |
597 by (simp add: i_def complex_of_real_def) |
614 |
598 |
615 lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)" |
599 lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)" |
616 by (simp add: i_def complex_one_def complex_mult complex_minus) |
600 by (simp add: i_def complex_one_def) |
617 |
601 |
618 lemma complex_eq_cancel_iff2 [simp]: |
602 lemma complex_eq_cancel_iff2 [simp]: |
619 "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" |
|
620 by (simp add: complex_of_real_def) |
|
621 |
|
622 lemma complex_eq_cancel_iff2a [simp]: |
|
623 "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" |
603 "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" |
624 by (simp add: complex_of_real_def) |
604 by (simp add: complex_of_real_def) |
625 |
605 |
626 lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)" |
606 lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)" |
627 by (simp add: complex_zero_def) |
607 by (simp add: complex_zero_def) |
655 |
635 |
656 lemma complex_inverse_complex_split: |
636 lemma complex_inverse_complex_split: |
657 "inverse(complex_of_real x + ii * complex_of_real y) = |
637 "inverse(complex_of_real x + ii * complex_of_real y) = |
658 complex_of_real(x/(x ^ 2 + y ^ 2)) - |
638 complex_of_real(x/(x ^ 2 + y ^ 2)) - |
659 ii * complex_of_real(y/(x ^ 2 + y ^ 2))" |
639 ii * complex_of_real(y/(x ^ 2 + y ^ 2))" |
660 by (simp add: complex_of_real_def i_def complex_mult complex_add |
640 by (simp add: complex_of_real_def i_def diff_minus divide_inverse) |
661 diff_minus complex_minus complex_inverse divide_inverse) |
|
662 |
641 |
663 (*----------------------------------------------------------------------------*) |
642 (*----------------------------------------------------------------------------*) |
664 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) |
643 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) |
665 (* many of the theorems are not used - so should they be kept? *) |
644 (* many of the theorems are not used - so should they be kept? *) |
666 (*----------------------------------------------------------------------------*) |
645 (*----------------------------------------------------------------------------*) |
667 |
646 |
668 lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)" |
647 lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)" |
669 by (auto simp add: complex_zero_def complex_of_real_def) |
648 by (rule of_real_eq_0_iff) |
670 |
649 |
671 lemma cos_arg_i_mult_zero_pos: |
650 lemma cos_arg_i_mult_zero_pos: |
672 "0 < y ==> cos (arg(Complex 0 y)) = 0" |
651 "0 < y ==> cos (arg(Complex 0 y)) = 0" |
673 apply (simp add: arg_def abs_if) |
652 apply (simp add: arg_def abs_if) |
674 apply (rule_tac a = "pi/2" in someI2, auto) |
653 apply (rule_tac a = "pi/2" in someI2, auto) |
703 expi :: "complex => complex" |
682 expi :: "complex => complex" |
704 "expi z = complex_of_real(exp (Re z)) * cis (Im z)" |
683 "expi z = complex_of_real(exp (Re z)) * cis (Im z)" |
705 |
684 |
706 lemma complex_split_polar: |
685 lemma complex_split_polar: |
707 "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))" |
686 "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))" |
708 apply (induct z) |
687 apply (induct z) |
709 apply (auto simp add: polar_Ex complex_of_real_mult_Complex) |
688 apply (auto simp add: polar_Ex complex_of_real_mult_Complex) |
710 done |
689 done |
711 |
690 |
712 lemma rcis_Ex: "\<exists>r a. z = rcis r a" |
691 lemma rcis_Ex: "\<exists>r a. z = rcis r a" |
713 apply (induct z) |
692 apply (induct z) |
714 apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) |
693 apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) |
715 done |
694 done |
716 |
695 |
717 lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" |
696 lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" |
718 by (simp add: rcis_def cis_def) |
697 by (simp add: rcis_def cis_def) |
721 by (simp add: rcis_def cis_def) |
700 by (simp add: rcis_def cis_def) |
722 |
701 |
723 lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>" |
702 lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>" |
724 proof - |
703 proof - |
725 have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)" |
704 have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)" |
726 by (simp only: power_mult_distrib right_distrib) |
705 by (simp only: power_mult_distrib right_distrib) |
727 thus ?thesis by simp |
706 thus ?thesis by simp |
728 qed |
707 qed |
729 |
708 |
730 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" |
709 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" |
731 by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) |
710 by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) |
732 |
711 |
733 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" |
712 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" |
734 apply (simp add: cmod_def) |
713 apply (simp add: cmod_def) |
735 apply (rule real_sqrt_eq_iff [THEN iffD2]) |
714 apply (rule real_sqrt_eq_iff [THEN iffD2]) |
736 apply (auto simp add: complex_mult_cnj) |
715 apply (auto simp add: complex_mult_cnj |
|
716 simp del: of_real_add) |
737 done |
717 done |
738 |
718 |
739 lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" |
719 lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" |
740 by (induct z, simp add: complex_cnj) |
720 by (induct z, simp add: complex_cnj) |
741 |
721 |
769 lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" |
749 lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" |
770 by (simp add: rcis_def) |
750 by (simp add: rcis_def) |
771 |
751 |
772 lemma complex_of_real_minus_one: |
752 lemma complex_of_real_minus_one: |
773 "complex_of_real (-(1::real)) = -(1::complex)" |
753 "complex_of_real (-(1::real)) = -(1::complex)" |
774 by (simp add: complex_of_real_def complex_one_def complex_minus) |
754 by (simp add: complex_of_real_def complex_one_def) |
775 |
755 |
776 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" |
756 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" |
777 by (simp add: complex_mult_assoc [symmetric]) |
757 by (simp add: complex_mult_assoc [symmetric]) |
778 |
758 |
779 |
759 |
788 |
768 |
789 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" |
769 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" |
790 by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow) |
770 by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow) |
791 |
771 |
792 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" |
772 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" |
793 by (simp add: cis_def complex_inverse_complex_split of_real_minus |
773 by (simp add: cis_def complex_inverse_complex_split diff_minus) |
794 diff_minus) |
|
795 |
774 |
796 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)" |
775 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)" |
797 by (simp add: divide_inverse rcis_def complex_of_real_inverse) |
776 by (simp add: divide_inverse rcis_def complex_of_real_inverse) |
798 |
777 |
799 lemma cis_divide: "cis a / cis b = cis (a - b)" |
778 lemma cis_divide: "cis a / cis b = cis (a - b)" |
816 |
795 |
817 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" |
796 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" |
818 by (auto simp add: DeMoivre) |
797 by (auto simp add: DeMoivre) |
819 |
798 |
820 lemma expi_add: "expi(a + b) = expi(a) * expi(b)" |
799 lemma expi_add: "expi(a + b) = expi(a) * expi(b)" |
821 by (simp add: expi_def complex_Re_add exp_add complex_Im_add |
800 by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac) |
822 cis_mult [symmetric] of_real_mult mult_ac) |
|
823 |
801 |
824 lemma expi_zero [simp]: "expi (0::complex) = 1" |
802 lemma expi_zero [simp]: "expi (0::complex) = 1" |
825 by (simp add: expi_def) |
803 by (simp add: expi_def) |
826 |
804 |
827 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" |
805 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" |
838 defs (overloaded) |
816 defs (overloaded) |
839 complex_number_of_def: "(number_of w :: complex) == of_int w" |
817 complex_number_of_def: "(number_of w :: complex) == of_int w" |
840 --{*the type constraint is essential!*} |
818 --{*the type constraint is essential!*} |
841 |
819 |
842 instance complex :: number_ring |
820 instance complex :: number_ring |
843 by (intro_classes, simp add: complex_number_of_def) |
821 by (intro_classes, simp add: complex_number_of_def) |
844 |
822 |
845 |
823 |
846 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*} |
824 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*} |
847 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w" |
825 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w" |
848 by (rule of_real_number_of_eq) |
826 by (rule of_real_number_of_eq) |
853 They work for type complex because the reals can be embedded in them.*} |
831 They work for type complex because the reals can be embedded in them.*} |
854 (* TODO: generalize and move to Real/RealVector.thy *) |
832 (* TODO: generalize and move to Real/RealVector.thy *) |
855 lemma iszero_complex_number_of [simp]: |
833 lemma iszero_complex_number_of [simp]: |
856 "iszero (number_of w :: complex) = iszero (number_of w :: real)" |
834 "iszero (number_of w :: complex) = iszero (number_of w :: real)" |
857 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] |
835 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] |
858 iszero_def) |
836 iszero_def) |
859 |
837 |
860 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v" |
838 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v" |
861 by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real) |
839 by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real) |
862 |
840 |
863 lemma complex_number_of_cmod: |
841 lemma complex_number_of_cmod: |