# HG changeset patch
# User huffman
# Date 1315157378 25200
# Node ID 1e490e891c88273d925c02917f4a45eba8a0276d
# Parent  cd8dbfc272df69a8cbc9f1e28c02d68e35a407af
replace lemma expi_imaginary with reoriented lemma cis_conv_exp

diff -r cd8dbfc272df -r 1e490e891c88 src/HOL/Complex.thy
--- 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))"