author huffman Wed Sep 07 22:44:26 2011 -0700 (2011-09-07) changeset 44828 3d6a79e0e1d0 parent 44827 4d1384a1fc82 child 44829 5a2cd5db0a11
add some new lemmas about cis and rcis;
simplify some proofs;
 src/HOL/Complex.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 20:44:39 2011 -0700
1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 22:44:26 2011 -0700
1.3 @@ -595,6 +595,15 @@
1.4  lemma cis_zero [simp]: "cis 0 = 1"
1.5    by (simp add: cis_def)
1.6
1.7 +lemma norm_cis [simp]: "norm (cis a) = 1"
1.8 +  by (simp add: cis_def)
1.9 +
1.10 +lemma sgn_cis [simp]: "sgn (cis a) = cis a"
1.11 +  by (simp add: sgn_div_norm)
1.12 +
1.13 +lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
1.14 +  by (metis norm_cis norm_zero zero_neq_one)
1.15 +
1.16  lemma cis_mult: "cis a * cis b = cis (a + b)"
1.17    by (simp add: cis_def cos_add sin_add)
1.18
1.19 @@ -619,25 +628,22 @@
1.20    "rcis r a = complex_of_real r * cis a"
1.21
1.22  lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
1.23 -  by (simp add: rcis_def cis_def)
1.24 +  by (simp add: rcis_def)
1.25
1.26  lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
1.27 -  by (simp add: rcis_def cis_def)
1.28 +  by (simp add: rcis_def)
1.29
1.30  lemma rcis_Ex: "\<exists>r a. z = rcis r a"
1.31 -apply (induct z)
1.32 -apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
1.33 -done
1.34 +  by (simp add: complex_eq_iff polar_Ex)
1.35
1.36  lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
1.37 -  by (simp add: rcis_def cis_def norm_mult)
1.38 +  by (simp add: rcis_def norm_mult)
1.39
1.40  lemma cis_rcis_eq: "cis a = rcis 1 a"
1.41    by (simp add: rcis_def)
1.42
1.43  lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
1.44 -  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
1.45 -    right_diff_distrib complex_of_real_def)
1.46 +  by (simp add: rcis_def cis_mult)
1.47
1.48  lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
1.49    by (simp add: rcis_def)
1.50 @@ -645,6 +651,9 @@
1.51  lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
1.52    by (simp add: rcis_def)
1.53
1.54 +lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \<longleftrightarrow> r = 0"
1.55 +  by (simp add: rcis_def)
1.56 +
1.57  lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
1.58    by (simp add: rcis_def power_mult_distrib DeMoivre)
1.59
1.60 @@ -652,10 +661,7 @@
1.61    by (simp add: divide_inverse rcis_def)
1.62
1.63  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
1.64 -apply (simp add: complex_divide_def)
1.65 -apply (case_tac "r2=0", simp)
1.66 -apply (simp add: rcis_inverse rcis_mult diff_minus)
1.67 -done
1.68 +  by (simp add: rcis_def cis_divide [symmetric])
1.69
1.70  subsubsection {* Complex exponential *}
1.71
1.72 @@ -683,6 +689,12 @@
1.73  lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
1.74    unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
1.75
1.76 +lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
1.77 +  unfolding expi_def by simp
1.78 +
1.79 +lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
1.80 +  unfolding expi_def by simp
1.81 +
1.82  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
1.83  apply (insert rcis_Ex [of z])
1.84  apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])
```