New material and binomial fix
authorpaulson <lp15@cam.ac.uk>
Tue Mar 31 15:00:03 2015 +0100 (2015-03-31)
changeset 5986244b3f4fa33ca
parent 59860 a979fc5db526
child 59863 30519ff3dffb
New material and binomial fix
src/HOL/Binomial.thy
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Binomial.thy	Tue Mar 31 00:21:07 2015 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Tue Mar 31 15:00:03 2015 +0100
     1.3 @@ -514,8 +514,7 @@
     1.4    unfolding pochhammer_eq_0_iff by auto
     1.5  
     1.6  lemma pochhammer_minus:
     1.7 -  assumes kn: "k \<le> n"
     1.8 -  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
     1.9 +    "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
    1.10  proof (cases k)
    1.11    case 0
    1.12    then show ?thesis by simp
    1.13 @@ -531,16 +530,15 @@
    1.14  qed
    1.15  
    1.16  lemma pochhammer_minus':
    1.17 -  assumes kn: "k \<le> n"
    1.18 -  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
    1.19 -  unfolding pochhammer_minus[OF kn, where b=b]
    1.20 +    "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
    1.21 +  unfolding pochhammer_minus[where b=b]
    1.22    unfolding mult.assoc[symmetric]
    1.23    unfolding power_add[symmetric]
    1.24    by simp
    1.25  
    1.26  lemma pochhammer_same: "pochhammer (- of_nat n) n =
    1.27      ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)"
    1.28 -  unfolding pochhammer_minus[OF le_refl[of n]]
    1.29 +  unfolding pochhammer_minus
    1.30    by (simp add: of_nat_diff pochhammer_fact)
    1.31  
    1.32  
     2.1 --- a/src/HOL/Complex.thy	Tue Mar 31 00:21:07 2015 +0200
     2.2 +++ b/src/HOL/Complex.thy	Tue Mar 31 15:00:03 2015 +0100
     2.3 @@ -93,10 +93,10 @@
     2.4  lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x"
     2.5    by (simp add: power2_eq_square)
     2.6  
     2.7 -lemma Re_power_real: "Im x = 0 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
     2.8 +lemma Re_power_real [simp]: "Im x = 0 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
     2.9    by (induct n) simp_all
    2.10  
    2.11 -lemma Im_power_real: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
    2.12 +lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
    2.13    by (induct n) simp_all
    2.14  
    2.15  subsection {* Scalar Multiplication *}
    2.16 @@ -823,6 +823,9 @@
    2.17  lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \<Longrightarrow> Re x \<le> 0 \<Longrightarrow> csqrt x = \<i> * sqrt \<bar>Re x\<bar>"
    2.18    by (simp add: complex_eq_iff norm_complex_def)
    2.19  
    2.20 +lemma of_real_sqrt: "x \<ge> 0 \<Longrightarrow> of_real (sqrt x) = csqrt (of_real x)"
    2.21 +  by (simp add: complex_eq_iff norm_complex_def)
    2.22 +
    2.23  lemma csqrt_0 [simp]: "csqrt 0 = 0"
    2.24    by simp
    2.25  
     3.1 --- a/src/HOL/Deriv.thy	Tue Mar 31 00:21:07 2015 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Tue Mar 31 15:00:03 2015 +0100
     3.3 @@ -561,6 +561,10 @@
     3.4     \<Longrightarrow> (f has_field_derivative f') (at x within t)"
     3.5    by (simp add: has_field_derivative_def has_derivative_within_subset)
     3.6  
     3.7 +lemma has_field_derivative_at_within:
     3.8 +    "(f has_field_derivative f') (at x) \<Longrightarrow> (f has_field_derivative f') (at x within s)"
     3.9 +  using DERIV_subset by blast
    3.10 +
    3.11  abbreviation (input)
    3.12    DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.13    ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
     4.1 --- a/src/HOL/Library/Convex.thy	Tue Mar 31 00:21:07 2015 +0200
     4.2 +++ b/src/HOL/Library/Convex.thy	Tue Mar 31 15:00:03 2015 +0100
     4.3 @@ -121,6 +121,9 @@
     4.4    then show "convex {a<..<b}" by (simp only: convex_Int 3 4)
     4.5  qed
     4.6  
     4.7 +lemma convex_Reals: "convex Reals"
     4.8 +  by (simp add: convex_def scaleR_conv_of_real)
     4.9 +    
    4.10  subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
    4.11  
    4.12  lemma convex_setsum:
     5.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 00:21:07 2015 +0200
     5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 31 15:00:03 2015 +0100
     5.3 @@ -2555,9 +2555,7 @@
     5.4    let ?KM = "{(k,m). k + m \<le> n}"
     5.5    let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
     5.6    have th0: "?KM = UNION {0..n} ?f"
     5.7 -    apply (simp add: set_eq_iff)
     5.8 -    apply presburger (* FIXME: slow! *)
     5.9 -    done
    5.10 +    by (auto simp add: set_eq_iff Bex_def)
    5.11    show "?l = ?r "
    5.12      unfolding th0
    5.13      apply (subst setsum.UNION_disjoint)
    5.14 @@ -3230,11 +3228,11 @@
    5.15        then obtain m where m: "n = Suc m" by (cases n) auto
    5.16        from k0 obtain h where h: "k = Suc h" by (cases k) auto
    5.17        {
    5.18 -        assume kn: "k = n"
    5.19 +        assume "k = n"
    5.20          then have "b gchoose (n - k) =
    5.21            (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
    5.22 -          using kn pochhammer_minus'[where k=k and n=n and b=b]
    5.23 -          apply (simp add:  pochhammer_same)
    5.24 +          using pochhammer_minus'[where k=k and b=b]
    5.25 +          apply (simp add: pochhammer_same)
    5.26            using bn0
    5.27            apply (simp add: field_simps power_add[symmetric])
    5.28            done
    5.29 @@ -3357,10 +3355,10 @@
    5.30      apply (auto simp add: of_nat_diff algebra_simps)
    5.31      done
    5.32    have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
    5.33 -    unfolding pochhammer_minus[OF le_refl]
    5.34 +    unfolding pochhammer_minus
    5.35      by (simp add: algebra_simps)
    5.36    have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n"
    5.37 -    unfolding pochhammer_minus[OF le_refl]
    5.38 +    unfolding pochhammer_minus
    5.39      by simp
    5.40    have nz: "pochhammer c n \<noteq> 0" using c
    5.41      by (simp add: pochhammer_eq_0_iff)
    5.42 @@ -3794,8 +3792,9 @@
    5.43        with LIMSEQ_inverse_realpow_zero[of 2, simplified, simplified filterlim_iff,
    5.44          THEN spec, of "\<lambda>x. x < e"]
    5.45        have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
    5.46 +        unfolding eventually_nhds
    5.47          apply safe
    5.48 -        apply (auto simp: eventually_nhds) --{*slow*}
    5.49 +        apply auto --{*slow*}
    5.50          done
    5.51        then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
    5.52        have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
     6.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Mar 31 00:21:07 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Mar 31 15:00:03 2015 +0100
     6.3 @@ -42,7 +42,7 @@
     6.4  
     6.5  theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
     6.6  proof -
     6.7 -  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) 
     6.8 +  have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
     6.9          = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
    6.10    proof
    6.11      fix n
    6.12 @@ -74,13 +74,11 @@
    6.13  
    6.14  subsection{*Relationships between real and complex trig functions*}
    6.15  
    6.16 -declare sin_of_real [simp] cos_of_real [simp]
    6.17 -
    6.18  lemma real_sin_eq [simp]:
    6.19    fixes x::real
    6.20    shows "Re(sin(of_real x)) = sin x"
    6.21    by (simp add: sin_of_real)
    6.22 -  
    6.23 +
    6.24  lemma real_cos_eq [simp]:
    6.25    fixes x::real
    6.26    shows "Re(cos(of_real x)) = cos x"
    6.27 @@ -100,10 +98,10 @@
    6.28      by (rule exp_converges)
    6.29    finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
    6.30    moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
    6.31 -    by (metis exp_converges sums_cnj) 
    6.32 +    by (metis exp_converges sums_cnj)
    6.33    ultimately show ?thesis
    6.34      using sums_unique2
    6.35 -    by blast 
    6.36 +    by blast
    6.37  qed
    6.38  
    6.39  lemma cnj_sin: "cnj(sin z) = sin(cnj z)"
    6.40 @@ -112,15 +110,6 @@
    6.41  lemma cnj_cos: "cnj(cos z) = cos(cnj z)"
    6.42    by (simp add: cos_exp_eq exp_cnj field_simps)
    6.43  
    6.44 -lemma exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
    6.45 -  by (metis Reals_cases Reals_of_real exp_of_real)
    6.46 -
    6.47 -lemma sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
    6.48 -  by (metis Reals_cases Reals_of_real sin_of_real)
    6.49 -
    6.50 -lemma cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
    6.51 -  by (metis Reals_cases Reals_of_real cos_of_real)
    6.52 -
    6.53  lemma complex_differentiable_at_sin: "sin complex_differentiable at z"
    6.54    using DERIV_sin complex_differentiable_def by blast
    6.55  
    6.56 @@ -141,7 +130,7 @@
    6.57  
    6.58  subsection{* Get a nice real/imaginary separation in Euler's formula.*}
    6.59  
    6.60 -lemma Euler: "exp(z) = of_real(exp(Re z)) * 
    6.61 +lemma Euler: "exp(z) = of_real(exp(Re z)) *
    6.62                (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
    6.63  by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
    6.64  
    6.65 @@ -156,11 +145,20 @@
    6.66  
    6.67  lemma Im_cos: "Im(cos z) = sin(Re z) * (exp(-(Im z)) - exp(Im z)) / 2"
    6.68    by (simp add: cos_exp_eq field_simps Im_divide Im_exp)
    6.69 -  
    6.70 +
    6.71 +lemma Re_sin_pos: "0 < Re z \<Longrightarrow> Re z < pi \<Longrightarrow> Re (sin z) > 0"
    6.72 +  by (auto simp: Re_sin Im_sin add_pos_pos sin_gt_zero)
    6.73 +
    6.74 +lemma Im_sin_nonneg: "Re z = 0 \<Longrightarrow> 0 \<le> Im z \<Longrightarrow> 0 \<le> Im (sin z)"
    6.75 +  by (simp add: Re_sin Im_sin algebra_simps)
    6.76 +
    6.77 +lemma Im_sin_nonneg2: "Re z = pi \<Longrightarrow> Im z \<le> 0 \<Longrightarrow> 0 \<le> Im (sin z)"
    6.78 +  by (simp add: Re_sin Im_sin algebra_simps)
    6.79 +
    6.80  subsection{*More on the Polar Representation of Complex Numbers*}
    6.81  
    6.82  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
    6.83 -  by (simp add: exp_add exp_Euler exp_of_real)
    6.84 +  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    6.85  
    6.86  lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
    6.87  apply auto
    6.88 @@ -183,7 +181,7 @@
    6.89  lemma exp_complex_eqI: "abs(Im w - Im z) < 2*pi \<Longrightarrow> exp w = exp z \<Longrightarrow> w = z"
    6.90    by (auto simp: exp_eq abs_mult)
    6.91  
    6.92 -lemma exp_integer_2pi: 
    6.93 +lemma exp_integer_2pi:
    6.94    assumes "n \<in> Ints"
    6.95    shows "exp((2 * n * pi) * ii) = 1"
    6.96  proof -
    6.97 @@ -208,10 +206,10 @@
    6.98    done
    6.99  qed
   6.100  
   6.101 -lemma exp_i_ne_1: 
   6.102 +lemma exp_i_ne_1:
   6.103    assumes "0 < x" "x < 2*pi"
   6.104    shows "exp(\<i> * of_real x) \<noteq> 1"
   6.105 -proof 
   6.106 +proof
   6.107    assume "exp (\<i> * of_real x) = 1"
   6.108    then have "exp (\<i> * of_real x) = exp 0"
   6.109      by simp
   6.110 @@ -225,18 +223,18 @@
   6.111      by (cases n) (auto simp: zero_less_mult_iff mult_less_0_iff)
   6.112  qed
   6.113  
   6.114 -lemma sin_eq_0: 
   6.115 +lemma sin_eq_0:
   6.116    fixes z::complex
   6.117    shows "sin z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi))"
   6.118    by (simp add: sin_exp_eq exp_eq of_real_numeral)
   6.119  
   6.120 -lemma cos_eq_0: 
   6.121 +lemma cos_eq_0:
   6.122    fixes z::complex
   6.123    shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
   6.124    using sin_eq_0 [of "z - of_real pi/2"]
   6.125    by (simp add: sin_diff algebra_simps)
   6.126  
   6.127 -lemma cos_eq_1: 
   6.128 +lemma cos_eq_1:
   6.129    fixes z::complex
   6.130    shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
   6.131  proof -
   6.132 @@ -248,7 +246,7 @@
   6.133      by simp
   6.134    show ?thesis
   6.135      by (auto simp: sin_eq_0 of_real_numeral)
   6.136 -qed  
   6.137 +qed
   6.138  
   6.139  lemma csin_eq_1:
   6.140    fixes z::complex
   6.141 @@ -275,15 +273,15 @@
   6.142      apply (simp_all add: algebra_simps)
   6.143      done
   6.144    finally show ?thesis .
   6.145 -qed  
   6.146 +qed
   6.147  
   6.148 -lemma ccos_eq_minus1: 
   6.149 +lemma ccos_eq_minus1:
   6.150    fixes z::complex
   6.151    shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
   6.152    using csin_eq_1 [of "z - of_real pi/2"]
   6.153    apply (simp add: sin_diff)
   6.154    apply (simp add: algebra_simps of_real_numeral equation_minus_iff)
   6.155 -  done       
   6.156 +  done
   6.157  
   6.158  lemma sin_eq_1: "sin x = 1 \<longleftrightarrow> (\<exists>n::int. x = (2 * n + 1 / 2) * pi)"
   6.159                  (is "_ = ?rhs")
   6.160 @@ -301,7 +299,7 @@
   6.161    also have "... = ?rhs"
   6.162      by (auto simp: algebra_simps)
   6.163    finally show ?thesis .
   6.164 -qed  
   6.165 +qed
   6.166  
   6.167  lemma sin_eq_minus1: "sin x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 3/2) * pi)"  (is "_ = ?rhs")
   6.168  proof -
   6.169 @@ -317,7 +315,7 @@
   6.170    also have "... = ?rhs"
   6.171      by (auto simp: algebra_simps)
   6.172    finally show ?thesis .
   6.173 -qed  
   6.174 +qed
   6.175  
   6.176  lemma cos_eq_minus1: "cos x = -1 \<longleftrightarrow> (\<exists>n::int. x = (2*n + 1) * pi)"
   6.177                        (is "_ = ?rhs")
   6.178 @@ -334,10 +332,10 @@
   6.179    also have "... = ?rhs"
   6.180      by (auto simp: algebra_simps)
   6.181    finally show ?thesis .
   6.182 -qed  
   6.183 +qed
   6.184  
   6.185  lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * abs(sin(t / 2))"
   6.186 -  apply (simp add: exp_Euler cmod_def power2_diff algebra_simps)
   6.187 +  apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   6.188    using cos_double_sin [of "t/2"]
   6.189    apply (simp add: real_sqrt_mult)
   6.190    done
   6.191 @@ -369,7 +367,7 @@
   6.192  
   6.193  lemmas cos_ii_times = cosh_complex [symmetric]
   6.194  
   6.195 -lemma norm_cos_squared: 
   6.196 +lemma norm_cos_squared:
   6.197      "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
   6.198    apply (cases z)
   6.199    apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
   6.200 @@ -387,12 +385,12 @@
   6.201    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
   6.202    apply (simp add: cos_squared_eq)
   6.203    apply (simp add: power2_eq_square algebra_simps divide_simps)
   6.204 -  done 
   6.205 +  done
   6.206  
   6.207  lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   6.208    using abs_Im_le_cmod linear order_trans by fastforce
   6.209  
   6.210 -lemma norm_cos_le: 
   6.211 +lemma norm_cos_le:
   6.212    fixes z::complex
   6.213    shows "norm(cos z) \<le> exp(norm z)"
   6.214  proof -
   6.215 @@ -405,7 +403,7 @@
   6.216      done
   6.217  qed
   6.218  
   6.219 -lemma norm_cos_plus1_le: 
   6.220 +lemma norm_cos_plus1_le:
   6.221    fixes z::complex
   6.222    shows "norm(1 + cos z) \<le> 2 * exp(norm z)"
   6.223  proof -
   6.224 @@ -431,12 +429,12 @@
   6.225  
   6.226  subsection{* Taylor series for complex exponential, sine and cosine.*}
   6.227  
   6.228 -context 
   6.229 +context
   6.230  begin
   6.231  
   6.232  declare power_Suc [simp del]
   6.233  
   6.234 -lemma Taylor_exp: 
   6.235 +lemma Taylor_exp:
   6.236    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   6.237  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
   6.238    show "convex (closed_segment 0 z)"
   6.239 @@ -459,11 +457,11 @@
   6.240    show "z \<in> closed_segment 0 z"
   6.241      apply (simp add: closed_segment_def scaleR_conv_of_real)
   6.242      using of_real_1 zero_le_one by blast
   6.243 -qed 
   6.244 +qed
   6.245  
   6.246 -lemma 
   6.247 +lemma
   6.248    assumes "0 \<le> u" "u \<le> 1"
   6.249 -  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" 
   6.250 +  shows cmod_sin_le_exp: "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   6.251      and cmod_cos_le_exp: "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>"
   6.252  proof -
   6.253    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   6.254 @@ -485,16 +483,16 @@
   6.255      apply (meson less_eq_real_def mult_nonneg_nonpos neg_0_le_iff_le order_trans)
   6.256      done
   6.257  qed
   6.258 -    
   6.259 -lemma Taylor_sin: 
   6.260 -  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) 
   6.261 +
   6.262 +lemma Taylor_sin:
   6.263 +  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   6.264     \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
   6.265  proof -
   6.266    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   6.267        by arith
   6.268    have *: "cmod (sin z -
   6.269                   (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
   6.270 -           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   6.271 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   6.272    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,
   6.273  simplified])
   6.274    show "convex (closed_segment 0 z)"
   6.275 @@ -519,7 +517,7 @@
   6.276      show "z \<in> closed_segment 0 z"
   6.277        apply (simp add: closed_segment_def scaleR_conv_of_real)
   6.278        using of_real_1 zero_le_one by blast
   6.279 -  qed 
   6.280 +  qed
   6.281    have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
   6.282              = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
   6.283      by (auto simp: sin_coeff_def elim!: oddE)
   6.284 @@ -529,15 +527,15 @@
   6.285      done
   6.286  qed
   6.287  
   6.288 -lemma Taylor_cos: 
   6.289 -  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k)) 
   6.290 +lemma Taylor_cos:
   6.291 +  "norm(cos z - (\<Sum>k\<le>n. complex_of_real (cos_coeff k) * z ^ k))
   6.292     \<le> exp\<bar>Im z\<bar> * (norm z) ^ Suc n / (fact n)"
   6.293  proof -
   6.294    have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
   6.295        by arith
   6.296    have *: "cmod (cos z -
   6.297                   (\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
   6.298 -           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)" 
   6.299 +           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
   6.300    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,
   6.301  simplified])
   6.302    show "convex (closed_segment 0 z)"
   6.303 @@ -563,7 +561,7 @@
   6.304      show "z \<in> closed_segment 0 z"
   6.305        apply (simp add: closed_segment_def scaleR_conv_of_real)
   6.306        using of_real_1 zero_le_one by blast
   6.307 -  qed 
   6.308 +  qed
   6.309    have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
   6.310              = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"
   6.311      by (auto simp: cos_coeff_def elim!: evenE)
   6.312 @@ -910,6 +908,21 @@
   6.313    apply (auto simp: exp_of_nat_mult [symmetric])
   6.314    done
   6.315  
   6.316 +subsection{*The Unwinding Number and the Ln-product Formula*}
   6.317 +
   6.318 +text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
   6.319 +
   6.320 +definition unwinding :: "complex \<Rightarrow> complex" where
   6.321 +   "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
   6.322 +
   6.323 +lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
   6.324 +  by (simp add: unwinding_def)
   6.325 +
   6.326 +lemma Ln_times_unwinding:
   6.327 +    "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
   6.328 +  using unwinding_2pi by (simp add: exp_add)
   6.329 +
   6.330 +
   6.331  subsection{*Derivative of Ln away from the branch cut*}
   6.332  
   6.333  lemma
   6.334 @@ -944,6 +957,10 @@
   6.335  lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
   6.336    by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
   6.337  
   6.338 +lemma isCont_Ln' [simp]:
   6.339 +   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   6.340 +  by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
   6.341 +
   6.342  lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
   6.343    using continuous_at_Ln continuous_at_imp_continuous_within by blast
   6.344  
   6.345 @@ -956,7 +973,7 @@
   6.346  
   6.347  subsection{*Relation to Real Logarithm*}
   6.348  
   6.349 -lemma ln_of_real:
   6.350 +lemma Ln_of_real:
   6.351    assumes "0 < z"
   6.352      shows "Ln(of_real z) = of_real(ln z)"
   6.353  proof -
   6.354 @@ -969,6 +986,9 @@
   6.355      using assms by simp
   6.356  qed
   6.357  
   6.358 +corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
   6.359 +  by (auto simp: Ln_of_real elim: Reals_cases)
   6.360 +
   6.361  
   6.362  subsection{*Quadrant-type results for Ln*}
   6.363  
   6.364 @@ -1091,7 +1111,7 @@
   6.365  lemma Ln_1 [simp]: "Ln(1) = 0"
   6.366  proof -
   6.367    have "Ln (exp 0) = 0"
   6.368 -    by (metis exp_zero ln_exp ln_of_real of_real_0 of_real_1 zero_less_one)
   6.369 +    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   6.370    then show ?thesis
   6.371      by simp
   6.372  qed
   6.373 @@ -1262,6 +1282,10 @@
   6.374      "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
   6.375    by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
   6.376  
   6.377 +corollary isCont_csqrt' [simp]:
   6.378 +   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
   6.379 +  by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
   6.380 +
   6.381  lemma continuous_within_csqrt:
   6.382      "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
   6.383    by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
     7.1 --- a/src/HOL/Transcendental.thy	Tue Mar 31 00:21:07 2015 +0200
     7.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 31 15:00:03 2015 +0100
     7.3 @@ -1130,6 +1130,9 @@
     7.4    apply (simp add: scaleR_conv_of_real)
     7.5    done
     7.6  
     7.7 +corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
     7.8 +  by (metis Reals_cases Reals_of_real exp_of_real)
     7.9 +
    7.10  lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
    7.11  proof
    7.12    have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
    7.13 @@ -2432,6 +2435,9 @@
    7.14      by blast
    7.15  qed
    7.16  
    7.17 +corollary sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
    7.18 +  by (metis Reals_cases Reals_of_real sin_of_real)
    7.19 +
    7.20  lemma cos_of_real:
    7.21    fixes x::real
    7.22    shows "cos (of_real x) = of_real (cos x)"
    7.23 @@ -2450,6 +2456,9 @@
    7.24      by blast
    7.25  qed
    7.26  
    7.27 +corollary cos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> cos z \<in> \<real>"
    7.28 +  by (metis Reals_cases Reals_of_real cos_of_real)
    7.29 +
    7.30  lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
    7.31    by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
    7.32  
    7.33 @@ -3661,6 +3670,16 @@
    7.34  definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
    7.35    where "tan = (\<lambda>x. sin x / cos x)"
    7.36  
    7.37 +lemma tan_of_real:
    7.38 +  fixes XXX :: "'a::{real_normed_field,banach,field_inverse_zero}"
    7.39 +  shows  "of_real(tan x) = (tan(of_real x) :: 'a)"
    7.40 +  by (simp add: tan_def sin_of_real cos_of_real)
    7.41 +
    7.42 +lemma tan_in_Reals [simp]:
    7.43 +  fixes z :: "'a::{real_normed_field,banach,field_inverse_zero}"
    7.44 +  shows "z \<in> \<real> \<Longrightarrow> tan z \<in> \<real>"
    7.45 +  by (simp add: tan_def)
    7.46 +
    7.47  lemma tan_zero [simp]: "tan 0 = 0"
    7.48    by (simp add: tan_def)
    7.49