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