1.1 --- a/src/HOL/Complex.thy Thu Aug 18 21:23:31 2011 -0700
1.2 +++ b/src/HOL/Complex.thy Thu Aug 18 22:31:52 2011 -0700
1.3 @@ -603,10 +603,42 @@
1.4 rcis :: "[real, real] => complex" where
1.5 "rcis r a = complex_of_real r * cis a"
1.6
1.7 -definition
1.8 - (* e ^ (x + iy) *)
1.9 - expi :: "complex => complex" where
1.10 - "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
1.11 +abbreviation expi :: "complex \<Rightarrow> complex"
1.12 + where "expi \<equiv> exp"
1.13 +
1.14 +lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
1.15 + unfolding cos_coeff_def sin_coeff_def
1.16 + by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
1.17 +
1.18 +lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
1.19 + unfolding cos_coeff_def sin_coeff_def
1.20 + by (simp del: mult_Suc)
1.21 +
1.22 +lemma expi_imaginary: "expi (Complex 0 b) = cis b"
1.23 +proof (rule complex_eqI)
1.24 + { fix n have "Complex 0 b ^ n =
1.25 + real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
1.26 + apply (induct n)
1.27 + apply (simp add: cos_coeff_def sin_coeff_def)
1.28 + apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
1.29 + done } note * = this
1.30 + show "Re (exp (Complex 0 b)) = Re (cis b)"
1.31 + unfolding exp_def cis_def cos_def
1.32 + by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
1.33 + simp add: * mult_assoc [symmetric])
1.34 + show "Im (exp (Complex 0 b)) = Im (cis b)"
1.35 + unfolding exp_def cis_def sin_def
1.36 + by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
1.37 + simp add: * mult_assoc [symmetric])
1.38 +qed
1.39 +
1.40 +lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
1.41 +proof -
1.42 + have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
1.43 + by simp
1.44 + thus ?thesis
1.45 + unfolding exp_add exp_of_real expi_imaginary .
1.46 +qed
1.47
1.48 lemma complex_split_polar:
1.49 "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
1.50 @@ -713,10 +745,10 @@
1.51 by (auto simp add: DeMoivre)
1.52
1.53 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
1.54 -by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac)
1.55 + by (rule exp_add) (* FIXME: redundant *)
1.56
1.57 -lemma expi_zero [simp]: "expi (0::complex) = 1"
1.58 -by (simp add: expi_def)
1.59 +lemma expi_zero: "expi (0::complex) = 1"
1.60 + by (rule exp_zero) (* FIXME: redundant *)
1.61
1.62 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
1.63 apply (insert rcis_Ex [of z])