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.7 -by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
     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.16 -  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    1.17 +  by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    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.71 -  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
    1.72 +  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
    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.75    apply (simp add: sin_squared_eq)
    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.80 -  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
    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.84    apply (simp add: cos_squared_eq)
    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])