1.1 --- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:07 2012 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:08 2012 +0100
     1.3 @@ -1627,35 +1627,18 @@
     1.4      and g: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g x :> (g' x)"
     1.5      unfolding eventually_within eventually_at by (auto simp: dist_real_def)
     1.6  
     1.7 -  { fix x assume x: "0 \<le> x" "x < a"
     1.8 -    from `0 \<le> x` have "isCont f x"
     1.9 -      unfolding le_less
    1.10 -    proof
    1.11 -      assume "0 = x" with `isCont f 0` show "isCont f x" by simp
    1.12 -    next
    1.13 -      assume "0 < x" with f x show ?thesis by (auto intro!: DERIV_isCont)
    1.14 -    qed }
    1.15 -  note isCont_f = this
    1.16 -
    1.17 -  { fix x assume x: "0 \<le> x" "x < a"
    1.18 -    from `0 \<le> x` have "isCont g x"
    1.19 -      unfolding le_less
    1.20 -    proof
    1.21 -      assume "0 = x" with `isCont g 0` show "isCont g x" by simp
    1.22 -    next
    1.23 -      assume "0 < x" with g x show ?thesis by (auto intro!: DERIV_isCont)
    1.24 -    qed }
    1.25 -  note isCont_g = this
    1.26 -
    1.27    have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)"
    1.28    proof (rule bchoice, rule)
    1.29      fix x assume "x \<in> {0 <..< a}"
    1.30      then have x[arith]: "0 < x" "x < a" by auto
    1.31      with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\<And>x. 0 < x \<Longrightarrow> x < a  \<Longrightarrow> 0 \<noteq> g' x" "g 0 \<noteq> g x"
    1.32        by auto
    1.33 -
    1.34 -    have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
    1.35 -      using isCont_f isCont_g f g `x < a` by (intro GMVT') auto
    1.36 +    have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont f x"
    1.37 +      using `isCont f 0` f by (auto intro: DERIV_isCont simp: le_less)
    1.38 +    moreover have "\<And>x. 0 \<le> x \<Longrightarrow> x < a \<Longrightarrow> isCont g x"
    1.39 +      using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less)
    1.40 +    ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
    1.41 +      using f g `x < a` by (intro GMVT') auto
    1.42      then guess c ..
    1.43      moreover
    1.44      with g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
    1.45 @@ -1679,10 +1662,8 @@
    1.46    from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
    1.47      by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
    1.48    ultimately show "((\<lambda>t. f t / g t) ---> x) (at_right 0)"
    1.49 -    apply (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
    1.50 -    apply (erule_tac eventually_elim1)
    1.51 -    apply simp_all
    1.52 -    done
    1.53 +    by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
    1.54 +       (auto elim: eventually_elim1)
    1.55  qed
    1.56  
    1.57  lemma lhopital_right_0_at_top:
    1.58 @@ -1709,18 +1690,13 @@
    1.59      unfolding eventually_within_le by (auto simp: dist_real_def)
    1.60  
    1.61    from Df have
    1.62 -    "eventually (\<lambda>t. t < a) (at_right 0)"
    1.63 -    "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
    1.64 +    "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
    1.65      unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
    1.66 -  moreover
    1.67 -
    1.68 -  have "eventually (\<lambda>t. 0 < g t) (at_right 0)"
    1.69 -    using g_0[unfolded filterlim_at_top, rule_format, of "1"] by eventually_elim auto
    1.70  
    1.71    moreover
    1.72 +  have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
    1.73 +    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top)
    1.74  
    1.75 -  have "eventually (\<lambda>t. g a < g t) (at_right 0)"
    1.76 -    using g_0[unfolded filterlim_at_top, rule_format, of "g a + 1"] by eventually_elim auto
    1.77    moreover
    1.78    have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
    1.79      using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl]