src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
author paulson <lp15@cam.ac.uk>
Wed Apr 01 14:48:38 2015 +0100 (2015-04-01)
changeset 59870 68d6b6aa4450
parent 59862 44b3f4fa33ca
child 60017 b785d6d06430
permissions -rw-r--r--
HOL Light Libraries for complex Arctan, Arcsin, Arccos
     1 (*  Author: John Harrison
     2     Ported from "hol_light/Multivariate/transcendentals.ml" by L C Paulson (2015)
     3 *)
     4 
     5 section {* Complex Transcendental Functions *}
     6 
     7 theory Complex_Transcendental
     8 imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
     9 begin
    10 
    11 
    12 lemma cmod_add_real_less:
    13   assumes "Im z \<noteq> 0" "r\<noteq>0"
    14     shows "cmod (z + r) < cmod z + abs r"
    15 proof (cases z)
    16   case (Complex x y)
    17   have "r * x / \<bar>r\<bar> < sqrt (x*x + y*y)"
    18     apply (rule real_less_rsqrt)
    19     using assms
    20     apply (simp add: Complex power2_eq_square)
    21     using not_real_square_gt_zero by blast
    22   then show ?thesis using assms Complex
    23     apply (auto simp: cmod_def)
    24     apply (rule power2_less_imp_less, auto)
    25     apply (simp add: power2_eq_square field_simps)
    26     done
    27 qed
    28 
    29 lemma cmod_diff_real_less: "Im z \<noteq> 0 \<Longrightarrow> x\<noteq>0 \<Longrightarrow> cmod (z - x) < cmod z + abs x"
    30   using cmod_add_real_less [of z "-x"]
    31   by simp
    32 
    33 lemma cmod_square_less_1_plus:
    34   assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
    35     shows "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
    36   using assms
    37   apply (cases "Im z = 0 \<or> Re z = 0")
    38   using abs_square_less_1
    39     apply (force simp add: Re_power2 Im_power2 cmod_def)
    40   using cmod_diff_real_less [of "1 - z\<^sup>2" "1"]
    41   apply (simp add: norm_power Im_power2)
    42   done
    43 
    44 subsection{*The Exponential Function is Differentiable and Continuous*}
    45 
    46 lemma complex_differentiable_at_exp: "exp complex_differentiable at z"
    47   using DERIV_exp complex_differentiable_def by blast
    48 
    49 lemma complex_differentiable_within_exp: "exp complex_differentiable (at z within s)"
    50   by (simp add: complex_differentiable_at_exp complex_differentiable_at_within)
    51 
    52 lemma continuous_within_exp:
    53   fixes z::"'a::{real_normed_field,banach}"
    54   shows "continuous (at z within s) exp"
    55 by (simp add: continuous_at_imp_continuous_within)
    56 
    57 lemma continuous_on_exp:
    58   fixes s::"'a::{real_normed_field,banach} set"
    59   shows "continuous_on s exp"
    60 by (simp add: continuous_on_exp continuous_on_id)
    61 
    62 lemma holomorphic_on_exp: "exp holomorphic_on s"
    63   by (simp add: complex_differentiable_within_exp holomorphic_on_def)
    64 
    65 subsection{*Euler and de Moivre formulas.*}
    66 
    67 text{*The sine series times @{term i}*}
    68 lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
    69 proof -
    70   have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
    71     using sin_converges sums_mult by blast
    72   then show ?thesis
    73     by (simp add: scaleR_conv_of_real field_simps)
    74 qed
    75 
    76 theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
    77 proof -
    78   have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
    79         = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    80   proof
    81     fix n
    82     show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
    83       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
    84   qed
    85   also have "... sums (exp (ii * z))"
    86     by (rule exp_converges)
    87   finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
    88   moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
    89     using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
    90     by (simp add: field_simps scaleR_conv_of_real)
    91   ultimately show ?thesis
    92     using sums_unique2 by blast
    93 qed
    94 
    95 corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
    96   using exp_Euler [of "-z"]
    97   by simp
    98 
    99 lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
   100   by (simp add: exp_Euler exp_minus_Euler)
   101 
   102 lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
   103   by (simp add: exp_Euler exp_minus_Euler)
   104 
   105 lemma cos_exp_eq:  "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
   106   by (simp add: exp_Euler exp_minus_Euler)
   107 
   108 subsection{*Relationships between real and complex trig functions*}
   109 
   110 lemma real_sin_eq [simp]:
   111   fixes x::real
   112   shows "Re(sin(of_real x)) = sin x"
   113   by (simp add: sin_of_real)
   114 
   115 lemma real_cos_eq [simp]:
   116   fixes x::real
   117   shows "Re(cos(of_real x)) = cos x"
   118   by (simp add: cos_of_real)
   119 
   120 lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
   121   apply (simp add: exp_Euler [symmetric])
   122   by (metis exp_of_nat_mult mult.left_commute)
   123 
   124 lemma exp_cnj:
   125   fixes z::complex
   126   shows "cnj (exp z) = exp (cnj z)"
   127 proof -
   128   have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
   129     by auto
   130   also have "... sums (exp (cnj z))"
   131     by (rule exp_converges)
   132   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   133   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
   134     by (metis exp_converges sums_cnj)
   135   ultimately show ?thesis
   136     using sums_unique2
   137     by blast
   138 qed
   139 
   140 lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
   141   by (simp add: sin_exp_eq exp_cnj field_simps)
   142 
   143 lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
   144   by (simp add: cos_exp_eq exp_cnj field_simps)
   145 
   146 lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
   147   using DERIV_sin complex_differentiable_def by blast
   148 
   149 lemma complex_differentiable_within_sin: "sin complex_differentiable (at z within s)"
   150   by (simp add: complex_differentiable_at_sin complex_differentiable_at_within)
   151 
   152 lemma complex_differentiable_at_cos: "cos complex_differentiable at z"
   153   using DERIV_cos complex_differentiable_def by blast
   154 
   155 lemma complex_differentiable_within_cos: "cos complex_differentiable (at z within s)"
   156   by (simp add: complex_differentiable_at_cos complex_differentiable_at_within)
   157 
   158 lemma holomorphic_on_sin: "sin holomorphic_on s"
   159   by (simp add: complex_differentiable_within_sin holomorphic_on_def)
   160 
   161 lemma holomorphic_on_cos: "cos holomorphic_on s"
   162   by (simp add: complex_differentiable_within_cos holomorphic_on_def)
   163 
   164 subsection{* Get a nice real/imaginary separation in Euler's formula.*}
   165 
   166 lemma Euler: "exp(z) = of_real(exp(Re z)) *
   167               (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
   168 by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
   169 
   170 lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   171   by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
   172 
   173 lemma Im_sin: "Im(sin z) = cos(Re z) * (exp(Im z) - exp(-(Im z))) / 2"
   174   by (simp add: sin_exp_eq field_simps Im_divide Re_exp)
   175 
   176 lemma Re_cos: "Re(cos z) = cos(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
   177   by (simp add: cos_exp_eq field_simps Re_divide Re_exp)
   178 
   179 lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
   180   by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
   181 
   182 lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
   183   by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
   184 
   185 lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
   186   by (simp add: Re_sin Im_sin algebra_simps)
   187 
   188 lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
   189   by (simp add: Re_sin Im_sin algebra_simps)
   190 
   191 subsection{*More on the Polar Representation of Complex Numbers*}
   192 
   193 lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
   194   by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
   195 
   196 lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
   197 apply auto
   198 apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
   199 apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1) real_of_int_def)
   200 by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 real_of_int_def sin_zero_iff_int2)
   201 
   202 lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
   203                 (is "?lhs = ?rhs")
   204 proof -
   205   have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
   206     by (simp add: exp_diff)
   207   also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
   208     by (simp add: exp_eq_1)
   209   also have "... \<longleftrightarrow> ?rhs"
   210     by (auto simp: algebra_simps intro!: complex_eqI)
   211   finally show ?thesis .
   212 qed
   213 
   214 lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
   215   by (auto simp: exp_eq abs_mult)
   216 
   217 lemma exp_integer_2pi:
   218   assumes "n \<in> Ints"
   219   shows "exp((2 * n * pi) * ii) = 1"
   220 proof -
   221   have "exp((2 * n * pi) * ii) = exp 0"
   222     using assms
   223     by (simp only: Ints_def exp_eq) auto
   224   also have "... = 1"
   225     by simp
   226   finally show ?thesis .
   227 qed
   228 
   229 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
   230 proof -
   231   { assume "sin y = sin x" "cos y = cos x"
   232     then have "cos (y-x) = 1"
   233       using cos_add [of y "-x"] by simp
   234     then have "\<exists>n::int. y-x = real n * 2 * pi"
   235       using cos_one_2pi_int by blast }
   236   then show ?thesis
   237   apply (auto simp: sin_add cos_add)
   238   apply (metis add.commute diff_add_cancel mult.commute)
   239   done
   240 qed
   241 
   242 lemma exp_i_ne_1:
   243   assumes "0 < x" "x < 2*pi"
   244   shows "exp(\<i> * of_real x) \<noteq> 1"
   245 proof
   246   assume "exp (\<i> * of_real x) = 1"
   247   then have "exp (\<i> * of_real x) = exp 0"
   248     by simp
   249   then obtain n where "\<i> * of_real x = (of_int (2 * n) * pi) * \<i>"
   250     by (simp only: Ints_def exp_eq) auto
   251   then have  "of_real x = (of_int (2 * n) * pi)"
   252     by (metis complex_i_not_zero mult.commute mult_cancel_left of_real_eq_iff real_scaleR_def scaleR_conv_of_real)
   253   then have  "x = (of_int (2 * n) * pi)"
   254     by simp
   255   then show False using assms
   256     by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   257 qed
   258 
   259 lemma sin_eq_0:
   260   fixes z::complex
   261   shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   262   by (simp add: sin_exp_eq exp_eq of_real_numeral)
   263 
   264 lemma cos_eq_0:
   265   fixes z::complex
   266   shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   267   using sin_eq_0 [of "z - of_real pi/2"]
   268   by (simp add: sin_diff algebra_simps)
   269 
   270 lemma cos_eq_1:
   271   fixes z::complex
   272   shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   273 proof -
   274   have "cos z = cos (2*(z/2))"
   275     by simp
   276   also have "... = 1 - 2 * sin (z/2) ^ 2"
   277     by (simp only: cos_double_sin)
   278   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
   279     by simp
   280   show ?thesis
   281     by (auto simp: sin_eq_0 of_real_numeral)
   282 qed
   283 
   284 lemma csin_eq_1:
   285   fixes z::complex
   286   shows "sin z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + of_real pi/2)"
   287   using cos_eq_1 [of "z - of_real pi/2"]
   288   by (simp add: cos_diff algebra_simps)
   289 
   290 lemma csin_eq_minus1:
   291   fixes z::complex
   292   shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
   293         (is "_ = ?rhs")
   294 proof -
   295   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
   296     by (simp add: equation_minus_iff)
   297   also have "...  \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
   298     by (simp only: csin_eq_1)
   299   also have "...  \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
   300     apply (rule iff_exI)
   301     by (metis (no_types)  is_num_normalize(8) minus_minus of_real_def real_vector.scale_minus_left uminus_add_conv_diff)
   302   also have "... = ?rhs"
   303     apply (auto simp: of_real_numeral)
   304     apply (rule_tac [2] x="-(x+1)" in exI)
   305     apply (rule_tac x="-(x+1)" in exI)
   306     apply (simp_all add: algebra_simps)
   307     done
   308   finally show ?thesis .
   309 qed
   310 
   311 lemma ccos_eq_minus1:
   312   fixes z::complex
   313   shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   314   using csin_eq_1 [of "z - of_real pi/2"]
   315   apply (simp add: sin_diff)
   316   apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   317   done
   318 
   319 lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   320                 (is "_ = ?rhs")
   321 proof -
   322   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
   323     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
   324   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
   325     by (simp only: csin_eq_1)
   326   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
   327     apply (rule iff_exI)
   328     apply (auto simp: algebra_simps of_real_numeral)
   329     apply (rule injD [OF inj_of_real [where 'a = complex]])
   330     apply (auto simp: of_real_numeral)
   331     done
   332   also have "... = ?rhs"
   333     by (auto simp: algebra_simps)
   334   finally show ?thesis .
   335 qed
   336 
   337 lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   338 proof -
   339   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
   340     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
   341   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
   342     by (simp only: csin_eq_minus1)
   343   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
   344     apply (rule iff_exI)
   345     apply (auto simp: algebra_simps)
   346     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   347     done
   348   also have "... = ?rhs"
   349     by (auto simp: algebra_simps)
   350   finally show ?thesis .
   351 qed
   352 
   353 lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   354                       (is "_ = ?rhs")
   355 proof -
   356   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
   357     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
   358   also have "...  \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
   359     by (simp only: ccos_eq_minus1)
   360   also have "...  \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
   361     apply (rule iff_exI)
   362     apply (auto simp: algebra_simps)
   363     apply (rule injD [OF inj_of_real [where 'a = complex]], auto)
   364     done
   365   also have "... = ?rhs"
   366     by (auto simp: algebra_simps)
   367   finally show ?thesis .
   368 qed
   369 
   370 lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   371   apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   372   using cos_double_sin [of "t/2"]
   373   apply (simp add: real_sqrt_mult)
   374   done
   375 
   376 lemma sinh_complex:
   377   fixes z :: complex
   378   shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
   379   by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
   380 
   381 lemma sin_ii_times:
   382   fixes z :: complex
   383   shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
   384   using sinh_complex by auto
   385 
   386 lemma sinh_real:
   387   fixes x :: real
   388   shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
   389   by (simp add: exp_of_real sin_ii_times of_real_numeral)
   390 
   391 lemma cosh_complex:
   392   fixes z :: complex
   393   shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
   394   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   395 
   396 lemma cosh_real:
   397   fixes x :: real
   398   shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
   399   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
   400 
   401 lemmas cos_ii_times = cosh_complex [symmetric]
   402 
   403 lemma norm_cos_squared:
   404     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   405   apply (cases z)
   406   apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   407   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   408   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   409   apply (simp add: sin_squared_eq)
   410   apply (simp add: power2_eq_square algebra_simps divide_simps)
   411   done
   412 
   413 lemma norm_sin_squared:
   414     "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
   415   apply (cases z)
   416   apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
   417   apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide)
   418   apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   419   apply (simp add: cos_squared_eq)
   420   apply (simp add: power2_eq_square algebra_simps divide_simps)
   421   done
   422 
   423 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   424   using abs_Im_le_cmod linear order_trans by fastforce
   425 
   426 lemma norm_cos_le:
   427   fixes z::complex
   428   shows "norm(cos z) \<le> exp(norm z)"
   429 proof -
   430   have "Im z \<le> cmod z"
   431     using abs_Im_le_cmod abs_le_D1 by auto
   432   with exp_uminus_Im show ?thesis
   433     apply (simp add: cos_exp_eq norm_divide)
   434     apply (rule order_trans [OF norm_triangle_ineq], simp)
   435     apply (metis add_mono exp_le_cancel_iff mult_2_right)
   436     done
   437 qed
   438 
   439 lemma norm_cos_plus1_le:
   440   fixes z::complex
   441   shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   442 proof -
   443   have mono: "\<And>u w z::real. (1 \<le> w | 1 \<le> z) \<Longrightarrow> (w \<le> u & z \<le> u) \<Longrightarrow> 2 + w + z \<le> 4 * u"
   444       by arith
   445   have *: "Im z \<le> cmod z"
   446     using abs_Im_le_cmod abs_le_D1 by auto
   447   have triangle3: "\<And>x y z. norm(x + y + z) \<le> norm(x) + norm(y) + norm(z)"
   448     by (simp add: norm_add_rule_thm)
   449   have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   450     by (simp add: cos_exp_eq)
   451   also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
   452     by (simp add: field_simps)
   453   also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
   454     by (simp add: norm_divide)
   455   finally show ?thesis
   456     apply (rule ssubst, simp)
   457     apply (rule order_trans [OF triangle3], simp)
   458     using exp_uminus_Im *
   459     apply (auto intro: mono)
   460     done
   461 qed
   462 
   463 subsection{* Taylor series for complex exponential, sine and cosine.*}
   464 
   465 context
   466 begin
   467 
   468 declare power_Suc [simp del]
   469 
   470 lemma Taylor_exp:
   471   "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   472 proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   473   show "convex (closed_segment 0 z)"
   474     by (rule convex_segment [of 0 z])
   475 next
   476   fix k x
   477   assume "x \<in> closed_segment 0 z" "k \<le> n"
   478   show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
   479     using DERIV_exp DERIV_subset by blast
   480 next
   481   fix x
   482   assume "x \<in> closed_segment 0 z"
   483   then show "Re x \<le> \<bar>Re z\<bar>"
   484     apply (auto simp: closed_segment_def scaleR_conv_of_real)
   485     by (meson abs_ge_self abs_ge_zero linear mult_left_le_one_le mult_nonneg_nonpos order_trans)
   486 next
   487   show "0 \<in> closed_segment 0 z"
   488     by (auto simp: closed_segment_def)
   489 next
   490   show "z \<in> closed_segment 0 z"
   491     apply (simp add: closed_segment_def scaleR_conv_of_real)
   492     using of_real_1 zero_le_one by blast
   493 qed
   494 
   495 lemma
   496   assumes "0 \<le> u" "u \<le> 1"
   497   shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   498     and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   499 proof -
   500   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   501     by arith
   502   show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   503     apply (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
   504     apply (rule order_trans [OF norm_triangle_ineq4])
   505     apply (rule mono)
   506     apply (auto simp: abs_if mult_left_le_one_le)
   507     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   508     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   509     done
   510   show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" using assms
   511     apply (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
   512     apply (rule order_trans [OF norm_triangle_ineq])
   513     apply (rule mono)
   514     apply (auto simp: abs_if mult_left_le_one_le)
   515     apply (meson mult_nonneg_nonneg neg_le_0_iff_le not_le order_trans)
   516     apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   517     done
   518 qed
   519 
   520 lemma Taylor_sin:
   521   "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   522    \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   523 proof -
   524   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   525       by arith
   526   have *: "cmod (sin z -
   527                  (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   528            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   529   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" "exp\<bar>Im z\<bar>" 0 z,
   530 simplified])
   531   show "convex (closed_segment 0 z)"
   532     by (rule convex_segment [of 0 z])
   533   next
   534     fix k x
   535     show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
   536             (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
   537             (at x within closed_segment 0 z)"
   538       apply (auto simp: power_Suc)
   539       apply (intro derivative_eq_intros | simp)+
   540       done
   541   next
   542     fix x
   543     assume "x \<in> closed_segment 0 z"
   544     then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
   545       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   546   next
   547     show "0 \<in> closed_segment 0 z"
   548       by (auto simp: closed_segment_def)
   549   next
   550     show "z \<in> closed_segment 0 z"
   551       apply (simp add: closed_segment_def scaleR_conv_of_real)
   552       using of_real_1 zero_le_one by blast
   553   qed
   554   have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   555             = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   556     by (auto simp: sin_coeff_def elim!: oddE)
   557   show ?thesis
   558     apply (rule order_trans [OF _ *])
   559     apply (simp add: **)
   560     done
   561 qed
   562 
   563 lemma Taylor_cos:
   564   "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
   565    \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   566 proof -
   567   have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   568       by arith
   569   have *: "cmod (cos z -
   570                  (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   571            \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   572   proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
   573 simplified])
   574   show "convex (closed_segment 0 z)"
   575     by (rule convex_segment [of 0 z])
   576   next
   577     fix k x
   578     assume "x \<in> closed_segment 0 z" "k \<le> n"
   579     show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
   580             (- 1) ^ Suc (k div 2) * (if odd k then cos x else sin x))
   581              (at x within closed_segment 0 z)"
   582       apply (auto simp: power_Suc)
   583       apply (intro derivative_eq_intros | simp)+
   584       done
   585   next
   586     fix x
   587     assume "x \<in> closed_segment 0 z"
   588     then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
   589       by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
   590   next
   591     show "0 \<in> closed_segment 0 z"
   592       by (auto simp: closed_segment_def)
   593   next
   594     show "z \<in> closed_segment 0 z"
   595       apply (simp add: closed_segment_def scaleR_conv_of_real)
   596       using of_real_1 zero_le_one by blast
   597   qed
   598   have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   599             = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   600     by (auto simp: cos_coeff_def elim!: evenE)
   601   show ?thesis
   602     apply (rule order_trans [OF _ *])
   603     apply (simp add: **)
   604     done
   605 qed
   606 
   607 end (* of context *)
   608 
   609 text{*32-bit Approximation to e*}
   610 lemma e_approx_32: "abs(exp(1) - 5837465777 / 2147483648) \<le> (inverse(2 ^ 32)::real)"
   611   using Taylor_exp [of 1 14] exp_le
   612   apply (simp add: setsum_left_distrib in_Reals_norm Re_exp atMost_nat_numeral fact_numeral)
   613   apply (simp only: pos_le_divide_eq [symmetric], linarith)
   614   done
   615 
   616 subsection{*The argument of a complex number*}
   617 
   618 definition Arg :: "complex \<Rightarrow> real" where
   619  "Arg z \<equiv> if z = 0 then 0
   620            else THE t. 0 \<le> t \<and> t < 2*pi \<and>
   621                     z = of_real(norm z) * exp(ii * of_real t)"
   622 
   623 lemma Arg_0 [simp]: "Arg(0) = 0"
   624   by (simp add: Arg_def)
   625 
   626 lemma Arg_unique_lemma:
   627   assumes z:  "z = of_real(norm z) * exp(ii * of_real t)"
   628       and z': "z = of_real(norm z) * exp(ii * of_real t')"
   629       and t:  "0 \<le> t"  "t < 2*pi"
   630       and t': "0 \<le> t'" "t' < 2*pi"
   631       and nz: "z \<noteq> 0"
   632   shows "t' = t"
   633 proof -
   634   have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
   635     by arith
   636   have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
   637     by (metis z z')
   638   then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   639     by (metis nz mult_left_cancel mult_zero_left z)
   640   then have "sin t' = sin t \<and> cos t' = cos t"
   641     apply (simp add: exp_Euler sin_of_real cos_of_real)
   642     by (metis Complex_eq complex.sel)
   643   then obtain n::int where n: "t' = t + 2 * real n * pi"
   644     by (auto simp: sin_cos_eq_iff)
   645   then have "n=0"
   646     apply (rule_tac z=n in int_cases)
   647     using t t'
   648     apply (auto simp: mult_less_0_iff algebra_simps)
   649     done
   650   then show "t' = t"
   651       by (simp add: n)
   652 qed
   653 
   654 lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
   655 proof (cases "z=0")
   656   case True then show ?thesis
   657     by (simp add: Arg_def)
   658 next
   659   case False
   660   obtain t where t: "0 \<le> t" "t < 2*pi"
   661              and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   662     using sincos_total_2pi [OF complex_unit_circle [OF False]]
   663     by blast
   664   have z: "z = of_real(norm z) * exp(ii * of_real t)"
   665     apply (rule complex_eqI)
   666     using t False ReIm
   667     apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   668     done
   669   show ?thesis
   670     apply (simp add: Arg_def False)
   671     apply (rule theI [where a=t])
   672     using t z False
   673     apply (auto intro: Arg_unique_lemma)
   674     done
   675 qed
   676 
   677 
   678 corollary
   679   shows Arg_ge_0: "0 \<le> Arg z"
   680     and Arg_lt_2pi: "Arg z < 2*pi"
   681     and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
   682   using Arg by auto
   683 
   684 lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
   685   using Arg [of z] by auto
   686 
   687 lemma Arg_unique: "\<lbrakk>of_real r * exp(ii * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
   688   apply (rule Arg_unique_lemma [OF _ Arg_eq])
   689   using Arg [of z]
   690   apply (auto simp: norm_mult)
   691   done
   692 
   693 lemma Arg_minus: "z \<noteq> 0 \<Longrightarrow> Arg (-z) = (if Arg z < pi then Arg z + pi else Arg z - pi)"
   694   apply (rule Arg_unique [of "norm z"])
   695   apply (rule complex_eqI)
   696   using Arg_ge_0 [of z] Arg_eq [of z] Arg_lt_2pi [of z] Arg_eq [of z]
   697   apply auto
   698   apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   699   apply (metis Re_rcis Im_rcis rcis_def)+
   700   done
   701 
   702 lemma Arg_times_of_real [simp]: "0 < r \<Longrightarrow> Arg (of_real r * z) = Arg z"
   703   apply (cases "z=0", simp)
   704   apply (rule Arg_unique [of "r * norm z"])
   705   using Arg
   706   apply auto
   707   done
   708 
   709 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   710   by (metis Arg_times_of_real mult.commute)
   711 
   712 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   713   by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   714 
   715 lemma Arg_le_pi: "Arg z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
   716 proof (cases "z=0")
   717   case True then show ?thesis
   718     by simp
   719 next
   720   case False
   721   have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   722     by (metis Arg_eq)
   723   also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg z))))"
   724     using False
   725     by (simp add: zero_le_mult_iff)
   726   also have "... \<longleftrightarrow> Arg z \<le> pi"
   727     by (simp add: Im_exp) (metis Arg_ge_0 Arg_lt_2pi sin_lt_zero sin_ge_zero not_le)
   728   finally show ?thesis
   729     by blast
   730 qed
   731 
   732 lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   733 proof (cases "z=0")
   734   case True then show ?thesis
   735     by simp
   736 next
   737   case False
   738   have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   739     by (metis Arg_eq)
   740   also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg z))))"
   741     using False
   742     by (simp add: zero_less_mult_iff)
   743   also have "... \<longleftrightarrow> 0 < Arg z \<and> Arg z < pi"
   744     using Arg_ge_0  Arg_lt_2pi sin_le_zero sin_gt_zero
   745     apply (auto simp: Im_exp)
   746     using le_less apply fastforce
   747     using not_le by blast
   748   finally show ?thesis
   749     by blast
   750 qed
   751 
   752 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
   753 proof (cases "z=0")
   754   case True then show ?thesis
   755     by simp
   756 next
   757   case False
   758   have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
   759     by (metis Arg_eq)
   760   also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
   761     using False
   762     by (simp add: zero_le_mult_iff)
   763   also have "... \<longleftrightarrow> Arg z = 0"
   764     apply (auto simp: Re_exp)
   765     apply (metis Arg_lt_pi Arg_ge_0 Arg_le_pi cos_pi complex_is_Real_iff leD less_linear less_minus_one_simps(2) minus_minus neg_less_eq_nonneg order_refl)
   766     using Arg_eq [of z]
   767     apply (auto simp: Reals_def)
   768     done
   769   finally show ?thesis
   770     by blast
   771 qed
   772 
   773 lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   774   by (simp add: Arg_eq_0)
   775 
   776 lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   777   apply  (cases "z=0", simp)
   778   using Arg_eq_0 [of "-z"]
   779   apply (auto simp: complex_is_Real_iff Arg_minus)
   780   apply (simp add: complex_Re_Im_cancel_iff)
   781   apply (metis Arg_minus pi_gt_zero add.left_neutral minus_minus minus_zero)
   782   done
   783 
   784 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   785   using Arg_eq_0 Arg_eq_pi not_le by auto
   786 
   787 lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   788   apply (cases "z=0", simp)
   789   apply (rule Arg_unique [of "inverse (norm z)"])
   790   using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
   791   apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   792   done
   793 
   794 lemma Arg_eq_iff:
   795   assumes "w \<noteq> 0" "z \<noteq> 0"
   796      shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
   797   using assms Arg_eq [of z] Arg_eq [of w]
   798   apply auto
   799   apply (rule_tac x="norm w / norm z" in exI)
   800   apply (simp add: divide_simps)
   801   by (metis mult.commute mult.left_commute)
   802 
   803 lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   804   using complex_is_Real_iff
   805   apply (simp add: Arg_eq_0)
   806   apply (auto simp: divide_simps not_sum_power2_lt_zero)
   807   done
   808 
   809 lemma Arg_divide:
   810   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   811     shows "Arg(z / w) = Arg z - Arg w"
   812   apply (rule Arg_unique [of "norm(z / w)"])
   813   using assms Arg_eq [of z] Arg_eq [of w] Arg_ge_0 [of w] Arg_lt_2pi [of z]
   814   apply (auto simp: exp_diff norm_divide algebra_simps divide_simps)
   815   done
   816 
   817 lemma Arg_le_div_sum:
   818   assumes "w \<noteq> 0" "z \<noteq> 0" "Arg w \<le> Arg z"
   819     shows "Arg z = Arg w + Arg(z / w)"
   820   by (simp add: Arg_divide assms)
   821 
   822 lemma Arg_le_div_sum_eq:
   823   assumes "w \<noteq> 0" "z \<noteq> 0"
   824     shows "Arg w \<le> Arg z \<longleftrightarrow> Arg z = Arg w + Arg(z / w)"
   825   using assms
   826   by (auto simp: Arg_ge_0 intro: Arg_le_div_sum)
   827 
   828 lemma Arg_diff:
   829   assumes "w \<noteq> 0" "z \<noteq> 0"
   830     shows "Arg w - Arg z = (if Arg z \<le> Arg w then Arg(w / z) else Arg(w/z) - 2*pi)"
   831   using assms
   832   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   833   using Arg_divide [of w z] Arg_inverse [of "w/z"]
   834   apply auto
   835   by (metis Arg_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   836 
   837 lemma Arg_add:
   838   assumes "w \<noteq> 0" "z \<noteq> 0"
   839     shows "Arg w + Arg z = (if Arg w + Arg z < 2*pi then Arg(w * z) else Arg(w * z) + 2*pi)"
   840   using assms
   841   using Arg_diff [of "w*z" z] Arg_le_div_sum_eq [of z "w*z"]
   842   apply (auto simp: Arg_ge_0 Arg_divide not_le)
   843   apply (metis Arg_lt_2pi add.commute)
   844   apply (metis (no_types) Arg add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
   845   done
   846 
   847 lemma Arg_times:
   848   assumes "w \<noteq> 0" "z \<noteq> 0"
   849     shows "Arg (w * z) = (if Arg w + Arg z < 2*pi then Arg w + Arg z
   850                             else (Arg w + Arg z) - 2*pi)"
   851   using Arg_add [OF assms]
   852   by auto
   853 
   854 lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   855   apply (cases "z=0", simp)
   856   apply (rule trans [of _ "Arg(inverse z)"])
   857   apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   858   apply (metis norm_eq_zero of_real_power zero_less_power2)
   859   apply (auto simp: of_real_numeral Arg_inverse)
   860   done
   861 
   862 lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   863   using Arg_eq_0 Arg_eq_0_pi
   864   by auto
   865 
   866 lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   867   by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   868 
   869 
   870 subsection{*Analytic properties of tangent function*}
   871 
   872 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
   873   by (simp add: cnj_cos cnj_sin tan_def)
   874 
   875 lemma complex_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan complex_differentiable at z"
   876   unfolding complex_differentiable_def
   877   using DERIV_tan by blast
   878 
   879 lemma complex_differentiable_within_tan: "~(cos z = 0)
   880          \<Longrightarrow> tan complex_differentiable (at z within s)"
   881   using complex_differentiable_at_tan complex_differentiable_at_within by blast
   882 
   883 lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
   884   using continuous_at_imp_continuous_within isCont_tan by blast
   885 
   886 lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
   887   by (simp add: continuous_at_imp_continuous_on)
   888 
   889 lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
   890   by (simp add: complex_differentiable_within_tan holomorphic_on_def)
   891 
   892 
   893 subsection{*Complex logarithms (the conventional principal value)*}
   894 
   895 definition Ln where
   896    "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   897 
   898 lemma
   899   assumes "z \<noteq> 0"
   900     shows exp_Ln [simp]: "exp(Ln z) = z"
   901       and mpi_less_Im_Ln: "-pi < Im(Ln z)"
   902       and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
   903 proof -
   904   obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
   905     using complex_unimodular_polar [of "z / (norm z)"] assms
   906     by (auto simp: norm_divide divide_simps)
   907   obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
   908     using sincos_principal_value [of "\<psi>"] assms
   909     by (auto simp: norm_divide divide_simps)
   910   have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
   911     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   912     using z assms \<phi>
   913     apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
   914     done
   915   then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
   916     by auto
   917 qed
   918 
   919 lemma Ln_exp [simp]:
   920   assumes "-pi < Im(z)" "Im(z) \<le> pi"
   921     shows "Ln(exp z) = z"
   922   apply (rule exp_complex_eqI)
   923   using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   924   apply auto
   925   done
   926 
   927 lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   928   by (metis exp_Ln)
   929 
   930 lemma Ln_unique: "exp(z) = w \<Longrightarrow> -pi < Im(z) \<Longrightarrow> Im(z) \<le> pi \<Longrightarrow> Ln w = z"
   931   using Ln_exp by blast
   932 
   933 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
   934 by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
   935 
   936 lemma exists_complex_root:
   937   fixes a :: complex
   938   shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a"
   939   apply (cases "a=0", simp)
   940   apply (rule_tac x= "exp(Ln(a) / n)" in exI)
   941   apply (auto simp: exp_of_nat_mult [symmetric])
   942   done
   943 
   944 subsection{*The Unwinding Number and the Ln-product Formula*}
   945 
   946 text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
   947 
   948 definition unwinding :: "complex \<Rightarrow> complex" where
   949    "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
   950 
   951 lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
   952   by (simp add: unwinding_def)
   953 
   954 lemma Ln_times_unwinding:
   955     "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
   956   using unwinding_2pi by (simp add: exp_add)
   957 
   958 
   959 subsection{*Derivative of Ln away from the branch cut*}
   960 
   961 lemma
   962   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
   963     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
   964       and Im_Ln_less_pi:           "Im (Ln z) < pi"
   965 proof -
   966   have znz: "z \<noteq> 0"
   967     using assms by auto
   968   then show *: "Im (Ln z) < pi" using assms
   969     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)
   970   show "(Ln has_field_derivative inverse(z)) (at z)"
   971     apply (rule has_complex_derivative_inverse_strong_x
   972               [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
   973     using znz *
   974     apply (auto simp: continuous_on_exp open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
   975     apply (metis DERIV_exp exp_Ln)
   976     apply (metis mpi_less_Im_Ln)
   977     done
   978 qed
   979 
   980 declare has_field_derivative_Ln [derivative_intros]
   981 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
   982 
   983 lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
   984   using complex_differentiable_def has_field_derivative_Ln by blast
   985 
   986 lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
   987          \<Longrightarrow> Ln complex_differentiable (at z within s)"
   988   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
   989 
   990 lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   991   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
   992 
   993 lemma isCont_Ln' [simp]:
   994    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   995   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
   996 
   997 lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   998   using continuous_at_Ln continuous_at_imp_continuous_within by blast
   999 
  1000 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
  1001   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
  1002 
  1003 lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
  1004   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
  1005 
  1006 
  1007 subsection{*Relation to Real Logarithm*}
  1008 
  1009 lemma Ln_of_real:
  1010   assumes "0 < z"
  1011     shows "Ln(of_real z) = of_real(ln z)"
  1012 proof -
  1013   have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
  1014     by (simp add: exp_of_real)
  1015   also have "... = of_real(ln z)"
  1016     using assms
  1017     by (subst Ln_exp) auto
  1018   finally show ?thesis
  1019     using assms by simp
  1020 qed
  1021 
  1022 corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
  1023   by (auto simp: Ln_of_real elim: Reals_cases)
  1024 
  1025 
  1026 subsection{*Quadrant-type results for Ln*}
  1027 
  1028 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
  1029   using cos_minus_pi cos_gt_zero_pi [of "x-pi"]
  1030   by simp
  1031 
  1032 lemma Re_Ln_pos_lt:
  1033   assumes "z \<noteq> 0"
  1034     shows "abs(Im(Ln z)) < pi/2 \<longleftrightarrow> 0 < Re(z)"
  1035 proof -
  1036   { fix w
  1037     assume "w = Ln z"
  1038     then have w: "Im w \<le> pi" "- pi < Im w"
  1039       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1040       by auto
  1041     then have "abs(Im w) < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
  1042       apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
  1043       using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
  1044       apply (simp add: abs_if split: split_if_asm)
  1045       apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
  1046                less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
  1047                mult_numeral_1_right)
  1048       done
  1049   }
  1050   then show ?thesis using assms
  1051     by auto
  1052 qed
  1053 
  1054 lemma Re_Ln_pos_le:
  1055   assumes "z \<noteq> 0"
  1056     shows "abs(Im(Ln z)) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(z)"
  1057 proof -
  1058   { fix w
  1059     assume "w = Ln z"
  1060     then have w: "Im w \<le> pi" "- pi < Im w"
  1061       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1062       by auto
  1063     then have "abs(Im w) \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
  1064       apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
  1065       using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
  1066       apply (auto simp: abs_if split: split_if_asm)
  1067       done
  1068   }
  1069   then show ?thesis using assms
  1070     by auto
  1071 qed
  1072 
  1073 lemma Im_Ln_pos_lt:
  1074   assumes "z \<noteq> 0"
  1075     shows "0 < Im(Ln z) \<and> Im(Ln z) < pi \<longleftrightarrow> 0 < Im(z)"
  1076 proof -
  1077   { fix w
  1078     assume "w = Ln z"
  1079     then have w: "Im w \<le> pi" "- pi < Im w"
  1080       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1081       by auto
  1082     then have "0 < Im w \<and> Im w < pi \<longleftrightarrow> 0 < Im(exp w)"
  1083       using sin_gt_zero [of "- (Im w)"] sin_gt_zero [of "(Im w)"]
  1084       apply (auto simp: Im_exp zero_less_mult_iff)
  1085       using less_linear apply fastforce
  1086       using less_linear apply fastforce
  1087       done
  1088   }
  1089   then show ?thesis using assms
  1090     by auto
  1091 qed
  1092 
  1093 lemma Im_Ln_pos_le:
  1094   assumes "z \<noteq> 0"
  1095     shows "0 \<le> Im(Ln z) \<and> Im(Ln z) \<le> pi \<longleftrightarrow> 0 \<le> Im(z)"
  1096 proof -
  1097   { fix w
  1098     assume "w = Ln z"
  1099     then have w: "Im w \<le> pi" "- pi < Im w"
  1100       using Im_Ln_le_pi [of z]  mpi_less_Im_Ln [of z]  assms
  1101       by auto
  1102     then have "0 \<le> Im w \<and> Im w \<le> pi \<longleftrightarrow> 0 \<le> Im(exp w)"
  1103       using sin_ge_zero [of "- (Im w)"] sin_ge_zero [of "(Im w)"]
  1104       apply (auto simp: Im_exp zero_le_mult_iff sin_ge_zero)
  1105       apply (metis not_le not_less_iff_gr_or_eq pi_not_less_zero sin_eq_0_pi)
  1106       done }
  1107   then show ?thesis using assms
  1108     by auto
  1109 qed
  1110 
  1111 lemma Re_Ln_pos_lt_imp: "0 < Re(z) \<Longrightarrow> abs(Im(Ln z)) < pi/2"
  1112   by (metis Re_Ln_pos_lt less_irrefl zero_complex.simps(1))
  1113 
  1114 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
  1115   by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
  1116 
  1117 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
  1118   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
  1119        complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
  1120 
  1121 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
  1122   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)
  1123 
  1124 
  1125 subsection{*More Properties of Ln*}
  1126 
  1127 lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
  1128   apply (cases "z=0", auto)
  1129   apply (rule exp_complex_eqI)
  1130   apply (auto simp: abs_if split: split_if_asm)
  1131   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)
  1132   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)
  1133   by (metis exp_Ln exp_cnj)
  1134 
  1135 lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
  1136   apply (cases "z=0", auto)
  1137   apply (rule exp_complex_eqI)
  1138   using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
  1139   apply (auto simp: abs_if exp_minus split: split_if_asm)
  1140   apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
  1141                inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
  1142   done
  1143 
  1144 lemma Ln_1 [simp]: "Ln(1) = 0"
  1145 proof -
  1146   have "Ln (exp 0) = 0"
  1147     by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
  1148   then show ?thesis
  1149     by simp
  1150 qed
  1151 
  1152 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
  1153   apply (rule exp_complex_eqI)
  1154   using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
  1155   apply (auto simp: abs_if)
  1156   done
  1157 
  1158 lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
  1159   using Ln_exp [of "ii * (of_real pi/2)"]
  1160   unfolding exp_Euler
  1161   by simp
  1162 
  1163 lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
  1164 proof -
  1165   have  "Ln(-ii) = Ln(1/ii)"
  1166     by simp
  1167   also have "... = - (Ln ii)"
  1168     by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
  1169   also have "... = - (ii * pi/2)"
  1170     by (simp add: Ln_ii)
  1171   finally show ?thesis .
  1172 qed
  1173 
  1174 lemma Ln_times:
  1175   assumes "w \<noteq> 0" "z \<noteq> 0"
  1176     shows "Ln(w * z) =
  1177                 (if Im(Ln w + Ln z) \<le> -pi then
  1178                   (Ln(w) + Ln(z)) + ii * of_real(2*pi)
  1179                 else if Im(Ln w + Ln z) > pi then
  1180                   (Ln(w) + Ln(z)) - ii * of_real(2*pi)
  1181                 else Ln(w) + Ln(z))"
  1182   using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
  1183   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
  1184   by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
  1185 
  1186 lemma Ln_times_simple:
  1187     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
  1188          \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z)"
  1189   by (simp add: Ln_times)
  1190 
  1191 lemma Ln_minus:
  1192   assumes "z \<noteq> 0"
  1193     shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
  1194                      then Ln(z) + ii * pi
  1195                      else Ln(z) - ii * pi)" (is "_ = ?rhs")
  1196   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1197         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
  1198     by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
  1199 
  1200 lemma Ln_inverse_if:
  1201   assumes "z \<noteq> 0"
  1202     shows "Ln (inverse z) =
  1203             (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
  1204              then -(Ln z)
  1205              else -(Ln z) + \<i> * 2 * complex_of_real pi)"
  1206 proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
  1207   case True then show ?thesis
  1208     by (simp add: Ln_inverse)
  1209 next
  1210   case False
  1211   then have z: "Im z = 0" "Re z < 0"
  1212     using assms
  1213     apply auto
  1214     by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
  1215   have "Ln(inverse z) = Ln(- (inverse (-z)))"
  1216     by simp
  1217   also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
  1218     using assms z
  1219     apply (simp add: Ln_minus)
  1220     apply (simp add: field_simps)
  1221     done
  1222   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
  1223     apply (subst Ln_inverse)
  1224     using z assms by auto
  1225   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
  1226     apply (subst Ln_minus [OF assms])
  1227     using assms z
  1228     apply simp
  1229     done
  1230   finally show ?thesis
  1231     using assms z
  1232     by simp
  1233 qed
  1234 
  1235 lemma Ln_times_ii:
  1236   assumes "z \<noteq> 0"
  1237     shows  "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
  1238                           then Ln(z) + ii * of_real pi/2
  1239                           else Ln(z) - ii * of_real(3 * pi/2))"
  1240   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
  1241         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
  1242   by (auto simp: of_real_numeral Ln_times)
  1243 
  1244 
  1245 subsection{*Relation between Square Root and exp/ln, hence its derivative*}
  1246 
  1247 lemma csqrt_exp_Ln:
  1248   assumes "z \<noteq> 0"
  1249     shows "csqrt z = exp(Ln(z) / 2)"
  1250 proof -
  1251   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
  1252     by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
  1253   also have "... = z"
  1254     using assms exp_Ln by blast
  1255   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
  1256     by simp
  1257   also have "... = exp (Ln z / 2)"
  1258     apply (subst csqrt_square)
  1259     using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
  1260     apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+)
  1261     done
  1262   finally show ?thesis using assms csqrt_square
  1263     by simp
  1264 qed
  1265 
  1266 lemma csqrt_inverse:
  1267   assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
  1268     shows "csqrt (inverse z) = inverse (csqrt z)"
  1269 proof (cases "z=0", simp)
  1270   assume "z \<noteq> 0 "
  1271   then show ?thesis
  1272     using assms
  1273     by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
  1274 qed
  1275 
  1276 lemma cnj_csqrt:
  1277   assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
  1278     shows "cnj(csqrt z) = csqrt(cnj z)"
  1279 proof (cases "z=0", simp)
  1280   assume z: "z \<noteq> 0"
  1281   then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1282     using assms cnj.code complex_cnj_zero_iff by fastforce
  1283   then show ?thesis
  1284    using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
  1285 qed
  1286 
  1287 lemma has_field_derivative_csqrt:
  1288   assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
  1289     shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
  1290 proof -
  1291   have z: "z \<noteq> 0"
  1292     using assms by auto
  1293   then have *: "inverse z = inverse (2*z) * 2"
  1294     by (simp add: divide_simps)
  1295   show ?thesis
  1296     apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
  1297     apply (intro derivative_eq_intros | simp add: assms)+
  1298     apply (rule *)
  1299     using z
  1300     apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
  1301     apply (metis power2_csqrt power2_eq_square)
  1302     apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
  1303     done
  1304 qed
  1305 
  1306 lemma complex_differentiable_at_csqrt:
  1307     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
  1308   using complex_differentiable_def has_field_derivative_csqrt by blast
  1309 
  1310 lemma complex_differentiable_within_csqrt:
  1311     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
  1312   using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
  1313 
  1314 lemma continuous_at_csqrt:
  1315     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
  1316   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
  1317 
  1318 corollary isCont_csqrt' [simp]:
  1319    "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
  1320   by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
  1321 
  1322 lemma continuous_within_csqrt:
  1323     "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
  1324   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
  1325 
  1326 lemma continuous_on_csqrt [continuous_intros]:
  1327     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
  1328   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
  1329 
  1330 lemma holomorphic_on_csqrt:
  1331     "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
  1332   by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
  1333 
  1334 lemma continuous_within_closed_nontrivial:
  1335     "closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
  1336   using open_Compl
  1337   by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
  1338 
  1339 lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
  1340   using closed_halfspace_Re_ge
  1341   by (simp add: closed_Int closed_complex_Reals)
  1342 
  1343 lemma continuous_within_csqrt_posreal:
  1344     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
  1345 proof (cases "Im z = 0 --> 0 < Re(z)")
  1346   case True then show ?thesis
  1347     by (blast intro: continuous_within_csqrt)
  1348 next
  1349   case False
  1350   then have "Im z = 0" "Re z < 0 \<or> z = 0"
  1351     using False cnj.code complex_cnj_zero_iff by auto force
  1352   then show ?thesis
  1353     apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
  1354     apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
  1355     apply (rule_tac x="e^2" in exI)
  1356     apply (auto simp: Reals_def)
  1357 by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
  1358 qed
  1359 
  1360 subsection{*Complex arctangent*}
  1361 
  1362 text{*branch cut gives standard bounds in real case.*}
  1363 
  1364 definition Arctan :: "complex \<Rightarrow> complex" where
  1365     "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
  1366 
  1367 lemma Arctan_0 [simp]: "Arctan 0 = 0"
  1368   by (simp add: Arctan_def)
  1369 
  1370 lemma Im_complex_div_lemma: "Im((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<longleftrightarrow> Re z = 0"
  1371   by (auto simp: Im_complex_div_eq_0 algebra_simps)
  1372 
  1373 lemma Re_complex_div_lemma: "0 < Re((1 - \<i>*z) / (1 + \<i>*z)) \<longleftrightarrow> norm z < 1"
  1374   by (simp add: Re_complex_div_gt_0 algebra_simps cmod_def power2_eq_square)
  1375 
  1376 lemma tan_Arctan:
  1377   assumes "z\<^sup>2 \<noteq> -1"
  1378     shows [simp]:"tan(Arctan z) = z"
  1379 proof -
  1380   have "1 + \<i>*z \<noteq> 0"
  1381     by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
  1382   moreover
  1383   have "1 - \<i>*z \<noteq> 0"
  1384     by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq)
  1385   ultimately
  1386   show ?thesis
  1387     by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric]
  1388                   divide_simps power2_eq_square [symmetric])
  1389 qed
  1390 
  1391 lemma Arctan_tan [simp]:
  1392   assumes "\<bar>Re z\<bar> < pi/2"
  1393     shows "Arctan(tan z) = z"
  1394 proof -
  1395   have ge_pi2: "\<And>n::int. abs (of_int (2*n + 1) * pi/2) \<ge> pi/2"
  1396     by (case_tac n rule: int_cases) (auto simp: abs_mult)
  1397   have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
  1398     by (metis distrib_right exp_add mult_2)
  1399   also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
  1400     using cis_conv_exp cis_pi by auto
  1401   also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
  1402     by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
  1403   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)"
  1404     by (simp add: exp_eq_1)
  1405   also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
  1406     by (simp add: algebra_simps)
  1407   also have "... \<longleftrightarrow> False"
  1408     using assms ge_pi2
  1409     apply (auto simp: algebra_simps)
  1410     by (metis abs_mult_pos not_less not_real_of_nat_less_zero real_of_nat_numeral)
  1411   finally have *: "exp (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 0"
  1412     by (auto simp: add.commute minus_unique)
  1413   show ?thesis
  1414     using assms *
  1415     apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
  1416                      ii_times_eq_iff power2_eq_square [symmetric])
  1417     apply (rule Ln_unique)
  1418     apply (auto simp: divide_simps exp_minus)
  1419     apply (simp add: algebra_simps exp_double [symmetric])
  1420     done
  1421 qed
  1422 
  1423 lemma
  1424   assumes "Re z = 0 \<Longrightarrow> abs(Im z) < 1"
  1425   shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
  1426     and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1427 proof -
  1428   have nz0: "1 + \<i>*z \<noteq> 0"
  1429     using assms
  1430     by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
  1431               less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
  1432   have "z \<noteq> -\<i>" using assms
  1433     by auto
  1434   then have zz: "1 + z * z \<noteq> 0"
  1435     by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
  1436   have nz1: "1 - \<i>*z \<noteq> 0"
  1437     using assms by (force simp add: ii_times_eq_iff)
  1438   have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
  1439     using assms
  1440     by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
  1441               less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2))
  1442   have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
  1443     using nz1 nz2 by auto
  1444   have *: "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
  1445     apply (simp add: divide_complex_def)
  1446     apply (simp add: divide_simps split: split_if_asm)
  1447     using assms
  1448     apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
  1449     done
  1450   show "abs(Re(Arctan z)) < pi/2"
  1451     unfolding Arctan_def divide_complex_def
  1452     using mpi_less_Im_Ln [OF nzi]
  1453     by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
  1454   show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
  1455     unfolding Arctan_def scaleR_conv_of_real
  1456     apply (rule DERIV_cong)
  1457     apply (intro derivative_eq_intros | simp add: nz0 *)+
  1458     using nz0 nz1 zz
  1459     apply (simp add: divide_simps power2_eq_square)
  1460     apply (auto simp: algebra_simps)
  1461     done
  1462 qed
  1463 
  1464 lemma complex_differentiable_at_Arctan: "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable at z"
  1465   using has_field_derivative_Arctan
  1466   by (auto simp: complex_differentiable_def)
  1467 
  1468 lemma complex_differentiable_within_Arctan:
  1469     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> Arctan complex_differentiable (at z within s)"
  1470   using complex_differentiable_at_Arctan complex_differentiable_at_within by blast
  1471 
  1472 declare has_field_derivative_Arctan [derivative_intros]
  1473 declare has_field_derivative_Arctan [THEN DERIV_chain2, derivative_intros]
  1474 
  1475 lemma continuous_at_Arctan:
  1476     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z) Arctan"
  1477   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Arctan)
  1478 
  1479 lemma continuous_within_Arctan:
  1480     "(Re z = 0 \<Longrightarrow> abs(Im z) < 1) \<Longrightarrow> continuous (at z within s) Arctan"
  1481   using continuous_at_Arctan continuous_at_imp_continuous_within by blast
  1482 
  1483 lemma continuous_on_Arctan [continuous_intros]:
  1484     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> continuous_on s Arctan"
  1485   by (auto simp: continuous_at_imp_continuous_on continuous_within_Arctan)
  1486 
  1487 lemma holomorphic_on_Arctan:
  1488     "(\<And>z. z \<in> s \<Longrightarrow> Re z = 0 \<Longrightarrow> abs \<bar>Im z\<bar> < 1) \<Longrightarrow> Arctan holomorphic_on s"
  1489   by (simp add: complex_differentiable_within_Arctan holomorphic_on_def)
  1490 
  1491 
  1492 subsection {*Real arctangent*}
  1493 
  1494 lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
  1495   by simp
  1496 
  1497 lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
  1498   by (simp add: complex_norm_eq_1_exp)
  1499 
  1500 lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
  1501   unfolding Arctan_def divide_complex_def
  1502   apply (simp add: complex_eq_iff)
  1503   apply (rule norm_exp_imaginary)
  1504   apply (subst exp_Ln, auto)
  1505   apply (simp_all add: cmod_def complex_eq_iff)
  1506   apply (auto simp: divide_simps)
  1507   apply (metis power_one realpow_two_sum_zero_iff zero_neq_one, algebra)
  1508   done
  1509 
  1510 lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
  1511 proof (rule arctan_unique)
  1512   show "- (pi / 2) < Re (Arctan (complex_of_real x))"
  1513     apply (simp add: Arctan_def)
  1514     apply (rule Im_Ln_less_pi)
  1515     apply (auto simp: Im_complex_div_lemma)
  1516     done
  1517 next
  1518   have *: " (1 - \<i>*x) / (1 + \<i>*x) \<noteq> 0"
  1519     by (simp add: divide_simps) ( simp add: complex_eq_iff)
  1520   show "Re (Arctan (complex_of_real x)) < pi / 2"
  1521     using mpi_less_Im_Ln [OF *]
  1522     by (simp add: Arctan_def)
  1523 next
  1524   have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
  1525     apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos)
  1526     apply (simp add: field_simps)
  1527     by (simp add: power2_eq_square)
  1528   also have "... = x"
  1529     apply (subst tan_Arctan, auto)
  1530     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)
  1531   finally show "tan (Re (Arctan (complex_of_real x))) = x" .
  1532 qed
  1533 
  1534 lemma Arctan_of_real: "Arctan (of_real x) = of_real (arctan x)"
  1535   unfolding arctan_eq_Re_Arctan divide_complex_def
  1536   by (simp add: complex_eq_iff)
  1537 
  1538 lemma Arctan_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Arctan z \<in> \<real>"
  1539   by (metis Reals_cases Reals_of_real Arctan_of_real)
  1540 
  1541 declare arctan_one [simp]
  1542 
  1543 lemma arctan_less_pi4_pos: "x < 1 \<Longrightarrow> arctan x < pi/4"
  1544   by (metis arctan_less_iff arctan_one)
  1545 
  1546 lemma arctan_less_pi4_neg: "-1 < x \<Longrightarrow> -(pi/4) < arctan x"
  1547   by (metis arctan_less_iff arctan_minus arctan_one)
  1548 
  1549 lemma arctan_less_pi4: "abs x < 1 \<Longrightarrow> abs(arctan x) < pi/4"
  1550   by (metis abs_less_iff arctan_less_pi4_pos arctan_minus)
  1551 
  1552 lemma arctan_le_pi4: "abs x \<le> 1 \<Longrightarrow> abs(arctan x) \<le> pi/4"
  1553   by (metis abs_le_iff arctan_le_iff arctan_minus arctan_one)
  1554 
  1555 lemma abs_arctan: "abs(arctan x) = arctan(abs x)"
  1556   by (simp add: abs_if arctan_minus)
  1557 
  1558 lemma arctan_add_raw:
  1559   assumes "abs(arctan x + arctan y) < pi/2"
  1560     shows "arctan x + arctan y = arctan((x + y) / (1 - x * y))"
  1561 proof (rule arctan_unique [symmetric])
  1562   show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
  1563     using assms by linarith+
  1564   show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
  1565     using cos_gt_zero_pi [OF 12]
  1566     by (simp add: arctan tan_add)
  1567 qed
  1568 
  1569 lemma arctan_inverse:
  1570   assumes "0 < x"
  1571     shows "arctan(inverse x) = pi/2 - arctan x"
  1572 proof -
  1573   have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
  1574     by (simp add: arctan)
  1575   also have "... = arctan (tan (pi / 2 - arctan x))"
  1576     by (simp add: tan_cot)
  1577   also have "... = pi/2 - arctan x"
  1578   proof -
  1579     have "0 < pi - arctan x"
  1580     using arctan_ubound [of x] pi_gt_zero by linarith
  1581     with assms show ?thesis
  1582       by (simp add: Transcendental.arctan_tan)
  1583   qed
  1584   finally show ?thesis .
  1585 qed
  1586 
  1587 lemma arctan_add_small:
  1588   assumes "abs(x * y) < 1"
  1589     shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))"
  1590 proof (cases "x = 0 \<or> y = 0")
  1591   case True then show ?thesis
  1592     by auto
  1593 next
  1594   case False
  1595   then have *: "\<bar>arctan x\<bar> < pi / 2 - \<bar>arctan y\<bar>" using assms
  1596     apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff)
  1597     apply (simp add: divide_simps abs_mult)
  1598     done
  1599   show ?thesis
  1600     apply (rule arctan_add_raw)
  1601     using * by linarith
  1602 qed
  1603 
  1604 lemma abs_arctan_le:
  1605   fixes x::real shows "abs(arctan x) \<le> abs x"
  1606 proof -
  1607   { fix w::complex and z::complex
  1608     assume *: "w \<in> \<real>" "z \<in> \<real>"
  1609     have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
  1610       apply (rule complex_differentiable_bound [OF convex_Reals, of Arctan _ 1])
  1611       apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
  1612       apply (force simp add: Reals_def)
  1613       apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
  1614       using * by auto
  1615   }
  1616   then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
  1617     using Reals_0 Reals_of_real by blast
  1618   then show ?thesis
  1619     by (simp add: Arctan_of_real)
  1620 qed
  1621 
  1622 lemma arctan_le_self: "0 \<le> x \<Longrightarrow> arctan x \<le> x"
  1623   by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff)
  1624 
  1625 lemma abs_tan_ge: "abs x < pi/2 \<Longrightarrow> abs x \<le> abs(tan x)"
  1626   by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
  1627 
  1628 
  1629 subsection{*Inverse Sine*}
  1630 
  1631 definition Arcsin :: "complex \<Rightarrow> complex" where
  1632    "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))"
  1633 
  1634 lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
  1635   using power2_csqrt [of "1 - z\<^sup>2"]
  1636   apply auto
  1637   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)
  1638 
  1639 lemma Arcsin_range_lemma: "abs (Re z) < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
  1640   using Complex.cmod_power2 [of z, symmetric]
  1641   by (simp add: real_less_rsqrt algebra_simps Re_power2 cmod_square_less_1_plus)
  1642 
  1643 lemma Re_Arcsin: "Re(Arcsin z) = Im (Ln (\<i> * z + csqrt(1 - z\<^sup>2)))"
  1644   by (simp add: Arcsin_def)
  1645 
  1646 lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
  1647   by (simp add: Arcsin_def Arcsin_body_lemma)
  1648 
  1649 lemma isCont_Arcsin:
  1650   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1651     shows "isCont Arcsin z"
  1652 proof -
  1653   have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
  1654     using assms
  1655     by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
  1656   have cmz: "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
  1657     by (blast intro: assms cmod_square_less_1_plus)
  1658   show ?thesis
  1659     using assms
  1660     apply (simp add: Arcsin_def)
  1661     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  1662     apply (erule rez)
  1663     apply (auto simp: Re_power2 Im_power2 abs_square_less_1 [symmetric] real_less_rsqrt algebra_simps split: split_if_asm)
  1664     apply (simp add: norm_complex_def)
  1665     using cmod_power2 [of z, symmetric] cmz
  1666     apply (simp add: real_less_rsqrt)
  1667     done
  1668 qed
  1669 
  1670 lemma isCont_Arcsin' [simp]:
  1671   shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
  1672   by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
  1673 
  1674 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
  1675 proof -  
  1676   have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
  1677     by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
  1678   moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
  1679     by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
  1680   ultimately show ?thesis
  1681     apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
  1682     apply (simp add: algebra_simps)
  1683     apply (simp add: power2_eq_square [symmetric] algebra_simps)
  1684     done
  1685 qed
  1686 
  1687 lemma Re_eq_pihalf_lemma:
  1688     "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
  1689       Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  1690   apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
  1691   by (metis cos_minus cos_pi_half)
  1692 
  1693 lemma Re_less_pihalf_lemma:
  1694   assumes "\<bar>Re z\<bar> < pi / 2"
  1695     shows "0 < Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
  1696 proof -
  1697   have "0 < cos (Re z)" using assms
  1698     using cos_gt_zero_pi by auto
  1699   then show ?thesis
  1700     by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
  1701 qed
  1702 
  1703 lemma Arcsin_sin:
  1704     assumes "\<bar>Re z\<bar> < pi/2 \<or> (\<bar>Re z\<bar> = pi/2 \<and> Im z = 0)"
  1705       shows "Arcsin(sin z) = z"
  1706 proof -
  1707   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))"
  1708     by (simp add: sin_exp_eq Arcsin_def exp_minus)
  1709   also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  1710     by (simp add: field_simps power2_eq_square)
  1711   also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
  1712     apply (subst csqrt_square)
  1713     using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma
  1714     apply auto
  1715     done
  1716   also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  1717     by (simp add: field_simps power2_eq_square)
  1718   also have "... = z"
  1719     apply (subst Complex_Transcendental.Ln_exp)
  1720     using assms
  1721     apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: split_if_asm)
  1722     done
  1723   finally show ?thesis .
  1724 qed
  1725 
  1726 lemma Arcsin_unique:
  1727     "\<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"
  1728   by (metis Arcsin_sin)
  1729 
  1730 lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
  1731   by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
  1732 
  1733 lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
  1734   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)
  1735 
  1736 lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
  1737   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)
  1738 
  1739 lemma has_field_derivative_Arcsin:
  1740   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1741     shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
  1742 proof -
  1743   have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
  1744     using assms
  1745     apply atomize
  1746     apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  1747     apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  1748     by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
  1749   then have "cos (Arcsin z) \<noteq> 0"
  1750     by (metis diff_0_right power_zero_numeral sin_squared_eq)
  1751   then show ?thesis
  1752     apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin])
  1753     apply (auto intro: isCont_Arcsin open_ball [of z 1] assms)
  1754     done
  1755 qed
  1756 
  1757 declare has_field_derivative_Arcsin [derivative_intros]
  1758 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  1759 
  1760 lemma complex_differentiable_at_Arcsin:
  1761     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable at z"
  1762   using complex_differentiable_def has_field_derivative_Arcsin by blast
  1763 
  1764 lemma complex_differentiable_within_Arcsin:
  1765     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin complex_differentiable (at z within s)"
  1766   using complex_differentiable_at_Arcsin complex_differentiable_within_subset by blast
  1767 
  1768 lemma continuous_within_Arcsin:
  1769     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arcsin"
  1770   using continuous_at_imp_continuous_within isCont_Arcsin by blast
  1771 
  1772 lemma continuous_on_Arcsin [continuous_intros]:
  1773     "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arcsin"
  1774   by (simp add: continuous_at_imp_continuous_on)
  1775 
  1776 lemma holomorphic_on_Arcsin: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arcsin holomorphic_on s"
  1777   by (simp add: complex_differentiable_within_Arcsin holomorphic_on_def)
  1778 
  1779 
  1780 subsection{*Inverse Cosine*}
  1781 
  1782 definition Arccos :: "complex \<Rightarrow> complex" where
  1783    "Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
  1784 
  1785 lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
  1786   using Arcsin_range_lemma [of "-z"]
  1787   by simp
  1788 
  1789 lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
  1790   using Arcsin_body_lemma [of z]
  1791   by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
  1792            power2_csqrt power2_eq_square zero_neq_one)
  1793 
  1794 lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
  1795   by (simp add: Arccos_def)
  1796 
  1797 lemma Im_Arccos: "Im(Arccos z) = - ln (cmod (z + \<i> * csqrt (1 - z\<^sup>2)))"
  1798   by (simp add: Arccos_def Arccos_body_lemma)
  1799 
  1800 text{*A very tricky argument to find!*}
  1801 lemma abs_Re_less_1_preserve:
  1802   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
  1803     shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
  1804 proof (cases "Im z = 0")
  1805   case True
  1806   then show ?thesis
  1807     using assms 
  1808     by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
  1809 next
  1810   case False
  1811   have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  1812     using assms abs_Re_le_cmod [of "1-z\<^sup>2"]
  1813     by (simp add: Re_power2 algebra_simps)
  1814   have "(cmod z)\<^sup>2 - 1 \<noteq> cmod (1 - z\<^sup>2)"
  1815   proof (clarsimp simp add: cmod_def)
  1816     assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 - 1 = sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
  1817     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)"
  1818       by simp
  1819     then show False using False
  1820       by (simp add: power2_eq_square algebra_simps)
  1821   qed
  1822   moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
  1823     apply (subst Imz, simp)
  1824     apply (subst real_sqrt_pow2)
  1825     using abs_Re_le_cmod [of "1-z\<^sup>2"]
  1826     apply (auto simp: Re_power2 field_simps)
  1827     done
  1828   ultimately show ?thesis
  1829     by (simp add: Re_power2 Im_power2 cmod_power2)
  1830 qed
  1831 
  1832 lemma isCont_Arccos:
  1833   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1834     shows "isCont Arccos z"
  1835 proof -
  1836   have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
  1837     using assms
  1838     by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
  1839   show ?thesis
  1840     using assms
  1841     apply (simp add: Arccos_def)
  1842     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
  1843     apply (erule rez)
  1844     apply (blast intro: abs_Re_less_1_preserve)
  1845     done
  1846 qed
  1847 
  1848 lemma isCont_Arccos' [simp]:
  1849   shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arccos (f x)) z"
  1850   by (blast intro: isCont_o2 [OF _ isCont_Arccos])
  1851 
  1852 lemma cos_Arccos [simp]: "cos(Arccos z) = z"
  1853 proof -
  1854   have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
  1855     by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
  1856   moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
  1857     by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
  1858   ultimately show ?thesis
  1859     apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps)
  1860     apply (simp add: power2_eq_square [symmetric])
  1861     done
  1862 qed
  1863 
  1864 lemma Arccos_cos:
  1865     assumes "0 < Re z & Re z < pi \<or>
  1866              Re z = 0 & 0 \<le> Im z \<or>
  1867              Re z = pi & Im z \<le> 0"
  1868       shows "Arccos(cos z) = z"
  1869 proof -
  1870   have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
  1871     by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
  1872   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"
  1873     by (simp add: field_simps power2_eq_square)
  1874   then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  1875                            \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
  1876     by (simp add: cos_exp_eq Arccos_def exp_minus)
  1877   also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  1878                               \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
  1879     apply (subst csqrt_square)
  1880     using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
  1881     apply (auto simp: * Re_sin Im_sin)
  1882     done
  1883   also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
  1884     by (simp add: field_simps power2_eq_square)
  1885   also have "... = z"
  1886     using assms
  1887     apply (subst Complex_Transcendental.Ln_exp, auto)
  1888     done
  1889   finally show ?thesis .
  1890 qed
  1891 
  1892 lemma Arccos_unique:
  1893     "\<lbrakk>cos z = w;
  1894       0 < Re z \<and> Re z < pi \<or>
  1895       Re z = 0 \<and> 0 \<le> Im z \<or>
  1896       Re z = pi \<and> Im z \<le> 0\<rbrakk> \<Longrightarrow> Arccos w = z"
  1897   using Arccos_cos by blast
  1898 
  1899 lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
  1900   by (rule Arccos_unique) (auto simp: of_real_numeral)
  1901 
  1902 lemma Arccos_1 [simp]: "Arccos 1 = 0"
  1903   by (rule Arccos_unique) auto
  1904 
  1905 lemma Arccos_minus1: "Arccos(-1) = pi"
  1906   by (rule Arccos_unique) auto
  1907 
  1908 lemma has_field_derivative_Arccos:
  1909   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
  1910     shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
  1911 proof -
  1912   have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
  1913     using assms
  1914     apply atomize
  1915     apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
  1916     apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
  1917     apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
  1918     done
  1919   then have "- sin (Arccos z) \<noteq> 0"
  1920     by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
  1921   then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
  1922     apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos])
  1923     apply (auto intro: isCont_Arccos open_ball [of z 1] assms)
  1924     done
  1925   then show ?thesis
  1926     by simp
  1927 qed
  1928 
  1929 declare has_field_derivative_Arcsin [derivative_intros]
  1930 declare has_field_derivative_Arcsin [THEN DERIV_chain2, derivative_intros]
  1931 
  1932 lemma complex_differentiable_at_Arccos:
  1933     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable at z"
  1934   using complex_differentiable_def has_field_derivative_Arccos by blast
  1935 
  1936 lemma complex_differentiable_within_Arccos:
  1937     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos complex_differentiable (at z within s)"
  1938   using complex_differentiable_at_Arccos complex_differentiable_within_subset by blast
  1939 
  1940 lemma continuous_within_Arccos:
  1941     "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous (at z within s) Arccos"
  1942   using continuous_at_imp_continuous_within isCont_Arccos by blast
  1943 
  1944 lemma continuous_on_Arccos [continuous_intros]:
  1945     "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> continuous_on s Arccos"
  1946   by (simp add: continuous_at_imp_continuous_on)
  1947 
  1948 lemma holomorphic_on_Arccos: "(\<And>z. z \<in> s \<Longrightarrow> Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1) \<Longrightarrow> Arccos holomorphic_on s"
  1949   by (simp add: complex_differentiable_within_Arccos holomorphic_on_def)
  1950 
  1951 
  1952 subsection{*Upper and Lower Bounds for Inverse Sine and Cosine*}
  1953 
  1954 lemma Arcsin_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> abs(Re(Arcsin z)) < pi/2"
  1955   unfolding Re_Arcsin
  1956   by (blast intro: Re_Ln_pos_lt_imp Arcsin_range_lemma)
  1957 
  1958 lemma Arccos_bounds: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(Arccos z) \<and> Re(Arccos z) < pi"
  1959   unfolding Re_Arccos
  1960   by (blast intro!: Im_Ln_pos_lt_imp Arccos_range_lemma)
  1961 
  1962 lemma Re_Arccos_bounds: "-pi < Re(Arccos z) \<and> Re(Arccos z) \<le> pi"
  1963   unfolding Re_Arccos
  1964   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
  1965 
  1966 lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
  1967   using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast
  1968 
  1969 lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
  1970   unfolding Re_Arcsin
  1971   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
  1972 
  1973 lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
  1974   using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
  1975 
  1976 
  1977 subsection{*Interrelations between Arcsin and Arccos*}
  1978 
  1979 lemma cos_Arcsin_nonzero:
  1980   assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
  1981 proof -
  1982   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
  1983     by (simp add: power_mult_distrib algebra_simps)
  1984   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
  1985   proof
  1986     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
  1987     then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
  1988       by simp
  1989     then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
  1990       using eq power2_eq_square by auto
  1991     then show False
  1992       using assms by simp
  1993   qed
  1994   then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
  1995     by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
  1996   then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2"  (*FIXME cancel_numeral_factor*)
  1997     by (metis mult_cancel_left zero_neq_numeral)
  1998   then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
  1999     using assms
  2000     apply (auto simp: power2_sum)
  2001     apply (simp add: power2_eq_square algebra_simps)
  2002     done
  2003   then show ?thesis
  2004     apply (simp add: cos_exp_eq Arcsin_def exp_minus)
  2005     apply (simp add: divide_simps Arcsin_body_lemma)
  2006     apply (metis add.commute minus_unique power2_eq_square)
  2007     done
  2008 qed
  2009 
  2010 lemma sin_Arccos_nonzero:
  2011   assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
  2012 proof -
  2013   have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
  2014     by (simp add: power_mult_distrib algebra_simps)
  2015   have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
  2016   proof
  2017     assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
  2018     then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
  2019       by simp
  2020     then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
  2021       using eq power2_eq_square by auto
  2022     then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
  2023       using assms
  2024       by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
  2025     then show False
  2026       using assms by simp
  2027   qed
  2028   then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
  2029     by (simp add: algebra_simps)
  2030   then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
  2031     by (metis mult_cancel_left2 zero_neq_numeral)  (*FIXME cancel_numeral_factor*)
  2032   then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
  2033     using assms
  2034     apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib)
  2035     apply (simp add: power2_eq_square algebra_simps)
  2036     done
  2037   then show ?thesis
  2038     apply (simp add: sin_exp_eq Arccos_def exp_minus)
  2039     apply (simp add: divide_simps Arccos_body_lemma)
  2040     apply (simp add: power2_eq_square)
  2041     done
  2042 qed
  2043 
  2044 lemma cos_sin_csqrt:
  2045   assumes "0 < cos(Re z)  \<or>  cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
  2046     shows "cos z = csqrt(1 - (sin z)\<^sup>2)"
  2047   apply (rule csqrt_unique [THEN sym])
  2048   apply (simp add: cos_squared_eq)
  2049   using assms
  2050   apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
  2051   apply (auto simp: algebra_simps)
  2052   done
  2053 
  2054 lemma sin_cos_csqrt:
  2055   assumes "0 < sin(Re z)  \<or>  sin(Re z) = 0 \<and> 0 \<le> Im z * cos(Re z)"
  2056     shows "sin z = csqrt(1 - (cos z)\<^sup>2)"
  2057   apply (rule csqrt_unique [THEN sym])
  2058   apply (simp add: sin_squared_eq)
  2059   using assms
  2060   apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
  2061   apply (auto simp: algebra_simps)
  2062   done
  2063 
  2064 lemma Arcsin_Arccos_csqrt_pos:
  2065     "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
  2066   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  2067 
  2068 lemma Arccos_Arcsin_csqrt_pos:
  2069     "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
  2070   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
  2071 
  2072 lemma sin_Arccos:
  2073     "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
  2074   by (simp add: Arccos_Arcsin_csqrt_pos)
  2075 
  2076 lemma cos_Arcsin:
  2077     "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
  2078   by (simp add: Arcsin_Arccos_csqrt_pos)
  2079 
  2080 
  2081 subsection{*Relationship with Arcsin on the Real Numbers*}
  2082 
  2083 lemma Im_Arcsin_of_real:
  2084   assumes "abs x \<le> 1"
  2085     shows "Im (Arcsin (of_real x)) = 0"
  2086 proof -
  2087   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  2088     by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  2089   then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  2090     using assms abs_square_le_1
  2091     by (force simp add: Complex.cmod_power2)
  2092   then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
  2093     by (simp add: norm_complex_def)
  2094   then show ?thesis
  2095     by (simp add: Im_Arcsin exp_minus)
  2096 qed
  2097 
  2098 corollary Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
  2099   by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  2100 
  2101 lemma arcsin_eq_Re_Arcsin:
  2102   assumes "abs x \<le> 1"
  2103     shows "arcsin x = Re (Arcsin (of_real x))"
  2104 unfolding arcsin_def
  2105 proof (rule the_equality, safe)
  2106   show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
  2107     using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  2108     by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  2109 next
  2110   show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
  2111     using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
  2112     by (auto simp: Complex.in_Reals_norm Re_Arcsin)
  2113 next
  2114   show "sin (Re (Arcsin (complex_of_real x))) = x"
  2115     using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
  2116     by (simp add: Im_Arcsin_of_real assms)
  2117 next
  2118   fix x'
  2119   assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
  2120   then show "x' = Re (Arcsin (complex_of_real (sin x')))"
  2121     apply (simp add: sin_of_real [symmetric])
  2122     apply (subst Arcsin_sin)
  2123     apply (auto simp: )
  2124     done
  2125 qed
  2126 
  2127 lemma of_real_arcsin: "abs x \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
  2128   by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
  2129 
  2130 
  2131 subsection{*Relationship with Arccos on the Real Numbers*}
  2132 
  2133 lemma Im_Arccos_of_real:
  2134   assumes "abs x \<le> 1"
  2135     shows "Im (Arccos (of_real x)) = 0"
  2136 proof -
  2137   have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  2138     by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  2139   then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
  2140     using assms abs_square_le_1
  2141     by (force simp add: Complex.cmod_power2)
  2142   then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
  2143     by (simp add: norm_complex_def)
  2144   then show ?thesis
  2145     by (simp add: Im_Arccos exp_minus)
  2146 qed
  2147 
  2148 corollary Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
  2149   by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
  2150 
  2151 lemma arccos_eq_Re_Arccos:
  2152   assumes "abs x \<le> 1"
  2153     shows "arccos x = Re (Arccos (of_real x))"
  2154 unfolding arccos_def
  2155 proof (rule the_equality, safe)
  2156   show "0 \<le> Re (Arccos (complex_of_real x))"
  2157     using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  2158     by (auto simp: Complex.in_Reals_norm Re_Arccos)
  2159 next
  2160   show "Re (Arccos (complex_of_real x)) \<le> pi"
  2161     using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
  2162     by (auto simp: Complex.in_Reals_norm Re_Arccos)
  2163 next
  2164   show "cos (Re (Arccos (complex_of_real x))) = x"
  2165     using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
  2166     by (simp add: Im_Arccos_of_real assms)
  2167 next
  2168   fix x'
  2169   assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
  2170   then show "x' = Re (Arccos (complex_of_real (cos x')))"
  2171     apply (simp add: cos_of_real [symmetric])
  2172     apply (subst Arccos_cos)
  2173     apply (auto simp: )
  2174     done
  2175 qed
  2176 
  2177 lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
  2178   by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
  2179 
  2180 end