23 Im: "Im (Complex x y) = y" |
23 Im: "Im (Complex x y) = y" |
24 |
24 |
25 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" |
25 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" |
26 by (induct z) simp |
26 by (induct z) simp |
27 |
27 |
28 lemma complex_equality [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y" |
28 lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y" |
29 by (induct x, induct y) simp |
29 by (induct x, induct y) simp |
30 |
30 |
31 lemma expand_complex_eq: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y" |
31 lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y" |
32 by (induct x, induct y) simp |
32 by (induct x, induct y) simp |
33 |
|
34 lemmas complex_Re_Im_cancel_iff = expand_complex_eq |
|
35 |
33 |
36 |
34 |
37 subsection {* Addition and Subtraction *} |
35 subsection {* Addition and Subtraction *} |
38 |
36 |
39 instantiation complex :: ab_group_add |
37 instantiation complex :: ab_group_add |
188 lemma complex_Im_number_of [simp]: "Im (number_of v) = 0" |
186 lemma complex_Im_number_of [simp]: "Im (number_of v) = 0" |
189 unfolding number_of_eq by (rule complex_Im_of_int) |
187 unfolding number_of_eq by (rule complex_Im_of_int) |
190 |
188 |
191 lemma Complex_eq_number_of [simp]: |
189 lemma Complex_eq_number_of [simp]: |
192 "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)" |
190 "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)" |
193 by (simp add: expand_complex_eq) |
191 by (simp add: complex_eq_iff) |
194 |
192 |
195 |
193 |
196 subsection {* Scalar Multiplication *} |
194 subsection {* Scalar Multiplication *} |
197 |
195 |
198 instantiation complex :: real_field |
196 instantiation complex :: real_field |
213 |
211 |
214 instance |
212 instance |
215 proof |
213 proof |
216 fix a b :: real and x y :: complex |
214 fix a b :: real and x y :: complex |
217 show "scaleR a (x + y) = scaleR a x + scaleR a y" |
215 show "scaleR a (x + y) = scaleR a x + scaleR a y" |
218 by (simp add: expand_complex_eq right_distrib) |
216 by (simp add: complex_eq_iff right_distrib) |
219 show "scaleR (a + b) x = scaleR a x + scaleR b x" |
217 show "scaleR (a + b) x = scaleR a x + scaleR b x" |
220 by (simp add: expand_complex_eq left_distrib) |
218 by (simp add: complex_eq_iff left_distrib) |
221 show "scaleR a (scaleR b x) = scaleR (a * b) x" |
219 show "scaleR a (scaleR b x) = scaleR (a * b) x" |
222 by (simp add: expand_complex_eq mult_assoc) |
220 by (simp add: complex_eq_iff mult_assoc) |
223 show "scaleR 1 x = x" |
221 show "scaleR 1 x = x" |
224 by (simp add: expand_complex_eq) |
222 by (simp add: complex_eq_iff) |
225 show "scaleR a x * y = scaleR a (x * y)" |
223 show "scaleR a x * y = scaleR a (x * y)" |
226 by (simp add: expand_complex_eq algebra_simps) |
224 by (simp add: complex_eq_iff algebra_simps) |
227 show "x * scaleR a y = scaleR a (x * y)" |
225 show "x * scaleR a y = scaleR a (x * y)" |
228 by (simp add: expand_complex_eq algebra_simps) |
226 by (simp add: complex_eq_iff algebra_simps) |
229 qed |
227 qed |
230 |
228 |
231 end |
229 end |
232 |
230 |
233 |
231 |
403 |
401 |
404 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)" |
402 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)" |
405 by (simp add: i_def) |
403 by (simp add: i_def) |
406 |
404 |
407 lemma complex_i_not_zero [simp]: "ii \<noteq> 0" |
405 lemma complex_i_not_zero [simp]: "ii \<noteq> 0" |
408 by (simp add: expand_complex_eq) |
406 by (simp add: complex_eq_iff) |
409 |
407 |
410 lemma complex_i_not_one [simp]: "ii \<noteq> 1" |
408 lemma complex_i_not_one [simp]: "ii \<noteq> 1" |
411 by (simp add: expand_complex_eq) |
409 by (simp add: complex_eq_iff) |
412 |
410 |
413 lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w" |
411 lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w" |
414 by (simp add: expand_complex_eq) |
412 by (simp add: complex_eq_iff) |
415 |
413 |
416 lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a" |
414 lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a" |
417 by (simp add: expand_complex_eq) |
415 by (simp add: complex_eq_iff) |
418 |
416 |
419 lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a" |
417 lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a" |
420 by (simp add: expand_complex_eq) |
418 by (simp add: complex_eq_iff) |
421 |
419 |
422 lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r" |
420 lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r" |
423 by (simp add: i_def complex_of_real_def) |
421 by (simp add: i_def complex_of_real_def) |
424 |
422 |
425 lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" |
423 lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" |
449 |
447 |
450 lemma complex_Im_cnj [simp]: "Im (cnj x) = - Im x" |
448 lemma complex_Im_cnj [simp]: "Im (cnj x) = - Im x" |
451 by (simp add: cnj_def) |
449 by (simp add: cnj_def) |
452 |
450 |
453 lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" |
451 lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" |
454 by (simp add: expand_complex_eq) |
452 by (simp add: complex_eq_iff) |
455 |
453 |
456 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" |
454 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" |
457 by (simp add: cnj_def) |
455 by (simp add: cnj_def) |
458 |
456 |
459 lemma complex_cnj_zero [simp]: "cnj 0 = 0" |
457 lemma complex_cnj_zero [simp]: "cnj 0 = 0" |
460 by (simp add: expand_complex_eq) |
458 by (simp add: complex_eq_iff) |
461 |
459 |
462 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" |
460 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" |
463 by (simp add: expand_complex_eq) |
461 by (simp add: complex_eq_iff) |
464 |
462 |
465 lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y" |
463 lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y" |
466 by (simp add: expand_complex_eq) |
464 by (simp add: complex_eq_iff) |
467 |
465 |
468 lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y" |
466 lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y" |
469 by (simp add: expand_complex_eq) |
467 by (simp add: complex_eq_iff) |
470 |
468 |
471 lemma complex_cnj_minus: "cnj (- x) = - cnj x" |
469 lemma complex_cnj_minus: "cnj (- x) = - cnj x" |
472 by (simp add: expand_complex_eq) |
470 by (simp add: complex_eq_iff) |
473 |
471 |
474 lemma complex_cnj_one [simp]: "cnj 1 = 1" |
472 lemma complex_cnj_one [simp]: "cnj 1 = 1" |
475 by (simp add: expand_complex_eq) |
473 by (simp add: complex_eq_iff) |
476 |
474 |
477 lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y" |
475 lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y" |
478 by (simp add: expand_complex_eq) |
476 by (simp add: complex_eq_iff) |
479 |
477 |
480 lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)" |
478 lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)" |
481 by (simp add: complex_inverse_def) |
479 by (simp add: complex_inverse_def) |
482 |
480 |
483 lemma complex_cnj_divide: "cnj (x / y) = cnj x / cnj y" |
481 lemma complex_cnj_divide: "cnj (x / y) = cnj x / cnj y" |
485 |
483 |
486 lemma complex_cnj_power: "cnj (x ^ n) = cnj x ^ n" |
484 lemma complex_cnj_power: "cnj (x ^ n) = cnj x ^ n" |
487 by (induct n, simp_all add: complex_cnj_mult) |
485 by (induct n, simp_all add: complex_cnj_mult) |
488 |
486 |
489 lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n" |
487 lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n" |
490 by (simp add: expand_complex_eq) |
488 by (simp add: complex_eq_iff) |
491 |
489 |
492 lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z" |
490 lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z" |
493 by (simp add: expand_complex_eq) |
491 by (simp add: complex_eq_iff) |
494 |
492 |
495 lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w" |
493 lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w" |
496 by (simp add: expand_complex_eq) |
494 by (simp add: complex_eq_iff) |
497 |
495 |
498 lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)" |
496 lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)" |
499 by (simp add: expand_complex_eq) |
497 by (simp add: complex_eq_iff) |
500 |
498 |
501 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" |
499 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" |
502 by (simp add: complex_norm_def) |
500 by (simp add: complex_norm_def) |
503 |
501 |
504 lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x" |
502 lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x" |
505 by (simp add: expand_complex_eq) |
503 by (simp add: complex_eq_iff) |
506 |
504 |
507 lemma complex_cnj_i [simp]: "cnj ii = - ii" |
505 lemma complex_cnj_i [simp]: "cnj ii = - ii" |
508 by (simp add: expand_complex_eq) |
506 by (simp add: complex_eq_iff) |
509 |
507 |
510 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)" |
508 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)" |
511 by (simp add: expand_complex_eq) |
509 by (simp add: complex_eq_iff) |
512 |
510 |
513 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii" |
511 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii" |
514 by (simp add: expand_complex_eq) |
512 by (simp add: complex_eq_iff) |
515 |
513 |
516 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" |
514 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" |
517 by (simp add: expand_complex_eq power2_eq_square) |
515 by (simp add: complex_eq_iff power2_eq_square) |
518 |
516 |
519 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
517 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
520 by (simp add: norm_mult power2_eq_square) |
518 by (simp add: norm_mult power2_eq_square) |
521 |
519 |
522 interpretation cnj: bounded_linear "cnj" |
520 interpretation cnj: bounded_linear "cnj" |