HOL Light Libraries for complex Arctan, Arcsin, Arccos
authorpaulson <lp15@cam.ac.uk>
Wed Apr 01 14:48:38 2015 +0100 (2015-04-01)
changeset 5987068d6b6aa4450
parent 59869 3b5b53eb78ba
child 59871 e1a49ac9c537
HOL Light Libraries for complex Arctan, Arcsin, Arccos
NEWS
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
     1.1 --- a/NEWS	Wed Apr 01 14:08:17 2015 +0100
     1.2 +++ b/NEWS	Wed Apr 01 14:48:38 2015 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4    Minor INCOMPATIBILITY: type constraints may be needed.
     1.5  
     1.6  * New library of properties of the complex transcendental functions sin, cos, tan, exp,
     1.7 -  ported from HOL Light.
     1.8 +  Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
     1.9  
    1.10  * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
    1.11    numeric types including nat, int, real and complex. INCOMPATIBILITY:
     2.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Apr 01 14:08:17 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Wed Apr 01 14:48:38 2015 +0100
     2.3 @@ -8,6 +8,39 @@
     2.4  imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
     2.5  begin
     2.6  
     2.7 +
     2.8 +lemma cmod_add_real_less:
     2.9 +  assumes "Im z \<noteq> 0" "r\<noteq>0"
    2.10 +    shows "cmod (z + r) < cmod z + abs r"
    2.11 +proof (cases z)
    2.12 +  case (Complex x y)
    2.13 +  have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
    2.14 +    apply (rule real_less_rsqrt)
    2.15 +    using assms
    2.16 +    apply (simp add: Complex power2_eq_square)
    2.17 +    using not_real_square_gt_zero by blast
    2.18 +  then show ?thesis using assms Complex
    2.19 +    apply (auto simp: cmod_def)
    2.20 +    apply (rule power2_less_imp_less, auto)
    2.21 +    apply (simp add: power2_eq_square field_simps)
    2.22 +    done
    2.23 +qed
    2.24 +
    2.25 +lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + abs x"
    2.26 +  using cmod_add_real_less [of z "-x"]
    2.27 +  by simp
    2.28 +
    2.29 +lemma cmod_square_less_1_plus:
    2.30 +  assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
    2.31 +    shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
    2.32 +  using assms
    2.33 +  apply (cases "Im z = 0 \<or> Re z = 0")
    2.34 +  using abs_square_less_1
    2.35 +    apply (force simp add: Re_power2 Im_power2 cmod_def)
    2.36 +  using cmod_diff_real_less [of "1 - z\<^sup>2" "1"]
    2.37 +  apply (simp add: norm_power Im_power2)
    2.38 +  done
    2.39 +
    2.40  subsection{*The Exponential Function is Differentiable and Continuous*}
    2.41  
    2.42  lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
    2.43 @@ -1324,5 +1357,824 @@
    2.44  by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
    2.45  qed
    2.46  
    2.47 +subsection{*Complex arctangent*}
    2.48 +
    2.49 +text{*branch cut gives standard bounds in real case.*}
    2.50 +
    2.51 +definition Arctan :: "complex \<Rightarrow> complex" where
    2.52 +    "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
    2.53 +
    2.54 +lemma Arctan_0 [simp]: "Arctan 0 = 0"
    2.55 +  by (simp add: Arctan_def)
    2.56 +
    2.57 +lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
    2.58 +  by (auto simp: Im_complex_div_eq_0 algebra_simps)
    2.59 +
    2.60 +lemma Re_complex_div_lemma: "0 < Re((1 - \<i>*z) / (1 + \<i>*z)) \<longleftrightarrow> norm z < 1"
    2.61 +  by (simp add: Re_complex_div_gt_0 algebra_simps cmod_def power2_eq_square)
    2.62 +
    2.63 +lemma tan_Arctan:
    2.64 +  assumes "z\<^sup>2 \<noteq> -1"
    2.65 +    shows [simp]:"tan(Arctan z) = z"
    2.66 +proof -
    2.67 +  have "1 + \<i>*z \<noteq> 0"
    2.68 +    by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
    2.69 +  moreover
    2.70 +  have "1 - \<i>*z \<noteq> 0"
    2.71 +    by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq)
    2.72 +  ultimately
    2.73 +  show ?thesis
    2.74 +    by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric]
    2.75 +                  divide_simps power2_eq_square [symmetric])
    2.76 +qed
    2.77 +
    2.78 +lemma Arctan_tan [simp]:
    2.79 +  assumes "\<bar>Re z\<bar> < pi/2"
    2.80 +    shows "Arctan(tan z) = z"
    2.81 +proof -
    2.82 +  have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
    2.83 +    by (case_tac n rule: int_cases) (auto simp: abs_mult)
    2.84 +  have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
    2.85 +    by (metis distrib_right exp_add mult_2)
    2.86 +  also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
    2.87 +    using cis_conv_exp cis_pi by auto
    2.88 +  also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
    2.89 +    by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
    2.90 +  also have "... \<longleftrightarrow> Re(\<i>*2*z - \<i>*pi) = 0 \<and> (\<exists>n::int. Im(\<i>*2*z - \<i>*pi) = of_int (2 * n) * pi)"
    2.91 +    by (simp add: exp_eq_1)
    2.92 +  also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
    2.93 +    by (simp add: algebra_simps)
    2.94 +  also have "... \<longleftrightarrow> False"
    2.95 +    using assms ge_pi2
    2.96 +    apply (auto simp: algebra_simps)
    2.97 +    by (metis abs_mult_pos not_less not_real_of_nat_less_zero real_of_nat_numeral)
    2.98 +  finally have *: "exp (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 0"
    2.99 +    by (auto simp: add.commute minus_unique)
   2.100 +  show ?thesis
   2.101 +    using assms *
   2.102 +    apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
   2.103 +                     ii_times_eq_iff power2_eq_square [symmetric])
   2.104 +    apply (rule Ln_unique)
   2.105 +    apply (auto simp: divide_simps exp_minus)
   2.106 +    apply (simp add: algebra_simps exp_double [symmetric])
   2.107 +    done
   2.108 +qed
   2.109 +
   2.110 +lemma
   2.111 +  assumes "Re z = 0 \<Longrightarrow> abs(Im z) < 1"
   2.112 +  shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
   2.113 +    and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
   2.114 +proof -
   2.115 +  have nz0: "1 + \<i>*z \<noteq> 0"
   2.116 +    using assms
   2.117 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
   2.118 +              less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
   2.119 +  have "z \<noteq> -\<i>" using assms
   2.120 +    by auto
   2.121 +  then have zz: "1 + z * z \<noteq> 0"
   2.122 +    by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
   2.123 +  have nz1: "1 - \<i>*z \<noteq> 0"
   2.124 +    using assms by (force simp add: ii_times_eq_iff)
   2.125 +  have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
   2.126 +    using assms
   2.127 +    by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
   2.128 +              less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2))
   2.129 +  have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
   2.130 +    using nz1 nz2 by auto
   2.131 +  have *: "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
   2.132 +    apply (simp add: divide_complex_def)
   2.133 +    apply (simp add: divide_simps split: split_if_asm)
   2.134 +    using assms
   2.135 +    apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
   2.136 +    done
   2.137 +  show "abs(Re(Arctan z)) < pi/2"
   2.138 +    unfolding Arctan_def divide_complex_def
   2.139 +    using mpi_less_Im_Ln [OF nzi]
   2.140 +    by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
   2.141 +  show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
   2.142 +    unfolding Arctan_def scaleR_conv_of_real
   2.143 +    apply (rule DERIV_cong)
   2.144 +    apply (intro derivative_eq_intros | simp add: nz0 *)+
   2.145 +    using nz0 nz1 zz
   2.146 +    apply (simp add: divide_simps power2_eq_square)
   2.147 +    apply (auto simp: algebra_simps)
   2.148 +    done
   2.149 +qed
   2.150 +
   2.151 +lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
   2.152 +  using has_field_derivative_Arctan
   2.153 +  by (auto simp: complex_differentiable_def)
   2.154 +
   2.155 +lemma complex_differentiable_within_Arctan:
   2.156 +    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
   2.157 +  using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
   2.158 +
   2.159 +declare has_field_derivative_Arctan [derivative_intros]
   2.160 +declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
   2.161 +
   2.162 +lemma continuous_at_Arctan:
   2.163 +    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
   2.164 +  by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
   2.165 +
   2.166 +lemma continuous_within_Arctan:
   2.167 +    "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
   2.168 +  using continuous_at_Arctan continuous_at_imp_continuous_within by blast
   2.169 +
   2.170 +lemma continuous_on_Arctan [continuous_intros]:
   2.171 +    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
   2.172 +  by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
   2.173 +
   2.174 +lemma holomorphic_on_Arctan:
   2.175 +    "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
   2.176 +  by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
   2.177 +
   2.178 +
   2.179 +subsection {*Real arctangent*}
   2.180 +
   2.181 +lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   2.182 +  by simp
   2.183 +
   2.184 +lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
   2.185 +  by (simp add: complex_norm_eq_1_exp)
   2.186 +
   2.187 +lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
   2.188 +  unfolding Arctan_def divide_complex_def
   2.189 +  apply (simp add: complex_eq_iff)
   2.190 +  apply (rule norm_exp_imaginary)
   2.191 +  apply (subst exp_Ln, auto)
   2.192 +  apply (simp_all add: cmod_def complex_eq_iff)
   2.193 +  apply (auto simp: divide_simps)
   2.194 +  apply (metis power_one realpow_two_sum_zero_iff zero_neq_one, algebra)
   2.195 +  done
   2.196 +
   2.197 +lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
   2.198 +proof (rule arctan_unique)
   2.199 +  show "- (pi / 2) < Re (Arctan (complex_of_real x))"
   2.200 +    apply (simp add: Arctan_def)
   2.201 +    apply (rule Im_Ln_less_pi)
   2.202 +    apply (auto simp: Im_complex_div_lemma)
   2.203 +    done
   2.204 +next
   2.205 +  have *: " (1 - \<i>*x) / (1 + \<i>*x) \<noteq> 0"
   2.206 +    by (simp add: divide_simps) ( simp add: complex_eq_iff)
   2.207 +  show "Re (Arctan (complex_of_real x)) < pi / 2"
   2.208 +    using mpi_less_Im_Ln [OF *]
   2.209 +    by (simp add: Arctan_def)
   2.210 +next
   2.211 +  have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
   2.212 +    apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos)
   2.213 +    apply (simp add: field_simps)
   2.214 +    by (simp add: power2_eq_square)
   2.215 +  also have "... = x"
   2.216 +    apply (subst tan_Arctan, auto)
   2.217 +    by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one)
   2.218 +  finally show "tan (Re (Arctan (complex_of_real x))) = x" .
   2.219 +qed
   2.220 +
   2.221 +lemma Arctan_of_real: "Arctan (of_real x) = of_real (arctan x)"
   2.222 +  unfolding arctan_eq_Re_Arctan divide_complex_def
   2.223 +  by (simp add: complex_eq_iff)
   2.224 +
   2.225 +lemma Arctan_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Arctan z \<in> \<real>"
   2.226 +  by (metis Reals_cases Reals_of_real Arctan_of_real)
   2.227 +
   2.228 +declare arctan_one [simp]
   2.229 +
   2.230 +lemma arctan_less_pi4_pos: "x < 1 \<Longrightarrow> arctan x < pi/4"
   2.231 +  by (metis arctan_less_iff arctan_one)
   2.232 +
   2.233 +lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
   2.234 +  by (metis arctan_less_iff arctan_minus arctan_one)
   2.235 +
   2.236 +lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
   2.237 +  by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
   2.238 +
   2.239 +lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> pi/4"
   2.240 +  by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
   2.241 +
   2.242 +lemma abs_arctan: "abs(arctan x) = arctan(abs x)"
   2.243 +  by (simp add: abs_if arctan_minus)
   2.244 +
   2.245 +lemma arctan_add_raw:
   2.246 +  assumes "abs(arctan x + arctan y) < pi/2"
   2.247 +    shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
   2.248 +proof (rule arctan_unique [symmetric])
   2.249 +  show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
   2.250 +    using assms by linarith+
   2.251 +  show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
   2.252 +    using cos_gt_zero_pi [OF 12]
   2.253 +    by (simp add: arctan tan_add)
   2.254 +qed
   2.255 +
   2.256 +lemma arctan_inverse:
   2.257 +  assumes "0 < x"
   2.258 +    shows "arctan(inverse x) = pi/2 - arctan x"
   2.259 +proof -
   2.260 +  have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
   2.261 +    by (simp add: arctan)
   2.262 +  also have "... = arctan (tan (pi / 2 - arctan x))"
   2.263 +    by (simp add: tan_cot)
   2.264 +  also have "... = pi/2 - arctan x"
   2.265 +  proof -
   2.266 +    have "0 < pi - arctan x"
   2.267 +    using arctan_ubound [of x] pi_gt_zero by linarith
   2.268 +    with assms show ?thesis
   2.269 +      by (simp add: Transcendental.arctan_tan)
   2.270 +  qed
   2.271 +  finally show ?thesis .
   2.272 +qed
   2.273 +
   2.274 +lemma arctan_add_small:
   2.275 +  assumes "abs(x * y) < 1"
   2.276 +    shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
   2.277 +proof (cases "x = 0 \<or> y = 0")
   2.278 +  case True then show ?thesis
   2.279 +    by auto
   2.280 +next
   2.281 +  case False
   2.282 +  then have *: "\<bar>arctan x\<bar> < pi / 2 - \<bar>arctan y\<bar>" using assms
   2.283 +    apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff)
   2.284 +    apply (simp add: divide_simps abs_mult)
   2.285 +    done
   2.286 +  show ?thesis
   2.287 +    apply (rule arctan_add_raw)
   2.288 +    using * by linarith
   2.289 +qed
   2.290 +
   2.291 +lemma abs_arctan_le:
   2.292 +  fixes x::real shows "abs(arctan x) \<le> abs x"
   2.293 +proof -
   2.294 +  { fix w::complex and z::complex
   2.295 +    assume *: "w \<in> \<real>" "z \<in> \<real>"
   2.296 +    have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
   2.297 +      apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1])
   2.298 +      apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
   2.299 +      apply (force simp add: Reals_def)
   2.300 +      apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
   2.301 +      using * by auto
   2.302 +  }
   2.303 +  then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
   2.304 +    using Reals_0 Reals_of_real by blast
   2.305 +  then show ?thesis
   2.306 +    by (simp add: Arctan_of_real)
   2.307 +qed
   2.308 +
   2.309 +lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
   2.310 +  by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
   2.311 +
   2.312 +lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
   2.313 +  by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
   2.314 +
   2.315 +
   2.316 +subsection{*Inverse Sine*}
   2.317 +
   2.318 +definition Arcsin :: "complex \<Rightarrow> complex" where
   2.319 +   "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
   2.320 +
   2.321 +lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
   2.322 +  using power2_csqrt [of "1 - z\<^sup>2"]
   2.323 +  apply auto
   2.324 +  by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral)
   2.325 +
   2.326 +lemma Arcsin_range_lemma: "abs (Re z) < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
   2.327 +  using Complex.cmod_power2 [of z, symmetric]
   2.328 +  by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
   2.329 +
   2.330 +lemma Re_Arcsin: "Re(Arcsin z) = Im (Ln (\<i> * z + csqrt(1 - z\<^sup>2)))"
   2.331 +  by (simp add: Arcsin_def)
   2.332 +
   2.333 +lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
   2.334 +  by (simp add: Arcsin_def Arcsin_body_lemma)
   2.335 +
   2.336 +lemma isCont_Arcsin:
   2.337 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
   2.338 +    shows "isCont Arcsin z"
   2.339 +proof -
   2.340 +  have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
   2.341 +    using assms
   2.342 +    by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
   2.343 +  have cmz: "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
   2.344 +    by (blast intro: assms cmod_square_less_1_plus)
   2.345 +  show ?thesis
   2.346 +    using assms
   2.347 +    apply (simp add: Arcsin_def)
   2.348 +    apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
   2.349 +    apply (erule rez)
   2.350 +    apply (auto simp: Re_power2 Im_power2 abs_square_less_1 [symmetric] real_less_rsqrt algebra_simps split: split_if_asm)
   2.351 +    apply (simp add: norm_complex_def)
   2.352 +    using cmod_power2 [of z, symmetric] cmz
   2.353 +    apply (simp add: real_less_rsqrt)
   2.354 +    done
   2.355 +qed
   2.356 +
   2.357 +lemma isCont_Arcsin' [simp]:
   2.358 +  shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
   2.359 +  by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
   2.360 +
   2.361 +lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
   2.362 +proof -  
   2.363 +  have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
   2.364 +    by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
   2.365 +  moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
   2.366 +    by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
   2.367 +  ultimately show ?thesis
   2.368 +    apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
   2.369 +    apply (simp add: algebra_simps)
   2.370 +    apply (simp add: power2_eq_square [symmetric] algebra_simps)
   2.371 +    done
   2.372 +qed
   2.373 +
   2.374 +lemma Re_eq_pihalf_lemma:
   2.375 +    "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
   2.376 +      Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
   2.377 +  apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
   2.378 +  by (metis cos_minus cos_pi_half)
   2.379 +
   2.380 +lemma Re_less_pihalf_lemma:
   2.381 +  assumes "\<bar>Re z\<bar> < pi / 2"
   2.382 +    shows "0 < Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
   2.383 +proof -
   2.384 +  have "0 < cos (Re z)" using assms
   2.385 +    using cos_gt_zero_pi by auto
   2.386 +  then show ?thesis
   2.387 +    by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
   2.388 +qed
   2.389 +
   2.390 +lemma Arcsin_sin:
   2.391 +    assumes "\<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)"
   2.392 +      shows "Arcsin(sin z) = z"
   2.393 +proof -
   2.394 +  have "Arcsin(sin z) = - (\<i> * Ln (csqrt (1 - (\<i> * (exp (\<i>*z) - inverse (exp (\<i>*z))))\<^sup>2 / 4) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
   2.395 +    by (simp add: sin_exp_eq Arcsin_def exp_minus)
   2.396 +  also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
   2.397 +    by (simp add: field_simps power2_eq_square)
   2.398 +  also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
   2.399 +    apply (subst csqrt_square)
   2.400 +    using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma
   2.401 +    apply auto
   2.402 +    done
   2.403 +  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
   2.404 +    by (simp add: field_simps power2_eq_square)
   2.405 +  also have "... = z"
   2.406 +    apply (subst Complex_Transcendental.Ln_exp)
   2.407 +    using assms
   2.408 +    apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: split_if_asm)
   2.409 +    done
   2.410 +  finally show ?thesis .
   2.411 +qed
   2.412 +
   2.413 +lemma Arcsin_unique:
   2.414 +    "\<lbrakk>sin z = w; \<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)\<rbrakk> \<Longrightarrow> Arcsin w = z"
   2.415 +  by (metis Arcsin_sin)
   2.416 +
   2.417 +lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
   2.418 +  by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
   2.419 +
   2.420 +lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
   2.421 +  by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half)
   2.422 +
   2.423 +lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
   2.424 +  by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)
   2.425 +
   2.426 +lemma has_field_derivative_Arcsin:
   2.427 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
   2.428 +    shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
   2.429 +proof -
   2.430 +  have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
   2.431 +    using assms
   2.432 +    apply atomize
   2.433 +    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
   2.434 +    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
   2.435 +    by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
   2.436 +  then have "cos (Arcsin z) \<noteq> 0"
   2.437 +    by (metis diff_0_right power_zero_numeral sin_squared_eq)
   2.438 +  then show ?thesis
   2.439 +    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin])
   2.440 +    apply (auto intro: isCont_Arcsin open_ball [of z 1] assms)
   2.441 +    done
   2.442 +qed
   2.443 +
   2.444 +declare has_field_derivative_Arcsin [derivative_intros]
   2.445 +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
   2.446 +
   2.447 +lemma complex_differentiable_at_Arcsin:
   2.448 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
   2.449 +  using complex_differentiable_def has_field_derivative_Arcsin by blast
   2.450 +
   2.451 +lemma complex_differentiable_within_Arcsin:
   2.452 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable (at z within s)"
   2.453 +  using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast
   2.454 +
   2.455 +lemma continuous_within_Arcsin:
   2.456 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
   2.457 +  using continuous_at_imp_continuous_within isCont_Arcsin by blast
   2.458 +
   2.459 +lemma continuous_on_Arcsin [continuous_intros]:
   2.460 +    "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arcsin"
   2.461 +  by (simp add: continuous_at_imp_continuous_on)
   2.462 +
   2.463 +lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
   2.464 +  by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
   2.465 +
   2.466 +
   2.467 +subsection{*Inverse Cosine*}
   2.468 +
   2.469 +definition Arccos :: "complex \<Rightarrow> complex" where
   2.470 +   "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
   2.471 +
   2.472 +lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
   2.473 +  using Arcsin_range_lemma [of "-z"]
   2.474 +  by simp
   2.475 +
   2.476 +lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
   2.477 +  using Arcsin_body_lemma [of z]
   2.478 +  by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
   2.479 +           power2_csqrt power2_eq_square zero_neq_one)
   2.480 +
   2.481 +lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
   2.482 +  by (simp add: Arccos_def)
   2.483 +
   2.484 +lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))"
   2.485 +  by (simp add: Arccos_def Arccos_body_lemma)
   2.486 +
   2.487 +text{*A very tricky argument to find!*}
   2.488 +lemma abs_Re_less_1_preserve:
   2.489 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
   2.490 +    shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
   2.491 +proof (cases "Im z = 0")
   2.492 +  case True
   2.493 +  then show ?thesis
   2.494 +    using assms 
   2.495 +    by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
   2.496 +next
   2.497 +  case False
   2.498 +  have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
   2.499 +    using assms abs_Re_le_cmod [of "1-z\<^sup>2"]
   2.500 +    by (simp add: Re_power2 algebra_simps)
   2.501 +  have "(cmod z)\<^sup>2 - 1 \<noteq> cmod (1 - z\<^sup>2)"
   2.502 +  proof (clarsimp simp add: cmod_def)
   2.503 +    assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 - 1 = sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
   2.504 +    then have "((Re z)\<^sup>2 + (Im z)\<^sup>2 - 1)\<^sup>2 = ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
   2.505 +      by simp
   2.506 +    then show False using False
   2.507 +      by (simp add: power2_eq_square algebra_simps)
   2.508 +  qed
   2.509 +  moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
   2.510 +    apply (subst Imz, simp)
   2.511 +    apply (subst real_sqrt_pow2)
   2.512 +    using abs_Re_le_cmod [of "1-z\<^sup>2"]
   2.513 +    apply (auto simp: Re_power2 field_simps)
   2.514 +    done
   2.515 +  ultimately show ?thesis
   2.516 +    by (simp add: Re_power2 Im_power2 cmod_power2)
   2.517 +qed
   2.518 +
   2.519 +lemma isCont_Arccos:
   2.520 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
   2.521 +    shows "isCont Arccos z"
   2.522 +proof -
   2.523 +  have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
   2.524 +    using assms
   2.525 +    by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
   2.526 +  show ?thesis
   2.527 +    using assms
   2.528 +    apply (simp add: Arccos_def)
   2.529 +    apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
   2.530 +    apply (erule rez)
   2.531 +    apply (blast intro: abs_Re_less_1_preserve)
   2.532 +    done
   2.533 +qed
   2.534 +
   2.535 +lemma isCont_Arccos' [simp]:
   2.536 +  shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arccos (f x)) z"
   2.537 +  by (blast intro: isCont_o2 [OF _ isCont_Arccos])
   2.538 +
   2.539 +lemma cos_Arccos [simp]: "cos(Arccos z) = z"
   2.540 +proof -
   2.541 +  have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
   2.542 +    by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
   2.543 +  moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
   2.544 +    by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
   2.545 +  ultimately show ?thesis
   2.546 +    apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps)
   2.547 +    apply (simp add: power2_eq_square [symmetric])
   2.548 +    done
   2.549 +qed
   2.550 +
   2.551 +lemma Arccos_cos:
   2.552 +    assumes "0 < Re z & Re z < pi \<or>
   2.553 +             Re z = 0 & 0 \<le> Im z \<or>
   2.554 +             Re z = pi & Im z \<le> 0"
   2.555 +      shows "Arccos(cos z) = z"
   2.556 +proof -
   2.557 +  have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
   2.558 +    by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
   2.559 +  have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
   2.560 +    by (simp add: field_simps power2_eq_square)
   2.561 +  then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
   2.562 +                           \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
   2.563 +    by (simp add: cos_exp_eq Arccos_def exp_minus)
   2.564 +  also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
   2.565 +                              \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
   2.566 +    apply (subst csqrt_square)
   2.567 +    using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
   2.568 +    apply (auto simp: * Re_sin Im_sin)
   2.569 +    done
   2.570 +  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
   2.571 +    by (simp add: field_simps power2_eq_square)
   2.572 +  also have "... = z"
   2.573 +    using assms
   2.574 +    apply (subst Complex_Transcendental.Ln_exp, auto)
   2.575 +    done
   2.576 +  finally show ?thesis .
   2.577 +qed
   2.578 +
   2.579 +lemma Arccos_unique:
   2.580 +    "\<lbrakk>cos z = w;
   2.581 +      0 < Re z \<and> Re z < pi \<or>
   2.582 +      Re z = 0 \<and> 0 \<le> Im z \<or>
   2.583 +      Re z = pi \<and> Im z \<le> 0\<rbrakk> \<Longrightarrow> Arccos w = z"
   2.584 +  using Arccos_cos by blast
   2.585 +
   2.586 +lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
   2.587 +  by (rule Arccos_unique) (auto simp: of_real_numeral)
   2.588 +
   2.589 +lemma Arccos_1 [simp]: "Arccos 1 = 0"
   2.590 +  by (rule Arccos_unique) auto
   2.591 +
   2.592 +lemma Arccos_minus1: "Arccos(-1) = pi"
   2.593 +  by (rule Arccos_unique) auto
   2.594 +
   2.595 +lemma has_field_derivative_Arccos:
   2.596 +  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
   2.597 +    shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
   2.598 +proof -
   2.599 +  have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
   2.600 +    using assms
   2.601 +    apply atomize
   2.602 +    apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
   2.603 +    apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
   2.604 +    apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
   2.605 +    done
   2.606 +  then have "- sin (Arccos z) \<noteq> 0"
   2.607 +    by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
   2.608 +  then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
   2.609 +    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos])
   2.610 +    apply (auto intro: isCont_Arccos open_ball [of z 1] assms)
   2.611 +    done
   2.612 +  then show ?thesis
   2.613 +    by simp
   2.614 +qed
   2.615 +
   2.616 +declare has_field_derivative_Arcsin [derivative_intros]
   2.617 +declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
   2.618 +
   2.619 +lemma complex_differentiable_at_Arccos:
   2.620 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
   2.621 +  using complex_differentiable_def has_field_derivative_Arccos by blast
   2.622 +
   2.623 +lemma complex_differentiable_within_Arccos:
   2.624 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable (at z within s)"
   2.625 +  using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast
   2.626 +
   2.627 +lemma continuous_within_Arccos:
   2.628 +    "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
   2.629 +  using continuous_at_imp_continuous_within isCont_Arccos by blast
   2.630 +
   2.631 +lemma continuous_on_Arccos [continuous_intros]:
   2.632 +    "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arccos"
   2.633 +  by (simp add: continuous_at_imp_continuous_on)
   2.634 +
   2.635 +lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
   2.636 +  by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
   2.637 +
   2.638 +
   2.639 +subsection{*Upper and Lower Bounds for Inverse Sine and Cosine*}
   2.640 +
   2.641 +lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
   2.642 +  unfolding Re_Arcsin
   2.643 +  by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
   2.644 +
   2.645 +lemma Arccos_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(Arccos z) \<and> Re(Arccos z) < pi"
   2.646 +  unfolding Re_Arccos
   2.647 +  by (blast intro!: Im_Ln_pos_lt_imp Arccos_range_lemma)
   2.648 +
   2.649 +lemma Re_Arccos_bounds: "-pi < Re(Arccos z) \<and> Re(Arccos z) \<le> pi"
   2.650 +  unfolding Re_Arccos
   2.651 +  by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
   2.652 +
   2.653 +lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
   2.654 +  using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast
   2.655 +
   2.656 +lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   2.657 +  unfolding Re_Arcsin
   2.658 +  by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
   2.659 +
   2.660 +lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
   2.661 +  using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
   2.662 +
   2.663 +
   2.664 +subsection{*Interrelations between Arcsin and Arccos*}
   2.665 +
   2.666 +lemma cos_Arcsin_nonzero:
   2.667 +  assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
   2.668 +proof -
   2.669 +  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
   2.670 +    by (simp add: power_mult_distrib algebra_simps)
   2.671 +  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
   2.672 +  proof
   2.673 +    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
   2.674 +    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
   2.675 +      by simp
   2.676 +    then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
   2.677 +      using eq power2_eq_square by auto
   2.678 +    then show False
   2.679 +      using assms by simp
   2.680 +  qed
   2.681 +  then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
   2.682 +    by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
   2.683 +  then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2"  (*FIXME cancel_numeral_factor*)
   2.684 +    by (metis mult_cancel_left zero_neq_numeral)
   2.685 +  then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
   2.686 +    using assms
   2.687 +    apply (auto simp: power2_sum)
   2.688 +    apply (simp add: power2_eq_square algebra_simps)
   2.689 +    done
   2.690 +  then show ?thesis
   2.691 +    apply (simp add: cos_exp_eq Arcsin_def exp_minus)
   2.692 +    apply (simp add: divide_simps Arcsin_body_lemma)
   2.693 +    apply (metis add.commute minus_unique power2_eq_square)
   2.694 +    done
   2.695 +qed
   2.696 +
   2.697 +lemma sin_Arccos_nonzero:
   2.698 +  assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
   2.699 +proof -
   2.700 +  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
   2.701 +    by (simp add: power_mult_distrib algebra_simps)
   2.702 +  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
   2.703 +  proof
   2.704 +    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
   2.705 +    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
   2.706 +      by simp
   2.707 +    then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
   2.708 +      using eq power2_eq_square by auto
   2.709 +    then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
   2.710 +      using assms
   2.711 +      by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
   2.712 +    then show False
   2.713 +      using assms by simp
   2.714 +  qed
   2.715 +  then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
   2.716 +    by (simp add: algebra_simps)
   2.717 +  then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
   2.718 +    by (metis mult_cancel_left2 zero_neq_numeral)  (*FIXME cancel_numeral_factor*)
   2.719 +  then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
   2.720 +    using assms
   2.721 +    apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib)
   2.722 +    apply (simp add: power2_eq_square algebra_simps)
   2.723 +    done
   2.724 +  then show ?thesis
   2.725 +    apply (simp add: sin_exp_eq Arccos_def exp_minus)
   2.726 +    apply (simp add: divide_simps Arccos_body_lemma)
   2.727 +    apply (simp add: power2_eq_square)
   2.728 +    done
   2.729 +qed
   2.730 +
   2.731 +lemma cos_sin_csqrt:
   2.732 +  assumes "0 < cos(Re z)  \<or>  cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
   2.733 +    shows "cos z = csqrt(1 - (sin z)\<^sup>2)"
   2.734 +  apply (rule csqrt_unique [THEN sym])
   2.735 +  apply (simp add: cos_squared_eq)
   2.736 +  using assms
   2.737 +  apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
   2.738 +  apply (auto simp: algebra_simps)
   2.739 +  done
   2.740 +
   2.741 +lemma sin_cos_csqrt:
   2.742 +  assumes "0 < sin(Re z)  \<or>  sin(Re z) = 0 \<and> 0 \<le> Im z * cos(Re z)"
   2.743 +    shows "sin z = csqrt(1 - (cos z)\<^sup>2)"
   2.744 +  apply (rule csqrt_unique [THEN sym])
   2.745 +  apply (simp add: sin_squared_eq)
   2.746 +  using assms
   2.747 +  apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
   2.748 +  apply (auto simp: algebra_simps)
   2.749 +  done
   2.750 +
   2.751 +lemma Arcsin_Arccos_csqrt_pos:
   2.752 +    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
   2.753 +  by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
   2.754 +
   2.755 +lemma Arccos_Arcsin_csqrt_pos:
   2.756 +    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
   2.757 +  by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
   2.758 +
   2.759 +lemma sin_Arccos:
   2.760 +    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
   2.761 +  by (simp add: Arccos_Arcsin_csqrt_pos)
   2.762 +
   2.763 +lemma cos_Arcsin:
   2.764 +    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
   2.765 +  by (simp add: Arcsin_Arccos_csqrt_pos)
   2.766 +
   2.767 +
   2.768 +subsection{*Relationship with Arcsin on the Real Numbers*}
   2.769 +
   2.770 +lemma Im_Arcsin_of_real:
   2.771 +  assumes "abs x \<le> 1"
   2.772 +    shows "Im (Arcsin (of_real x)) = 0"
   2.773 +proof -
   2.774 +  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
   2.775 +    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
   2.776 +  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
   2.777 +    using assms abs_square_le_1
   2.778 +    by (force simp add: Complex.cmod_power2)
   2.779 +  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
   2.780 +    by (simp add: norm_complex_def)
   2.781 +  then show ?thesis
   2.782 +    by (simp add: Im_Arcsin exp_minus)
   2.783 +qed
   2.784 +
   2.785 +corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
   2.786 +  by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
   2.787 +
   2.788 +lemma arcsin_eq_Re_Arcsin:
   2.789 +  assumes "abs x \<le> 1"
   2.790 +    shows "arcsin x = Re (Arcsin (of_real x))"
   2.791 +unfolding arcsin_def
   2.792 +proof (rule the_equality, safe)
   2.793 +  show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
   2.794 +    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
   2.795 +    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
   2.796 +next
   2.797 +  show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
   2.798 +    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
   2.799 +    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
   2.800 +next
   2.801 +  show "sin (Re (Arcsin (complex_of_real x))) = x"
   2.802 +    using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
   2.803 +    by (simp add: Im_Arcsin_of_real assms)
   2.804 +next
   2.805 +  fix x'
   2.806 +  assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
   2.807 +  then show "x' = Re (Arcsin (complex_of_real (sin x')))"
   2.808 +    apply (simp add: sin_of_real [symmetric])
   2.809 +    apply (subst Arcsin_sin)
   2.810 +    apply (auto simp: )
   2.811 +    done
   2.812 +qed
   2.813 +
   2.814 +lemma of_real_arcsin: "abs x \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
   2.815 +  by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
   2.816 +
   2.817 +
   2.818 +subsection{*Relationship with Arccos on the Real Numbers*}
   2.819 +
   2.820 +lemma Im_Arccos_of_real:
   2.821 +  assumes "abs x \<le> 1"
   2.822 +    shows "Im (Arccos (of_real x)) = 0"
   2.823 +proof -
   2.824 +  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
   2.825 +    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
   2.826 +  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
   2.827 +    using assms abs_square_le_1
   2.828 +    by (force simp add: Complex.cmod_power2)
   2.829 +  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
   2.830 +    by (simp add: norm_complex_def)
   2.831 +  then show ?thesis
   2.832 +    by (simp add: Im_Arccos exp_minus)
   2.833 +qed
   2.834 +
   2.835 +corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
   2.836 +  by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
   2.837 +
   2.838 +lemma arccos_eq_Re_Arccos:
   2.839 +  assumes "abs x \<le> 1"
   2.840 +    shows "arccos x = Re (Arccos (of_real x))"
   2.841 +unfolding arccos_def
   2.842 +proof (rule the_equality, safe)
   2.843 +  show "0 \<le> Re (Arccos (complex_of_real x))"
   2.844 +    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
   2.845 +    by (auto simp: Complex.in_Reals_norm Re_Arccos)
   2.846 +next
   2.847 +  show "Re (Arccos (complex_of_real x)) \<le> pi"
   2.848 +    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
   2.849 +    by (auto simp: Complex.in_Reals_norm Re_Arccos)
   2.850 +next
   2.851 +  show "cos (Re (Arccos (complex_of_real x))) = x"
   2.852 +    using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
   2.853 +    by (simp add: Im_Arccos_of_real assms)
   2.854 +next
   2.855 +  fix x'
   2.856 +  assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
   2.857 +  then show "x' = Re (Arccos (complex_of_real (cos x')))"
   2.858 +    apply (simp add: cos_of_real [symmetric])
   2.859 +    apply (subst Arccos_cos)
   2.860 +    apply (auto simp: )
   2.861 +    done
   2.862 +qed
   2.863 +
   2.864 +lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
   2.865 +  by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
   2.866  
   2.867  end