src/HOL/Analysis/Complex_Transcendental.thy
 changeset 65274 db2de50de28e parent 65064 a4abec71279a child 65578 e4997c181cce
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Mar 16 13:55:29 2017 +0000
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Mar 16 16:02:18 2017 +0000
1.3 @@ -176,7 +176,7 @@
1.4
1.5  lemma Euler: "exp(z) = of_real(exp(Re z)) *
1.6                (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
1.8 +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
1.9
1.10  lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
1.11    by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
1.12 @@ -202,13 +202,20 @@
1.13  subsection\<open>More on the Polar Representation of Complex Numbers\<close>
1.14
1.15  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
1.18
1.19  lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
1.20 -apply auto
1.21 -apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
1.22 -apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1))
1.23 -by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 sin_zero_iff_int2)
1.24 +                 (is "?lhs = ?rhs")
1.25 +proof
1.26 +  assume "exp z = 1"
1.27 +  then have "Re z = 0"
1.28 +    by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
1.29 +  with \<open>?lhs\<close> show ?rhs
1.30 +    by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)
1.31 +next
1.32 +  assume ?rhs then show ?lhs
1.33 +    using Im_exp Re_exp complex_Re_Im_cancel_iff by force
1.34 +qed
1.35
1.36  lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
1.37                  (is "?lhs = ?rhs")
1.38 @@ -487,7 +494,7 @@
1.39  lemma sinh_complex:
1.40    fixes z :: complex
1.41    shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
1.42 -  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
1.43 +  by (simp add: sin_exp_eq divide_simps exp_minus)
1.44
1.45  lemma sin_i_times:
1.46    fixes z :: complex
1.47 @@ -497,24 +504,24 @@
1.48  lemma sinh_real:
1.49    fixes x :: real
1.50    shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
1.51 -  by (simp add: exp_of_real sin_i_times of_real_numeral)
1.52 +  by (simp add: exp_of_real sin_i_times)
1.53
1.54  lemma cosh_complex:
1.55    fixes z :: complex
1.56    shows "(exp z + inverse (exp z)) / 2 = cos(\<i> * z)"
1.57 -  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
1.58 +  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
1.59
1.60  lemma cosh_real:
1.61    fixes x :: real
1.62    shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
1.63 -  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
1.64 +  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
1.65
1.66  lemmas cos_i_times = cosh_complex [symmetric]
1.67
1.68  lemma norm_cos_squared:
1.69      "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
1.70    apply (cases z)
1.73    apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
1.74    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
1.76 @@ -524,7 +531,7 @@
1.77  lemma norm_sin_squared:
1.78      "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
1.79    apply (cases z)
1.81 +  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
1.82    apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
1.83    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
1.85 @@ -969,7 +976,7 @@
1.86
1.87  lemma complex_split_polar:
1.88    obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
1.89 -  using Arg cis.ctr cis_conv_exp by fastforce
1.90 +  using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
1.91
1.92  lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
1.93  proof (cases w rule: complex_split_polar)
1.94 @@ -2112,7 +2119,7 @@
1.95  proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
1.96    case True
1.97    then have "Im z = 0" "Re z < 0 \<or> z = 0"
1.98 -    using cnj.code complex_cnj_zero_iff  by (auto simp: complex_nonpos_Reals_iff) fastforce
1.99 +    using cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
1.100    then show ?thesis
1.101      apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
1.102      apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
```