src/HOL/Ln.thy
 changeset 44289 d81d09cdab9c parent 43336 05aa7380f7fc child 44305 3bdc02eb1637
```     1.1 --- a/src/HOL/Ln.thy	Thu Aug 18 18:10:23 2011 -0700
1.2 +++ b/src/HOL/Ln.thy	Thu Aug 18 19:53:03 2011 -0700
1.3 @@ -18,7 +18,7 @@
1.4        inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
1.5      by (rule suminf_split_initial_segment)
1.6    also have "?a = 1 + x"
1.7 -    by (simp add: numerals)
1.8 +    by (simp add: numeral_2_eq_2)
1.9    finally show ?thesis .
1.10  qed
1.11
1.12 @@ -70,13 +70,7 @@
1.13        finally show ?thesis .
1.14      qed
1.15      moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
1.16 -      apply (simp add: mult_compare_simps)
1.17 -      apply (simp add: assms)
1.18 -      apply (subgoal_tac "0 <= x * (x * x^n)")
1.19 -      apply force
1.20 -      apply (rule mult_nonneg_nonneg, rule a)+
1.21 -      apply (rule zero_le_power, rule a)
1.22 -      done
1.23 +      by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b)
1.24      ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
1.25          (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
1.26        apply (rule mult_mono)
1.27 @@ -162,7 +156,7 @@
1.28      apply auto
1.29      done
1.30    also from a have "... <= 1 + x"
1.31 -    by (simp add: field_simps zero_compare_simps)
1.33    finally show ?thesis .
1.34  qed
1.35
1.36 @@ -344,24 +338,17 @@
1.37  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
1.38  proof -
1.39    assume x: "exp 1 <= x" "x <= y"
1.40 -  have a: "0 < x" and b: "0 < y"
1.41 -    apply (insert x)
1.42 -    apply (subgoal_tac "0 < exp (1::real)")
1.43 -    apply arith
1.44 -    apply auto
1.45 -    apply (subgoal_tac "0 < exp (1::real)")
1.46 -    apply arith
1.47 -    apply auto
1.48 -    done
1.49 +  moreover have "0 < exp (1::real)" by simp
1.50 +  ultimately have a: "0 < x" and b: "0 < y"
1.51 +    by (fast intro: less_le_trans order_trans)+
1.52    have "x * ln y - x * ln x = x * (ln y - ln x)"
1.54    also have "... = x * ln(y / x)"
1.55 -    apply (subst ln_div)
1.56 -    apply (rule b, rule a, rule refl)
1.57 -    done
1.58 +    by (simp only: ln_div a b)
1.59    also have "y / x = (x + (y - x)) / x"
1.60      by simp
1.61 -  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
1.62 +  also have "... = 1 + (y - x) / x"
1.63 +    using x a by (simp add: field_simps)
1.64    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
1.65      apply (rule mult_left_mono)