new HOL Light material about exp, sin, cos
authorpaulson <lp15@cam.ac.uk>
Wed Mar 18 17:23:22 2015 +0000 (2015-03-18)
changeset 59746ddae5727c5a9
parent 59745 390476a0ef13
child 59747 7325ffa35038
new HOL Light material about exp, sin, cos
NEWS
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Wed Mar 18 14:55:17 2015 +0000
     1.2 +++ b/NEWS	Wed Mar 18 17:23:22 2015 +0000
     1.3 @@ -79,10 +79,13 @@
     1.4  * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
     1.5    single-step rewriting with subterm selection based on patterns.
     1.6  
     1.7 -* the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
     1.8 +* The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
     1.9    type, so in particular on "real" and "complex" uniformly.
    1.10    Minor INCOMPATIBILITY: type constraints may be needed.
    1.11  
    1.12 +* New library of properties of the complex transcendental functions sin, cos, exp,
    1.13 +  ported from HOL Light.
    1.14 +
    1.15  * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
    1.16    numeric types including nat, int, real and complex. INCOMPATIBILITY:
    1.17    an expression such as "fact 3 = 6" may require a type constraint, and the combination
     2.1 --- a/src/HOL/Complex.thy	Wed Mar 18 14:55:17 2015 +0000
     2.2 +++ b/src/HOL/Complex.thy	Wed Mar 18 17:23:22 2015 +0000
     2.3 @@ -612,7 +612,11 @@
     2.4      done
     2.5  qed
     2.6  
     2.7 -subsection{*Finally! Polar Form for Complex Numbers*}
     2.8 +subsection{*Polar Form for Complex Numbers*}
     2.9 +
    2.10 +lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
    2.11 +  using sincos_total_2pi [of "Re z" "Im z"]
    2.12 +  by auto (metis cmod_power2 complex_eq power_one)
    2.13  
    2.14  subsubsection {* $\cos \theta + i \sin \theta$ *}
    2.15  
    2.16 @@ -724,11 +728,17 @@
    2.17  lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
    2.18    unfolding Exp_eq_polar by simp
    2.19  
    2.20 +lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
    2.21 +  by (simp add: norm_complex_def)
    2.22 +
    2.23 +lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
    2.24 +  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
    2.25 +
    2.26  lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
    2.27 -apply (insert rcis_Ex [of z])
    2.28 -apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
    2.29 -apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
    2.30 -done
    2.31 +  apply (insert rcis_Ex [of z])
    2.32 +  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
    2.33 +  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
    2.34 +  done
    2.35  
    2.36  lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
    2.37    by (simp add: Exp_eq_polar complex_eq_iff)
    2.38 @@ -865,6 +875,10 @@
    2.39      by auto
    2.40  qed
    2.41  
    2.42 +lemma csqrt_unique:
    2.43 +    "w^2 = z \<Longrightarrow> (0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w) \<Longrightarrow> csqrt z = w"
    2.44 +  by (auto simp: csqrt_square)
    2.45 +
    2.46  lemma csqrt_minus [simp]:
    2.47    assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
    2.48    shows "csqrt (- x) = \<i> * csqrt x"
    2.49 @@ -877,7 +891,7 @@
    2.50        by (auto simp add: Re_csqrt simp del: csqrt.simps)
    2.51    qed
    2.52    also have "(\<i> * csqrt x)^2 = - x"
    2.53 -    by (simp add: power2_csqrt power_mult_distrib)
    2.54 +    by (simp add: power_mult_distrib)
    2.55    finally show ?thesis .
    2.56  qed
    2.57  
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Mar 18 17:23:22 2015 +0000
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno
     3.5 +(*  Author: John Harrison
     3.6      Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
     3.7  *)
     3.8  
     3.9 @@ -8,6 +8,7 @@
    3.10  imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
    3.11  begin
    3.12  
    3.13 +subsection{*The Exponential Function is Differentiable and Continuous*}
    3.14  
    3.15  lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
    3.16    using DERIV_exp complex_differentiable_def by blast
    3.17 @@ -28,8 +29,6 @@
    3.18  lemma holomorphic_on_exp: "exp holomorphic_on s"
    3.19    by (simp add: complex_differentiable_within_exp holomorphic_on_def)
    3.20  
    3.21 -
    3.22 -
    3.23  subsection{*Euler and de Moivre formulas.*}
    3.24  
    3.25  text{*The sine series times @{term i}*}
    3.26 @@ -158,7 +157,8 @@
    3.27  lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
    3.28    by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
    3.29  
    3.30 -(* Now more relatively easy consequences.*)
    3.31 +
    3.32 +subsection {* More Corollaries about Sine and Cosine *}
    3.33  
    3.34  lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
    3.35    by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
    3.36 @@ -226,4 +226,699 @@
    3.37    finally show ?thesis .
    3.38  qed
    3.39  
    3.40 +  
    3.41 +subsection{*More on the Polar Representation of Complex Numbers*}
    3.42 +
    3.43 +lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
    3.44 +  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
    3.45 +
    3.46 +lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
    3.47 +  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
    3.48 +
    3.49 +lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
    3.50 +  by (simp add: cos_one_2pi_int)
    3.51 +
    3.52 +lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
    3.53 +  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
    3.54 +
    3.55 +lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
    3.56 +  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
    3.57 +  apply (auto simp: field_simps frac_lt_1)
    3.58 +  apply (simp_all add: frac_def divide_simps)
    3.59 +  apply (simp_all add: add_divide_distrib diff_divide_distrib)
    3.60 +  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
    3.61 +  done
    3.62 +
    3.63 +lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
    3.64 +  by (simp add: exp_add exp_Euler exp_of_real)
    3.65 +
    3.66 +
    3.67 +
    3.68 +lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
    3.69 +apply auto
    3.70 +apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
    3.71 +apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1) real_of_int_def)
    3.72 +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 real_of_int_def sin_zero_iff_int2)
    3.73 +
    3.74 +lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
    3.75 +                (is "?lhs = ?rhs")
    3.76 +proof -
    3.77 +  have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
    3.78 +    by (simp add: exp_diff)
    3.79 +  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
    3.80 +    by (simp add: exp_eq_1)
    3.81 +  also have "... \<longleftrightarrow> ?rhs"
    3.82 +    by (auto simp: algebra_simps intro!: complex_eqI)
    3.83 +  finally show ?thesis .
    3.84 +qed
    3.85 +
    3.86 +lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
    3.87 +  by (auto simp: exp_eq abs_mult)
    3.88 +
    3.89 +lemma exp_integer_2pi: 
    3.90 +  assumes "n \<in> Ints"
    3.91 +  shows "exp((2 * n * pi) * ii) = 1"
    3.92 +proof -
    3.93 +  have "exp((2 * n * pi) * ii) = exp 0"
    3.94 +    using assms
    3.95 +    by (simp only: Ints_def exp_eq) auto
    3.96 +  also have "... = 1"
    3.97 +    by simp
    3.98 +  finally show ?thesis .
    3.99 +qed
   3.100 +
   3.101 +lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
   3.102 +proof -
   3.103 +  { assume "sin y = sin x" "cos y = cos x"
   3.104 +    then have "cos (y-x) = 1"
   3.105 +      using cos_add [of y "-x"] by simp
   3.106 +    then have "\<exists>n::int. y-x = real n * 2 * pi"
   3.107 +      using cos_one_2pi_int by blast }
   3.108 +  then show ?thesis
   3.109 +  apply (auto simp: sin_add cos_add)
   3.110 +  apply (metis add.commute diff_add_cancel mult.commute)
   3.111 +  done
   3.112 +qed
   3.113 +
   3.114 +lemma exp_i_ne_1: 
   3.115 +  assumes "0 < x" "x < 2*pi"
   3.116 +  shows "exp(\<i> * of_real x) \<noteq> 1"
   3.117 +proof 
   3.118 +  assume "exp (\<i> * of_real x) = 1"
   3.119 +  then have "exp (\<i> * of_real x) = exp 0"
   3.120 +    by simp
   3.121 +  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
   3.122 +    by (simp only: Ints_def exp_eq) auto
   3.123 +  then have  "of_real x = (of_int (2 * n) * pi)"
   3.124 +    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
   3.125 +  then have  "x = (of_int (2 * n) * pi)"
   3.126 +    by simp
   3.127 +  then show False using assms
   3.128 +    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   3.129 +qed
   3.130 +
   3.131 +lemma sin_eq_0: 
   3.132 +  fixes z::complex
   3.133 +  shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   3.134 +  by (simp add: sin_exp_eq exp_eq of_real_numeral)
   3.135 +
   3.136 +lemma cos_eq_0: 
   3.137 +  fixes z::complex
   3.138 +  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   3.139 +  using sin_eq_0 [of "z - of_real pi/2"]
   3.140 +  by (simp add: sin_diff algebra_simps)
   3.141 +
   3.142 +lemma cos_eq_1: 
   3.143 +  fixes z::complex
   3.144 +  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   3.145 +proof -
   3.146 +  have "cos z = cos (2*(z/2))"
   3.147 +    by simp
   3.148 +  also have "... = 1 - 2 * sin (z/2) ^ 2"
   3.149 +    by (simp only: cos_double_sin)
   3.150 +  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
   3.151 +    by simp
   3.152 +  show ?thesis
   3.153 +    by (auto simp: sin_eq_0 of_real_numeral)
   3.154 +qed  
   3.155 +
   3.156 +lemma csin_eq_1:
   3.157 +  fixes z::complex
   3.158 +  shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   3.159 +  using cos_eq_1 [of "z - of_real pi/2"]
   3.160 +  by (simp add: cos_diff algebra_simps)
   3.161 +
   3.162 +lemma csin_eq_minus1:
   3.163 +  fixes z::complex
   3.164 +  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
   3.165 +        (is "_ = ?rhs")
   3.166 +proof -
   3.167 +  have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
   3.168 +    by (simp add: equation_minus_iff)
   3.169 +  also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
   3.170 +    by (simp only: csin_eq_1)
   3.171 +  also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
   3.172 +    apply (rule iff_exI)
   3.173 +    by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
   3.174 +  also have "... = ?rhs"
   3.175 +    apply (auto simp: of_real_numeral)
   3.176 +    apply (rule_tac [2] x="-(x+1)" in exI)
   3.177 +    apply (rule_tac x="-(x+1)" in exI)
   3.178 +    apply (simp_all add: algebra_simps)
   3.179 +    done
   3.180 +  finally show ?thesis .
   3.181 +qed  
   3.182 +
   3.183 +lemma ccos_eq_minus1: 
   3.184 +  fixes z::complex
   3.185 +  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   3.186 +  using csin_eq_1 [of "z - of_real pi/2"]
   3.187 +  apply (simp add: sin_diff)
   3.188 +  apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   3.189 +  done       
   3.190 +
   3.191 +lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   3.192 +                (is "_ = ?rhs")
   3.193 +proof -
   3.194 +  have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
   3.195 +    by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
   3.196 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
   3.197 +    by (simp only: csin_eq_1)
   3.198 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
   3.199 +    apply (rule iff_exI)
   3.200 +    apply (auto simp: algebra_simps of_real_numeral)
   3.201 +    apply (rule injD [OF inj_of_real [where 'a = complex]])
   3.202 +    apply (auto simp: of_real_numeral)
   3.203 +    done
   3.204 +  also have "... = ?rhs"
   3.205 +    by (auto simp: algebra_simps)
   3.206 +  finally show ?thesis .
   3.207 +qed  
   3.208 +
   3.209 +lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   3.210 +proof -
   3.211 +  have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
   3.212 +    by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
   3.213 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
   3.214 +    by (simp only: csin_eq_minus1)
   3.215 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
   3.216 +    apply (rule iff_exI)
   3.217 +    apply (auto simp: algebra_simps)
   3.218 +    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   3.219 +    done
   3.220 +  also have "... = ?rhs"
   3.221 +    by (auto simp: algebra_simps)
   3.222 +  finally show ?thesis .
   3.223 +qed  
   3.224 +
   3.225 +lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   3.226 +                      (is "_ = ?rhs")
   3.227 +proof -
   3.228 +  have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
   3.229 +    by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
   3.230 +  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
   3.231 +    by (simp only: ccos_eq_minus1)
   3.232 +  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
   3.233 +    apply (rule iff_exI)
   3.234 +    apply (auto simp: algebra_simps)
   3.235 +    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   3.236 +    done
   3.237 +  also have "... = ?rhs"
   3.238 +    by (auto simp: algebra_simps)
   3.239 +  finally show ?thesis .
   3.240 +qed  
   3.241 +
   3.242 +lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   3.243 +  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
   3.244 +  using cos_double_sin [of "t/2"]
   3.245 +  apply (simp add: real_sqrt_mult)
   3.246 +  done
   3.247 +
   3.248 +lemma sinh_complex:
   3.249 +  fixes z :: complex
   3.250 +  shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
   3.251 +  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
   3.252 +
   3.253 +lemma sin_ii_times:
   3.254 +  fixes z :: complex
   3.255 +  shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
   3.256 +  using sinh_complex by auto
   3.257 +
   3.258 +lemma sinh_real:
   3.259 +  fixes x :: real
   3.260 +  shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
   3.261 +  by (simp add: exp_of_real sin_ii_times of_real_numeral)
   3.262 +
   3.263 +lemma cosh_complex:
   3.264 +  fixes z :: complex
   3.265 +  shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
   3.266 +  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   3.267 +
   3.268 +lemma cosh_real:
   3.269 +  fixes x :: real
   3.270 +  shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
   3.271 +  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   3.272 +
   3.273 +lemmas cos_ii_times = cosh_complex [symmetric]
   3.274 +
   3.275 +lemma norm_cos_squared: 
   3.276 +    "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   3.277 +  apply (cases z)
   3.278 +  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   3.279 +  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   3.280 +  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   3.281 +  apply (simp add: sin_squared_eq)
   3.282 +  apply (simp add: power2_eq_square algebra_simps divide_simps)
   3.283 +  done
   3.284 +
   3.285 +lemma norm_sin_squared:
   3.286 +    "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
   3.287 +  apply (cases z)
   3.288 +  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   3.289 +  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   3.290 +  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   3.291 +  apply (simp add: cos_squared_eq)
   3.292 +  apply (simp add: power2_eq_square algebra_simps divide_simps)
   3.293 +  done 
   3.294 +
   3.295 +lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   3.296 +  using abs_Im_le_cmod linear order_trans by fastforce
   3.297 +
   3.298 +lemma norm_cos_le: 
   3.299 +  fixes z::complex
   3.300 +  shows "norm(cos z) \<le> exp(norm z)"
   3.301 +proof -
   3.302 +  have "Im z \<le> cmod z"
   3.303 +    using abs_Im_le_cmod abs_le_D1 by auto
   3.304 +  with exp_uminus_Im show ?thesis
   3.305 +    apply (simp add: cos_exp_eq norm_divide)
   3.306 +    apply (rule order_trans [OF norm_triangle_ineq], simp)
   3.307 +    apply (metis add_mono exp_le_cancel_iff mult_2_right)
   3.308 +    done
   3.309 +qed
   3.310 +
   3.311 +lemma norm_cos_plus1_le: 
   3.312 +  fixes z::complex
   3.313 +  shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   3.314 +proof -
   3.315 +  have mono: "\<And>u w z::real. (1 \<le> w | 1 \<le> z) \<Longrightarrow> (w \<le> u & z \<le> u) \<Longrightarrow> 2 + w + z \<le> 4 * u"
   3.316 +      by arith
   3.317 +  have *: "Im z \<le> cmod z"
   3.318 +    using abs_Im_le_cmod abs_le_D1 by auto
   3.319 +  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
   3.320 +    by (simp add: norm_add_rule_thm)
   3.321 +  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   3.322 +    by (simp add: cos_exp_eq)
   3.323 +  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   3.324 +    by (simp add: field_simps)
   3.325 +  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
   3.326 +    by (simp add: norm_divide)
   3.327 +  finally show ?thesis
   3.328 +    apply (rule ssubst, simp)
   3.329 +    apply (rule order_trans [OF triangle3], simp)
   3.330 +    using exp_uminus_Im *
   3.331 +    apply (auto intro: mono)
   3.332 +    done
   3.333 +qed
   3.334 +
   3.335 +subsection{* Taylor series for complex exponential, sine and cosine.*}
   3.336 +
   3.337 +context 
   3.338 +begin
   3.339 +
   3.340 +declare power_Suc [simp del]
   3.341 +
   3.342 +lemma Taylor_exp: 
   3.343 +  "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   3.344 +proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   3.345 +  show "convex (closed_segment 0 z)"
   3.346 +    by (rule convex_segment [of 0 z])
   3.347 +next
   3.348 +  fix k x
   3.349 +  assume "x \<in> closed_segment 0 z" "k \<le> n"
   3.350 +  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
   3.351 +    using DERIV_exp DERIV_subset by blast
   3.352 +next
   3.353 +  fix x
   3.354 +  assume "x \<in> closed_segment 0 z"
   3.355 +  then show "Re x \<le> \<bar>Re z\<bar>"
   3.356 +    apply (auto simp: closed_segment_def scaleR_conv_of_real)
   3.357 +    by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
   3.358 +next
   3.359 +  show "0 \<in> closed_segment 0 z"
   3.360 +    by (auto simp: closed_segment_def)
   3.361 +next
   3.362 +  show "z \<in> closed_segment 0 z"
   3.363 +    apply (simp add: closed_segment_def scaleR_conv_of_real)
   3.364 +    using of_real_1 zero_le_one by blast
   3.365 +qed 
   3.366 +
   3.367 +lemma 
   3.368 +  assumes "0 \<le> u" "u \<le> 1"
   3.369 +  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
   3.370 +    and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   3.371 +proof -
   3.372 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   3.373 +    by arith
   3.374 +  show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   3.375 +    apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
   3.376 +    apply (rule order_trans [OF norm_triangle_ineq4])
   3.377 +    apply (rule mono)
   3.378 +    apply (auto simp: abs_if mult_left_le_one_le)
   3.379 +    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   3.380 +    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   3.381 +    done
   3.382 +  show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   3.383 +    apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
   3.384 +    apply (rule order_trans [OF norm_triangle_ineq])
   3.385 +    apply (rule mono)
   3.386 +    apply (auto simp: abs_if mult_left_le_one_le)
   3.387 +    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   3.388 +    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   3.389 +    done
   3.390 +qed
   3.391 +    
   3.392 +lemma Taylor_sin: 
   3.393 +  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
   3.394 +   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   3.395 +proof -
   3.396 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   3.397 +      by arith
   3.398 +  have *: "cmod (sin z -
   3.399 +                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   3.400 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   3.401 +  proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
   3.402 +simplified])
   3.403 +  show "convex (closed_segment 0 z)"
   3.404 +    by (rule convex_segment [of 0 z])
   3.405 +  next
   3.406 +    fix k x
   3.407 +    show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
   3.408 +            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
   3.409 +            (at x within closed_segment 0 z)"
   3.410 +      apply (auto simp: power_Suc)
   3.411 +      apply (intro derivative_eq_intros | simp)+
   3.412 +      done
   3.413 +  next
   3.414 +    fix x
   3.415 +    assume "x \<in> closed_segment 0 z"
   3.416 +    then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
   3.417 +      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   3.418 +  next
   3.419 +    show "0 \<in> closed_segment 0 z"
   3.420 +      by (auto simp: closed_segment_def)
   3.421 +  next
   3.422 +    show "z \<in> closed_segment 0 z"
   3.423 +      apply (simp add: closed_segment_def scaleR_conv_of_real)
   3.424 +      using of_real_1 zero_le_one by blast
   3.425 +  qed 
   3.426 +  have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   3.427 +            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   3.428 +    by (auto simp: sin_coeff_def elim!: oddE)
   3.429 +  show ?thesis
   3.430 +    apply (rule order_trans [OF _ *])
   3.431 +    apply (simp add: **)
   3.432 +    done
   3.433 +qed
   3.434 +
   3.435 +lemma Taylor_cos: 
   3.436 +  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
   3.437 +   \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   3.438 +proof -
   3.439 +  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   3.440 +      by arith
   3.441 +  have *: "cmod (cos z -
   3.442 +                 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   3.443 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   3.444 +  proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
   3.445 +simplified])
   3.446 +  show "convex (closed_segment 0 z)"
   3.447 +    by (rule convex_segment [of 0 z])
   3.448 +  next
   3.449 +    fix k x
   3.450 +    assume "x \<in> closed_segment 0 z" "k \<le> n"
   3.451 +    show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
   3.452 +            (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
   3.453 +             (at x within closed_segment 0 z)"
   3.454 +      apply (auto simp: power_Suc)
   3.455 +      apply (intro derivative_eq_intros | simp)+
   3.456 +      done
   3.457 +  next
   3.458 +    fix x
   3.459 +    assume "x \<in> closed_segment 0 z"
   3.460 +    then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
   3.461 +      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   3.462 +  next
   3.463 +    show "0 \<in> closed_segment 0 z"
   3.464 +      by (auto simp: closed_segment_def)
   3.465 +  next
   3.466 +    show "z \<in> closed_segment 0 z"
   3.467 +      apply (simp add: closed_segment_def scaleR_conv_of_real)
   3.468 +      using of_real_1 zero_le_one by blast
   3.469 +  qed 
   3.470 +  have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   3.471 +            = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   3.472 +    by (auto simp: cos_coeff_def elim!: evenE)
   3.473 +  show ?thesis
   3.474 +    apply (rule order_trans [OF _ *])
   3.475 +    apply (simp add: **)
   3.476 +    done
   3.477 +qed
   3.478 +
   3.479 +end (* of context *)
   3.480 +
   3.481 +subsection{*The argument of a complex number*}
   3.482 +
   3.483 +definition Arg :: "complex \<Rightarrow> real" where
   3.484 + "Arg z \<equiv> if z = 0 then 0
   3.485 +           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
   3.486 +                    z = of_real(norm z) * exp(ii * of_real t)"
   3.487 +
   3.488 +lemma Arg_0 [simp]: "Arg(0) = 0"
   3.489 +  by (simp add: Arg_def)
   3.490 +
   3.491 +lemma Arg_unique_lemma:
   3.492 +  assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
   3.493 +      and z': "z = of_real(norm z) * exp(ii * of_real t')"
   3.494 +      and t:  "0 \<le> t"  "t < 2*pi"
   3.495 +      and t': "0 \<le> t'" "t' < 2*pi"
   3.496 +      and nz: "z \<noteq> 0"
   3.497 +  shows "t' = t"
   3.498 +proof -
   3.499 +  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
   3.500 +    by arith
   3.501 +  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
   3.502 +    by (metis z z')
   3.503 +  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   3.504 +    by (metis nz mult_left_cancel mult_zero_left z)
   3.505 +  then have "sin t' = sin t \<and> cos t' = cos t"
   3.506 +    apply (simp add: exp_Euler sin_of_real cos_of_real)
   3.507 +    by (metis Complex_eq complex.sel)
   3.508 +  then obtain n::int where n: "t' = t + 2 * real n * pi"
   3.509 +    by (auto simp: sin_cos_eq_iff)
   3.510 +  then have "n=0"
   3.511 +    apply (rule_tac z=n in int_cases)
   3.512 +    using t t'
   3.513 +    apply (auto simp: mult_less_0_iff algebra_simps)
   3.514 +    done
   3.515 +  then show "t' = t"
   3.516 +      by (simp add: n)
   3.517 +qed
   3.518 +
   3.519 +lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
   3.520 +proof (cases "z=0")
   3.521 +  case True then show ?thesis
   3.522 +    by (simp add: Arg_def)
   3.523 +next
   3.524 +  case False
   3.525 +  obtain t where t: "0 \<le> t" "t < 2*pi"
   3.526 +             and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   3.527 +    using sincos_total_2pi [OF complex_unit_circle [OF False]]
   3.528 +    by blast
   3.529 +  have z: "z = of_real(norm z) * exp(ii * of_real t)"
   3.530 +    apply (rule complex_eqI)
   3.531 +    using t False ReIm
   3.532 +    apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   3.533 +    done
   3.534 +  show ?thesis
   3.535 +    apply (simp add: Arg_def False)
   3.536 +    apply (rule theI [where a=t])
   3.537 +    using t z False
   3.538 +    apply (auto intro: Arg_unique_lemma)
   3.539 +    done
   3.540 +qed
   3.541 +
   3.542 +
   3.543 +corollary
   3.544 +  shows Arg_ge_0: "0 \<le> Arg z"
   3.545 +    and Arg_lt_2pi: "Arg z < 2*pi"
   3.546 +    and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
   3.547 +  using Arg by auto
   3.548 +
   3.549 +lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
   3.550 +  using Arg [of z] by auto
   3.551 +
   3.552 +lemma Arg_unique: "\<lbrakk>of_real r * exp(ii * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
   3.553 +  apply (rule Arg_unique_lemma [OF _ Arg_eq])
   3.554 +  using Arg [of z]
   3.555 +  apply (auto simp: norm_mult)
   3.556 +  done
   3.557 +
   3.558 +lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
   3.559 +  apply (rule Arg_unique [of "norm z"])
   3.560 +  apply (rule complex_eqI)
   3.561 +  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
   3.562 +  apply auto
   3.563 +  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   3.564 +  apply (metis Re_rcis Im_rcis rcis_def)+
   3.565 +  done
   3.566 +
   3.567 +lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
   3.568 +  apply (cases "z=0", simp)
   3.569 +  apply (rule Arg_unique [of "r * norm z"])
   3.570 +  using Arg
   3.571 +  apply auto
   3.572 +  done
   3.573 +
   3.574 +lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   3.575 +  by (metis Arg_times_of_real mult.commute)
   3.576 +
   3.577 +lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   3.578 +  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   3.579 +
   3.580 +lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
   3.581 +proof (cases "z=0")
   3.582 +  case True then show ?thesis
   3.583 +    by simp
   3.584 +next
   3.585 +  case False
   3.586 +  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   3.587 +    by (metis Arg_eq)
   3.588 +  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
   3.589 +    using False
   3.590 +    by (simp add: zero_le_mult_iff)
   3.591 +  also have "... \<longleftrightarrow> Arg z \<le> pi"
   3.592 +    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
   3.593 +  finally show ?thesis
   3.594 +    by blast
   3.595 +qed
   3.596 +
   3.597 +lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   3.598 +proof (cases "z=0")
   3.599 +  case True then show ?thesis
   3.600 +    by simp
   3.601 +next
   3.602 +  case False
   3.603 +  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   3.604 +    by (metis Arg_eq)
   3.605 +  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
   3.606 +    using False
   3.607 +    by (simp add: zero_less_mult_iff)
   3.608 +  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
   3.609 +    using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
   3.610 +    apply (auto simp: Im_exp)
   3.611 +    using le_less apply fastforce
   3.612 +    using not_le by blast
   3.613 +  finally show ?thesis
   3.614 +    by blast
   3.615 +qed
   3.616 +
   3.617 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
   3.618 +proof (cases "z=0")
   3.619 +  case True then show ?thesis
   3.620 +    by simp
   3.621 +next
   3.622 +  case False
   3.623 +  have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   3.624 +    by (metis Arg_eq)
   3.625 +  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
   3.626 +    using False
   3.627 +    by (simp add: zero_le_mult_iff)
   3.628 +  also have "... \<longleftrightarrow> Arg z = 0"
   3.629 +    apply (auto simp: Re_exp)
   3.630 +    apply (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
   3.631 +    using Arg_eq [of z]
   3.632 +    apply (auto simp: Reals_def)
   3.633 +    done
   3.634 +  finally show ?thesis
   3.635 +    by blast
   3.636 +qed
   3.637 +
   3.638 +lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   3.639 +  by (simp add: Arg_eq_0)
   3.640 +
   3.641 +lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   3.642 +  apply  (cases "z=0", simp)
   3.643 +  using Arg_eq_0 [of "-z"]
   3.644 +  apply (auto simp: complex_is_Real_iff Arg_minus)
   3.645 +  apply (simp add: complex_Re_Im_cancel_iff)
   3.646 +  apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
   3.647 +  done
   3.648 +
   3.649 +lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   3.650 +  using Arg_eq_0 Arg_eq_pi not_le by auto
   3.651 +
   3.652 +lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   3.653 +  apply (cases "z=0", simp)
   3.654 +  apply (rule Arg_unique [of "inverse (norm z)"])
   3.655 +  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
   3.656 +  apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   3.657 +  done
   3.658 +
   3.659 +lemma Arg_eq_iff:
   3.660 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.661 +     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
   3.662 +  using assms Arg_eq [of z] Arg_eq [of w]
   3.663 +  apply auto
   3.664 +  apply (rule_tac x="norm w / norm z" in exI)
   3.665 +  apply (simp add: divide_simps)
   3.666 +  by (metis mult.commute mult.left_commute)
   3.667 +
   3.668 +lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   3.669 +  using complex_is_Real_iff
   3.670 +  apply (simp add: Arg_eq_0)
   3.671 +  apply (auto simp: divide_simps not_sum_power2_lt_zero)
   3.672 +  done
   3.673 +
   3.674 +lemma Arg_divide:
   3.675 +  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   3.676 +    shows "Arg(z / w) = Arg z - Arg w"
   3.677 +  apply (rule Arg_unique [of "norm(z / w)"])
   3.678 +  using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
   3.679 +  apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
   3.680 +  done
   3.681 +
   3.682 +lemma Arg_le_div_sum:
   3.683 +  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   3.684 +    shows "Arg z = Arg w + Arg(z / w)"
   3.685 +  by (simp add: Arg_divide assms)
   3.686 +
   3.687 +lemma Arg_le_div_sum_eq:
   3.688 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.689 +    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
   3.690 +  using assms
   3.691 +  by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
   3.692 +
   3.693 +lemma Arg_diff:
   3.694 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.695 +    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
   3.696 +  using assms
   3.697 +  apply (auto simp: Arg_ge_0 Arg_divide not_le)
   3.698 +  using Arg_divide [of w z] Arg_inverse [of "w/z"]
   3.699 +  apply auto
   3.700 +  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   3.701 +
   3.702 +
   3.703 +lemma Arg_add:
   3.704 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.705 +    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   3.706 +  using assms
   3.707 +  using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
   3.708 +  apply (auto simp: Arg_ge_0 Arg_divide not_le)
   3.709 +  apply (metis Arg_lt_2pi add.commute)
   3.710 +  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   3.711 +  done
   3.712 +
   3.713 +lemma Arg_times:
   3.714 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   3.715 +    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
   3.716 +                            else (Arg w + Arg z) - 2*pi)"
   3.717 +  using Arg_add [OF assms]
   3.718 +  by auto
   3.719 +
   3.720 +lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   3.721 +  apply (cases "z=0", simp)
   3.722 +  apply (rule trans [of _ "Arg(inverse z)"])
   3.723 +  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   3.724 +  apply (metis norm_eq_zero of_real_power zero_less_power2)
   3.725 +  apply (auto simp: of_real_numeral Arg_inverse)
   3.726 +  done
   3.727 +
   3.728 +lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   3.729 +  using Arg_eq_0 Arg_eq_0_pi
   3.730 +  by auto
   3.731 +
   3.732 +lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   3.733 +  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   3.734 +
   3.735  end
     4.1 --- a/src/HOL/Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
     4.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 18 17:23:22 2015 +0000
     4.3 @@ -1303,6 +1303,10 @@
     4.4  lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
     4.5    by (rule ln_unique) (simp add: exp_add)
     4.6  
     4.7 +lemma ln_setprod:
     4.8 +    "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i > 0\<rbrakk> \<Longrightarrow> ln(setprod f I) = setsum (\<lambda>x. ln(f x)) I"
     4.9 +  by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
    4.10 +
    4.11  lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
    4.12    by (rule ln_unique) (simp add: exp_minus)
    4.13  
    4.14 @@ -4153,6 +4157,85 @@
    4.15    by simp
    4.16  
    4.17  
    4.18 +subsection{* Prove Totality of the Trigonometric Functions *}
    4.19 +
    4.20 +lemma arccos_0 [simp]: "arccos 0 = pi/2"
    4.21 +by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One)
    4.22 +
    4.23 +lemma arccos_1 [simp]: "arccos 1 = 0"
    4.24 +  using arccos_cos by force
    4.25 +
    4.26 +lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
    4.27 +  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
    4.28 +      cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
    4.29 +
    4.30 +lemma sincos_total_pi_half:
    4.31 +  assumes "0 \<le> x" "0 \<le> y" "x\<^sup>2 + y\<^sup>2 = 1"
    4.32 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi/2 \<and> x = cos t \<and> y = sin t"
    4.33 +proof -
    4.34 +  have x1: "x \<le> 1"
    4.35 +    using assms
    4.36 +    by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2) 
    4.37 +  moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
    4.38 +    by (auto simp: arccos)
    4.39 +  moreover have "y = sqrt (1 - x\<^sup>2)" using assms
    4.40 +    by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
    4.41 +  ultimately show ?thesis using assms arccos_le_pi2 [of x] 
    4.42 +    by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
    4.43 +qed    
    4.44 +
    4.45 +lemma sincos_total_pi:
    4.46 +  assumes "0 \<le> y" and "x\<^sup>2 + y\<^sup>2 = 1"
    4.47 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi \<and> x = cos t \<and> y = sin t"
    4.48 +proof (cases rule: le_cases [of 0 x])
    4.49 +  case le from sincos_total_pi_half [OF le]  
    4.50 +  show ?thesis
    4.51 +    by (metis pi_ge_two pi_half_le_two add.commute add_le_cancel_left add_mono assms)
    4.52 +next
    4.53 +  case ge 
    4.54 +  then have "0 \<le> -x"
    4.55 +    by simp
    4.56 +  then obtain t where "t\<ge>0" "t \<le> pi/2" "-x = cos t" "y = sin t"
    4.57 +    using sincos_total_pi_half assms
    4.58 +    apply auto
    4.59 +    by (metis `0 \<le> - x` power2_minus)
    4.60 +  then show ?thesis
    4.61 +    by (rule_tac x="pi-t" in exI, auto)
    4.62 +qed    
    4.63 +    
    4.64 +lemma sincos_total_2pi_le:
    4.65 +  assumes "x\<^sup>2 + y\<^sup>2 = 1"
    4.66 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> 2*pi \<and> x = cos t \<and> y = sin t"
    4.67 +proof (cases rule: le_cases [of 0 y])
    4.68 +  case le from sincos_total_pi [OF le]  
    4.69 +  show ?thesis
    4.70 +    by (metis assms le_add_same_cancel1 mult.commute mult_2_right order.trans)
    4.71 +next
    4.72 +  case ge 
    4.73 +  then have "0 \<le> -y"
    4.74 +    by simp
    4.75 +  then obtain t where "t\<ge>0" "t \<le> pi" "x = cos t" "-y = sin t"
    4.76 +    using sincos_total_pi assms
    4.77 +    apply auto
    4.78 +    by (metis `0 \<le> - y` power2_minus)
    4.79 +  then show ?thesis
    4.80 +    by (rule_tac x="2*pi-t" in exI, auto)
    4.81 +qed    
    4.82 +
    4.83 +lemma sincos_total_2pi:
    4.84 +  assumes "x\<^sup>2 + y\<^sup>2 = 1"
    4.85 +    obtains t where "0 \<le> t" "t < 2*pi" "x = cos t" "y = sin t"
    4.86 +proof -
    4.87 +  from sincos_total_2pi_le [OF assms]
    4.88 +  obtain t where t: "0 \<le> t" "t \<le> 2*pi" "x = cos t" "y = sin t"
    4.89 +    by blast
    4.90 +  show ?thesis
    4.91 +    apply (cases "t = 2*pi")
    4.92 +    using t that
    4.93 +    apply force+
    4.94 +    done
    4.95 +qed
    4.96 +
    4.97  subsection {* Machins formula *}
    4.98  
    4.99  lemma arctan_one: "arctan 1 = pi / 4"