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.156  by(auto simp add: algebra_simps power_add [symmetric])
   1.157  
   1.158 @@ -535,7 +536,7 @@
   1.159        apply (simp add: diffs_def)
   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.237        by (rule add_strict_mono [OF add_less_le_mono])
   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.282  apply (rule exp_ge_add_one_self_aux, 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.411  lemma lemma_DERIV_sin_cos_add:
   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.419  lemma sin_cos_add [simp]:
   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.425         in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
   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.486  apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
   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.546 -apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
   1.547 +apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
   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.574  by (simp add: cos_double)
   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.625              simp add: differentiable_def)
   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.636  apply (simp (no_asm) add: add_assoc)
   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.681 -apply (simp_all add: add_increasing)  
   1.682 +apply (simp_all add: add_increasing)
   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.701  apply (auto simp add: cos_add)
   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.722  by (simp add: tan_def)
   1.723  
   1.724 -lemma lemma_tan_add1: 
   1.725 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
   1.726 +lemma lemma_tan_add1:
   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.736              simp add: mult_assoc left_diff_distrib cos_add)
   1.737  done
   1.738  
   1.739 -lemma add_tan_eq: 
   1.740 -      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
   1.741 +lemma add_tan_eq:
   1.742 +      "[| cos x \<noteq> 0; cos y \<noteq> 0 |]
   1.743         ==> tan x + tan y = sin(x + y)/(cos x * cos y)"
   1.744  apply (simp add: tan_def)
   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.749  lemma tan_add:
   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.753  apply (simp (no_asm_simp) add: add_tan_eq lemma_tan_add1)
   1.754  apply (simp add: tan_def)
   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.799              simp add: differentiable_def)
   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.832    by (simp add: tan_def)
   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.925      by (auto simp add: algebra_simps sin_add)
   1.926    thus ?thesis
   1.927 -    by (simp add: real_of_nat_Suc left_distrib add_divide_distrib 
   1.928 +    by (simp add: real_of_nat_Suc left_distrib add_divide_distrib
   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.979    from arctan_add[OF this]
   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 ..