Rationalisation of complex transcendentals, esp the Arg function
authorpaulson <lp15@cam.ac.uk>
Tue Jun 26 14:51:18 2018 +0100 (17 months ago ago)
changeset 68495d4312962161a
parent 68494 ebdd5508f386
child 68500 e3e742b9eed4
Rationalisation of complex transcendentals, esp the Arg function
NEWS
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/Library/Nonpos_Ints.thy
src/HOL/Nonstandard_Analysis/NSComplex.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Mon Jun 25 14:06:50 2018 +0100
     1.2 +++ b/NEWS	Tue Jun 26 14:51:18 2018 +0100
     1.3 @@ -386,6 +386,10 @@
     1.4  The set of isomorphisms between two groups is now denoted iso rather than iso_set.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOL-Analysis: the Arg function now respects the same interval as
     1.8 +Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. 
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Session HOL-Analysis: infinite products, Moebius functions, the
    1.12  Riemann mapping theorem, the Vitali covering theorem,
    1.13  change-of-variables results for integration and measures.
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 25 14:06:50 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jun 26 14:51:18 2018 +0100
     2.3 @@ -9,12 +9,6 @@
     2.4     "HOL-Library.Periodic_Fun"
     2.5  begin
     2.6  
     2.7 -(* TODO: MOVE *)
     2.8 -lemma nonpos_Reals_inverse_iff [simp]:
     2.9 -  fixes a :: "'a::real_div_algebra"
    2.10 -  shows "inverse a \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> a \<in> \<real>\<^sub>\<le>\<^sub>0"
    2.11 -  using nonpos_Reals_inverse_I by fastforce
    2.12 -
    2.13  (* TODO: Figure out what to do with Möbius transformations *)
    2.14  definition "moebius a b c d = (\<lambda>z. (a*z+b) / (c*z+d :: 'a :: field))"
    2.15  
    2.16 @@ -70,6 +64,12 @@
    2.17  
    2.18  subsection\<open>The Exponential Function is Differentiable and Continuous\<close>
    2.19  
    2.20 +lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
    2.21 +  by simp
    2.22 +
    2.23 +lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
    2.24 +  by simp
    2.25 +
    2.26  lemma field_differentiable_within_exp: "exp field_differentiable (at z within s)"
    2.27    using DERIV_exp field_differentiable_at_within field_differentiable_def by blast
    2.28  
    2.29 @@ -218,7 +218,8 @@
    2.30      by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)
    2.31  next
    2.32    assume ?rhs then show ?lhs
    2.33 -    using Im_exp Re_exp complex_Re_Im_cancel_iff by force
    2.34 +    using Im_exp Re_exp complex_eq_iff
    2.35 +    by (simp add: cos_one_2pi_int cos_one_sin_zero mult.commute)
    2.36  qed
    2.37  
    2.38  lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
    2.39 @@ -277,16 +278,16 @@
    2.40      by (auto simp: norm_mult)
    2.41  qed
    2.42  
    2.43 -lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
    2.44 +lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * pi * n)"
    2.45  proof -
    2.46    { assume "sin y = sin x" "cos y = cos x"
    2.47      then have "cos (y-x) = 1"
    2.48        using cos_add [of y "-x"] by simp
    2.49 -    then have "\<exists>n::int. y-x = n * 2 * pi"
    2.50 -      using cos_one_2pi_int by blast }
    2.51 +    then have "\<exists>n::int. y-x = 2 * pi * n"
    2.52 +      using cos_one_2pi_int by auto }
    2.53    then show ?thesis
    2.54    apply (auto simp: sin_add cos_add)
    2.55 -  apply (metis add.commute diff_add_cancel mult.commute)
    2.56 +  apply (metis add.commute diff_add_cancel)
    2.57    done
    2.58  qed
    2.59  
    2.60 @@ -768,19 +769,26 @@
    2.61  lemma ln3_gt_1: "ln 3 > (1::real)"
    2.62    by (simp add: less_trans [OF ln_272_gt_1])
    2.63  
    2.64 -subsection\<open>The argument of a complex number\<close>
    2.65 -
    2.66 -definition Arg2pi :: "complex \<Rightarrow> real" where
    2.67 - "Arg2pi z \<equiv> if z = 0 then 0
    2.68 -           else THE t. 0 \<le> t \<and> t < 2*pi \<and>
    2.69 -                    z = of_real(norm z) * exp(\<i> * of_real t)"
    2.70 +subsection\<open>The argument of a complex number (HOL Light version)\<close>
    2.71 +
    2.72 +definition is_Arg :: "[complex,real] \<Rightarrow> bool"
    2.73 +  where "is_Arg z r \<equiv> z = of_real(norm z) * exp(\<i> * of_real r)"
    2.74 +
    2.75 +definition Arg2pi :: "complex \<Rightarrow> real"
    2.76 +  where "Arg2pi z \<equiv> if z = 0 then 0 else THE t. 0 \<le> t \<and> t < 2*pi \<and> is_Arg z t"
    2.77 +
    2.78 +text\<open>This function returns the angle of a complex number from its representation in polar coordinates.
    2.79 +Due to periodicity, its range is arbitrary. @{term Arg2pi} follows HOL Light in adopting the interval $[0,2\pi)$.
    2.80 +But we have the same periodicity issue with logarithms, and it is usual to adopt the same interval
    2.81 +for the complex logarithm and argument functions. Further on down, we shall define both functions for the interval $(-\pi,\pi]$.
    2.82 +The present version is provided for compatibility.\<close>
    2.83  
    2.84  lemma Arg2pi_0 [simp]: "Arg2pi(0) = 0"
    2.85    by (simp add: Arg2pi_def)
    2.86  
    2.87  lemma Arg2pi_unique_lemma:
    2.88 -  assumes z:  "z = of_real(norm z) * exp(\<i> * of_real t)"
    2.89 -      and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
    2.90 +  assumes z:  "is_Arg z t"
    2.91 +      and z': "is_Arg z t'"
    2.92        and t:  "0 \<le> t"  "t < 2*pi"
    2.93        and t': "0 \<le> t'" "t' < 2*pi"
    2.94        and nz: "z \<noteq> 0"
    2.95 @@ -789,9 +797,9 @@
    2.96    have [dest]: "\<And>x y z::real. x\<ge>0 \<Longrightarrow> x+y < z \<Longrightarrow> y<z"
    2.97      by arith
    2.98    have "of_real (cmod z) * exp (\<i> * of_real t') = of_real (cmod z) * exp (\<i> * of_real t)"
    2.99 -    by (metis z z')
   2.100 +    by (metis z z' is_Arg_def)
   2.101    then have "exp (\<i> * of_real t') = exp (\<i> * of_real t)"
   2.102 -    by (metis nz mult_left_cancel mult_zero_left z)
   2.103 +    by (metis nz mult_left_cancel mult_zero_left z is_Arg_def)
   2.104    then have "sin t' = sin t \<and> cos t' = cos t"
   2.105      apply (simp add: exp_Euler sin_of_real cos_of_real)
   2.106      by (metis Complex_eq complex.sel)
   2.107 @@ -803,17 +811,18 @@
   2.108      by (simp add: n)
   2.109  qed
   2.110  
   2.111 -lemma Arg2pi: "0 \<le> Arg2pi z & Arg2pi z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
   2.112 +lemma Arg2pi: "0 \<le> Arg2pi z \<and> Arg2pi z < 2*pi \<and> is_Arg z (Arg2pi z)"
   2.113  proof (cases "z=0")
   2.114    case True then show ?thesis
   2.115 -    by (simp add: Arg2pi_def)
   2.116 +    by (simp add: Arg2pi_def is_Arg_def)
   2.117  next
   2.118    case False
   2.119    obtain t where t: "0 \<le> t" "t < 2*pi"
   2.120               and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
   2.121      using sincos_total_2pi [OF complex_unit_circle [OF False]]
   2.122      by blast
   2.123 -  have z: "z = of_real(norm z) * exp(\<i> * of_real t)"
   2.124 +  have z: "is_Arg z t"
   2.125 +    unfolding is_Arg_def
   2.126      apply (rule complex_eqI)
   2.127      using t False ReIm
   2.128      apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
   2.129 @@ -830,14 +839,13 @@
   2.130    shows Arg2pi_ge_0: "0 \<le> Arg2pi z"
   2.131      and Arg2pi_lt_2pi: "Arg2pi z < 2*pi"
   2.132      and Arg2pi_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg2pi z))"
   2.133 -  using Arg2pi by auto
   2.134 +  using Arg2pi is_Arg_def by auto
   2.135  
   2.136  lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg2pi z)) = z"
   2.137    by (metis Arg2pi_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
   2.138  
   2.139  lemma Arg2pi_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg2pi z = a"
   2.140 -  by (rule Arg2pi_unique_lemma [OF _ Arg2pi_eq])
   2.141 -  (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)
   2.142 +  by (rule Arg2pi_unique_lemma [unfolded is_Arg_def, OF _ Arg2pi_eq]) (use Arg2pi [of z] in \<open>auto simp: norm_mult\<close>)
   2.143  
   2.144  lemma Arg2pi_minus: "z \<noteq> 0 \<Longrightarrow> Arg2pi (-z) = (if Arg2pi z < pi then Arg2pi z + pi else Arg2pi z - pi)"
   2.145    apply (rule Arg2pi_unique [of "norm z"])
   2.146 @@ -852,7 +860,7 @@
   2.147  proof (cases "z=0")
   2.148    case False
   2.149    show ?thesis
   2.150 -    by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms in auto)
   2.151 +    by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto)
   2.152  qed auto
   2.153  
   2.154  lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
   2.155 @@ -911,28 +919,31 @@
   2.156  qed auto
   2.157  
   2.158  corollary Arg2pi_gt_0:
   2.159 -  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
   2.160 +  assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
   2.161      shows "Arg2pi z > 0"
   2.162 -  using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order by fastforce
   2.163 +  using Arg2pi_eq_0 Arg2pi_ge_0 assms dual_order.strict_iff_order
   2.164 +  unfolding nonneg_Reals_def by fastforce
   2.165  
   2.166  lemma Arg2pi_of_real: "Arg2pi(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   2.167    by (simp add: Arg2pi_eq_0)
   2.168  
   2.169  lemma Arg2pi_eq_pi: "Arg2pi z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   2.170 -  using Arg2pi_eq_0 [of "-z"]
   2.171 -  by (metis Arg2pi_eq_0 Arg2pi_gt_0 Arg2pi_le_pi Arg2pi_lt_pi complex_is_Real_iff dual_order.order_iff_strict not_less pi_neq_zero)
   2.172 +    using Arg2pi_le_pi [of z] Arg2pi_lt_pi [of z] Arg2pi_eq_0 [of z] Arg2pi_ge_0 [of z] 
   2.173 +    by (fastforce simp: complex_is_Real_iff)
   2.174  
   2.175  lemma Arg2pi_eq_0_pi: "Arg2pi z = 0 \<or> Arg2pi z = pi \<longleftrightarrow> z \<in> \<real>"
   2.176    using Arg2pi_eq_0 Arg2pi_eq_pi not_le by auto
   2.177  
   2.178 -lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
   2.179 +lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
   2.180 +  using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
   2.181 +
   2.182 +lemma Arg2pi_inverse: "Arg2pi(inverse z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
   2.183  proof (cases "z=0")
   2.184    case False
   2.185    show ?thesis
   2.186      apply (rule Arg2pi_unique [of "inverse (norm z)"])
   2.187 -    using False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq [of z] Arg2pi_eq_0 [of z]
   2.188 -       apply (auto simp: exp_diff field_simps)
   2.189 -    done
   2.190 +    using Arg2pi_eq False Arg2pi_ge_0 [of z] Arg2pi_lt_2pi [of z] Arg2pi_eq_0 [of z]
   2.191 +    by (auto simp: Arg2pi_real in_Reals_norm exp_diff field_simps)
   2.192  qed auto
   2.193  
   2.194  lemma Arg2pi_eq_iff:
   2.195 @@ -968,9 +979,8 @@
   2.196  lemma Arg2pi_diff:
   2.197    assumes "w \<noteq> 0" "z \<noteq> 0"
   2.198      shows "Arg2pi w - Arg2pi z = (if Arg2pi z \<le> Arg2pi w then Arg2pi(w / z) else Arg2pi(w/z) - 2*pi)"
   2.199 -  using assms Arg2pi_divide Arg2pi_inverse [of "w/z"]
   2.200 -  apply (clarsimp simp add: Arg2pi_ge_0 Arg2pi_divide not_le)
   2.201 -  by (metis Arg2pi_eq_0 less_irrefl minus_diff_eq right_minus_eq)
   2.202 +  using assms Arg2pi_divide Arg2pi_inverse [of "w/z"] Arg2pi_eq_0_pi
   2.203 +  by (force simp add: Arg2pi_ge_0 Arg2pi_divide not_le split: if_split_asm)
   2.204  
   2.205  lemma Arg2pi_add:
   2.206    assumes "w \<noteq> 0" "z \<noteq> 0"
   2.207 @@ -992,22 +1002,19 @@
   2.208    apply (simp add: Arg2pi_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   2.209    by (metis of_real_power zero_less_norm_iff zero_less_power)
   2.210  
   2.211 -lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg2pi z else 2*pi - Arg2pi z)"
   2.212 +lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
   2.213  proof (cases "z=0")
   2.214    case False
   2.215    then show ?thesis
   2.216      by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
   2.217  qed auto
   2.218  
   2.219 -lemma Arg2pi_real: "z \<in> \<real> \<Longrightarrow> Arg2pi z = (if 0 \<le> Re z then 0 else pi)"
   2.220 -  using Arg2pi_eq_0 Arg2pi_eq_0_pi by auto
   2.221 -
   2.222  lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
   2.223    by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
   2.224  
   2.225  lemma complex_split_polar:
   2.226    obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
   2.227 -  using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
   2.228 +  using Arg2pi cis.ctr cis_conv_exp unfolding Complex_eq is_Arg_def by fastforce
   2.229  
   2.230  lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
   2.231  proof (cases w rule: complex_split_polar)
   2.232 @@ -1447,6 +1454,23 @@
   2.233  by (simp add: ln_inverse Ln_of_real mult.commute divide_inverse of_real_inverse [symmetric]
   2.234           del: of_real_inverse)
   2.235  
   2.236 +corollary Ln_prod:
   2.237 +  fixes f :: "'a \<Rightarrow> complex"
   2.238 +  assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
   2.239 +  shows "\<exists>n. Ln (prod f A) = (\<Sum>x \<in> A. Ln (f x) + (of_int (n x) * (2 * pi)) * \<i>)"
   2.240 +  using assms
   2.241 +proof (induction A)
   2.242 +  case (insert x A)
   2.243 +  then obtain n where n: "Ln (prod f A) = (\<Sum>x\<in>A. Ln (f x) + of_real (of_int (n x) * (2 * pi)) * \<i>)"
   2.244 +    by auto
   2.245 +  define D where "D \<equiv> Im (Ln (f x)) + Im (Ln (prod f A))"
   2.246 +  define q::int where "q \<equiv> (if D \<le> -pi then 1 else if D > pi then -1 else 0)"
   2.247 +  have "prod f A \<noteq> 0" "f x \<noteq> 0"
   2.248 +    by (auto simp: insert.hyps insert.prems)
   2.249 +  with insert.hyps pi_ge_zero show ?case
   2.250 +    by (rule_tac x="n(x:=q)" in exI) (force simp: Ln_times q_def D_def n intro!: sum.cong)
   2.251 +qed auto
   2.252 +
   2.253  lemma Ln_minus:
   2.254    assumes "z \<noteq> 0"
   2.255      shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
   2.256 @@ -1528,6 +1552,167 @@
   2.257    shows   "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel"
   2.258    using assms by (simp add: powr_def)
   2.259  
   2.260 +subsection\<open>The Argument of a Complex Number\<close>
   2.261 +
   2.262 +definition Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
   2.263 +
   2.264 +text\<open>Finally the Argument is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
   2.265 +
   2.266 +lemma Arg_unique_lemma:
   2.267 +  assumes z:  "is_Arg z t"
   2.268 +      and z': "is_Arg z t'"
   2.269 +      and t:  "- pi < t"  "t \<le> pi"
   2.270 +      and t': "- pi < t'" "t' \<le> pi"
   2.271 +      and nz: "z \<noteq> 0"
   2.272 +    shows "t' = t"
   2.273 +  using Arg2pi_unique_lemma [of "- (inverse z)"]
   2.274 +proof -
   2.275 +  have "pi - t' = pi - t"
   2.276 +  proof (rule Arg2pi_unique_lemma [of "- (inverse z)"])
   2.277 +    have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t)))"
   2.278 +      by (metis is_Arg_def z)
   2.279 +    also have "... = (cmod (- inverse z)) * exp (\<i> * (pi - t))"
   2.280 +      by (auto simp: field_simps exp_diff norm_divide)
   2.281 +    finally show "is_Arg (- inverse z) (pi - t)"
   2.282 +      unfolding is_Arg_def .
   2.283 +    have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t')))"
   2.284 +      by (metis is_Arg_def z')
   2.285 +    also have "... = (cmod (- inverse z)) * exp (\<i> * (pi - t'))"
   2.286 +      by (auto simp: field_simps exp_diff norm_divide)
   2.287 +    finally show "is_Arg (- inverse z) (pi - t')"
   2.288 +      unfolding is_Arg_def .
   2.289 +  qed (use assms in auto)
   2.290 +  then show ?thesis
   2.291 +    by simp
   2.292 +qed
   2.293 +
   2.294 +lemma
   2.295 +  assumes "z \<noteq> 0"
   2.296 +  shows mpi_less_Arg: "-pi < Arg z"
   2.297 +    and Arg_le_pi: "Arg z \<le> pi"
   2.298 +    and Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
   2.299 +  using assms exp_Ln exp_eq_polar
   2.300 +  by (auto simp: mpi_less_Im_Ln Im_Ln_le_pi Arg_def)
   2.301 +
   2.302 +lemma complex_norm_eq_1_exp_eq: "norm z = 1 \<longleftrightarrow> exp(\<i> * (Arg z)) = z"
   2.303 +  by (metis Arg_eq exp_not_eq_zero exp_zero mult.left_neutral norm_zero of_real_1 norm_exp_i_times)
   2.304 +
   2.305 +lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * a) = z; 0 < r; -pi < a; a \<le> pi\<rbrakk> \<Longrightarrow> Arg z = a"
   2.306 +  by (rule Arg_unique_lemma [unfolded is_Arg_def, OF _ Arg_eq])
   2.307 +     (use mpi_less_Arg Arg_le_pi in \<open>auto simp: norm_mult\<close>)
   2.308 +
   2.309 +
   2.310 +lemma Arg_minus:
   2.311 +  assumes "z \<noteq> 0"
   2.312 +  shows "Arg (-z) = (if Arg z \<le> 0 then Arg z + pi else Arg z - pi)"
   2.313 +proof -
   2.314 +  have [simp]: "cmod z * cos (Arg z) = Re z"
   2.315 +    using assms Arg_eq [of z] by (metis Re_exp exp_Ln norm_exp_eq_Re Arg_def)
   2.316 +  have [simp]: "cmod z * sin (Arg z) = Im z"
   2.317 +    using assms Arg_eq [of z] by (metis Im_exp exp_Ln norm_exp_eq_Re Arg_def)
   2.318 +  show ?thesis
   2.319 +    apply (rule Arg_unique [of "norm z"])
   2.320 +       apply (rule complex_eqI)
   2.321 +    using mpi_less_Arg [of z] Arg_le_pi [of z] assms
   2.322 +        apply (auto simp: Re_exp Im_exp cos_diff sin_diff cis_conv_exp [symmetric])
   2.323 +    done
   2.324 +qed
   2.325 +
   2.326 +lemma Arg_times_of_real [simp]:
   2.327 +  assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
   2.328 +proof (cases "z=0")
   2.329 +  case True
   2.330 +  then show ?thesis
   2.331 +    by (simp add: Arg_def)
   2.332 +next
   2.333 +  case False
   2.334 +  with Arg_eq assms show ?thesis
   2.335 +  by (auto simp: mpi_less_Arg Arg_le_pi intro!:  Arg_unique [of "r * norm z"])
   2.336 +qed
   2.337 +
   2.338 +lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   2.339 +  by (metis Arg_times_of_real mult.commute)
   2.340 +
   2.341 +lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
   2.342 +  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
   2.343 +
   2.344 +lemma Arg_less_0: "0 \<le> Arg z \<longleftrightarrow> 0 \<le> Im z"
   2.345 +  using Im_Ln_le_pi Im_Ln_pos_le
   2.346 +  by (simp add: Arg_def)
   2.347 +
   2.348 +lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> Re z < 0 \<and> Im z = 0"
   2.349 +  by (auto simp: Arg_def Im_Ln_eq_pi)
   2.350 +
   2.351 +lemma Arg_lt_pi: "0 < Arg z \<and> Arg z < pi \<longleftrightarrow> 0 < Im z"
   2.352 +  using Arg_less_0 [of z] Im_Ln_pos_lt
   2.353 +  by (auto simp: order.order_iff_strict Arg_def)
   2.354 +
   2.355 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
   2.356 +  using complex_is_Real_iff
   2.357 +  by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)
   2.358 +
   2.359 +corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
   2.360 +  using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
   2.361 +
   2.362 +lemma Arg_of_real: "Arg(of_real x) = 0 \<longleftrightarrow> 0 \<le> x"
   2.363 +  by (simp add: Arg_eq_0)
   2.364 +
   2.365 +lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
   2.366 +proof (cases "z=0")
   2.367 +  case False
   2.368 +  then show ?thesis
   2.369 +    using Arg_eq_0 [of "-z"] Arg_eq_pi complex_is_Real_iff by blast
   2.370 +qed (simp add: Arg_def)
   2.371 +
   2.372 +lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   2.373 +  using Arg_eq_pi_iff Arg_eq_0 by force
   2.374 +
   2.375 +lemma Arg_real: "z \<in> \<real> \<Longrightarrow> Arg z = (if 0 \<le> Re z then 0 else pi)"
   2.376 +  using Arg_eq_0 Arg_eq_0_pi by auto
   2.377 +
   2.378 +lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> then Arg z else - Arg z)"
   2.379 +proof (cases "z \<in> \<real>")
   2.380 +  case True
   2.381 +  then show ?thesis
   2.382 +    by simp (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
   2.383 +next
   2.384 +  case False
   2.385 +  then have "Arg z < pi" "z \<noteq> 0"
   2.386 +    using Arg_def Arg_eq_0_pi Arg_le_pi by fastforce+
   2.387 +  then show ?thesis
   2.388 +    apply (simp add: False)
   2.389 +    apply (rule Arg_unique [of "inverse (norm z)"])
   2.390 +    using False mpi_less_Arg [of z] Arg_eq [of z]
   2.391 +    apply (auto simp: exp_minus field_simps)
   2.392 +    done
   2.393 +qed
   2.394 +
   2.395 +lemma Arg_eq_iff:
   2.396 +  assumes "w \<noteq> 0" "z \<noteq> 0"
   2.397 +     shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)"
   2.398 +  using assms Arg_eq [of z] Arg_eq [of w]
   2.399 +  apply auto
   2.400 +  apply (rule_tac x="norm w / norm z" in exI)
   2.401 +  apply (simp add: divide_simps)
   2.402 +  by (metis mult.commute mult.left_commute)
   2.403 +
   2.404 +lemma Arg_inverse_eq_0: "Arg(inverse z) = 0 \<longleftrightarrow> Arg z = 0"
   2.405 +  by (metis Arg_eq_0 Arg_inverse inverse_inverse_eq)
   2.406 +
   2.407 +lemma Arg_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg (cnj z) = Arg (inverse z)"
   2.408 +  apply (simp add: Arg_eq_iff divide_simps complex_norm_square [symmetric] mult.commute)
   2.409 +  by (metis of_real_power zero_less_norm_iff zero_less_power)
   2.410 +
   2.411 +lemma Arg_cnj: "Arg(cnj z) = (if z \<in> \<real> then Arg z else - Arg z)"
   2.412 +  by (metis Arg_cnj_eq_inverse Arg_inverse Reals_0 complex_cnj_zero)
   2.413 +
   2.414 +lemma Arg_exp: "-pi < Im z \<Longrightarrow> Im z \<le> pi \<Longrightarrow> Arg(exp z) = Im z"
   2.415 +  by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
   2.416 +
   2.417 +lemma Ln_Arg: "z\<noteq>0 \<Longrightarrow> Ln(z) = ln(norm z) + \<i> * Arg(z)"
   2.418 +  by (metis Arg_def Re_Ln complex_eq)
   2.419 +
   2.420 +
   2.421  
   2.422  subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
   2.423  
   2.424 @@ -1541,7 +1726,7 @@
   2.425    case False
   2.426    then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
   2.427      using Arg2pi [of z]
   2.428 -    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
   2.429 +    by (metis is_Arg_def abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
   2.430    then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
   2.431      using cis_conv_exp cis_pi
   2.432      by (auto simp: exp_diff algebra_simps)
   2.433 @@ -1565,12 +1750,12 @@
   2.434  proof -
   2.435    have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
   2.436      by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
   2.437 -  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
   2.438 -    using Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff by auto
   2.439 +  have [simp]: "Im x \<noteq> 0 \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x" for x
   2.440 +    using Arg2pi_Ln  by (simp add: Arg2pi_gt_0 complex_nonneg_Reals_iff)
   2.441    consider "Re z < 0" | "Im z \<noteq> 0" using assms
   2.442      using complex_nonneg_Reals_iff not_le by blast
   2.443    then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
   2.444 -    using "*"  by (simp add: isCont_def) (metis Arg2pi_Ln Arg2pi_gt_0 complex_is_Real_iff)
   2.445 +    using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within) 
   2.446    show ?thesis
   2.447      unfolding continuous_at
   2.448    proof (rule Lim_transform_within_open)
   2.449 @@ -2672,12 +2857,6 @@
   2.450  
   2.451  subsection \<open>Real arctangent\<close>
   2.452  
   2.453 -lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   2.454 -  by simp
   2.455 -
   2.456 -lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
   2.457 -  by simp
   2.458 -
   2.459  lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
   2.460  proof -
   2.461    have ne: "1 + x\<^sup>2 \<noteq> 0"
   2.462 @@ -3875,7 +4054,7 @@
   2.463            by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
   2.464        qed
   2.465        with xy show "x = y"
   2.466 -        by (metis Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
   2.467 +        by (metis is_Arg_def Arg2pi Arg2pi_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
   2.468      qed
   2.469      have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg2pi z / (2*pi)) = \<gamma> x"
   2.470         by (metis Arg2pi_ge_0 Arg2pi_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
     3.1 --- a/src/HOL/Analysis/Further_Topology.thy	Mon Jun 25 14:06:50 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Jun 26 14:51:18 2018 +0100
     3.3 @@ -3242,7 +3242,7 @@
     3.4          have [simp]: "cmod (z - z * x / z') = cmod (z' - x)" if "x \<noteq> 0" for x
     3.5          proof -
     3.6            have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')"
     3.7 -            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) complex_divide_def mult.right_neutral norm_mult right_diff_distrib')
     3.8 +            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) divide_complex_def mult.right_neutral norm_mult right_diff_distrib')
     3.9            also have "... = cmod z' * cmod (1 - x / z')"
    3.10              by (simp add: nz')
    3.11            also have "... = cmod (z' - x)"
    3.12 @@ -3256,7 +3256,7 @@
    3.13            have "cmod (z * (1 - x * inverse z)) = cmod (z - x)"
    3.14              by (metis \<open>z \<noteq> 0\<close> diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7))
    3.15            then show ?thesis
    3.16 -            by (metis (no_types) mult.assoc complex_divide_def mult.right_neutral norm_mult nz' right_diff_distrib')
    3.17 +            by (metis (no_types) mult.assoc divide_complex_def mult.right_neutral norm_mult nz' right_diff_distrib')
    3.18          qed
    3.19          show ?thesis
    3.20            unfolding image_def ball_def
     4.1 --- a/src/HOL/Analysis/Inner_Product.thy	Mon Jun 25 14:06:50 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Jun 26 14:51:18 2018 +0100
     4.3 @@ -322,9 +322,9 @@
     4.4      unfolding inner_complex_def by simp
     4.5    show "inner x x = 0 \<longleftrightarrow> x = 0"
     4.6      unfolding inner_complex_def
     4.7 -    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
     4.8 +    by (simp add: add_nonneg_eq_0_iff complex_eq_iff)
     4.9    show "norm x = sqrt (inner x x)"
    4.10 -    unfolding inner_complex_def complex_norm_def
    4.11 +    unfolding inner_complex_def norm_complex_def
    4.12      by (simp add: power2_eq_square)
    4.13  qed
    4.14  
     5.1 --- a/src/HOL/Archimedean_Field.thy	Mon Jun 25 14:06:50 2018 +0100
     5.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Jun 26 14:51:18 2018 +0100
     5.3 @@ -453,6 +453,16 @@
     5.4      by simp
     5.5  qed
     5.6  
     5.7 +lemma floor_divide_lower:
     5.8 +  fixes q :: "'a::floor_ceiling"
     5.9 +  shows "q > 0 \<Longrightarrow> of_int \<lfloor>p / q\<rfloor> * q \<le> p"
    5.10 +  using of_int_floor_le pos_le_divide_eq by blast
    5.11 +
    5.12 +lemma floor_divide_upper:
    5.13 +  fixes q :: "'a::floor_ceiling"
    5.14 +  shows "q > 0 \<Longrightarrow> p < (of_int \<lfloor>p / q\<rfloor> + 1) * q"
    5.15 +  by (meson floor_eq_iff pos_divide_less_eq)
    5.16 +
    5.17  
    5.18  subsection \<open>Ceiling function\<close>
    5.19  
    5.20 @@ -650,6 +660,16 @@
    5.21      by metis 
    5.22  qed
    5.23  
    5.24 +lemma ceiling_divide_upper:
    5.25 +  fixes q :: "'a::floor_ceiling"
    5.26 +  shows "q > 0 \<Longrightarrow> p \<le> of_int (ceiling (p / q)) * q"
    5.27 +  by (meson divide_le_eq le_of_int_ceiling)
    5.28 +
    5.29 +lemma ceiling_divide_lower:
    5.30 +  fixes q :: "'a::floor_ceiling"
    5.31 +  shows "q > 0 \<Longrightarrow> (of_int \<lceil>p / q\<rceil> - 1) * q < p"
    5.32 +  by (meson ceiling_eq_iff pos_less_divide_eq)
    5.33 +
    5.34  subsection \<open>Negation\<close>
    5.35  
    5.36  lemma floor_minus: "\<lfloor>- x\<rfloor> = - \<lceil>x\<rceil>"
    5.37 @@ -658,7 +678,6 @@
    5.38  lemma ceiling_minus: "\<lceil>- x\<rceil> = - \<lfloor>x\<rfloor>"
    5.39    unfolding ceiling_def by simp
    5.40  
    5.41 -
    5.42  subsection \<open>Natural numbers\<close>
    5.43  
    5.44  lemma of_nat_floor: "r\<ge>0 \<Longrightarrow> of_nat (nat \<lfloor>r\<rfloor>) \<le> r"
     6.1 --- a/src/HOL/Complex.thy	Mon Jun 25 14:06:50 2018 +0100
     6.2 +++ b/src/HOL/Complex.thy	Tue Jun 26 14:51:18 2018 +0100
     6.3 @@ -211,7 +211,7 @@
     6.4      by simp
     6.5    also from insert.prems have "f x \<in> \<real>" by simp
     6.6    hence "Im (f x) = 0" by (auto elim!: Reals_cases)
     6.7 -  also have "Re (prod f A) = (\<Prod>x\<in>A. Re (f x))" 
     6.8 +  also have "Re (prod f A) = (\<Prod>x\<in>A. Re (f x))"
     6.9      by (intro insert.IH insert.prems) auto
    6.10    finally show ?case using insert.hyps by simp
    6.11  qed auto
    6.12 @@ -590,6 +590,9 @@
    6.13  lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
    6.14    by (simp add: complex_eq_iff power2_eq_square)
    6.15  
    6.16 +lemma cnj_add_mult_eq_Re: "z * cnj w + cnj z * w = 2 * Re (z * cnj w)"
    6.17 +  by (rule complex_eqI) auto
    6.18 +
    6.19  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"
    6.20    by (simp add: norm_mult power2_eq_square)
    6.21  
    6.22 @@ -796,7 +799,7 @@
    6.23  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"
    6.24    by (auto simp add: DeMoivre)
    6.25  
    6.26 -lemma cis_pi: "cis pi = -1"
    6.27 +lemma cis_pi [simp]: "cis pi = -1"
    6.28    by (simp add: complex_eq_iff)
    6.29  
    6.30  
    6.31 @@ -976,7 +979,7 @@
    6.32  
    6.33  lemma bij_betw_roots_unity:
    6.34    assumes "n > 0"
    6.35 -  shows   "bij_betw (\<lambda>k. cis (2 * pi * real k / real n)) {..<n} {z. z ^ n = 1}" 
    6.36 +  shows   "bij_betw (\<lambda>k. cis (2 * pi * real k / real n)) {..<n} {z. z ^ n = 1}"
    6.37      (is "bij_betw ?f _ _")
    6.38    unfolding bij_betw_def
    6.39  proof (intro conjI)
    6.40 @@ -1015,7 +1018,7 @@
    6.41    finally have card: "card {z::complex. z ^ n = 1} = n"
    6.42      using assms by (intro antisym card_roots_unity) auto
    6.43  
    6.44 -  have "card (?f ` {..<n}) = card {z::complex. z ^ n = 1}" 
    6.45 +  have "card (?f ` {..<n}) = card {z::complex. z ^ n = 1}"
    6.46      using card inj by (subst card_image) auto
    6.47    with subset and assms show "?f ` {..<n} = {z::complex. z ^ n = 1}"
    6.48      by (intro card_subset_eq finite_roots_unity) auto
    6.49 @@ -1219,12 +1222,7 @@
    6.50  
    6.51  text \<open>Legacy theorem names\<close>
    6.52  
    6.53 -lemmas expand_complex_eq = complex_eq_iff
    6.54 -lemmas complex_Re_Im_cancel_iff = complex_eq_iff
    6.55 -lemmas complex_equality = complex_eqI
    6.56  lemmas cmod_def = norm_complex_def
    6.57 -lemmas complex_norm_def = norm_complex_def
    6.58 -lemmas complex_divide_def = divide_complex_def
    6.59  
    6.60  lemma legacy_Complex_simps:
    6.61    shows Complex_eq_0: "Complex a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
     7.1 --- a/src/HOL/Library/Nonpos_Ints.thy	Mon Jun 25 14:06:50 2018 +0100
     7.2 +++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Jun 26 14:51:18 2018 +0100
     7.3 @@ -291,6 +291,11 @@
     7.4    apply (auto simp: divide_simps mult_le_0_iff)
     7.5    done
     7.6  
     7.7 +lemma nonpos_Reals_inverse_iff [simp]:
     7.8 +  fixes a :: "'a::real_div_algebra"
     7.9 +  shows "inverse a \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> a \<in> \<real>\<^sub>\<le>\<^sub>0"
    7.10 +  using nonpos_Reals_inverse_I by fastforce
    7.11 +
    7.12  lemma nonpos_Reals_pow_I: "\<lbrakk>a \<in> \<real>\<^sub>\<le>\<^sub>0; odd n\<rbrakk> \<Longrightarrow> a^n \<in> \<real>\<^sub>\<le>\<^sub>0"
    7.13    by (metis nonneg_Reals_pow_I power_minus_odd uminus_nonneg_Reals_iff)
    7.14  
     8.1 --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Mon Jun 25 14:06:50 2018 +0100
     8.2 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Tue Jun 26 14:51:18 2018 +0100
     8.3 @@ -111,10 +111,10 @@
     8.4  subsection \<open>Properties of Nonstandard Real and Imaginary Parts\<close>
     8.5  
     8.6  lemma hcomplex_hRe_hIm_cancel_iff: "\<And>w z. w = z \<longleftrightarrow> hRe w = hRe z \<and> hIm w = hIm z"
     8.7 -  by transfer (rule complex_Re_Im_cancel_iff)
     8.8 +  by transfer (rule complex_eq_iff)
     8.9  
    8.10  lemma hcomplex_equality [intro?]: "\<And>z w. hRe z = hRe w \<Longrightarrow> hIm z = hIm w \<Longrightarrow> z = w"
    8.11 -  by transfer (rule complex_equality)
    8.12 +  by transfer (rule complex_eqI)
    8.13  
    8.14  lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
    8.15    by transfer simp
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jun 25 14:06:50 2018 +0100
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Jun 26 14:51:18 2018 +0100
     9.3 @@ -388,6 +388,10 @@
     9.4  lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
     9.5    by (auto simp add: Reals_def)
     9.6  
     9.7 +lemma Reals_minus_iff [simp]: "- a \<in> \<real> \<longleftrightarrow> a \<in> \<real>"
     9.8 +  apply (auto simp: Reals_def)
     9.9 +  by (metis add.inverse_inverse of_real_minus rangeI)
    9.10 +
    9.11  lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
    9.12    apply (auto simp add: Reals_def)
    9.13    apply (rule range_eqI)
    10.1 --- a/src/HOL/Series.thy	Mon Jun 25 14:06:50 2018 +0100
    10.2 +++ b/src/HOL/Series.thy	Tue Jun 26 14:51:18 2018 +0100
    10.3 @@ -36,6 +36,21 @@
    10.4  lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
    10.5    by (simp add: sums_def' atMost_atLeast0)
    10.6  
    10.7 +lemma bounded_imp_summable:
    10.8 +  fixes a :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder,linorder_topology,linordered_comm_semiring_strict}"
    10.9 +  assumes 0: "\<And>n. a n \<ge> 0" and bounded: "\<And>n. (\<Sum>k\<le>n. a k) \<le> B"
   10.10 +  shows "summable a" 
   10.11 +proof -
   10.12 +  have "bdd_above (range(\<lambda>n. \<Sum>k\<le>n. a k))"
   10.13 +    by (meson bdd_aboveI2 bounded)
   10.14 +  moreover have "incseq (\<lambda>n. \<Sum>k\<le>n. a k)"
   10.15 +    by (simp add: mono_def "0" sum_mono2)
   10.16 +  ultimately obtain s where "(\<lambda>n. \<Sum>k\<le>n. a k) \<longlonglongrightarrow> s"
   10.17 +    using LIMSEQ_incseq_SUP by blast
   10.18 +  then show ?thesis
   10.19 +    by (auto simp: sums_def_le summable_def)
   10.20 +qed
   10.21 +
   10.22  
   10.23  subsection \<open>Infinite summability on topological monoids\<close>
   10.24  
    11.1 --- a/src/HOL/Transcendental.thy	Mon Jun 25 14:06:50 2018 +0100
    11.2 +++ b/src/HOL/Transcendental.thy	Tue Jun 26 14:51:18 2018 +0100
    11.3 @@ -4512,13 +4512,11 @@
    11.4  lemma sin_integer_2pi: "n \<in> \<int> \<Longrightarrow> sin(2 * pi * n) = 0"
    11.5    by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
    11.6  
    11.7 -lemma cos_int_2npi [simp]: "cos (2 * of_int n * pi) = 1"
    11.8 -  for n :: int
    11.9 +lemma cos_int_2pin [simp]: "cos ((2 * pi) * of_int n) = 1"
   11.10    by (simp add: cos_one_2pi_int)
   11.11  
   11.12 -lemma sin_int_2npi [simp]: "sin (2 * of_int n * pi) = 0"
   11.13 -  for n :: int
   11.14 -  by (metis Ints_of_int mult.assoc mult.commute sin_integer_2pi)
   11.15 +lemma sin_int_2pin [simp]: "sin ((2 * pi) * of_int n) = 0"
   11.16 +  by (metis Ints_of_int sin_integer_2pi)
   11.17  
   11.18  lemma sincos_principal_value: "\<exists>y. (- pi < y \<and> y \<le> pi) \<and> (sin y = sin x \<and> cos y = cos x)"
   11.19    apply (rule exI [where x="pi - (2 * pi) * frac ((pi - x) / (2 * pi))"])
   11.20 @@ -5435,6 +5433,62 @@
   11.21    using cos_arccos_abs by fastforce
   11.22  
   11.23  
   11.24 +lemma arccos_cos_eq_abs:
   11.25 +  assumes "\<bar>\<theta>\<bar> \<le> pi"
   11.26 +  shows "arccos (cos \<theta>) = \<bar>\<theta>\<bar>"
   11.27 +  unfolding arccos_def 
   11.28 +proof (intro the_equality conjI; clarify?)
   11.29 +  show "cos \<bar>\<theta>\<bar> = cos \<theta>"
   11.30 +    by (simp add: abs_real_def)
   11.31 +  show "x = \<bar>\<theta>\<bar>" if "cos x = cos \<theta>" "0 \<le> x" "x \<le> pi" for x
   11.32 +    by (simp add: \<open>cos \<bar>\<theta>\<bar> = cos \<theta>\<close> assms cos_inj_pi that)
   11.33 +qed (use assms in auto)
   11.34 +
   11.35 +lemma arccos_cos_eq_abs_2pi:
   11.36 +  obtains k where "arccos (cos \<theta>) = \<bar>\<theta> - of_int k * (2 * pi)\<bar>"
   11.37 +proof -
   11.38 +  define k where "k \<equiv>  \<lfloor>(\<theta> + pi) / (2 * pi)\<rfloor>"
   11.39 +  have lepi: "\<bar>\<theta> - of_int k * (2 * pi)\<bar> \<le> pi"
   11.40 +    using floor_divide_lower [of "2*pi" "\<theta> + pi"] floor_divide_upper [of "2*pi" "\<theta> + pi"]
   11.41 +    by (auto simp: k_def abs_if algebra_simps)
   11.42 +  have "arccos (cos \<theta>) = arccos (cos (\<theta> - of_int k * (2 * pi)))"
   11.43 +    using cos_int_2pin sin_int_2pin by (simp add: cos_diff mult.commute)
   11.44 +  also have "... = \<bar>\<theta> - of_int k * (2 * pi)\<bar>"
   11.45 +    using arccos_cos_eq_abs lepi by blast
   11.46 +  finally show ?thesis 
   11.47 +    using that by metis
   11.48 +qed
   11.49 +
   11.50 +lemma cos_limit_1:
   11.51 +  assumes "(\<lambda>j. cos (\<theta> j)) \<longlonglongrightarrow> 1"
   11.52 +  shows "\<exists>k. (\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> 0"
   11.53 +proof -
   11.54 +  have "\<forall>\<^sub>F j in sequentially. cos (\<theta> j) \<in> {- 1..1}"
   11.55 +    by auto
   11.56 +  then have "(\<lambda>j. arccos (cos (\<theta> j))) \<longlonglongrightarrow> arccos 1"
   11.57 +    using continuous_on_tendsto_compose [OF continuous_on_arccos' assms] by auto
   11.58 +  moreover have "\<And>j. \<exists>k. arccos (cos (\<theta> j)) = \<bar>\<theta> j - of_int k * (2 * pi)\<bar>"
   11.59 +    using arccos_cos_eq_abs_2pi by metis
   11.60 +  then have "\<exists>k. \<forall>j. arccos (cos (\<theta> j)) = \<bar>\<theta> j - of_int (k j) * (2 * pi)\<bar>"
   11.61 +    by metis
   11.62 +  ultimately have "\<exists>k. (\<lambda>j. \<bar>\<theta> j - of_int (k j) * (2 * pi)\<bar>) \<longlonglongrightarrow> 0"
   11.63 +    by auto
   11.64 +  then show ?thesis
   11.65 +    by (simp add: tendsto_rabs_zero_iff)
   11.66 +qed
   11.67 +
   11.68 +lemma cos_diff_limit_1:
   11.69 +  assumes "(\<lambda>j. cos (\<theta> j - \<Theta>)) \<longlonglongrightarrow> 1"
   11.70 +  obtains k where "(\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> \<Theta>"
   11.71 +proof -
   11.72 +  obtain k where "(\<lambda>j. (\<theta> j - \<Theta>) - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> 0"
   11.73 +    using cos_limit_1 [OF assms] by auto
   11.74 +  then have "(\<lambda>j. \<Theta> + ((\<theta> j - \<Theta>) - of_int (k j) * (2 * pi))) \<longlonglongrightarrow> \<Theta> + 0"
   11.75 +    by (rule tendsto_add [OF tendsto_const])
   11.76 +  with that show ?thesis
   11.77 +    by (auto simp: )
   11.78 +qed
   11.79 +
   11.80  subsection \<open>Machin's formula\<close>
   11.81  
   11.82  lemma arctan_one: "arctan 1 = pi / 4"