# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426699402 0
# Node ID ddae5727c5a961d9cd0ea30dfb71f17f516b8e41
# Parent  390476a0ef1377efde6dae54ad64f45970a28be3
new HOL Light material about exp, sin, cos

diff -r 390476a0ef13 -r ddae5727c5a9 NEWS
--- a/NEWS	Wed Mar 18 14:55:17 2015 +0000
+++ b/NEWS	Wed Mar 18 17:23:22 2015 +0000
@@ -79,10 +79,13 @@
 * New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
   single-step rewriting with subterm selection based on patterns.
 
-* the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
+* The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
   type, so in particular on "real" and "complex" uniformly.
   Minor INCOMPATIBILITY: type constraints may be needed.
 
+* New library of properties of the complex transcendental functions sin, cos, exp,
+  ported from HOL Light.
+
 * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
   numeric types including nat, int, real and complex. INCOMPATIBILITY:
   an expression such as "fact 3 = 6" may require a type constraint, and the combination
diff -r 390476a0ef13 -r ddae5727c5a9 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Mar 18 14:55:17 2015 +0000
+++ b/src/HOL/Complex.thy	Wed Mar 18 17:23:22 2015 +0000
@@ -612,7 +612,11 @@
     done
 qed
 
-subsection{*Finally! Polar Form for Complex Numbers*}
+subsection{*Polar Form for Complex Numbers*}
+
+lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
+  using sincos_total_2pi [of "Re z" "Im z"]
+  by auto (metis cmod_power2 complex_eq power_one)
 
 subsubsection {* $\cos \theta + i \sin \theta$ *}
 
@@ -724,11 +728,17 @@
 lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
   unfolding Exp_eq_polar by simp
 
+lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
+  by (simp add: norm_complex_def)
+
+lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
+  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
+
 lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
-apply (insert rcis_Ex [of z])
-apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
-apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
-done
+  apply (insert rcis_Ex [of z])
+  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
+  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
+  done
 
 lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
   by (simp add: Exp_eq_polar complex_eq_iff)
@@ -865,6 +875,10 @@
     by auto
 qed
 
+lemma csqrt_unique:
+    "w^2 = z \<Longrightarrow> (0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w) \<Longrightarrow> csqrt z = w"
+  by (auto simp: csqrt_square)
+
 lemma csqrt_minus [simp]:
   assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
   shows "csqrt (- x) = \<i> * csqrt x"
@@ -877,7 +891,7 @@
       by (auto simp add: Re_csqrt simp del: csqrt.simps)
   qed
   also have "(\<i> * csqrt x)^2 = - x"
-    by (simp add: power2_csqrt power_mult_distrib)
+    by (simp add: power_mult_distrib)
   finally show ?thesis .
 qed
 
diff -r 390476a0ef13 -r ddae5727c5a9 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Mar 18 17:23:22 2015 +0000
@@ -1,4 +1,4 @@
-(*  Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno
+(*  Author: John Harrison
     Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
 *)
 
@@ -8,6 +8,7 @@
 imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
 begin
 
+subsection{*The Exponential Function is Differentiable and Continuous*}
 
 lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
   using DERIV_exp complex_differentiable_def by blast
@@ -28,8 +29,6 @@
 lemma holomorphic_on_exp: "exp holomorphic_on s"
   by (simp add: complex_differentiable_within_exp holomorphic_on_def)
 
-
-
 subsection{*Euler and de Moivre formulas.*}
 
 text{*The sine series times @{term i}*}
@@ -158,7 +157,8 @@
 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
 
-(* Now more relatively easy consequences.*)
+
+subsection {* More Corollaries about Sine and Cosine *}
 
 lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
   by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
@@ -226,4 +226,699 @@
   finally show ?thesis .
 qed
 
+  
+subsection{*More on the Polar Representation of Complex Numbers*}
+
+lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
+  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
+
+lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
+  by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
+
+lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
+  by (simp add: cos_one_2pi_int)
+
+lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
+  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
+
+lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
+  apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
+  apply (auto simp: field_simps frac_lt_1)
+  apply (simp_all add: frac_def divide_simps)
+  apply (simp_all add: add_divide_distrib diff_divide_distrib)
+  apply (simp_all add: sin_diff cos_diff mult.assoc [symmetric] cos_integer_2pi sin_integer_2pi)
+  done
+
+lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
+  by (simp add: exp_add exp_Euler exp_of_real)
+
+
+
+lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
+apply auto
+apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
+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)
+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)
+
+lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
+                (is "?lhs = ?rhs")
+proof -
+  have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
+    by (simp add: exp_diff)
+  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
+    by (simp add: exp_eq_1)
+  also have "... \<longleftrightarrow> ?rhs"
+    by (auto simp: algebra_simps intro!: complex_eqI)
+  finally show ?thesis .
+qed
+
+lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
+  by (auto simp: exp_eq abs_mult)
+
+lemma exp_integer_2pi: 
+  assumes "n \<in> Ints"
+  shows "exp((2 * n * pi) * ii) = 1"
+proof -
+  have "exp((2 * n * pi) * ii) = exp 0"
+    using assms
+    by (simp only: Ints_def exp_eq) auto
+  also have "... = 1"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
+proof -
+  { assume "sin y = sin x" "cos y = cos x"
+    then have "cos (y-x) = 1"
+      using cos_add [of y "-x"] by simp
+    then have "\<exists>n::int. y-x = real n * 2 * pi"
+      using cos_one_2pi_int by blast }
+  then show ?thesis
+  apply (auto simp: sin_add cos_add)
+  apply (metis add.commute diff_add_cancel mult.commute)
+  done
+qed
+
+lemma exp_i_ne_1: 
+  assumes "0 < x" "x < 2*pi"
+  shows "exp(\<i> * of_real x) \<noteq> 1"
+proof 
+  assume "exp (\<i> * of_real x) = 1"
+  then have "exp (\<i> * of_real x) = exp 0"
+    by simp
+  then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
+    by (simp only: Ints_def exp_eq) auto
+  then have  "of_real x = (of_int (2 * n) * pi)"
+    by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
+  then have  "x = (of_int (2 * n) * pi)"
+    by simp
+  then show False using assms
+    by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
+qed
+
+lemma sin_eq_0: 
+  fixes z::complex
+  shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
+  by (simp add: sin_exp_eq exp_eq of_real_numeral)
+
+lemma cos_eq_0: 
+  fixes z::complex
+  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
+  using sin_eq_0 [of "z - of_real pi/2"]
+  by (simp add: sin_diff algebra_simps)
+
+lemma cos_eq_1: 
+  fixes z::complex
+  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
+proof -
+  have "cos z = cos (2*(z/2))"
+    by simp
+  also have "... = 1 - 2 * sin (z/2) ^ 2"
+    by (simp only: cos_double_sin)
+  finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
+    by simp
+  show ?thesis
+    by (auto simp: sin_eq_0 of_real_numeral)
+qed  
+
+lemma csin_eq_1:
+  fixes z::complex
+  shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
+  using cos_eq_1 [of "z - of_real pi/2"]
+  by (simp add: cos_diff algebra_simps)
+
+lemma csin_eq_minus1:
+  fixes z::complex
+  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
+        (is "_ = ?rhs")
+proof -
+  have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
+    by (simp add: equation_minus_iff)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
+    by (simp only: csin_eq_1)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
+    apply (rule iff_exI)
+    by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
+  also have "... = ?rhs"
+    apply (auto simp: of_real_numeral)
+    apply (rule_tac [2] x="-(x+1)" in exI)
+    apply (rule_tac x="-(x+1)" in exI)
+    apply (simp_all add: algebra_simps)
+    done
+  finally show ?thesis .
+qed  
+
+lemma ccos_eq_minus1: 
+  fixes z::complex
+  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
+  using csin_eq_1 [of "z - of_real pi/2"]
+  apply (simp add: sin_diff)
+  apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
+  done       
+
+lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
+                (is "_ = ?rhs")
+proof -
+  have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
+    by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
+    by (simp only: csin_eq_1)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
+    apply (rule iff_exI)
+    apply (auto simp: algebra_simps of_real_numeral)
+    apply (rule injD [OF inj_of_real [where 'a = complex]])
+    apply (auto simp: of_real_numeral)
+    done
+  also have "... = ?rhs"
+    by (auto simp: algebra_simps)
+  finally show ?thesis .
+qed  
+
+lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
+proof -
+  have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
+    by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
+    by (simp only: csin_eq_minus1)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
+    apply (rule iff_exI)
+    apply (auto simp: algebra_simps)
+    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
+    done
+  also have "... = ?rhs"
+    by (auto simp: algebra_simps)
+  finally show ?thesis .
+qed  
+
+lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
+                      (is "_ = ?rhs")
+proof -
+  have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
+    by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
+    by (simp only: ccos_eq_minus1)
+  also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
+    apply (rule iff_exI)
+    apply (auto simp: algebra_simps)
+    apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
+    done
+  also have "... = ?rhs"
+    by (auto simp: algebra_simps)
+  finally show ?thesis .
+qed  
+
+lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
+  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
+  using cos_double_sin [of "t/2"]
+  apply (simp add: real_sqrt_mult)
+  done
+
+lemma sinh_complex:
+  fixes z :: complex
+  shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
+  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
+
+lemma sin_ii_times:
+  fixes z :: complex
+  shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
+  using sinh_complex by auto
+
+lemma sinh_real:
+  fixes x :: real
+  shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
+  by (simp add: exp_of_real sin_ii_times of_real_numeral)
+
+lemma cosh_complex:
+  fixes z :: complex
+  shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
+  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
+
+lemma cosh_real:
+  fixes x :: real
+  shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
+  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
+
+lemmas cos_ii_times = cosh_complex [symmetric]
+
+lemma norm_cos_squared: 
+    "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
+  apply (cases z)
+  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
+  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
+  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
+  apply (simp add: sin_squared_eq)
+  apply (simp add: power2_eq_square algebra_simps divide_simps)
+  done
+
+lemma norm_sin_squared:
+    "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
+  apply (cases z)
+  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
+  apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
+  apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
+  apply (simp add: cos_squared_eq)
+  apply (simp add: power2_eq_square algebra_simps divide_simps)
+  done 
+
+lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
+  using abs_Im_le_cmod linear order_trans by fastforce
+
+lemma norm_cos_le: 
+  fixes z::complex
+  shows "norm(cos z) \<le> exp(norm z)"
+proof -
+  have "Im z \<le> cmod z"
+    using abs_Im_le_cmod abs_le_D1 by auto
+  with exp_uminus_Im show ?thesis
+    apply (simp add: cos_exp_eq norm_divide)
+    apply (rule order_trans [OF norm_triangle_ineq], simp)
+    apply (metis add_mono exp_le_cancel_iff mult_2_right)
+    done
+qed
+
+lemma norm_cos_plus1_le: 
+  fixes z::complex
+  shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
+proof -
+  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"
+      by arith
+  have *: "Im z \<le> cmod z"
+    using abs_Im_le_cmod abs_le_D1 by auto
+  have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
+    by (simp add: norm_add_rule_thm)
+  have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
+    by (simp add: cos_exp_eq)
+  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
+    by (simp add: field_simps)
+  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
+    by (simp add: norm_divide)
+  finally show ?thesis
+    apply (rule ssubst, simp)
+    apply (rule order_trans [OF triangle3], simp)
+    using exp_uminus_Im *
+    apply (auto intro: mono)
+    done
+qed
+
+subsection{* Taylor series for complex exponential, sine and cosine.*}
+
+context 
+begin
+
+declare power_Suc [simp del]
+
+lemma Taylor_exp: 
+  "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
+proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
+  show "convex (closed_segment 0 z)"
+    by (rule convex_segment [of 0 z])
+next
+  fix k x
+  assume "x \<in> closed_segment 0 z" "k \<le> n"
+  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
+    using DERIV_exp DERIV_subset by blast
+next
+  fix x
+  assume "x \<in> closed_segment 0 z"
+  then show "Re x \<le> \<bar>Re z\<bar>"
+    apply (auto simp: closed_segment_def scaleR_conv_of_real)
+    by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
+next
+  show "0 \<in> closed_segment 0 z"
+    by (auto simp: closed_segment_def)
+next
+  show "z \<in> closed_segment 0 z"
+    apply (simp add: closed_segment_def scaleR_conv_of_real)
+    using of_real_1 zero_le_one by blast
+qed 
+
+lemma 
+  assumes "0 \<le> u" "u \<le> 1"
+  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
+    and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
+proof -
+  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
+    by arith
+  show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
+    apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
+    apply (rule order_trans [OF norm_triangle_ineq4])
+    apply (rule mono)
+    apply (auto simp: abs_if mult_left_le_one_le)
+    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
+    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
+    done
+  show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
+    apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
+    apply (rule order_trans [OF norm_triangle_ineq])
+    apply (rule mono)
+    apply (auto simp: abs_if mult_left_le_one_le)
+    apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
+    apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
+    done
+qed
+    
+lemma Taylor_sin: 
+  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
+   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
+proof -
+  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
+      by arith
+  have *: "cmod (sin z -
+                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
+           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
+  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,
+simplified])
+  show "convex (closed_segment 0 z)"
+    by (rule convex_segment [of 0 z])
+  next
+    fix k x
+    show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
+            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
+            (at x within closed_segment 0 z)"
+      apply (auto simp: power_Suc)
+      apply (intro derivative_eq_intros | simp)+
+      done
+  next
+    fix x
+    assume "x \<in> closed_segment 0 z"
+    then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
+      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
+  next
+    show "0 \<in> closed_segment 0 z"
+      by (auto simp: closed_segment_def)
+  next
+    show "z \<in> closed_segment 0 z"
+      apply (simp add: closed_segment_def scaleR_conv_of_real)
+      using of_real_1 zero_le_one by blast
+  qed 
+  have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
+            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
+    by (auto simp: sin_coeff_def elim!: oddE)
+  show ?thesis
+    apply (rule order_trans [OF _ *])
+    apply (simp add: **)
+    done
+qed
+
+lemma Taylor_cos: 
+  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
+   \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
+proof -
+  have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
+      by arith
+  have *: "cmod (cos z -
+                 (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
+           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
+  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,
+simplified])
+  show "convex (closed_segment 0 z)"
+    by (rule convex_segment [of 0 z])
+  next
+    fix k x
+    assume "x \<in> closed_segment 0 z" "k \<le> n"
+    show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
+            (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
+             (at x within closed_segment 0 z)"
+      apply (auto simp: power_Suc)
+      apply (intro derivative_eq_intros | simp)+
+      done
+  next
+    fix x
+    assume "x \<in> closed_segment 0 z"
+    then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
+      by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
+  next
+    show "0 \<in> closed_segment 0 z"
+      by (auto simp: closed_segment_def)
+  next
+    show "z \<in> closed_segment 0 z"
+      apply (simp add: closed_segment_def scaleR_conv_of_real)
+      using of_real_1 zero_le_one by blast
+  qed 
+  have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
+            = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
+    by (auto simp: cos_coeff_def elim!: evenE)
+  show ?thesis
+    apply (rule order_trans [OF _ *])
+    apply (simp add: **)
+    done
+qed
+
+end (* of context *)
+
+subsection{*The argument of a complex number*}
+
+definition Arg :: "complex \<Rightarrow> real" where
+ "Arg z \<equiv> if z = 0 then 0
+           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
+                    z = of_real(norm z) * exp(ii * of_real t)"
+
+lemma Arg_0 [simp]: "Arg(0) = 0"
+  by (simp add: Arg_def)
+
+lemma Arg_unique_lemma:
+  assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
+      and z': "z = of_real(norm z) * exp(ii * of_real t')"
+      and t:  "0 \<le> t"  "t < 2*pi"
+      and t': "0 \<le> t'" "t' < 2*pi"
+      and nz: "z \<noteq> 0"
+  shows "t' = t"
+proof -
+  have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
+    by arith
+  have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
+    by (metis z z')
+  then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
+    by (metis nz mult_left_cancel mult_zero_left z)
+  then have "sin t' = sin t \<and> cos t' = cos t"
+    apply (simp add: exp_Euler sin_of_real cos_of_real)
+    by (metis Complex_eq complex.sel)
+  then obtain n::int where n: "t' = t + 2 * real n * pi"
+    by (auto simp: sin_cos_eq_iff)
+  then have "n=0"
+    apply (rule_tac z=n in int_cases)
+    using t t'
+    apply (auto simp: mult_less_0_iff algebra_simps)
+    done
+  then show "t' = t"
+      by (simp add: n)
+qed
+
+lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
+proof (cases "z=0")
+  case True then show ?thesis
+    by (simp add: Arg_def)
+next
+  case False
+  obtain t where t: "0 \<le> t" "t < 2*pi"
+             and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
+    using sincos_total_2pi [OF complex_unit_circle [OF False]]
+    by blast
+  have z: "z = of_real(norm z) * exp(ii * of_real t)"
+    apply (rule complex_eqI)
+    using t False ReIm
+    apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
+    done
+  show ?thesis
+    apply (simp add: Arg_def False)
+    apply (rule theI [where a=t])
+    using t z False
+    apply (auto intro: Arg_unique_lemma)
+    done
+qed
+
+
+corollary
+  shows Arg_ge_0: "0 \<le> Arg z"
+    and Arg_lt_2pi: "Arg z < 2*pi"
+    and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
+  using Arg by auto
+
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
+  using Arg [of z] by auto
+
+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"
+  apply (rule Arg_unique_lemma [OF _ Arg_eq])
+  using Arg [of z]
+  apply (auto simp: norm_mult)
+  done
+
+lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
+  apply (rule Arg_unique [of "norm z"])
+  apply (rule complex_eqI)
+  using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
+  apply auto
+  apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
+  apply (metis Re_rcis Im_rcis rcis_def)+
+  done
+
+lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
+  apply (cases "z=0", simp)
+  apply (rule Arg_unique [of "r * norm z"])
+  using Arg
+  apply auto
+  done
+
+lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
+  by (metis Arg_times_of_real mult.commute)
+
+lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
+  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+
+lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
+proof (cases "z=0")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
+    by (metis Arg_eq)
+  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
+    using False
+    by (simp add: zero_le_mult_iff)
+  also have "... \<longleftrightarrow> Arg z \<le> pi"
+    by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
+  finally show ?thesis
+    by blast
+qed
+
+lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
+proof (cases "z=0")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
+    by (metis Arg_eq)
+  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
+    using False
+    by (simp add: zero_less_mult_iff)
+  also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
+    using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
+    apply (auto simp: Im_exp)
+    using le_less apply fastforce
+    using not_le by blast
+  finally show ?thesis
+    by blast
+qed
+
+lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
+proof (cases "z=0")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  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)))"
+    by (metis Arg_eq)
+  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+    using False
+    by (simp add: zero_le_mult_iff)
+  also have "... \<longleftrightarrow> Arg z = 0"
+    apply (auto simp: Re_exp)
+    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)
+    using Arg_eq [of z]
+    apply (auto simp: Reals_def)
+    done
+  finally show ?thesis
+    by blast
+qed
+
+lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
+  by (simp add: Arg_eq_0)
+
+lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
+  apply  (cases "z=0", simp)
+  using Arg_eq_0 [of "-z"]
+  apply (auto simp: complex_is_Real_iff Arg_minus)
+  apply (simp add: complex_Re_Im_cancel_iff)
+  apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
+  done
+
+lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
+  using Arg_eq_0 Arg_eq_pi not_le by auto
+
+lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+  apply (cases "z=0", simp)
+  apply (rule Arg_unique [of "inverse (norm z)"])
+  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
+  apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
+  done
+
+lemma Arg_eq_iff:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
+  using assms Arg_eq [of z] Arg_eq [of w]
+  apply auto
+  apply (rule_tac x="norm w / norm z" in exI)
+  apply (simp add: divide_simps)
+  by (metis mult.commute mult.left_commute)
+
+lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
+  using complex_is_Real_iff
+  apply (simp add: Arg_eq_0)
+  apply (auto simp: divide_simps not_sum_power2_lt_zero)
+  done
+
+lemma Arg_divide:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
+    shows "Arg(z / w) = Arg z - Arg w"
+  apply (rule Arg_unique [of "norm(z / w)"])
+  using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
+  apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
+  done
+
+lemma Arg_le_div_sum:
+  assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
+    shows "Arg z = Arg w + Arg(z / w)"
+  by (simp add: Arg_divide assms)
+
+lemma Arg_le_div_sum_eq:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+    shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
+  using assms
+  by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
+
+lemma Arg_diff:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+    shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
+  using assms
+  apply (auto simp: Arg_ge_0 Arg_divide not_le)
+  using Arg_divide [of w z] Arg_inverse [of "w/z"]
+  apply auto
+  by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
+
+
+lemma Arg_add:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+    shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
+  using assms
+  using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
+  apply (auto simp: Arg_ge_0 Arg_divide not_le)
+  apply (metis Arg_lt_2pi add.commute)
+  apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
+  done
+
+lemma Arg_times:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+    shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
+                            else (Arg w + Arg z) - 2*pi)"
+  using Arg_add [OF assms]
+  by auto
+
+lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
+  apply (cases "z=0", simp)
+  apply (rule trans [of _ "Arg(inverse z)"])
+  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
+  apply (metis norm_eq_zero of_real_power zero_less_power2)
+  apply (auto simp: of_real_numeral Arg_inverse)
+  done
+
+lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
+  using Arg_eq_0 Arg_eq_0_pi
+  by auto
+
+lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
+  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
+
 end
diff -r 390476a0ef13 -r ddae5727c5a9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
+++ b/src/HOL/Transcendental.thy	Wed Mar 18 17:23:22 2015 +0000
@@ -1303,6 +1303,10 @@
 lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   by (rule ln_unique) (simp add: exp_add)
 
+lemma ln_setprod:
+    "\<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"
+  by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
+
 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   by (rule ln_unique) (simp add: exp_minus)
 
@@ -4153,6 +4157,85 @@
   by simp
 
 
+subsection{* Prove Totality of the Trigonometric Functions *}
+
+lemma arccos_0 [simp]: "arccos 0 = pi/2"
+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)
+
+lemma arccos_1 [simp]: "arccos 1 = 0"
+  using arccos_cos by force
+
+lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
+  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
+      cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
+
+lemma sincos_total_pi_half:
+  assumes "0 \<le> x" "0 \<le> y" "x\<^sup>2 + y\<^sup>2 = 1"
+    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi/2 \<and> x = cos t \<and> y = sin t"
+proof -
+  have x1: "x \<le> 1"
+    using assms
+    by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2) 
+  moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
+    by (auto simp: arccos)
+  moreover have "y = sqrt (1 - x\<^sup>2)" using assms
+    by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
+  ultimately show ?thesis using assms arccos_le_pi2 [of x] 
+    by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
+qed    
+
+lemma sincos_total_pi:
+  assumes "0 \<le> y" and "x\<^sup>2 + y\<^sup>2 = 1"
+    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi \<and> x = cos t \<and> y = sin t"
+proof (cases rule: le_cases [of 0 x])
+  case le from sincos_total_pi_half [OF le]  
+  show ?thesis
+    by (metis pi_ge_two pi_half_le_two add.commute add_le_cancel_left add_mono assms)
+next
+  case ge 
+  then have "0 \<le> -x"
+    by simp
+  then obtain t where "t\<ge>0" "t \<le> pi/2" "-x = cos t" "y = sin t"
+    using sincos_total_pi_half assms
+    apply auto
+    by (metis `0 \<le> - x` power2_minus)
+  then show ?thesis
+    by (rule_tac x="pi-t" in exI, auto)
+qed    
+    
+lemma sincos_total_2pi_le:
+  assumes "x\<^sup>2 + y\<^sup>2 = 1"
+    shows "\<exists>t. 0 \<le> t \<and> t \<le> 2*pi \<and> x = cos t \<and> y = sin t"
+proof (cases rule: le_cases [of 0 y])
+  case le from sincos_total_pi [OF le]  
+  show ?thesis
+    by (metis assms le_add_same_cancel1 mult.commute mult_2_right order.trans)
+next
+  case ge 
+  then have "0 \<le> -y"
+    by simp
+  then obtain t where "t\<ge>0" "t \<le> pi" "x = cos t" "-y = sin t"
+    using sincos_total_pi assms
+    apply auto
+    by (metis `0 \<le> - y` power2_minus)
+  then show ?thesis
+    by (rule_tac x="2*pi-t" in exI, auto)
+qed    
+
+lemma sincos_total_2pi:
+  assumes "x\<^sup>2 + y\<^sup>2 = 1"
+    obtains t where "0 \<le> t" "t < 2*pi" "x = cos t" "y = sin t"
+proof -
+  from sincos_total_2pi_le [OF assms]
+  obtain t where t: "0 \<le> t" "t \<le> 2*pi" "x = cos t" "y = sin t"
+    by blast
+  show ?thesis
+    apply (cases "t = 2*pi")
+    using t that
+    apply force+
+    done
+qed
+
 subsection {* Machins formula *}
 
 lemma arctan_one: "arctan 1 = pi / 4"