--- a/src/HOL/Complex.thy Sun Sep 04 10:05:52 2011 -0700
+++ b/src/HOL/Complex.thy Sun Sep 04 10:29:38 2011 -0700
@@ -606,7 +606,7 @@
abbreviation expi :: "complex \<Rightarrow> complex"
where "expi \<equiv> exp"
-lemma expi_imaginary: "expi (Complex 0 b) = cis b"
+lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
proof (rule complex_eqI)
{ fix n have "Complex 0 b ^ n =
real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
@@ -614,23 +614,18 @@
apply (simp add: cos_coeff_def sin_coeff_def)
apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
done } note * = this
- show "Re (exp (Complex 0 b)) = Re (cis b)"
+ show "Re (cis b) = Re (exp (Complex 0 b))"
unfolding exp_def cis_def cos_def
by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
simp add: * mult_assoc [symmetric])
- show "Im (exp (Complex 0 b)) = Im (cis b)"
+ show "Im (cis b) = Im (exp (Complex 0 b))"
unfolding exp_def cis_def sin_def
by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
simp add: * mult_assoc [symmetric])
qed
lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
-proof -
- have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
- by simp
- thus ?thesis
- unfolding exp_add exp_of_real expi_imaginary .
-qed
+ unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
lemma complex_split_polar:
"\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"