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
```