src/HOL/Ln.thy
changeset 41550 efa734d9b221
parent 40864 4abaaadfdaf2
child 41959 b460124855b8
     1.1 --- a/src/HOL/Ln.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Ln.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4      qed
     1.5      moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
     1.6        apply (simp add: mult_compare_simps)
     1.7 -      apply (simp add: prems)
     1.8 +      apply (simp add: assms)
     1.9        apply (subgoal_tac "0 <= x * (x * x^n)")
    1.10        apply force
    1.11        apply (rule mult_nonneg_nonneg, rule a)+
    1.12 @@ -91,7 +91,7 @@
    1.13        by simp
    1.14      also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
    1.15        apply (rule mult_left_mono)
    1.16 -      apply (rule prems)
    1.17 +      apply (rule c)
    1.18        apply simp
    1.19        done
    1.20      also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
    1.21 @@ -129,7 +129,7 @@
    1.22      have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
    1.23          suminf (%n. (x^2/2) * ((1/2)^n))"
    1.24        apply (rule summable_le)
    1.25 -      apply (auto simp only: aux1 prems)
    1.26 +      apply (auto simp only: aux1 a b)
    1.27        apply (rule exp_tail_after_first_two_terms_summable)
    1.28        by (rule sums_summable, rule aux2)  
    1.29      also have "... = x^2"
    1.30 @@ -155,14 +155,14 @@
    1.31      apply (rule divide_left_mono)
    1.32      apply (auto simp add: exp_ge_add_one_self_aux)
    1.33      apply (rule add_nonneg_nonneg)
    1.34 -    apply (insert prems, auto)
    1.35 +    using a apply auto
    1.36      apply (rule mult_pos_pos)
    1.37      apply auto
    1.38      apply (rule add_pos_nonneg)
    1.39      apply auto
    1.40      done
    1.41    also from a have "... <= 1 + x"
    1.42 -    by(simp add:field_simps zero_compare_simps)
    1.43 +    by (simp add: field_simps zero_compare_simps)
    1.44    finally show ?thesis .
    1.45  qed
    1.46  
    1.47 @@ -192,14 +192,14 @@
    1.48    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    1.49    moreover have "0 < 1 + x + x^2"
    1.50      apply (rule add_pos_nonneg)
    1.51 -    apply (insert a, auto)
    1.52 +    using a apply auto
    1.53      done
    1.54    ultimately have "1 - x <= 1 / (1 + x + x^2)"
    1.55      by (elim mult_imp_le_div_pos)
    1.56    also have "... <= 1 / exp x"
    1.57      apply (rule divide_left_mono)
    1.58      apply (rule exp_bound, rule a)
    1.59 -    apply (insert prems, auto)
    1.60 +    using a b apply auto
    1.61      apply (rule mult_pos_pos)
    1.62      apply (rule add_pos_nonneg)
    1.63      apply auto
    1.64 @@ -256,10 +256,10 @@
    1.65    also have "- (x / (1 - x)) = -x / (1 - x)"
    1.66      by auto
    1.67    finally have d: "- x / (1 - x) <= ln (1 - x)" .
    1.68 -  have "0 < 1 - x" using prems by simp
    1.69 +  have "0 < 1 - x" using a b by simp
    1.70    hence e: "-x - 2 * x^2 <= - x / (1 - x)"
    1.71 -    using mult_right_le_one_le[of "x*x" "2*x"] prems
    1.72 -    by(simp add:field_simps power2_eq_square)
    1.73 +    using mult_right_le_one_le[of "x*x" "2*x"] a b
    1.74 +    by (simp add:field_simps power2_eq_square)
    1.75    from e d show "- x - 2 * x^2 <= ln (1 - x)"
    1.76      by (rule order_trans)
    1.77  qed
    1.78 @@ -292,7 +292,7 @@
    1.79      "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
    1.80  proof -
    1.81    assume x: "0 <= x"
    1.82 -  assume "x <= 1"
    1.83 +  assume x1: "x <= 1"
    1.84    from x have "ln (1 + x) <= x"
    1.85      by (rule ln_add_one_self_le_self)
    1.86    then have "ln (1 + x) - x <= 0" 
    1.87 @@ -303,7 +303,7 @@
    1.88      by simp
    1.89    also have "... <= x^2"
    1.90    proof -
    1.91 -    from prems have "x - x^2 <= ln (1 + x)"
    1.92 +    from x x1 have "x - x^2 <= ln (1 + x)"
    1.93        by (intro ln_one_plus_pos_lower_bound)
    1.94      thus ?thesis
    1.95        by simp
    1.96 @@ -314,19 +314,19 @@
    1.97  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
    1.98      "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
    1.99  proof -
   1.100 -  assume "-(1 / 2) <= x"
   1.101 -  assume "x <= 0"
   1.102 +  assume a: "-(1 / 2) <= x"
   1.103 +  assume b: "x <= 0"
   1.104    have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" 
   1.105      apply (subst abs_of_nonpos)
   1.106      apply simp
   1.107      apply (rule ln_add_one_self_le_self2)
   1.108 -    apply (insert prems, auto)
   1.109 +    using a apply auto
   1.110      done
   1.111    also have "... <= 2 * x^2"
   1.112      apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
   1.113      apply (simp add: algebra_simps)
   1.114      apply (rule ln_one_minus_pos_lower_bound)
   1.115 -    apply (insert prems, auto)
   1.116 +    using a b apply auto
   1.117      done
   1.118    finally show ?thesis .
   1.119  qed
   1.120 @@ -343,9 +343,9 @@
   1.121  
   1.122  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
   1.123  proof -
   1.124 -  assume "exp 1 <= x" and "x <= y"
   1.125 +  assume x: "exp 1 <= x" "x <= y"
   1.126    have a: "0 < x" and b: "0 < y"
   1.127 -    apply (insert prems)
   1.128 +    apply (insert x)
   1.129      apply (subgoal_tac "0 < exp (1::real)")
   1.130      apply arith
   1.131      apply auto
   1.132 @@ -361,12 +361,12 @@
   1.133      done
   1.134    also have "y / x = (x + (y - x)) / x"
   1.135      by simp
   1.136 -  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
   1.137 +  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
   1.138    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
   1.139      apply (rule mult_left_mono)
   1.140      apply (rule ln_add_one_self_le_self)
   1.141      apply (rule divide_nonneg_pos)
   1.142 -    apply (insert prems a, simp_all) 
   1.143 +    using x a apply simp_all
   1.144      done
   1.145    also have "... = y - x" using a by simp
   1.146    also have "... = (y - x) * ln (exp 1)" by simp
   1.147 @@ -375,16 +375,16 @@
   1.148      apply (subst ln_le_cancel_iff)
   1.149      apply force
   1.150      apply (rule a)
   1.151 -    apply (rule prems)
   1.152 -    apply (insert prems, simp)
   1.153 +    apply (rule x)
   1.154 +    using x apply simp
   1.155      done
   1.156    also have "... = y * ln x - x * ln x"
   1.157      by (rule left_diff_distrib)
   1.158    finally have "x * ln y <= y * ln x"
   1.159      by arith
   1.160 -  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
   1.161 -  also have "... = y * (ln x / x)"  by simp
   1.162 -  finally show ?thesis using b by(simp add:field_simps)
   1.163 +  then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
   1.164 +  also have "... = y * (ln x / x)" by simp
   1.165 +  finally show ?thesis using b by (simp add: field_simps)
   1.166  qed
   1.167  
   1.168  end