src/HOL/Complex.thy
changeset 59658 0cc388370041
parent 59613 7103019278f0
child 59741 5b762cd73a8e
     1.1 --- a/src/HOL/Complex.thy	Mon Mar 09 11:32:32 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Mon Mar 09 16:28:19 2015 +0000
     1.3 @@ -681,8 +681,8 @@
     1.4  
     1.5  subsubsection {* Complex exponential *}
     1.6  
     1.7 -abbreviation expi :: "complex \<Rightarrow> complex"
     1.8 -  where "expi \<equiv> exp"
     1.9 +abbreviation Exp :: "complex \<Rightarrow> complex"
    1.10 +  where "Exp \<equiv> exp"
    1.11  
    1.12  lemma cis_conv_exp: "cis b = exp (\<i> * b)"
    1.13  proof -
    1.14 @@ -695,28 +695,28 @@
    1.15      then have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
    1.16          of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
    1.17        by (simp add: field_simps) }
    1.18 -  then show ?thesis
    1.19 +  then show ?thesis using sin_converges [of b] cos_converges [of b]
    1.20      by (auto simp add: cis.ctr exp_def simp del: of_real_mult
    1.21 -             intro!: sums_unique sums_add sums_mult sums_of_real sin_converges cos_converges)
    1.22 +             intro!: sums_unique sums_add sums_mult sums_of_real)
    1.23  qed
    1.24  
    1.25 -lemma expi_def: "expi z = exp (Re z) * cis (Im z)"
    1.26 +lemma Exp_eq_polar: "Exp z = exp (Re z) * cis (Im z)"
    1.27    unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
    1.28  
    1.29  lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
    1.30 -  unfolding expi_def by simp
    1.31 +  unfolding Exp_eq_polar by simp
    1.32  
    1.33  lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
    1.34 -  unfolding expi_def by simp
    1.35 +  unfolding Exp_eq_polar by simp
    1.36  
    1.37 -lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
    1.38 +lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
    1.39  apply (insert rcis_Ex [of z])
    1.40 -apply (auto simp add: expi_def rcis_def mult.assoc [symmetric])
    1.41 +apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
    1.42  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
    1.43  done
    1.44  
    1.45 -lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
    1.46 -  by (simp add: expi_def complex_eq_iff)
    1.47 +lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
    1.48 +  by (simp add: Exp_eq_polar complex_eq_iff)
    1.49  
    1.50  subsubsection {* Complex argument *}
    1.51