src/HOL/Transcendental.thy
 changeset 41970 47d6e13d1710 parent 41550 efa734d9b221 child 43335 9f8766a8ebe0
```     1.1 --- a/src/HOL/Transcendental.thy	Mon Mar 14 14:37:33 2011 +0100
1.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 14 14:37:35 2011 +0100
1.3 @@ -22,14 +22,14 @@
1.4
1.5  lemma lemma_realpow_diff_sumr:
1.6    fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
1.7 -     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
1.8 +     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
1.9        y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.10  by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
1.11           del: setsum_op_ivl_Suc)
1.12
1.13  lemma lemma_realpow_diff_sumr2:
1.14    fixes y :: "'a::{comm_ring,monoid_mult}" shows
1.15 -     "x ^ (Suc n) - y ^ (Suc n) =
1.16 +     "x ^ (Suc n) - y ^ (Suc n) =
1.17        (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
1.18  apply (induct n, simp)
1.19  apply (simp del: setsum_op_ivl_Suc)
1.20 @@ -42,7 +42,7 @@
1.21  done
1.22
1.23  lemma lemma_realpow_rev_sumr:
1.24 -     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
1.25 +     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
1.26        (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
1.27  apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
1.28  apply (rule inj_onI, simp)
1.29 @@ -107,16 +107,16 @@
1.30
1.31  lemma powser_inside:
1.32    fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
1.33 -     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
1.34 +     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]
1.35        ==> summable (%n. f(n) * (z ^ n))"
1.36  by (rule powser_insidea [THEN summable_norm_cancel])
1.37
1.38  lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows
1.39 -  "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) =
1.40 +  "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) =
1.41     (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))"
1.42  proof (induct n)
1.43    case (Suc n)
1.44 -  have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
1.45 +  have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
1.46          (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
1.47      using Suc.hyps unfolding One_nat_def by auto
1.48    also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
1.49 @@ -133,7 +133,7 @@
1.50
1.51    let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i - 1) div 2)"
1.52    { fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto
1.53 -    have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }"
1.54 +    have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }"
1.55        using sum_split_even_odd by auto
1.56      hence "(norm (?SUM (2 * (m div 2)) - x) < r)" using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
1.57      moreover
1.58 @@ -161,13 +161,13 @@
1.59    { fix B T E have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
1.60        by (cases B) auto } note if_sum = this
1.61    have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x" using sums_if'[OF `g sums x`] .
1.62 -  {
1.63 +  {
1.64      have "?s 0 = 0" by auto
1.65      have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
1.66      have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
1.67
1.68      have "?s sums y" using sums_if'[OF `f sums y`] .
1.69 -    from this[unfolded sums_def, THEN LIMSEQ_Suc]
1.70 +    from this[unfolded sums_def, THEN LIMSEQ_Suc]
1.71      have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
1.72        unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric]
1.73                  image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def]
1.74 @@ -181,7 +181,7 @@
1.75  lemma sums_alternating_upper_lower:
1.76    fixes a :: "nat \<Rightarrow> real"
1.77    assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
1.78 -  shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and>
1.79 +  shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and>
1.80               ((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
1.81    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
1.82  proof -
1.83 @@ -194,21 +194,21 @@
1.84    proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
1.85      unfolding One_nat_def by auto qed
1.86    moreover
1.87 -  have "\<forall> n. ?f n \<le> ?g n"
1.88 +  have "\<forall> n. ?f n \<le> ?g n"
1.89    proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
1.90      unfolding One_nat_def by auto qed
1.91    moreover
1.92    have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
1.93    proof (rule LIMSEQ_I)
1.94      fix r :: real assume "0 < r"
1.95 -    with `a ----> 0`[THEN LIMSEQ_D]
1.96 +    with `a ----> 0`[THEN LIMSEQ_D]
1.97      obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r" by auto
1.98      hence "\<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.99      thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
1.100    qed
1.101    ultimately
1.102    show ?thesis by (rule lemma_nest_unique)
1.103 -qed
1.104 +qed
1.105
1.106  lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"
1.107    assumes a_zero: "a ----> 0" and a_pos: "\<And> n. 0 \<le> a n"
1.108 @@ -225,16 +225,16 @@
1.109    let "?g n" = "?P (2 * n + 1)"
1.110    obtain l :: real where below_l: "\<forall> n. ?f n \<le> l" and "?f ----> l" and above_l: "\<forall> n. l \<le> ?g n" and "?g ----> l"
1.111      using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
1.112 -
1.113 +
1.114    let ?Sa = "\<lambda> m. \<Sum> n = 0..<m. ?S n"
1.115    have "?Sa ----> l"
1.116    proof (rule LIMSEQ_I)
1.117      fix r :: real assume "0 < r"
1.118
1.119 -    with `?f ----> l`[THEN LIMSEQ_D]
1.120 +    with `?f ----> l`[THEN LIMSEQ_D]
1.121      obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
1.122
1.123 -    from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
1.124 +    from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
1.125      obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
1.126
1.127      { fix n :: nat
1.128 @@ -302,7 +302,7 @@
1.129      hence ?summable unfolding summable_def by auto
1.130      moreover
1.131      have "\<And> a b :: real. \<bar> - a - - b \<bar> = \<bar>a - b\<bar>" unfolding minus_diff_minus by auto
1.132 -
1.133 +
1.134      from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
1.135      have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)" by auto
1.136
1.137 @@ -336,8 +336,9 @@
1.138  done
1.139
1.140  lemma diffs_equiv:
1.141 -     "summable (%n. (diffs c)(n) * (x ^ n)) ==>
1.142 -      (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
1.143 +  fixes x :: "'a::{real_normed_vector, ring_1}"
1.144 +  shows "summable (%n. (diffs c)(n) * (x ^ n)) ==>
1.145 +      (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
1.146           (\<Sum>n. (diffs c)(n) * (x ^ n))"
1.147  unfolding diffs_def
1.148  apply (drule summable_sums)
1.149 @@ -346,7 +347,7 @@
1.150
1.151  lemma lemma_termdiff1:
1.152    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
1.153 -  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
1.154 +  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
1.155     (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
1.157
1.158 @@ -535,7 +536,7 @@
1.160        apply (case_tac n, simp_all add: r_neq_0)
1.161        done
1.162 -    finally have "summable
1.163 +    finally have "summable
1.164        (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
1.165        by (rule diffs_equiv [THEN sums_summable])
1.166      also have
1.167 @@ -596,7 +597,7 @@
1.168      have C: "summable (\<lambda>n. diffs c n * x ^ n)"
1.169        by (rule powser_inside [OF 2 4])
1.170      show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
1.171 -             - (\<Sum>n. diffs c n * x ^ n) =
1.172 +             - (\<Sum>n. diffs c n * x ^ n) =
1.173            (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
1.174        apply (subst sums_unique [OF diffs_equiv [OF C]])
1.175        apply (subst suminf_diff [OF B A])
1.176 @@ -646,10 +647,10 @@
1.177  proof (rule LIM_I)
1.178    fix r :: real assume "0 < r" hence "0 < r/3" by auto
1.179
1.180 -  obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
1.181 +  obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
1.182      using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
1.183
1.184 -  obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
1.185 +  obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
1.186      using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto
1.187
1.188    let ?N = "Suc (max N_L N_f')"
1.189 @@ -672,7 +673,7 @@
1.190      proof (rule ballI)
1.191        fix x assume "x \<in> ?s ` {0..<?N}"
1.192        then obtain n where "x = ?s n" and "n \<in> {0..<?N}" using image_iff[THEN iffD1] by blast
1.193 -      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
1.194 +      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
1.195        obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)" by auto
1.196        have "0 < ?s n" by (rule someI2[where a=s], auto simp add: s_bound)
1.197        thus "0 < x" unfolding `x = ?s n` .
1.198 @@ -685,7 +686,7 @@
1.199
1.200    { fix x assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
1.201      hence x_in_I: "x0 + x \<in> { a <..< b }" using S_a S_b by auto
1.202 -
1.203 +
1.204      note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
1.205      note div_smbl = summable_divide[OF diff_smbl]
1.206      note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`]
1.207 @@ -695,7 +696,7 @@
1.208      note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
1.209
1.210      { fix n
1.211 -      have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
1.212 +      have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
1.213          using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] unfolding abs_divide .
1.214        hence "\<bar> ( \<bar> ?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)" using `x \<noteq> 0` by auto
1.215      } note L_ge = summable_le2[OF allI[OF this] ign[OF `summable L`]]
1.216 @@ -709,7 +710,7 @@
1.217        fix n assume "n \<in> { 0 ..< ?N}"
1.218        have "\<bar> x \<bar> < S" using `\<bar> x \<bar> < S` .
1.219        also have "S \<le> S'" using `S \<le> S'` .
1.220 -      also have "S' \<le> ?s n" unfolding S'_def
1.221 +      also have "S' \<le> ?s n" unfolding S'_def
1.222        proof (rule Min_le_iff[THEN iffD2])
1.223          have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n" using `n \<in> { 0 ..< ?N}` by auto
1.224          thus "\<exists> a \<in> (?s ` {0..<?N}). a \<le> ?s n" by blast
1.225 @@ -727,16 +728,16 @@
1.226      finally have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
1.227
1.228      from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
1.229 -    have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> =
1.230 +    have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> =
1.231                      \<bar> \<Sum>n. ?diff n x - f' x0 n \<bar>" unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric] using suminf_divide[OF diff_smbl, symmetric] by auto
1.232      also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq)
1.233      also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto
1.234 -    also have "\<dots> < r /3 + r/3 + r/3"
1.235 +    also have "\<dots> < r /3 + r/3 + r/3"
1.236        using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
1.238      finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r"
1.239        by auto
1.240 -  } thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
1.241 +  } thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
1.242        norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r" using `0 < S`
1.243      unfolding real_norm_def diff_0_right by blast
1.244  qed
1.245 @@ -761,9 +762,9 @@
1.246        { fix n x y assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
1.247          show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
1.248          proof -
1.249 -          have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> = (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>"
1.250 +          have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> = (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>"
1.251              unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult by auto
1.252 -          also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
1.253 +          also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
1.254            proof (rule mult_left_mono)
1.255              have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)" by (rule setsum_abs)
1.256              also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)"
1.257 @@ -809,7 +810,7 @@
1.258    next
1.259      case False
1.260      have "- ?R < 0" using assms by auto
1.261 -    also have "\<dots> \<le> x0" using False by auto
1.262 +    also have "\<dots> \<le> x0" using False by auto
1.263      finally show ?thesis .
1.264    qed
1.265    hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R" using assms by auto
1.266 @@ -871,7 +872,7 @@
1.267  unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
1.268
1.269
1.270 -lemma exp_fdiffs:
1.271 +lemma exp_fdiffs:
1.272        "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
1.273  by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def of_nat_mult
1.274           del: mult_Suc of_nat_Suc)
1.275 @@ -1081,7 +1082,7 @@
1.276  lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
1.277  apply (rule IVT)
1.278  apply (auto intro: isCont_exp simp add: le_diff_eq)
1.279 -apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)")
1.280 +apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)")
1.281  apply simp
1.283  done
1.284 @@ -1160,12 +1161,12 @@
1.285  qed
1.286
1.287  lemma ln_ge_zero_imp_ge_one:
1.288 -  assumes ln: "0 \<le> ln x"
1.289 +  assumes ln: "0 \<le> ln x"
1.290        and x:  "0 < x"
1.291    shows "1 \<le> x"
1.292  proof -
1.293    from ln have "ln 1 \<le> ln x" by simp
1.294 -  thus ?thesis by (simp add: x del: ln_one)
1.295 +  thus ?thesis by (simp add: x del: ln_one)
1.296  qed
1.297
1.298  lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
1.299 @@ -1183,12 +1184,12 @@
1.300  qed
1.301
1.302  lemma ln_gt_zero_imp_gt_one:
1.303 -  assumes ln: "0 < ln x"
1.304 +  assumes ln: "0 < ln x"
1.305        and x:  "0 < x"
1.306    shows "1 < x"
1.307  proof -
1.308    from ln have "ln 1 < ln x" by simp
1.309 -  thus ?thesis by (simp add: x del: ln_one)
1.310 +  thus ?thesis by (simp add: x del: ln_one)
1.311  qed
1.312
1.313  lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
1.314 @@ -1285,22 +1286,22 @@
1.315  done
1.316
1.317  lemma lemma_STAR_sin:
1.318 -     "(if even n then 0
1.319 +     "(if even n then 0
1.320         else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
1.321  by (induct "n", auto)
1.322
1.323  lemma lemma_STAR_cos:
1.324 -     "0 < n -->
1.325 +     "0 < n -->
1.326        -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
1.327  by (induct "n", auto)
1.328
1.329  lemma lemma_STAR_cos1:
1.330 -     "0 < n -->
1.331 +     "0 < n -->
1.332        (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
1.333  by (induct "n", auto)
1.334
1.335  lemma lemma_STAR_cos2:
1.336 -  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
1.337 +  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
1.338                           else 0) = 0"
1.339  apply (induct "n")
1.340  apply (case_tac [2] "n", auto)
1.341 @@ -1314,7 +1315,7 @@
1.342
1.343  lemma sin_fdiffs: "diffs sin_coeff = cos_coeff"
1.344  unfolding sin_coeff_def cos_coeff_def
1.345 -by (auto intro!: ext
1.346 +by (auto intro!: ext
1.347           simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
1.348           simp del: mult_Suc of_nat_Suc)
1.349
1.350 @@ -1323,7 +1324,7 @@
1.351
1.352  lemma cos_fdiffs: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
1.353  unfolding sin_coeff_def cos_coeff_def
1.354 -by (auto intro!: ext
1.355 +by (auto intro!: ext
1.356           simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
1.357           simp del: mult_Suc of_nat_Suc)
1.358
1.359 @@ -1424,8 +1425,8 @@
1.360       "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
1.361    by (auto intro!: DERIV_intros)
1.362
1.363 -lemma DERIV_sin_circle_all:
1.364 -     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
1.365 +lemma DERIV_sin_circle_all:
1.366 +     "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
1.367               (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
1.368    by (auto intro!: DERIV_intros)
1.369
1.370 @@ -1462,29 +1463,29 @@
1.371  by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
1.372
1.373  lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
1.374 -apply (insert abs_sin_le_one [of x])
1.375 -apply (simp add: abs_le_iff del: abs_sin_le_one)
1.376 +apply (insert abs_sin_le_one [of x])
1.377 +apply (simp add: abs_le_iff del: abs_sin_le_one)
1.378  done
1.379
1.380  lemma sin_le_one [simp]: "sin x \<le> 1"
1.381 -apply (insert abs_sin_le_one [of x])
1.382 -apply (simp add: abs_le_iff del: abs_sin_le_one)
1.383 +apply (insert abs_sin_le_one [of x])
1.384 +apply (simp add: abs_le_iff del: abs_sin_le_one)
1.385  done
1.386
1.387  lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
1.388  by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
1.389
1.390  lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
1.391 -apply (insert abs_cos_le_one [of x])
1.392 -apply (simp add: abs_le_iff del: abs_cos_le_one)
1.393 +apply (insert abs_cos_le_one [of x])
1.394 +apply (simp add: abs_le_iff del: abs_cos_le_one)
1.395  done
1.396
1.397  lemma cos_le_one [simp]: "cos x \<le> 1"
1.398 -apply (insert abs_cos_le_one [of x])
1.399 +apply (insert abs_cos_le_one [of x])
1.400  apply (simp add: abs_le_iff del: abs_cos_le_one)
1.401  done
1.402
1.403 -lemma DERIV_fun_pow: "DERIV g x :> m ==>
1.404 +lemma DERIV_fun_pow: "DERIV g x :> m ==>
1.405        DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
1.406  unfolding One_nat_def
1.407  apply (rule lemma_DERIV_subst)
1.408 @@ -1515,15 +1516,15 @@
1.409
1.410  (* lemma *)
1.412 -     "\<forall>x.
1.413 -         DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.414 +     "\<forall>x.
1.415 +         DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.416                 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
1.417    by (auto intro!: DERIV_intros simp add: algebra_simps)
1.418
1.420 -     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.421 +     "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.422        (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
1.423 -apply (cut_tac y = 0 and x = x and y7 = y
1.424 +apply (cut_tac y = 0 and x = x and y7 = y
1.426  apply (auto simp add: numeral_2_eq_2)
1.427  done
1.428 @@ -1543,9 +1544,9 @@
1.429    by (auto intro!: DERIV_intros simp add: algebra_simps)
1.430
1.431
1.432 -lemma sin_cos_minus:
1.433 +lemma sin_cos_minus:
1.434      "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
1.435 -apply (cut_tac y = 0 and x = x
1.436 +apply (cut_tac y = 0 and x = x
1.437         in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
1.438  apply simp
1.439  done
1.440 @@ -1582,27 +1583,27 @@
1.441    pi :: "real" where
1.442    "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
1.443
1.444 -text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
1.445 +text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
1.446     hence define pi.*}
1.447
1.448  lemma sin_paired:
1.449 -     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1))
1.450 +     "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1))
1.451        sums  sin x"
1.452  proof -
1.453    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
1.454      unfolding sin_def
1.455 -    by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
1.456 +    by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
1.457    thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
1.458  qed
1.459
1.460  text {* FIXME: This is a long, ugly proof! *}
1.461  lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
1.462 -apply (subgoal_tac
1.463 +apply (subgoal_tac
1.464         "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
1.465 -              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
1.466 +              -1 ^ k / real (fact (2 * k + 1)) * x ^ (2 * k + 1))
1.467       sums (\<Sum>n. -1 ^ n / real (fact (2 * n + 1)) * x ^ (2 * n + 1))")
1.468   prefer 2
1.469 - apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
1.470 + apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
1.471  apply (rotate_tac 2)
1.472  apply (drule sin_paired [THEN sums_unique, THEN ssubst])
1.473  unfolding One_nat_def
1.474 @@ -1614,10 +1615,10 @@
1.475  apply (erule sums_summable)
1.476  apply (case_tac "m=0")
1.477  apply (simp (no_asm_simp))
1.478 -apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
1.479 -apply (simp only: mult_less_cancel_left, simp)
1.480 +apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
1.481 +apply (simp only: mult_less_cancel_left, simp)
1.482  apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
1.483 -apply (subgoal_tac "x*x < 2*3", simp)
1.484 +apply (subgoal_tac "x*x < 2*3", simp)
1.485  apply (rule mult_strict_mono)
1.487  apply (subst fact_Suc)
1.488 @@ -1630,15 +1631,15 @@
1.489  apply (subst real_of_nat_mult)
1.490  apply (simp (no_asm) add: divide_inverse del: fact_Suc)
1.491  apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
1.492 -apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
1.493 +apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
1.494  apply (auto simp add: mult_assoc simp del: fact_Suc)
1.495 -apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
1.496 +apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
1.497  apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
1.498 -apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
1.499 +apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
1.500  apply (erule ssubst)+
1.501  apply (auto simp del: fact_Suc)
1.502  apply (subgoal_tac "0 < x ^ (4 * m) ")
1.503 - prefer 2 apply (simp only: zero_less_power)
1.504 + prefer 2 apply (simp only: zero_less_power)
1.505  apply (simp (no_asm_simp) add: mult_less_cancel_left)
1.506  apply (rule mult_strict_mono)
1.507  apply (simp_all (no_asm_simp))
1.508 @@ -1657,7 +1658,7 @@
1.509  proof -
1.510    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
1.511      unfolding cos_def
1.512 -    by (rule cos_converges [THEN sums_summable, THEN sums_group], simp)
1.513 +    by (rule cos_converges [THEN sums_summable, THEN sums_group], simp)
1.514    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
1.515  qed
1.516
1.517 @@ -1665,12 +1666,12 @@
1.518  by simp
1.519
1.520  lemma real_mult_inverse_cancel:
1.521 -     "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
1.522 +     "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
1.523        ==> inverse x * y < inverse x1 * u"
1.524 -apply (rule_tac c=x in mult_less_imp_less_left)
1.525 +apply (rule_tac c=x in mult_less_imp_less_left)
1.526  apply (auto simp add: mult_assoc [symmetric])
1.527  apply (simp (no_asm) add: mult_ac)
1.528 -apply (rule_tac c=x1 in mult_less_imp_less_right)
1.529 +apply (rule_tac c=x1 in mult_less_imp_less_right)
1.530  apply (auto simp add: mult_ac)
1.531  done
1.532
1.533 @@ -1687,7 +1688,7 @@
1.534  lemma cos_two_less_zero [simp]: "cos (2) < 0"
1.535  apply (cut_tac x = 2 in cos_paired)
1.536  apply (drule sums_minus)
1.537 -apply (rule neg_less_iff_less [THEN iffD1])
1.538 +apply (rule neg_less_iff_less [THEN iffD1])
1.539  apply (frule sums_unique, auto)
1.540  apply (rule_tac y =
1.541   "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
1.542 @@ -1697,12 +1698,12 @@
1.543  apply (rule sumr_pos_lt_pair)
1.544  apply (erule sums_summable, safe)
1.545  unfolding One_nat_def
1.548              del: fact_Suc)
1.549  apply (rule real_mult_inverse_cancel2)
1.550  apply (rule real_of_nat_fact_gt_zero)+
1.551  apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
1.552 -apply (subst fact_lemma)
1.553 +apply (subst fact_lemma)
1.554  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
1.555  apply (simp only: real_of_nat_mult)
1.556  apply (rule mult_strict_mono, force)
1.557 @@ -1822,7 +1823,7 @@
1.558  lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
1.559  proof -
1.560    have "cos (pi * real n) = cos (real n * pi)" by (simp only: mult_commute)
1.561 -  also have "... = -1 ^ n" by (rule cos_npi)
1.562 +  also have "... = -1 ^ n" by (rule cos_npi)
1.563    finally show ?thesis .
1.564  qed
1.565
1.566 @@ -1832,7 +1833,7 @@
1.567  done
1.568
1.569  lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
1.570 -by (simp add: mult_commute [of pi])
1.571 +by (simp add: mult_commute [of pi])
1.572
1.573  lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
1.575 @@ -1846,10 +1847,10 @@
1.576  apply (rule pi_half_less_two)
1.577  done
1.578
1.579 -lemma sin_less_zero:
1.580 +lemma sin_less_zero:
1.581    assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
1.582  proof -
1.583 -  have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
1.584 +  have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2)
1.585    thus ?thesis by simp
1.586  qed
1.587
1.588 @@ -1862,7 +1863,7 @@
1.589  apply (cut_tac cos_is_zero, safe)
1.590  apply (rename_tac y z)
1.591  apply (drule_tac x = y in spec)
1.592 -apply (drule_tac x = "pi/2" in spec, simp)
1.593 +apply (drule_tac x = "pi/2" in spec, simp)
1.594  done
1.595
1.596  lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
1.597 @@ -1871,10 +1872,10 @@
1.598  apply (rule cos_gt_zero)
1.599  apply (auto intro: cos_gt_zero)
1.600  done
1.601 -
1.602 +
1.603  lemma cos_ge_zero: "[| -(pi/2) \<le> x; x \<le> pi/2 |] ==> 0 \<le> cos x"
1.604  apply (auto simp add: order_le_less cos_gt_zero_pi)
1.605 -apply (subgoal_tac "x = pi/2", auto)
1.606 +apply (subgoal_tac "x = pi/2", auto)
1.607  done
1.608
1.609  lemma sin_gt_zero_pi: "[| 0 < x; x < pi  |] ==> 0 < sin x"
1.610 @@ -1897,7 +1898,7 @@
1.611    qed
1.612    then obtain y where "pi < y" and "y < 2" and "y < 2 * pi" by blast
1.613    hence "0 < sin y" using sin_gt_zero by auto
1.614 -  moreover
1.615 +  moreover
1.616    have "sin y < 0" using sin_gt_zero_pi[of "y - pi"] `pi < y` and `y < 2 * pi` sin_periodic_pi[of "y - pi"] by auto
1.617    ultimately show False by auto
1.618  qed
1.619 @@ -1914,7 +1915,7 @@
1.620  apply (drule_tac f = cos in Rolle)
1.621  apply (drule_tac [5] f = cos in Rolle)
1.622  apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos
1.623 -            dest!: DERIV_cos [THEN DERIV_unique]
1.624 +            dest!: DERIV_cos [THEN DERIV_unique]
1.626  apply (auto dest: sin_gt_zero_pi [OF order_le_less_trans order_less_le_trans])
1.627  done
1.628 @@ -1925,32 +1926,32 @@
1.629  apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
1.630  apply (erule contrapos_np)
1.631  apply (simp del: minus_sin_cos_eq [symmetric])
1.632 -apply (cut_tac y="-y" in cos_total, simp) apply simp
1.633 +apply (cut_tac y="-y" in cos_total, simp) apply simp
1.634  apply (erule ex1E)
1.635  apply (rule_tac a = "x - (pi/2)" in ex1I)
1.637  apply (rotate_tac 3)
1.638 -apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all)
1.639 +apply (drule_tac x = "xa + pi/2" in spec, safe, simp_all)
1.640  done
1.641
1.642  lemma reals_Archimedean4:
1.643       "[| 0 < y; 0 \<le> x |] ==> \<exists>n. real n * y \<le> x & x < real (Suc n) * y"
1.644  apply (auto dest!: reals_Archimedean3)
1.645 -apply (drule_tac x = x in spec, clarify)
1.646 +apply (drule_tac x = x in spec, clarify)
1.647  apply (subgoal_tac "x < real(LEAST m::nat. x < real m * y) * y")
1.648 - prefer 2 apply (erule LeastI)
1.649 -apply (case_tac "LEAST m::nat. x < real m * y", simp)
1.650 + prefer 2 apply (erule LeastI)
1.651 +apply (case_tac "LEAST m::nat. x < real m * y", simp)
1.652  apply (subgoal_tac "~ x < real nat * y")
1.653 - prefer 2 apply (rule not_less_Least, simp, force)
1.654 + prefer 2 apply (rule not_less_Least, simp, force)
1.655  done
1.656
1.657 -(* Pre Isabelle99-2 proof was simpler- numerals arithmetic
1.658 +(* Pre Isabelle99-2 proof was simpler- numerals arithmetic
1.659     now causes some unwanted re-arrangements of literals!   *)
1.660  lemma cos_zero_lemma:
1.661 -     "[| 0 \<le> x; cos x = 0 |] ==>
1.662 +     "[| 0 \<le> x; cos x = 0 |] ==>
1.663        \<exists>n::nat. ~even n & x = real n * (pi/2)"
1.664  apply (drule pi_gt_zero [THEN reals_Archimedean4], safe)
1.665 -apply (subgoal_tac "0 \<le> x - real n * pi &
1.666 +apply (subgoal_tac "0 \<le> x - real n * pi &
1.667                      (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
1.668  apply (auto simp add: algebra_simps real_of_nat_Suc)
1.669   prefer 2 apply (simp add: cos_diff)
1.670 @@ -1965,39 +1966,39 @@
1.671  done
1.672
1.673  lemma sin_zero_lemma:
1.674 -     "[| 0 \<le> x; sin x = 0 |] ==>
1.675 +     "[| 0 \<le> x; sin x = 0 |] ==>
1.676        \<exists>n::nat. even n & x = real n * (pi/2)"
1.677  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
1.678   apply (clarify, rule_tac x = "n - 1" in exI)
1.679   apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
1.680  apply (rule cos_zero_lemma)
1.683  done
1.684
1.685
1.686  lemma cos_zero_iff:
1.687 -     "(cos x = 0) =
1.688 -      ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
1.689 +     "(cos x = 0) =
1.690 +      ((\<exists>n::nat. ~even n & (x = real n * (pi/2))) |
1.691         (\<exists>n::nat. ~even n & (x = -(real n * (pi/2)))))"
1.692  apply (rule iffI)
1.693  apply (cut_tac linorder_linear [of 0 x], safe)
1.694  apply (drule cos_zero_lemma, assumption+)
1.695 -apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
1.696 -apply (force simp add: minus_equation_iff [of x])
1.697 -apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
1.698 +apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
1.699 +apply (force simp add: minus_equation_iff [of x])
1.700 +apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
1.702  done
1.703
1.704  (* ditto: but to a lesser extent *)
1.705  lemma sin_zero_iff:
1.706 -     "(sin x = 0) =
1.707 -      ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
1.708 +     "(sin x = 0) =
1.709 +      ((\<exists>n::nat. even n & (x = real n * (pi/2))) |
1.710         (\<exists>n::nat. even n & (x = -(real n * (pi/2)))))"
1.711  apply (rule iffI)
1.712  apply (cut_tac linorder_linear [of 0 x], safe)
1.713  apply (drule sin_zero_lemma, assumption+)
1.714  apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
1.715 -apply (force simp add: minus_equation_iff [of x])
1.716 +apply (force simp add: minus_equation_iff [of x])
1.717  apply (auto simp add: even_mult_two_ex)
1.718  done
1.719
1.720 @@ -2066,19 +2067,19 @@
1.721  lemma tan_periodic [simp]: "tan (x + 2*pi) = tan x"
1.723
1.725 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
1.727 +      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
1.728          ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)"
1.729  apply (simp add: tan_def divide_inverse)
1.730 -apply (auto simp del: inverse_mult_distrib
1.731 +apply (auto simp del: inverse_mult_distrib
1.732              simp add: inverse_mult_distrib [symmetric] mult_ac)
1.733  apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
1.734 -apply (auto simp del: inverse_mult_distrib
1.735 +apply (auto simp del: inverse_mult_distrib
1.737  done
1.738
1.740 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
1.742 +      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
1.743         ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
1.745  apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
1.746 @@ -2087,27 +2088,27 @@
1.747  done
1.748
1.750 -     "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
1.751 +     "[| cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0 |]
1.752        ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
1.755  done
1.756
1.757  lemma tan_double:
1.758 -     "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
1.759 +     "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |]
1.760        ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))"
1.761 -apply (insert tan_add [of x x])
1.762 -apply (simp add: mult_2 [symmetric])
1.763 +apply (insert tan_add [of x x])
1.764 +apply (simp add: mult_2 [symmetric])
1.765  apply (auto simp add: numeral_2_eq_2)
1.766  done
1.767
1.768  lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x"
1.769 -by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
1.770 -
1.771 -lemma tan_less_zero:
1.772 +by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
1.773 +
1.774 +lemma tan_less_zero:
1.775    assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
1.776  proof -
1.777 -  have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
1.778 +  have "0 < tan (- x)" using assms by (simp only: tan_gt_zero)
1.779    thus ?thesis by simp
1.780  qed
1.781
1.782 @@ -2143,8 +2144,8 @@
1.783  apply (rule LIM_mult)
1.784  apply (rule_tac [2] inverse_1 [THEN subst])
1.785  apply (rule_tac [2] LIM_inverse)
1.786 -apply (simp_all add: divide_inverse [symmetric])
1.787 -apply (simp_all only: isCont_def [symmetric] cos_pi_half [symmetric] sin_pi_half [symmetric])
1.788 +apply (simp_all add: divide_inverse [symmetric])
1.789 +apply (simp_all only: isCont_def [symmetric] cos_pi_half [symmetric] sin_pi_half [symmetric])
1.790  apply (blast intro!: DERIV_isCont DERIV_sin DERIV_cos)+
1.791  done
1.792
1.793 @@ -2189,12 +2190,12 @@
1.794  apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
1.795  apply (rule_tac [4] Rolle)
1.796  apply (rule_tac [2] Rolle)
1.797 -apply (auto intro!: DERIV_tan DERIV_isCont exI
1.798 +apply (auto intro!: DERIV_tan DERIV_isCont exI
1.800  txt{*Now, simulate TRYALL*}
1.801  apply (rule_tac [!] DERIV_tan asm_rl)
1.802  apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
1.803 -            simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
1.804 +            simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
1.805  done
1.806
1.807  lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2"
1.808 @@ -2208,7 +2209,7 @@
1.809      have "cos x' \<noteq> 0" by auto
1.810      thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan)
1.811    qed
1.812 -  from MVT2[OF `y < x` this]
1.813 +  from MVT2[OF `y < x` this]
1.814    obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<twosuperior>)" by auto
1.815    hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto
1.816    hence "0 < cos z" using cos_gt_zero_pi by auto
1.817 @@ -2228,7 +2229,7 @@
1.818    show "y < x"
1.819    proof (rule ccontr)
1.820      assume "\<not> y < x" hence "x \<le> y" by auto
1.821 -    hence "tan x \<le> tan y"
1.822 +    hence "tan x \<le> tan y"
1.823      proof (cases "x = y")
1.824        case True thus ?thesis by auto
1.825      next
1.826 @@ -2241,10 +2242,10 @@
1.827
1.828  lemma tan_inverse: "1 / (tan y) = tan (pi / 2 - y)" unfolding tan_def sin_cos_eq[of y] cos_sin_eq[of y] by auto
1.829
1.830 -lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
1.831 +lemma tan_periodic_pi[simp]: "tan (x + pi) = tan x"
1.833
1.834 -lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
1.835 +lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
1.836  proof (induct n arbitrary: x)
1.837    case (Suc n)
1.838    have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
1.839 @@ -2275,18 +2276,18 @@
1.840    arccos :: "real => real" where
1.841    "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
1.842
1.843 -definition
1.844 +definition
1.845    arctan :: "real => real" where
1.846    "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
1.847
1.848  lemma arcsin:
1.849 -     "[| -1 \<le> y; y \<le> 1 |]
1.850 -      ==> -(pi/2) \<le> arcsin y &
1.851 +     "[| -1 \<le> y; y \<le> 1 |]
1.852 +      ==> -(pi/2) \<le> arcsin y &
1.853             arcsin y \<le> pi/2 & sin(arcsin y) = y"
1.854  unfolding arcsin_def by (rule theI' [OF sin_total])
1.855
1.856  lemma arcsin_pi:
1.857 -     "[| -1 \<le> y; y \<le> 1 |]
1.858 +     "[| -1 \<le> y; y \<le> 1 |]
1.859        ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi & sin(arcsin y) = y"
1.860  apply (drule (1) arcsin)
1.861  apply (force intro: order_trans)
1.862 @@ -2294,7 +2295,7 @@
1.863
1.864  lemma sin_arcsin [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> sin(arcsin y) = y"
1.865  by (blast dest: arcsin)
1.866 -
1.867 +
1.868  lemma arcsin_bounded:
1.869       "[| -1 \<le> y; y \<le> 1 |] ==> -(pi/2) \<le> arcsin y & arcsin y \<le> pi/2"
1.870  by (blast dest: arcsin)
1.871 @@ -2323,13 +2324,13 @@
1.872  done
1.873
1.874  lemma arccos:
1.875 -     "[| -1 \<le> y; y \<le> 1 |]
1.876 +     "[| -1 \<le> y; y \<le> 1 |]
1.877        ==> 0 \<le> arccos y & arccos y \<le> pi & cos(arccos y) = y"
1.878  unfolding arccos_def by (rule theI' [OF cos_total])
1.879
1.880  lemma cos_arccos [simp]: "[| -1 \<le> y; y \<le> 1 |] ==> cos(arccos y) = y"
1.881  by (blast dest: arccos)
1.882 -
1.883 +
1.884  lemma arccos_bounded: "[| -1 \<le> y; y \<le> 1 |] ==> 0 \<le> arccos y & arccos y \<le> pi"
1.885  by (blast dest: arccos)
1.886
1.887 @@ -2340,7 +2341,7 @@
1.888  by (blast dest: arccos)
1.889
1.890  lemma arccos_lt_bounded:
1.891 -     "[| -1 < y; y < 1 |]
1.892 +     "[| -1 < y; y < 1 |]
1.893        ==> 0 < arccos y & arccos y < pi"
1.894  apply (frule order_less_imp_le)
1.895  apply (frule_tac y = y in order_less_imp_le)
1.896 @@ -2400,7 +2401,7 @@
1.897  lemma arctan_ubound: "arctan y < pi/2"
1.898  by (auto simp only: arctan)
1.899
1.900 -lemma arctan_tan:
1.901 +lemma arctan_tan:
1.902        "[|-(pi/2) < x; x < pi/2 |] ==> arctan(tan x) = x"
1.903  apply (unfold arctan_def)
1.904  apply (rule the1_equality)
1.905 @@ -2415,7 +2416,7 @@
1.906  apply (case_tac "n")
1.907  apply (case_tac [3] "n")
1.908  apply (cut_tac [2] y = x in arctan_ubound)
1.909 -apply (cut_tac [4] y = x in arctan_lbound)
1.910 +apply (cut_tac [4] y = x in arctan_lbound)
1.911  apply (auto simp add: real_of_nat_Suc left_distrib mult_less_0_iff)
1.912  done
1.913
1.914 @@ -2423,7 +2424,7 @@
1.915  apply (rule power_inverse [THEN subst])
1.916  apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
1.917  apply (auto dest: field_power_not_zero
1.918 -        simp add: power_mult_distrib left_distrib power_divide tan_def
1.919 +        simp add: power_mult_distrib left_distrib power_divide tan_def
1.920                    mult_assoc power_inverse [symmetric])
1.921  done
1.922
1.923 @@ -2588,7 +2589,7 @@
1.924    have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
1.926    thus ?thesis
1.929                    mult_commute [of pi])
1.930  qed
1.931
1.932 @@ -2627,7 +2628,7 @@
1.933  proof -
1.934    obtain z where "- (pi / 2) < z" and "z < pi / 2" and "tan z = x" using tan_total by blast
1.935    have "tan (pi / 4) = 1" and "tan (- (pi / 4)) = - 1" using tan_45 tan_minus by auto
1.936 -  have "z \<noteq> pi / 4"
1.937 +  have "z \<noteq> pi / 4"
1.938    proof (rule ccontr)
1.939      assume "\<not> (z \<noteq> pi / 4)" hence "z = pi / 4" by auto
1.940      have "tan z = 1" unfolding `z = pi / 4` `tan (pi / 4) = 1` ..
1.941 @@ -2644,11 +2645,11 @@
1.942    proof (rule ccontr)
1.943      assume "\<not> (z < pi / 4)" hence "pi / 4 < z" using `z \<noteq> pi / 4` by auto
1.944      have "- (pi / 2) < pi / 4" using m2pi_less_pi by auto
1.945 -    from tan_monotone[OF this `pi / 4 < z` `z < pi / 2`]
1.946 +    from tan_monotone[OF this `pi / 4 < z` `z < pi / 2`]
1.947      have "1 < x" unfolding `tan z = x` `tan (pi / 4) = 1` .
1.948      thus False using `\<bar>x\<bar> < 1` by auto
1.949    qed
1.950 -  moreover
1.951 +  moreover
1.952    have "-(pi / 4) < z"
1.953    proof (rule ccontr)
1.954      assume "\<not> (-(pi / 4) < z)" hence "z < - (pi / 4)" using `z \<noteq> - (pi / 4)` by auto
1.955 @@ -2677,14 +2678,14 @@
1.956      show ?thesis
1.957      proof (cases "x = 1")
1.958        case True hence "tan (pi/4) = x" using tan_45 by auto
1.959 -      moreover
1.960 +      moreover
1.961        have "- pi \<le> pi" unfolding minus_le_self_iff by auto
1.962        hence "-(pi/4) \<le> pi/4" and "pi/4 \<le> pi/4" by auto
1.963        ultimately show ?thesis by blast
1.964      next
1.965        case False hence "x = -1" using `\<not> \<bar>x\<bar> < 1` and `\<bar>x\<bar> \<le> 1` by auto
1.966        hence "tan (-(pi/4)) = x" using tan_45 tan_minus by auto
1.967 -      moreover
1.968 +      moreover
1.969        have "- pi \<le> pi" unfolding minus_le_self_iff by auto
1.970        hence "-(pi/4) \<le> pi/4" and "-(pi/4) \<le> -(pi/4)" by auto
1.971        ultimately show ?thesis by blast
1.972 @@ -2723,7 +2724,7 @@
1.973    have "\<bar>5 / 12\<bar> < (1 :: real)" by auto
1.974    from arctan_add[OF less_imp_le[OF this] this]
1.975    have "2 * arctan (5 / 12) = arctan (120 / 119)" by auto
1.976 -  moreover
1.977 +  moreover
1.978    have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)" by auto
1.980    have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)" by auto
1.981 @@ -2749,7 +2750,7 @@
1.982          show "0 \<le> x ^ Suc (Suc n * 2)" by (rule zero_le_power) (simp add: `0 \<le> x`)
1.983        qed
1.984      } note mono = this
1.985 -
1.986 +
1.987      show ?thesis
1.988      proof (cases "0 \<le> x")
1.989        case True from mono[OF this `x \<le> 1`, THEN allI]
1.990 @@ -2793,7 +2794,7 @@
1.991    from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
1.992    have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
1.993    thus ?thesis using zero_le_power2 by auto
1.994 -qed
1.995 +qed
1.996
1.997  lemma DERIV_arctan_series: assumes "\<bar> x \<bar> < 1"
1.998    shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))" (is "DERIV ?arctan _ :> ?Int")
1.999 @@ -2812,7 +2813,7 @@
1.1000    { fix f :: "nat \<Rightarrow> real"
1.1001      have "\<And> x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x"
1.1002      proof
1.1003 -      fix x :: real assume "f sums x"
1.1004 +      fix x :: real assume "f sums x"
1.1005        from sums_if[OF sums_zero this]
1.1006        show "(\<lambda> n. if even n then f (n div 2) else 0) sums x" by auto
1.1007      next
1.1008 @@ -2827,10 +2828,10 @@
1.1009      by auto
1.1010
1.1011    { fix x :: real
1.1012 -    have if_eq': "\<And> n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
1.1013 +    have if_eq': "\<And> n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
1.1014        (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
1.1015        using n_even by auto
1.1016 -    have idx_eq: "\<And> n. n * 2 + 1 = Suc (2 * n)" by auto
1.1017 +    have idx_eq: "\<And> n. n * 2 + 1 = Suc (2 * n)" by auto
1.1018      have "(\<Sum> n. ?f n * x^(Suc n)) = ?arctan x" 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.1019        by auto
1.1020    } note arctan_eq = this
1.1021 @@ -2893,10 +2894,10 @@
1.1022          show "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> isCont (\<lambda> x. suminf (?c x) - arctan x) y" using DERIV_in_rball DERIV_isCont by auto
1.1023        qed
1.1024      qed
1.1025 -
1.1026 +
1.1027      have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
1.1028        unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
1.1029 -
1.1030 +
1.1031      have "suminf (?c x) - arctan x = 0"
1.1032      proof (cases "x = 0")
1.1033        case True thus ?thesis using suminf_arctan_zero by auto
1.1034 @@ -2909,7 +2910,7 @@
1.1035        have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
1.1036          by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
1.1037            (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
1.1038 -      ultimately
1.1039 +      ultimately
1.1040        show ?thesis using suminf_arctan_zero by auto
1.1041      qed
1.1042      thus ?thesis by auto
1.1043 @@ -2971,16 +2972,16 @@
1.1044      from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
1.1045      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
1.1046      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
1.1047 -
1.1048 +
1.1049      show ?thesis
1.1050      proof (cases "x = 1", simp add: `arctan 1 = (\<Sum> i. ?c 1 i)`)
1.1051        assume "x \<noteq> 1" hence "x = -1" using `\<bar>x\<bar> = 1` by auto
1.1052 -
1.1053 +
1.1054        have "- (pi / 2) < 0" using pi_gt_zero by auto
1.1055        have "- (2 * pi) < 0" using pi_gt_zero by auto
1.1056 -
1.1057 +
1.1058        have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
1.1059 -
1.1060 +
1.1061        have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
1.1062        also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
1.1063        also have "\<dots> = - (arctan (tan (pi / 4)))" unfolding neg_equal_iff_equal by (rule arctan_tan[symmetric], auto simp add: order_less_trans[OF `- (2 * pi) < 0` pi_gt_zero])
1.1064 @@ -2999,7 +3000,7 @@
1.1065    hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto
1.1066
1.1067    have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)" by auto
1.1068 -
1.1069 +
1.1070    have "0 < cos y" using cos_gt_zero_pi[OF low high] .
1.1071    hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y) ^ 2) = cos y" by auto
1.1072
1.1073 @@ -3032,14 +3033,14 @@
1.1074  qed
1.1075
1.1076  lemma arctan_monotone': assumes "x \<le> y" shows "arctan x \<le> arctan y"
1.1077 -proof (cases "x = y")
1.1078 +proof (cases "x = y")
1.1079    case False hence "x < y" using `x \<le> y` by auto from arctan_monotone[OF this] show ?thesis by auto
1.1080  qed auto
1.1081
1.1082 -lemma arctan_minus: "arctan (- x) = - arctan x"
1.1083 +lemma arctan_minus: "arctan (- x) = - arctan x"
1.1084  proof -
1.1085    obtain y where "- (pi / 2) < y" and "y < pi / 2" and "tan y = x" using tan_total by blast
1.1086 -  thus ?thesis unfolding `tan y = x`[symmetric] tan_minus[symmetric] using arctan_tan[of y] arctan_tan[of "-y"] by auto
1.1087 +  thus ?thesis unfolding `tan y = x`[symmetric] tan_minus[symmetric] using arctan_tan[of y] arctan_tan[of "-y"] by auto
1.1088  qed
1.1089
1.1090  lemma arctan_inverse: assumes "x \<noteq> 0" shows "arctan (1 / x) = sgn x * pi / 2 - arctan x"
1.1091 @@ -3062,7 +3063,7 @@
1.1092      case True from pos_y[OF this `y < pi / 2` `y = arctan x` `tan y = x`] show ?thesis .
1.1093    next
1.1094      case False hence "y \<le> 0" by auto
1.1095 -    moreover have "y \<noteq> 0"
1.1096 +    moreover have "y \<noteq> 0"
1.1097      proof (rule ccontr)
1.1098        assume "\<not> y \<noteq> 0" hence "y = 0" by auto
1.1099        have "x = 0" unfolding `tan y = x`[symmetric] `y = 0` tan_zero ..
```