src/HOL/Transcendental.thy
changeset 54575 0b9ca2c865cb
parent 54573 07864001495d
child 54576 e877eec2b698
     1.1 --- a/src/HOL/Transcendental.thy	Sun Nov 24 13:07:47 2013 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Nov 24 18:37:25 2013 +0000
     1.3 @@ -641,11 +641,8 @@
     1.4            \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
     1.5        apply (simp only: norm_mult mult_assoc)
     1.6        apply (rule mult_left_mono [OF _ norm_ge_zero])
     1.7 -      apply (simp (no_asm) add: mult_assoc [symmetric])
     1.8 -      apply (rule lemma_termdiff3)
     1.9 -      apply (rule h)
    1.10 -      apply (rule r1 [THEN order_less_imp_le])
    1.11 -      apply (rule xh [THEN order_less_imp_le])
    1.12 +      apply (simp add: mult_assoc [symmetric])
    1.13 +      apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
    1.14        done
    1.15    qed
    1.16  qed
    1.17 @@ -653,9 +650,9 @@
    1.18  lemma termdiffs:
    1.19    fixes K x :: "'a::{real_normed_field,banach}"
    1.20    assumes 1: "summable (\<lambda>n. c n * K ^ n)"
    1.21 -    and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
    1.22 -    and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
    1.23 -    and 4: "norm x < norm K"
    1.24 +      and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
    1.25 +      and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
    1.26 +      and 4: "norm x < norm K"
    1.27    shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
    1.28    unfolding deriv_def
    1.29  proof (rule LIM_zero_cancel)
    1.30 @@ -676,20 +673,23 @@
    1.31        by (rule powser_inside [OF 1 5])
    1.32      have C: "summable (\<lambda>n. diffs c n * x ^ n)"
    1.33        by (rule powser_inside [OF 2 4])
    1.34 -    show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
    1.35 -             - (\<Sum>n. diffs c n * x ^ n) =
    1.36 -          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
    1.37 -      apply (subst sums_unique [OF diffs_equiv [OF C]])
    1.38 -      apply (subst suminf_diff [OF B A])
    1.39 -      apply (subst suminf_divide [symmetric])
    1.40 -      apply (rule summable_diff [OF B A])
    1.41 +    let ?dp = "(\<Sum>n. of_nat n * c n * x ^ (n - Suc 0))"
    1.42 +    have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
    1.43 +          ((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - ?dp"  
    1.44 +      by (metis sums_unique [OF diffs_equiv [OF C]])
    1.45 +    also have "... = (\<Sum>n. c n * (x + h) ^ n - c n * x ^ n) / h - ?dp"  
    1.46 +      by (metis suminf_diff [OF B A])
    1.47 +    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h)  - ?dp"
    1.48 +      by (metis suminf_divide [OF summable_diff [OF B A]] )  
    1.49 +    also have "... = (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
    1.50        apply (subst suminf_diff)
    1.51 -      apply (rule summable_divide)
    1.52 -      apply (rule summable_diff [OF B A])
    1.53 -      apply (rule sums_summable [OF diffs_equiv [OF C]])
    1.54 -      apply (rule arg_cong [where f="suminf"], rule ext)
    1.55 -      apply (simp add: algebra_simps)
    1.56 +      apply (auto intro: summable_divide summable_diff [OF B A] sums_summable [OF diffs_equiv [OF C]])
    1.57        done
    1.58 +    also have "... = (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
    1.59 +      by (simp add: algebra_simps)
    1.60 +    finally show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
    1.61 +                   - (\<Sum>n. diffs c n * x ^ n) =
    1.62 +                  (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))" . 
    1.63    next
    1.64      show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
    1.65        by (rule termdiffs_aux [OF 3 4])
    1.66 @@ -1159,13 +1159,25 @@
    1.67  
    1.68  text {* Strict monotonicity of exponential. *}
    1.69  
    1.70 -lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) \<Longrightarrow> (1 + x) \<le> exp(x)"
    1.71 -  apply (drule order_le_imp_less_or_eq, auto)
    1.72 -  apply (simp add: exp_def)
    1.73 -  apply (rule order_trans)
    1.74 -  apply (rule_tac [2] n = 2 and f = "(\<lambda>n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
    1.75 -  apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
    1.76 -  done
    1.77 +lemma exp_ge_add_one_self_aux: 
    1.78 +  assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
    1.79 +using order_le_imp_less_or_eq [OF assms]
    1.80 +proof 
    1.81 +  assume "0 < x"
    1.82 +  have "1+x \<le> (\<Sum>n = 0..<2. inverse (real (fact n)) * x ^ n)"
    1.83 +    by (auto simp add: numeral_2_eq_2)
    1.84 +  also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
    1.85 +    apply (rule series_pos_le [OF summable_exp])
    1.86 +    using `0 < x`
    1.87 +    apply (auto  simp add:  zero_le_mult_iff)
    1.88 +    done
    1.89 +  finally show "1+x \<le> exp x" 
    1.90 +    by (simp add: exp_def)
    1.91 +next
    1.92 +  assume "0 = x"
    1.93 +  then show "1 + x \<le> exp x"
    1.94 +    by auto
    1.95 +qed
    1.96  
    1.97  lemma exp_gt_one: "0 < (x::real) \<Longrightarrow> 1 < exp x"
    1.98  proof -
    1.99 @@ -1188,9 +1200,8 @@
   1.100  qed
   1.101  
   1.102  lemma exp_less_cancel: "exp (x::real) < exp y \<Longrightarrow> x < y"
   1.103 -  apply (simp add: linorder_not_le [symmetric])
   1.104 -  apply (auto simp add: order_le_less exp_less_mono)
   1.105 -  done
   1.106 +  unfolding linorder_not_le [symmetric]
   1.107 +  by (auto simp add: order_le_less exp_less_mono)
   1.108  
   1.109  lemma exp_less_cancel_iff [iff]: "exp (x::real) < exp y \<longleftrightarrow> x < y"
   1.110    by (auto intro: exp_less_mono exp_less_cancel)
   1.111 @@ -2090,55 +2101,32 @@
   1.112  lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
   1.113    apply (case_tac "a = 0", simp)
   1.114    apply (case_tac "x = y", simp)
   1.115 -  apply (rule order_less_imp_le)
   1.116 -  apply (rule powr_less_mono2, auto)
   1.117 +  apply (metis less_eq_real_def powr_less_mono2)
   1.118    done
   1.119  
   1.120  lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   1.121    unfolding powr_def exp_inj_iff by simp
   1.122  
   1.123  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
   1.124 -  apply (rule mult_imp_le_div_pos)
   1.125 -  apply (assumption)
   1.126 -  apply (subst mult_commute)
   1.127 -  apply (subst ln_powr [THEN sym])
   1.128 -  apply auto
   1.129 -  apply (rule ln_bound)
   1.130 -  apply (erule ge_one_powr_ge_zero)
   1.131 -  apply (erule order_less_imp_le)
   1.132 -  done
   1.133 +  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult_commute 
   1.134 +            order.strict_trans2 powr_gt_zero zero_less_one)
   1.135  
   1.136  lemma ln_powr_bound2:
   1.137    assumes "1 < x" and "0 < a"
   1.138    shows "(ln x) powr a <= (a powr a) * x"
   1.139  proof -
   1.140    from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
   1.141 -    apply (intro ln_powr_bound)
   1.142 -    apply (erule order_less_imp_le)
   1.143 -    apply (rule divide_pos_pos)
   1.144 -    apply simp_all
   1.145 -    done
   1.146 +    by (metis less_eq_real_def ln_powr_bound zero_less_divide_1_iff)
   1.147    also have "... = a * (x powr (1 / a))"
   1.148      by simp
   1.149    finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
   1.150 -    apply (intro powr_mono2)
   1.151 -    apply (rule order_less_imp_le, rule assms)
   1.152 -    apply (rule ln_gt_zero)
   1.153 -    apply (rule assms)
   1.154 -    apply assumption
   1.155 -    done
   1.156 +    by (metis assms less_imp_le ln_gt_zero powr_mono2)
   1.157    also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
   1.158 -    apply (rule powr_mult)
   1.159 -    apply (rule assms)
   1.160 -    apply (rule powr_gt_zero)
   1.161 -    done
   1.162 +    by (metis assms(2) powr_mult powr_gt_zero)
   1.163    also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
   1.164      by (rule powr_powr)
   1.165 -  also have "... = x"
   1.166 -    apply simp
   1.167 -    apply (subgoal_tac "a ~= 0")
   1.168 -    using assms apply auto
   1.169 -    done
   1.170 +  also have "... = x" using assms
   1.171 +    by auto
   1.172    finally show ?thesis .
   1.173  qed
   1.174  
   1.175 @@ -2488,12 +2476,7 @@
   1.176  lemma real_mult_inverse_cancel:
   1.177       "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
   1.178        ==> inverse x * y < inverse x1 * u"
   1.179 -  apply (rule_tac c=x in mult_less_imp_less_left)
   1.180 -  apply (auto simp add: mult_assoc [symmetric])
   1.181 -  apply (simp (no_asm) add: mult_ac)
   1.182 -  apply (rule_tac c=x1 in mult_less_imp_less_right)
   1.183 -  apply (auto simp add: mult_ac)
   1.184 -  done
   1.185 +  by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)
   1.186  
   1.187  lemma real_mult_inverse_cancel2:
   1.188       "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
   1.189 @@ -2574,7 +2557,7 @@
   1.190  lemma pi_half_gt_zero [simp]: "0 < pi / 2"
   1.191    apply (rule order_le_neq_trans)
   1.192    apply (simp add: pi_half cos_is_zero [THEN theI'])
   1.193 -  apply (rule notI, drule arg_cong [where f=cos], simp)
   1.194 +  apply (metis cos_pi_half cos_zero zero_neq_one)
   1.195    done
   1.196  
   1.197  lemmas pi_half_neq_zero [simp] = pi_half_gt_zero [THEN less_imp_neq, symmetric]
   1.198 @@ -2583,7 +2566,7 @@
   1.199  lemma pi_half_less_two [simp]: "pi / 2 < 2"
   1.200    apply (rule order_le_neq_trans)
   1.201    apply (simp add: pi_half cos_is_zero [THEN theI'])
   1.202 -  apply (rule notI, drule arg_cong [where f=cos], simp)
   1.203 +  apply (metis cos_pi_half cos_two_neq_zero)
   1.204    done
   1.205  
   1.206  lemmas pi_half_neq_two [simp] = pi_half_less_two [THEN less_imp_neq]
   1.207 @@ -2646,11 +2629,7 @@
   1.208    by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
   1.209  
   1.210  lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
   1.211 -proof -
   1.212 -  have "cos (pi * real n) = cos (real n * pi)" by (simp only: mult_commute)
   1.213 -  also have "... = -1 ^ n" by (rule cos_npi)
   1.214 -  finally show ?thesis .
   1.215 -qed
   1.216 +  by (metis cos_npi mult_commute)
   1.217  
   1.218  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
   1.219    by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
   1.220 @@ -2665,10 +2644,7 @@
   1.221    by simp
   1.222  
   1.223  lemma sin_gt_zero2: "[| 0 < x; x < pi/2 |] ==> 0 < sin x"
   1.224 -  apply (rule sin_gt_zero, assumption)
   1.225 -  apply (rule order_less_trans, assumption)
   1.226 -  apply (rule pi_half_less_two)
   1.227 -  done
   1.228 +  by (metis sin_gt_zero order_less_trans pi_half_less_two)
   1.229  
   1.230  lemma sin_less_zero:
   1.231    assumes "- pi/2 < x" and "x < 0"
   1.232 @@ -2692,8 +2668,7 @@
   1.233  
   1.234  lemma cos_gt_zero_pi: "[| -(pi/2) < x; x < pi/2 |] ==> 0 < cos x"
   1.235    apply (rule_tac x = x and y = 0 in linorder_cases)
   1.236 -  apply (rule cos_minus [THEN subst])
   1.237 -  apply (rule cos_gt_zero)
   1.238 +  apply (metis cos_gt_zero cos_minus minus_less_iff neg_0_less_iff_less)
   1.239    apply (auto intro: cos_gt_zero)
   1.240    done
   1.241