src/HOL/Transcendental.thy
changeset 44755 257ac9da021f
parent 44746 9e4f7d3b5376
child 44756 efcd71fbaeec
     1.1 --- a/src/HOL/Transcendental.thy	Tue Sep 06 08:00:28 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Sep 06 09:56:09 2011 -0700
     1.3 @@ -1065,22 +1065,24 @@
     1.4    using exp_inj_iff [where x=x and y=0] by simp
     1.5  
     1.6  lemma lemma_exp_total: "1 \<le> y ==> \<exists>x. 0 \<le> x & x \<le> y - 1 & exp(x::real) = y"
     1.7 -apply (rule IVT)
     1.8 -apply (auto intro: isCont_exp simp add: le_diff_eq)
     1.9 -apply (subgoal_tac "1 + (y - 1) \<le> exp (y - 1)")
    1.10 -apply simp
    1.11 -apply (rule exp_ge_add_one_self_aux, simp)
    1.12 -done
    1.13 +proof (rule IVT)
    1.14 +  assume "1 \<le> y"
    1.15 +  hence "0 \<le> y - 1" by simp
    1.16 +  hence "1 + (y - 1) \<le> exp (y - 1)" by (rule exp_ge_add_one_self_aux)
    1.17 +  thus "y \<le> exp (y - 1)" by simp
    1.18 +qed (simp_all add: le_diff_eq)
    1.19  
    1.20  lemma exp_total: "0 < (y::real) ==> \<exists>x. exp x = y"
    1.21 -apply (rule_tac x = 1 and y = y in linorder_cases)
    1.22 -apply (drule order_less_imp_le [THEN lemma_exp_total])
    1.23 -apply (rule_tac [2] x = 0 in exI)
    1.24 -apply (frule_tac [3] one_less_inverse)
    1.25 -apply (drule_tac [4] order_less_imp_le [THEN lemma_exp_total], auto)
    1.26 -apply (rule_tac x = "-x" in exI)
    1.27 -apply (simp add: exp_minus)
    1.28 -done
    1.29 +proof (rule linorder_le_cases [of 1 y])
    1.30 +  assume "1 \<le> y" thus "\<exists>x. exp x = y"
    1.31 +    by (fast dest: lemma_exp_total)
    1.32 +next
    1.33 +  assume "0 < y" and "y \<le> 1"
    1.34 +  hence "1 \<le> inverse y" by (simp add: one_le_inverse_iff)
    1.35 +  then obtain x where "exp x = inverse y" by (fast dest: lemma_exp_total)
    1.36 +  hence "exp (- x) = y" by (simp add: exp_minus)
    1.37 +  thus "\<exists>x. exp x = y" ..
    1.38 +qed
    1.39  
    1.40  
    1.41  subsection {* Natural Logarithm *}