author huffman Sun Sep 04 10:29:38 2011 -0700 (2011-09-04) changeset 44712 1e490e891c88 parent 44711 cd8dbfc272df child 44713 8c3d4063bf52 child 44714 a8990b5d7365
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
 src/HOL/Complex.thy file | annotate | diff | revisions
```     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))"
```