# HG changeset patch
# User huffman
# Date 1313731912 25200
# Node ID dbd9965745fdb4b5858d039b447c69aab74462c7
# Parent  23a5137162ea94e6ea6b09eeeba0c9c8e7db1782
define complex exponential 'expi' as abbreviation for 'exp'

diff -r 23a5137162ea -r dbd9965745fd src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Aug 18 21:23:31 2011 -0700
+++ b/src/HOL/Complex.thy	Thu Aug 18 22:31:52 2011 -0700
@@ -603,10 +603,42 @@
   rcis :: "[real, real] => complex" where
   "rcis r a = complex_of_real r * cis a"
 
-definition
-  (* e ^ (x + iy) *)
-  expi :: "complex => complex" where
-  "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
+abbreviation expi :: "complex \<Rightarrow> complex"
+  where "expi \<equiv> exp"
+
+lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
+  unfolding cos_coeff_def sin_coeff_def
+  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
+
+lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
+  unfolding cos_coeff_def sin_coeff_def
+  by (simp del: mult_Suc)
+
+lemma expi_imaginary: "expi (Complex 0 b) = cis 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)"
+      apply (induct n)
+      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)"
+    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)"
+    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
 
 lemma complex_split_polar:
      "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
@@ -713,10 +745,10 @@
 by (auto simp add: DeMoivre)
 
 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
-by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac)
+  by (rule exp_add) (* FIXME: redundant *)
 
-lemma expi_zero [simp]: "expi (0::complex) = 1"
-by (simp add: expi_def)
+lemma expi_zero: "expi (0::complex) = 1"
+  by (rule exp_zero) (* FIXME: redundant *)
 
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])