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])