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.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.34 -    apply (insert prems, auto)
1.35 +    using a apply auto
1.36      apply (rule mult_pos_pos)
1.37      apply auto
1.39      apply auto
1.40      done
1.41    also from a have "... <= 1 + x"
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.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.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.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.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.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.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.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
```