# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426775091 0
# Node ID 916c0f6c83e3b5c44fe7ec55ed68f3f0dd0983f2
# Parent  118f4995df8c92de4ae4ec185964a4f5491a1249
New material for complex sin, cos, tan, Ln, also some reorganisation

diff -r 118f4995df8c -r 916c0f6c83e3 NEWS
--- a/NEWS	Thu Mar 19 11:54:20 2015 +0100
+++ b/NEWS	Thu Mar 19 14:24:51 2015 +0000
@@ -83,14 +83,14 @@
   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,
+* New library of properties of the complex transcendental functions sin, cos, tan, 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
   "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
-  then use "of_nat (fact k)".
+  then use "of_nat (fact k)" or "real_of_nat (fact k)".
 
 * removed functions "natfloor" and "natceiling",
   use "nat o floor" and "nat o ceiling" instead.
diff -r 118f4995df8c -r 916c0f6c83e3 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Mar 19 14:24:51 2015 +0000
@@ -959,7 +959,7 @@
       unfolding cos_coeff_def atLeast0LessThan by auto
 
     have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
-    also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)  
+    also have "\<dots> = cos (t + n * pi)" by (simp add: cos_add)
     also have "\<dots> = ?rest" by auto
     finally have "cos t * (- 1) ^ n = ?rest" .
     moreover
@@ -1029,7 +1029,7 @@
   { fix n
     have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
     have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
-      unfolding F by auto } 
+      unfolding F by auto }
   note f_eq = this
   from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
     OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
@@ -1046,7 +1046,7 @@
   hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   have "0 < x * x" using `0 < x` by simp
 
-  { fix x::real and n 
+  { fix x::real and n
     have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
     = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * x ^ i)" (is "?SUM = _")
     proof -
@@ -1354,7 +1354,7 @@
       by auto
 
     have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
-      using cos_monotone_0_pi'[OF lx_0 lx pi_x]
+      using cos_monotone_0_pi_le[OF lx_0 lx pi_x]
       by (simp only: real_of_int_minus
         cos_minus mult_minus_left) simp
     also have "\<dots> \<le> (ub_cos prec ?lx)"
@@ -1386,7 +1386,7 @@
     have "(lb_cos prec ?ux) \<le> cos ?ux"
       using lb_cos[OF ux_0 pi_ux] by simp
     also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
-      using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
+      using cos_monotone_0_pi_le[OF x_ge_0 ux pi_ux]
       by (simp only: real_of_int_minus
         cos_minus mult_minus_left) simp
     finally have "(lb_cos prec ?ux) \<le> cos x"
@@ -1505,7 +1505,7 @@
       have "cos x = cos (x + (-k) * (2 * pi) + (1 :: int) * (2 * pi))"
         unfolding cos_periodic_int ..
       also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
-        using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
+        using cos_monotone_0_pi_le[OF lx_0 lx_le_x pi_x]
         by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
           mult_minus_left mult_1_left) simp
       also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
@@ -1535,7 +1535,7 @@
 proof -
   { fix n
     have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
-    have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto 
+    have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto
   } note f_eq = this
 
   note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
@@ -2022,7 +2022,7 @@
   hence "0 \<le> bl" by (simp add: bitlen_def bl_def)
   show ?thesis
   proof (cases "0 \<le> e")
-    case True 
+    case True
     thus ?thesis
       unfolding bl_def[symmetric] using `0 < real m` `0 \<le> bl`
       apply (simp add: ln_mult)
@@ -3234,7 +3234,7 @@
 qed
 
 lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
-  using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat 
+  using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat
   by presburger
 
 lemma approx_tse:
diff -r 118f4995df8c -r 916c0f6c83e3 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Mar 19 14:24:51 2015 +0000
@@ -156,104 +156,12 @@
 
 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)
-
-
-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)
-
-lemma cos_one_2pi: 
-    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
-    (is "?lhs = ?rhs")
-proof
-  assume "cos(x) = 1"
-  then have "sin x = 0"
-    by (simp add: cos_one_sin_zero)
-  then show ?rhs
-  proof (simp only: sin_zero_iff, elim exE disjE conjE)
-    fix n::nat
-    assume n: "even n" "x = real n * (pi/2)"
-    then obtain m where m: "n = 2 * m"
-      using dvdE by blast
-    then have me: "even m" using `?lhs` n
-      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
-    show ?rhs
-      using m me n
-      by (auto simp: field_simps elim!: evenE)
-  next    
-    fix n::nat
-    assume n: "even n" "x = - (real n * (pi/2))"
-    then obtain m where m: "n = 2 * m"
-      using dvdE by blast
-    then have me: "even m" using `?lhs` n
-      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
-    show ?rhs
-      using m me n
-      by (auto simp: field_simps elim!: evenE)
-  qed
-next
-  assume "?rhs"
-  then show "cos x = 1"
-    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
-qed
-
-lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
-  apply auto  --{*FIXME simproc bug*}
-  apply (auto simp: cos_one_2pi)
-  apply (metis real_of_int_of_nat_eq)
-  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
-  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
-
-lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
-  using sin_squared_eq real_sqrt_unique by fastforce
-
-lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
-  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
-
-lemma cos_treble_cos: 
-  fixes x :: "'a::{real_normed_field,banach}"
-  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
-proof -
-  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
-    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
-  have "cos(3 * x) = cos(2*x + x)"
-    by simp
-  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
-    apply (simp only: cos_add cos_double sin_double)
-    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
-    done
-  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)
@@ -667,6 +575,13 @@
 
 end (* of context *)
 
+text{*32-bit Approximation to e*}
+lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
+  using Taylor_exp [of 1 14] exp_le
+  apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
+  apply (simp only: pos_le_divide_eq [symmetric], linarith)
+  done
+
 subsection{*The argument of a complex number*}
 
 definition Arg :: "complex \<Rightarrow> real" where
@@ -888,7 +803,6 @@
   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)"
@@ -921,4 +835,470 @@
 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)
 
+
+subsection{*Analytic properties of tangent function*}
+
+lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
+  by (simp add: cnj_cos cnj_sin tan_def)
+
+lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
+  unfolding complex_differentiable_def
+  using DERIV_tan by blast
+
+lemma complex_differentiable_within_tan: "~(cos z = 0)
+         \<Longrightarrow> tan complex_differentiable (at z within s)"
+  using complex_differentiable_at_tan complex_differentiable_at_within by blast
+
+lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
+  using continuous_at_imp_continuous_within isCont_tan by blast
+
+lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
+  by (simp add: continuous_at_imp_continuous_on)
+
+lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
+  by (simp add: complex_differentiable_within_tan holomorphic_on_def)
+
+
+subsection{*Complex logarithms (the conventional principal value)*}
+
+definition Ln where
+   "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+
+lemma
+  assumes "z \<noteq> 0"
+    shows exp_Ln [simp]: "exp(Ln z) = z"
+      and mpi_less_Im_Ln: "-pi < Im(Ln z)"
+      and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
+proof -
+  obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
+    using complex_unimodular_polar [of "z / (norm z)"] assms
+    by (auto simp: norm_divide divide_simps)
+  obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
+    using sincos_principal_value [of "\<psi>"] assms
+    by (auto simp: norm_divide divide_simps)
+  have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
+    apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
+    using z assms \<phi>
+    apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
+    done
+  then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
+    by auto
+qed
+
+lemma Ln_exp [simp]:
+  assumes "-pi < Im(z)" "Im(z) \<le> pi"
+    shows "Ln(exp z) = z"
+  apply (rule exp_complex_eqI)
+  using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
+  apply auto
+  done
+
+lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
+  by (metis exp_Ln)
+
+lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
+  using Ln_exp by blast
+
+lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
+by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+
+lemma exists_complex_root:
+  fixes a :: complex
+  shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
+  apply (cases "a=0", simp)
+  apply (rule_tac x= "exp(Ln(a) / n)" in exI)
+  apply (auto simp: exp_of_nat_mult [symmetric])
+  done
+
+subsection{*Derivative of Ln away from the branch cut*}
+
+lemma
+  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
+    shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
+      and Im_Ln_less_pi:           "Im (Ln z) < pi"
+proof -
+  have znz: "z \<noteq> 0"
+    using assms by auto
+  then show *: "Im (Ln z) < pi" using assms
+    by (metis exp_Ln Im_Ln_le_pi Im_exp Re_exp abs_of_nonneg cmod_eq_Re cos_pi mult.right_neutral mult_minus_right mult_zero_right neg_less_0_iff_less norm_exp_eq_Re not_less not_less_iff_gr_or_eq sin_pi)
+  show "(Ln has_field_derivative inverse(z)) (at z)"
+    apply (rule has_complex_derivative_inverse_strong_x
+              [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
+    using znz *
+    apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
+    apply (metis DERIV_exp exp_Ln)
+    apply (metis mpi_less_Im_Ln)
+    done
+qed
+
+declare has_field_derivative_Ln [derivative_intros]
+declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
+
+lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
+  using complex_differentiable_def has_field_derivative_Ln by blast
+
+lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
+         \<Longrightarrow> Ln complex_differentiable (at z within s)"
+  using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
+
+lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
+  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
+
+lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
+  using continuous_at_Ln continuous_at_imp_continuous_within by blast
+
+lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
+  by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
+
+lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
+  by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
+
+
+subsection{*Relation to Real Logarithm*}
+
+lemma ln_of_real:
+  assumes "0 < z"
+    shows "Ln(of_real z) = of_real(ln z)"
+proof -
+  have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
+    by (simp add: exp_of_real)
+  also have "... = of_real(ln z)"
+    using assms
+    by (subst Ln_exp) auto
+  finally show ?thesis
+    using assms by simp
+qed
+
+
+subsection{*Quadrant-type results for Ln*}
+
+lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
+  using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
+  by simp
+
+lemma Re_Ln_pos_lt:
+  assumes "z \<noteq> 0"
+    shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
+proof -
+  { fix w
+    assume "w = Ln z"
+    then have w: "Im w \<le> pi" "- pi < Im w"
+      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
+      by auto
+    then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
+      apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
+      using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
+      apply (simp add: abs_if split: split_if_asm)
+      apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
+               less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
+               mult_numeral_1_right)
+      done
+  }
+  then show ?thesis using assms
+    by auto
+qed
+
+lemma Re_Ln_pos_le:
+  assumes "z \<noteq> 0"
+    shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
+proof -
+  { fix w
+    assume "w = Ln z"
+    then have w: "Im w \<le> pi" "- pi < Im w"
+      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
+      by auto
+    then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
+      apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
+      using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
+      apply (auto simp: abs_if split: split_if_asm)
+      done
+  }
+  then show ?thesis using assms
+    by auto
+qed
+
+lemma Im_Ln_pos_lt:
+  assumes "z \<noteq> 0"
+    shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
+proof -
+  { fix w
+    assume "w = Ln z"
+    then have w: "Im w \<le> pi" "- pi < Im w"
+      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
+      by auto
+    then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
+      using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
+      apply (auto simp: Im_exp zero_less_mult_iff)
+      using less_linear apply fastforce
+      using less_linear apply fastforce
+      done
+  }
+  then show ?thesis using assms
+    by auto
+qed
+
+lemma Im_Ln_pos_le:
+  assumes "z \<noteq> 0"
+    shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
+proof -
+  { fix w
+    assume "w = Ln z"
+    then have w: "Im w \<le> pi" "- pi < Im w"
+      using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
+      by auto
+    then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
+      using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
+      apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
+      apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
+      done }
+  then show ?thesis using assms
+    by auto
+qed
+
+lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
+  by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
+
+lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
+  by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
+
+lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
+  by (metis exp_Ln Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt Re_complex_of_real add.commute add.left_neutral
+       complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
+
+lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
+  by (metis Im_Ln_eq_0 Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt add.right_neutral complex_eq mult_zero_right not_less not_less_iff_gr_or_eq of_real_0)
+
+
+subsection{*More Properties of Ln*}
+
+lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
+  apply (cases "z=0", auto)
+  apply (rule exp_complex_eqI)
+  apply (auto simp: abs_if split: split_if_asm)
+  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
+  apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
+  by (metis exp_Ln exp_cnj)
+
+lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
+  apply (cases "z=0", auto)
+  apply (rule exp_complex_eqI)
+  using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
+  apply (auto simp: abs_if exp_minus split: split_if_asm)
+  apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
+               inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
+  done
+
+lemma Ln_1 [simp]: "Ln(1) = 0"
+proof -
+  have "Ln (exp 0) = 0"
+    by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
+  then show ?thesis
+    by simp
+qed
+
+lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
+  apply (rule exp_complex_eqI)
+  using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
+  apply (auto simp: abs_if)
+  done
+
+lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
+  using Ln_exp [of "ii * (of_real pi/2)"]
+  unfolding exp_Euler
+  by simp
+
+lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
+proof -
+  have  "Ln(-ii) = Ln(1/ii)"
+    by simp
+  also have "... = - (Ln ii)"
+    by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
+  also have "... = - (ii * pi/2)"
+    by (simp add: Ln_ii)
+  finally show ?thesis .
+qed
+
+lemma Ln_times:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+    shows "Ln(w * z) =
+                (if Im(Ln w + Ln z) \<le> -pi then
+                  (Ln(w) + Ln(z)) + ii * of_real(2*pi)
+                else if Im(Ln w + Ln z) > pi then
+                  (Ln(w) + Ln(z)) - ii * of_real(2*pi)
+                else Ln(w) + Ln(z))"
+  using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
+  using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
+  by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
+
+lemma Ln_times_simple:
+    "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
+         \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
+  by (simp add: Ln_times)
+
+lemma Ln_minus:
+  assumes "z \<noteq> 0"
+    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
+                     then Ln(z) + ii * pi
+                     else Ln(z) - ii * pi)" (is "_ = ?rhs")
+  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
+    by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
+
+lemma Ln_inverse_if:
+  assumes "z \<noteq> 0"
+    shows "Ln (inverse z) =
+            (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
+             then -(Ln z)
+             else -(Ln z) + \<i> * 2 * complex_of_real pi)"
+proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
+  case True then show ?thesis
+    by (simp add: Ln_inverse)
+next
+  case False
+  then have z: "Im z = 0" "Re z < 0"
+    using assms
+    apply auto
+    by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
+  have "Ln(inverse z) = Ln(- (inverse (-z)))"
+    by simp
+  also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
+    using assms z
+    apply (simp add: Ln_minus)
+    apply (simp add: field_simps)
+    done
+  also have "... = - Ln (- z) + \<i> * complex_of_real pi"
+    apply (subst Ln_inverse)
+    using z assms by auto
+  also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
+    apply (subst Ln_minus [OF assms])
+    using assms z
+    apply simp
+    done
+  finally show ?thesis
+    using assms z
+    by simp
+qed
+
+lemma Ln_times_ii:
+  assumes "z \<noteq> 0"
+    shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
+                          then Ln(z) + ii * of_real pi/2
+                          else Ln(z) - ii * of_real(3 * pi/2))"
+  using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
+        Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
+  by (auto simp: of_real_numeral Ln_times)
+
+
+subsection{*Relation between Square Root and exp/ln, hence its derivative*}
+
+lemma csqrt_exp_Ln:
+  assumes "z \<noteq> 0"
+    shows "csqrt z = exp(Ln(z) / 2)"
+proof -
+  have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
+    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
+  also have "... = z"
+    using assms exp_Ln by blast
+  finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
+    by simp
+  also have "... = exp (Ln z / 2)"
+    apply (subst csqrt_square)
+    using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
+    apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
+    done
+  finally show ?thesis using assms csqrt_square
+    by simp
+qed
+
+lemma csqrt_inverse:
+  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
+    shows "csqrt (inverse z) = inverse (csqrt z)"
+proof (cases "z=0", simp)
+  assume "z \<noteq> 0 "
+  then show ?thesis
+    using assms
+    by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
+qed
+
+lemma cnj_csqrt:
+  assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
+    shows "cnj(csqrt z) = csqrt(cnj z)"
+proof (cases "z=0", simp)
+  assume z: "z \<noteq> 0"
+  then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
+    using assms cnj.code complex_cnj_zero_iff by fastforce
+  then show ?thesis
+   using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
+qed
+
+lemma has_field_derivative_csqrt:
+  assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
+    shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
+proof -
+  have z: "z \<noteq> 0"
+    using assms by auto
+  then have *: "inverse z = inverse (2*z) * 2"
+    by (simp add: divide_simps)
+  show ?thesis
+    apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
+    apply (intro derivative_eq_intros | simp add: assms)+
+    apply (rule *)
+    using z
+    apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
+    apply (metis power2_csqrt power2_eq_square)
+    apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
+    done
+qed
+
+lemma complex_differentiable_at_csqrt:
+    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
+  using complex_differentiable_def has_field_derivative_csqrt by blast
+
+lemma complex_differentiable_within_csqrt:
+    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
+  using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
+
+lemma continuous_at_csqrt:
+    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
+  by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
+
+lemma continuous_within_csqrt:
+    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
+  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
+
+lemma continuous_on_csqrt [continuous_intros]:
+    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
+  by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
+
+lemma holomorphic_on_csqrt:
+    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
+  by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
+
+lemma continuous_within_closed_nontrivial:
+    "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
+  using open_Compl
+  by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
+
+lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
+  using closed_halfspace_Re_ge
+  by (simp add: closed_Int closed_complex_Reals)
+
+lemma continuous_within_csqrt_posreal:
+    "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
+proof (cases "Im z = 0 --> 0 < Re(z)")
+  case True then show ?thesis
+    by (blast intro: continuous_within_csqrt)
+next
+  case False
+  then have "Im z = 0" "Re z < 0 \<or> z = 0"
+    using False cnj.code complex_cnj_zero_iff by auto force
+  then show ?thesis
+    apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
+    apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
+    apply (rule_tac x="e^2" in exI)
+    apply (auto simp: Reals_def)
+by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+qed
+
+
 end
diff -r 118f4995df8c -r 916c0f6c83e3 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 19 11:54:20 2015 +0100
+++ b/src/HOL/Transcendental.thy	Thu Mar 19 14:24:51 2015 +0000
@@ -3391,7 +3391,7 @@
   thus ?thesis by auto
 qed
 
-lemma cos_monotone_0_pi':
+lemma cos_monotone_0_pi_le:
   assumes "0 \<le> y" and "y \<le> x" and "x \<le> pi"
   shows "cos x \<le> cos y"
 proof (cases "y < x")
@@ -3427,16 +3427,19 @@
   thus ?thesis by auto
 qed
 
-lemma sin_monotone_2pi':
+lemma sin_monotone_2pi:
+  assumes "- (pi/2) \<le> y" and "y < x" and "x \<le> pi/2"
+  shows "sin y < sin x"
+    apply (simp add: sin_cos_eq)
+    apply (rule cos_monotone_0_pi)
+    using assms
+    apply auto
+    done
+
+lemma sin_monotone_2pi_le:
   assumes "- (pi / 2) \<le> y" and "y \<le> x" and "x \<le> pi / 2"
   shows "sin y \<le> sin x"
-proof -
-  have "0 \<le> y + pi / 2" and "y + pi / 2 \<le> x + pi / 2" and "x + pi /2 \<le> pi"
-    using pi_ge_two and assms by auto
-  from cos_monotone_0_pi'[OF this] show ?thesis
-    unfolding minus_sin_cos_eq[symmetric]
-    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
-qed
+  by (metis assms le_less sin_monotone_2pi)
 
 lemma sin_x_le_x:
   fixes x::real assumes x: "x \<ge> 0" shows "sin x \<le> x"
@@ -3468,6 +3471,191 @@
   by (auto simp: abs_real_def)
 
 
+subsection {* More Corollaries about Sine and Cosine *}
+
+lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
+proof -
+  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
+    by (auto simp: algebra_simps sin_add)
+  thus ?thesis
+    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
+                  mult.commute [of pi])
+qed
+
+lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
+  by (cases "even n") (simp_all add: cos_double mult.assoc)
+
+lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
+  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
+  apply (subst cos_add, simp)
+  done
+
+lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
+  by (auto simp: mult.assoc sin_double)
+
+lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
+  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
+  apply (subst sin_add, simp)
+  done
+
+lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
+by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
+
+lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
+  by (auto intro!: derivative_eq_intros)
+
+lemma sin_zero_norm_cos_one:
+  fixes x :: "'a::{real_normed_field,banach}"
+  assumes "sin x = 0" shows "norm (cos x) = 1"
+  using sin_cos_squared_add [of x, unfolded assms]
+  by (simp add: square_norm_one)
+
+lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
+  using sin_zero_norm_cos_one by fastforce
+
+lemma cos_one_sin_zero:
+  fixes x :: "'a::{real_normed_field,banach}"
+  assumes "cos x = 1" shows "sin x = 0"
+  using sin_cos_squared_add [of x, unfolded assms]
+  by simp
+
+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)
+
+lemma cos_one_2pi: 
+    "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
+    (is "?lhs = ?rhs")
+proof
+  assume "cos(x) = 1"
+  then have "sin x = 0"
+    by (simp add: cos_one_sin_zero)
+  then show ?rhs
+  proof (simp only: sin_zero_iff, elim exE disjE conjE)
+    fix n::nat
+    assume n: "even n" "x = real n * (pi/2)"
+    then obtain m where m: "n = 2 * m"
+      using dvdE by blast
+    then have me: "even m" using `?lhs` n
+      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
+    show ?rhs
+      using m me n
+      by (auto simp: field_simps elim!: evenE)
+  next    
+    fix n::nat
+    assume n: "even n" "x = - (real n * (pi/2))"
+    then obtain m where m: "n = 2 * m"
+      using dvdE by blast
+    then have me: "even m" using `?lhs` n
+      by (auto simp: field_simps) (metis one_neq_neg_one  power_minus_odd power_one)
+    show ?rhs
+      using m me n
+      by (auto simp: field_simps elim!: evenE)
+  qed
+next
+  assume "?rhs"
+  then show "cos x = 1"
+    by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
+qed
+
+lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
+  apply auto  --{*FIXME simproc bug*}
+  apply (auto simp: cos_one_2pi)
+  apply (metis real_of_int_of_nat_eq)
+  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
+  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
+
+lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
+  using sin_squared_eq real_sqrt_unique by fastforce
+
+lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
+  by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
+
+lemma cos_treble_cos: 
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
+proof -
+  have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
+    by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
+  have "cos(3 * x) = cos(2*x + x)"
+    by simp
+  also have "... = 4 * cos(x) ^ 3 - 3 * cos x"
+    apply (simp only: cos_add cos_double sin_double)
+    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
+    done
+  finally show ?thesis .
+qed
+
+lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
+proof -
+  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
+  have nonneg: "0 \<le> ?c"
+    by (simp add: cos_ge_zero)
+  have "0 = cos (pi / 4 + pi / 4)"
+    by simp
+  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
+    by (simp only: cos_add power2_eq_square)
+  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
+    by (simp add: sin_squared_eq)
+  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
+    by (simp add: power_divide)
+  thus ?thesis
+    using nonneg by (rule power2_eq_imp_eq) simp
+qed
+
+lemma cos_30: "cos (pi / 6) = sqrt 3/2"
+proof -
+  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
+  have pos_c: "0 < ?c"
+    by (rule cos_gt_zero, simp, simp)
+  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
+    by simp
+  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
+    by (simp only: cos_add sin_add)
+  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
+    by (simp add: algebra_simps power2_eq_square)
+  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
+    using pos_c by (simp add: sin_squared_eq power_divide)
+  thus ?thesis
+    using pos_c [THEN order_less_imp_le]
+    by (rule power2_eq_imp_eq) simp
+qed
+
+lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
+  by (simp add: sin_cos_eq cos_45)
+
+lemma sin_60: "sin (pi / 3) = sqrt 3/2"
+  by (simp add: sin_cos_eq cos_30)
+
+lemma cos_60: "cos (pi / 3) = 1 / 2"
+  apply (rule power2_eq_imp_eq)
+  apply (simp add: cos_squared_eq sin_60 power_divide)
+  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
+  done
+
+lemma sin_30: "sin (pi / 6) = 1 / 2"
+  by (simp add: sin_cos_eq cos_60)
+
+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
+
+
 subsection {* Tangent *}
 
 definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
@@ -3528,6 +3716,15 @@
   unfolding tan_def sin_double cos_double sin_squared_eq
   by (simp add: power2_eq_square)
 
+lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
+  unfolding tan_def by (simp add: sin_30 cos_30)
+
+lemma tan_45: "tan (pi / 4) = 1"
+  unfolding tan_def by (simp add: sin_45 cos_45)
+
+lemma tan_60: "tan (pi / 3) = sqrt 3"
+  unfolding tan_def by (simp add: sin_60 cos_60)
+
 lemma DERIV_tan [simp]:
   fixes x :: "'a::{real_normed_field,banach}"
   shows "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
@@ -3705,9 +3902,48 @@
 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
   using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
 
+lemma tan_minus_45: "tan (-(pi/4)) = -1"
+  unfolding tan_def by (simp add: sin_45 cos_45)
+
+lemma tan_diff:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows
+     "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x - y) \<noteq> 0\<rbrakk>
+      \<Longrightarrow> tan(x - y) = (tan(x) - tan(y))/(1 + tan(x) * tan(y))"
+  using tan_add [of x "-y"]
+  by simp
+
+
+lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
+  using less_eq_real_def tan_gt_zero by auto
+
+lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
+  using cos_gt_zero_pi [of x]
+  by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+
+lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
+  using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
+  by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+
+lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
+  using less_eq_real_def tan_monotone by auto
+
+lemma tan_mono_lt_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
+         \<Longrightarrow> (tan(x) < tan(y) \<longleftrightarrow> x < y)"
+  using tan_monotone' by blast
+
+lemma tan_mono_le_eq: "-(pi/2) < x ==> x < pi/2 ==> -(pi/2) < y ==> y < pi/2
+         \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
+  by (meson tan_mono_le not_le tan_monotone)
+
+lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
+  using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
+  by (auto simp: abs_if split: split_if_asm)
+
+lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
+  by (simp add: tan_def sin_diff cos_diff)
 
 subsection {* Inverse Trigonometric Functions *}
-text{*STILL DEFINED FOR THE REALS ONLY*}
 
 definition arcsin :: "real => real"
   where "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
@@ -3820,6 +4056,12 @@
   apply (rule power_mono, simp, simp)
   done
 
+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 arctan [simp]: "- (pi/2) < arctan y  & arctan y < pi/2 & tan (arctan y) = y"
   unfolding arctan_def by (rule theI' [OF tan_total])
 
@@ -4049,124 +4291,34 @@
   by (intro tendsto_minus tendsto_arctan_at_top)
 
 
-subsection {* More Theorems about Sin and Cos *}
-
-lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
-proof -
-  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
-  have nonneg: "0 \<le> ?c"
-    by (simp add: cos_ge_zero)
-  have "0 = cos (pi / 4 + pi / 4)"
-    by simp
-  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
-    by (simp only: cos_add power2_eq_square)
-  also have "\<dots> = 2 * ?c\<^sup>2 - 1"
-    by (simp add: sin_squared_eq)
-  finally have "?c\<^sup>2 = (sqrt 2 / 2)\<^sup>2"
-    by (simp add: power_divide)
-  thus ?thesis
-    using nonneg by (rule power2_eq_imp_eq) simp
-qed
-
-lemma cos_30: "cos (pi / 6) = sqrt 3/2"
-proof -
-  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
-  have pos_c: "0 < ?c"
-    by (rule cos_gt_zero, simp, simp)
-  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
-    by simp
-  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
-    by (simp only: cos_add sin_add)
-  also have "\<dots> = ?c * (?c\<^sup>2 - 3 * ?s\<^sup>2)"
-    by (simp add: algebra_simps power2_eq_square)
-  finally have "?c\<^sup>2 = (sqrt 3/2)\<^sup>2"
-    using pos_c by (simp add: sin_squared_eq power_divide)
-  thus ?thesis
-    using pos_c [THEN order_less_imp_le]
-    by (rule power2_eq_imp_eq) simp
-qed
-
-lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
-  by (simp add: sin_cos_eq cos_45)
-
-lemma sin_60: "sin (pi / 3) = sqrt 3/2"
-  by (simp add: sin_cos_eq cos_30)
-
-lemma cos_60: "cos (pi / 3) = 1 / 2"
-  apply (rule power2_eq_imp_eq)
-  apply (simp add: cos_squared_eq sin_60 power_divide)
-  apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
-  done
-
-lemma sin_30: "sin (pi / 6) = 1 / 2"
-  by (simp add: sin_cos_eq cos_60)
-
-lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
-  unfolding tan_def by (simp add: sin_30 cos_30)
-
-lemma tan_45: "tan (pi / 4) = 1"
-  unfolding tan_def by (simp add: sin_45 cos_45)
-
-lemma tan_60: "tan (pi / 3) = sqrt 3"
-  unfolding tan_def by (simp add: sin_60 cos_60)
-
-lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
-proof -
-  have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
-    by (auto simp: algebra_simps sin_add)
-  thus ?thesis
-    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
-                  mult.commute [of pi])
-qed
-
-lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
-  by (cases "even n") (simp_all add: cos_double mult.assoc)
-
-lemma cos_3over2_pi [simp]: "cos (3/2*pi) = 0"
-  apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
-  apply (subst cos_add, simp)
-  done
-
-lemma sin_2npi [simp]: "sin (2 * real (n::nat) * pi) = 0"
-  by (auto simp: mult.assoc sin_double)
-
-lemma sin_3over2_pi [simp]: "sin (3/2*pi) = - 1"
-  apply (subgoal_tac "sin (pi + pi/2) = - 1", simp)
-  apply (subst sin_add, simp)
-  done
-
-lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
-
-lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
-  by (auto intro!: derivative_eq_intros)
-
-lemma sin_zero_norm_cos_one:
-  fixes x :: "'a::{real_normed_field,banach}"
-  assumes "sin x = 0" shows "norm (cos x) = 1"
-  using sin_cos_squared_add [of x, unfolded assms]
-  by (simp add: square_norm_one)
-
-lemma sin_zero_abs_cos_one: "sin x = 0 \<Longrightarrow> \<bar>cos x\<bar> = (1::real)"
-  using sin_zero_norm_cos_one by fastforce
-
-lemma cos_one_sin_zero:
-  fixes x :: "'a::{real_normed_field,banach}"
-  assumes "cos x = 1" shows "sin x = 0"
-  using sin_cos_squared_add [of x, unfolded assms]
-  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 sin_mono_less_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
+         \<Longrightarrow> (sin(x) < sin(y) \<longleftrightarrow> x < y)"
+by (metis not_less_iff_gr_or_eq sin_monotone_2pi)
+
+lemma sin_mono_le_eq: "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2; -(pi/2) \<le> y; y \<le> pi/2\<rbrakk>
+         \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
+by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
+
+lemma sin_inj_pi: "-(pi/2) \<le> x ==> x \<le> pi/2 ==>
+         -(pi/2) \<le> y ==> y \<le> pi/2 ==> sin(x) = sin(y) \<Longrightarrow> x = y"
+by (metis arcsin_sin)
+
+lemma cos_mono_lt_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
+         \<Longrightarrow> (cos(x) < cos(y) \<longleftrightarrow> y < x)"
+by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)
+
+lemma cos_mono_le_eq: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi
+         \<Longrightarrow> (cos(x) \<le> cos(y) \<longleftrightarrow> y \<le> x)"
+  by (metis arccos_cos cos_monotone_0_pi_le eq_iff linear)
+
+lemma cos_inj_pi: "0 \<le> x ==> x \<le> pi ==> 0 \<le> y ==> y \<le> pi ==> cos(x) = cos(y)
+         \<Longrightarrow> x = y"
+by (metis arccos_cos)
 
 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'
+  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi_le
       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: