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.32 +    by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
    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.53      by (simp add: algebra_simps)
    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)
    1.66      apply (rule ln_add_one_self_le_self)
    1.67 @@ -373,7 +360,7 @@
    1.68    also have "... <= (y - x) * ln x"
    1.69      apply (rule mult_left_mono)
    1.70      apply (subst ln_le_cancel_iff)
    1.71 -    apply force
    1.72 +    apply fact
    1.73      apply (rule a)
    1.74      apply (rule x)
    1.75      using x apply simp