define complex exponential 'expi' as abbreviation for 'exp'
authorhuffman
Thu Aug 18 22:31:52 2011 -0700 (2011-08-18)
changeset 44291dbd9965745fd
parent 44290 23a5137162ea
child 44292 453803d28c4b
define complex exponential 'expi' as abbreviation for 'exp'
src/HOL/Complex.thy
     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])