diff -r 5b11f36fcacb -r 257ac9da021f src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Sep 06 08:00:28 2011 -0700 +++ b/src/HOL/Transcendental.thy Tue Sep 06 09:56:09 2011 -0700 @@ -1065,22 +1065,24 @@ using exp_inj_iff [where x=x and y=0] by simp lemma lemma_exp_total: "1 \ y ==> \x. 0 \ x & x \ y - 1 & exp(x::real) = y" -apply (rule IVT) -apply (auto intro: isCont_exp simp add: le_diff_eq) -apply (subgoal_tac "1 + (y - 1) \ exp (y - 1)") -apply simp -apply (rule exp_ge_add_one_self_aux, simp) -done +proof (rule IVT) + assume "1 \ y" + hence "0 \ y - 1" by simp + hence "1 + (y - 1) \ exp (y - 1)" by (rule exp_ge_add_one_self_aux) + thus "y \ exp (y - 1)" by simp +qed (simp_all add: le_diff_eq) lemma exp_total: "0 < (y::real) ==> \x. exp x = y" -apply (rule_tac x = 1 and y = y in linorder_cases) -apply (drule order_less_imp_le [THEN lemma_exp_total]) -apply (rule_tac [2] x = 0 in exI) -apply (frule_tac [3] one_less_inverse) -apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto) -apply (rule_tac x = "-x" in exI) -apply (simp add: exp_minus) -done +proof (rule linorder_le_cases [of 1 y]) + assume "1 \ y" thus "\x. exp x = y" + by (fast dest: lemma_exp_total) +next + assume "0 < y" and "y \ 1" + hence "1 \ inverse y" by (simp add: one_le_inverse_iff) + then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total) + hence "exp (- x) = y" by (simp add: exp_minus) + thus "\x. exp x = y" .. +qed subsection {* Natural Logarithm *}