replace lemma expi_imaginary with reoriented lemma cis_conv_exp
authorhuffman
Sun Sep 04 10:29:38 2011 -0700 (2011-09-04)
changeset 447121e490e891c88
parent 44711 cd8dbfc272df
child 44713 8c3d4063bf52
child 44714 a8990b5d7365
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Sun Sep 04 10:05:52 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun Sep 04 10:29:38 2011 -0700
     1.3 @@ -606,7 +606,7 @@
     1.4  abbreviation expi :: "complex \<Rightarrow> complex"
     1.5    where "expi \<equiv> exp"
     1.6  
     1.7 -lemma expi_imaginary: "expi (Complex 0 b) = cis b"
     1.8 +lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
     1.9  proof (rule complex_eqI)
    1.10    { fix n have "Complex 0 b ^ n =
    1.11      real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
    1.12 @@ -614,23 +614,18 @@
    1.13        apply (simp add: cos_coeff_def sin_coeff_def)
    1.14        apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
    1.15        done } note * = this
    1.16 -  show "Re (exp (Complex 0 b)) = Re (cis b)"
    1.17 +  show "Re (cis b) = Re (exp (Complex 0 b))"
    1.18      unfolding exp_def cis_def cos_def
    1.19      by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
    1.20        simp add: * mult_assoc [symmetric])
    1.21 -  show "Im (exp (Complex 0 b)) = Im (cis b)"
    1.22 +  show "Im (cis b) = Im (exp (Complex 0 b))"
    1.23      unfolding exp_def cis_def sin_def
    1.24      by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
    1.25        simp add: * mult_assoc [symmetric])
    1.26  qed
    1.27  
    1.28  lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
    1.29 -proof -
    1.30 -  have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
    1.31 -    by simp
    1.32 -  thus ?thesis
    1.33 -    unfolding exp_add exp_of_real expi_imaginary .
    1.34 -qed
    1.35 +  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
    1.36  
    1.37  lemma complex_split_polar:
    1.38       "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"