src/HOL/Transcendental.thy
changeset 58410 6d46ad54a2ab
parent 57514 bdc2c6b40bf2
child 58656 7f14d5d9b933
     1.1 --- a/src/HOL/Transcendental.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -247,8 +247,8 @@
     1.4  lemma sums_alternating_upper_lower:
     1.5    fixes a :: "nat \<Rightarrow> real"
     1.6    assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
     1.7 -  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. -1^i*a i) ----> l) \<and>
     1.8 -             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. -1^i*a i) ----> l)"
     1.9 +  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
    1.10 +             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
    1.11    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
    1.12  proof (rule nested_sequence_unique)
    1.13    have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
    1.14 @@ -367,11 +367,11 @@
    1.15    assumes a_zero: "a ----> 0" and "monoseq a"
    1.16    shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
    1.17      and "0 < a 0 \<longrightarrow>
    1.18 -      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n. -1^i * a i .. \<Sum>i<2*n+1. -1^i * a i})" (is "?pos")
    1.19 +      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
    1.20      and "a 0 < 0 \<longrightarrow>
    1.21 -      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n+1. -1^i * a i .. \<Sum>i<2*n. -1^i * a i})" (is "?neg")
    1.22 -    and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
    1.23 -    and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
    1.24 +      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
    1.25 +    and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
    1.26 +    and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
    1.27  proof -
    1.28    have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
    1.29    proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
    1.30 @@ -413,7 +413,7 @@
    1.31        unfolding minus_diff_minus by auto
    1.32  
    1.33      from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
    1.34 -    have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
    1.35 +    have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
    1.36        by auto
    1.37  
    1.38      have ?pos using `0 \<le> ?a 0` by auto
    1.39 @@ -1383,7 +1383,7 @@
    1.40        fix x :: real
    1.41        assume "x \<in> {- 1<..<1}"
    1.42        hence "norm (-x) < 1" by auto
    1.43 -      show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
    1.44 +      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
    1.45          unfolding One_nat_def
    1.46          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
    1.47      qed
    1.48 @@ -2216,10 +2216,10 @@
    1.49  subsection {* Sine and Cosine *}
    1.50  
    1.51  definition sin_coeff :: "nat \<Rightarrow> real" where
    1.52 -  "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
    1.53 +  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
    1.54  
    1.55  definition cos_coeff :: "nat \<Rightarrow> real" where
    1.56 -  "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
    1.57 +  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
    1.58  
    1.59  definition sin :: "real \<Rightarrow> real"
    1.60    where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
    1.61 @@ -2472,7 +2472,7 @@
    1.62     hence define pi.*}
    1.63  
    1.64  lemma sin_paired:
    1.65 -  "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
    1.66 +  "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
    1.67  proof -
    1.68    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
    1.69      by (rule sin_converges [THEN sums_group], simp)
    1.70 @@ -2483,7 +2483,7 @@
    1.71    assumes "0 < x" and "x < 2"
    1.72    shows "0 < sin x"
    1.73  proof -
    1.74 -  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
    1.75 +  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
    1.76    have pos: "\<forall>n. 0 < ?f n"
    1.77    proof
    1.78      fix n :: nat
    1.79 @@ -2508,7 +2508,7 @@
    1.80  lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
    1.81    using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
    1.82  
    1.83 -lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
    1.84 +lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
    1.85  proof -
    1.86    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
    1.87      by (rule cos_converges [THEN sums_group], simp)
    1.88 @@ -2541,16 +2541,16 @@
    1.89  proof -
    1.90    note fact_Suc [simp del]
    1.91    from cos_paired
    1.92 -  have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
    1.93 +  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
    1.94      by (rule sums_minus)
    1.95 -  then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
    1.96 +  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
    1.97      by simp
    1.98 -  then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
    1.99 +  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.100      by (rule sums_summable)
   1.101 -  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.102 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.103      by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
   1.104 -  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
   1.105 -    < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.106 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
   1.107 +    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.108    proof -
   1.109      { fix d
   1.110        have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
   1.111 @@ -2569,9 +2569,9 @@
   1.112      from ** show ?thesis by (rule sumr_pos_lt_pair)
   1.113        (simp add: divide_inverse mult.assoc [symmetric] ***)
   1.114    qed
   1.115 -  ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.116 +  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.117      by (rule order_less_trans)
   1.118 -  moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.119 +  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.120      by (rule sums_unique)
   1.121    ultimately have "0 < - cos 2" by simp
   1.122    then show ?thesis by simp
   1.123 @@ -2677,10 +2677,10 @@
   1.124  lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
   1.125    by (simp add: cos_add cos_double)
   1.126  
   1.127 -lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
   1.128 +lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
   1.129    by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
   1.130  
   1.131 -lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
   1.132 +lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
   1.133    by (metis cos_npi mult.commute)
   1.134  
   1.135  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
   1.136 @@ -3754,9 +3754,9 @@
   1.137      fix x :: real
   1.138      assume "\<bar>x\<bar> < 1"
   1.139      hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
   1.140 -    have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
   1.141 +    have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
   1.142        by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
   1.143 -    hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
   1.144 +    hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
   1.145    } note summable_Integral = this
   1.146  
   1.147    {
   1.148 @@ -3778,17 +3778,17 @@
   1.149    } note sums_even = this
   1.150  
   1.151    have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
   1.152 -    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
   1.153 +    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
   1.154      by auto
   1.155  
   1.156    {
   1.157      fix x :: real
   1.158 -    have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
   1.159 -      (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
   1.160 +    have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
   1.161 +      (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
   1.162        using n_even by auto
   1.163      have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
   1.164      have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
   1.165 -      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
   1.166 +      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
   1.167        by auto
   1.168    } note arctan_eq = this
   1.169  
   1.170 @@ -3798,11 +3798,18 @@
   1.171      {
   1.172        fix x' :: real
   1.173        assume x'_bounds: "x' \<in> {- 1 <..< 1}"
   1.174 -      hence "\<bar>x'\<bar> < 1" by auto
   1.175 -
   1.176 +      then have "\<bar>x'\<bar> < 1" by auto
   1.177 +      then
   1.178 +        have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
   1.179 +        by (rule summable_Integral)
   1.180        let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
   1.181        show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
   1.182 -        by (rule sums_summable[where l="0 + ?S"], rule sums_if, rule sums_zero, rule summable_sums, rule summable_Integral[OF `\<bar>x'\<bar> < 1`])
   1.183 +        apply (rule sums_summable [where l="0 + ?S"])
   1.184 +        apply (rule sums_if)
   1.185 +        apply (rule sums_zero)
   1.186 +        apply (rule summable_sums)
   1.187 +        apply (rule *)
   1.188 +        done
   1.189      }
   1.190    qed auto
   1.191    thus ?thesis unfolding Int_eq arctan_eq .