src/HOL/Ln.thy
changeset 43336 05aa7380f7fc
parent 41959 b460124855b8
child 44289 d81d09cdab9c
     1.1 --- a/src/HOL/Ln.thy	Tue May 31 21:33:49 2011 +0200
     1.2 +++ b/src/HOL/Ln.thy	Thu Jun 09 11:50:16 2011 +0200
     1.3 @@ -387,4 +387,47 @@
     1.4    finally show ?thesis using b by (simp add: field_simps)
     1.5  qed
     1.6  
     1.7 +lemma ln_le_minus_one:
     1.8 +  "0 < x \<Longrightarrow> ln x \<le> x - 1"
     1.9 +  using exp_ge_add_one_self[of "ln x"] by simp
    1.10 +
    1.11 +lemma ln_eq_minus_one:
    1.12 +  assumes "0 < x" "ln x = x - 1" shows "x = 1"
    1.13 +proof -
    1.14 +  let "?l y" = "ln y - y + 1"
    1.15 +  have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
    1.16 +    by (auto intro!: DERIV_intros)
    1.17 +
    1.18 +  show ?thesis
    1.19 +  proof (cases rule: linorder_cases)
    1.20 +    assume "x < 1"
    1.21 +    from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
    1.22 +    from `x < a` have "?l x < ?l a"
    1.23 +    proof (rule DERIV_pos_imp_increasing, safe)
    1.24 +      fix y assume "x \<le> y" "y \<le> a"
    1.25 +      with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
    1.26 +        by (auto simp: field_simps)
    1.27 +      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
    1.28 +        by auto
    1.29 +    qed
    1.30 +    also have "\<dots> \<le> 0"
    1.31 +      using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
    1.32 +    finally show "x = 1" using assms by auto
    1.33 +  next
    1.34 +    assume "1 < x"
    1.35 +    from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast
    1.36 +    from `a < x` have "?l x < ?l a"
    1.37 +    proof (rule DERIV_neg_imp_decreasing, safe)
    1.38 +      fix y assume "a \<le> y" "y \<le> x"
    1.39 +      with `1 < a` have "1 / y - 1 < 0" "0 < y"
    1.40 +        by (auto simp: field_simps)
    1.41 +      with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
    1.42 +        by blast
    1.43 +    qed
    1.44 +    also have "\<dots> \<le> 0"
    1.45 +      using ln_le_minus_one `1 < a` by (auto simp: field_simps)
    1.46 +    finally show "x = 1" using assms by auto
    1.47 +  qed simp
    1.48 +qed
    1.49 +
    1.50  end