--- a/src/HOL/Deriv.thy Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Deriv.thy Tue Sep 03 22:04:23 2013 +0200
@@ -1319,7 +1319,8 @@
and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
- shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
+ shows "\<exists>g'c f'c c.
+ DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
proof -
let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
from assms have "a < b" by simp
@@ -1466,7 +1467,7 @@
ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
qed
- then guess \<zeta> ..
+ then obtain \<zeta> where "\<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)" ..
then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
moreover
@@ -1582,9 +1583,10 @@
have "\<exists>y. t < y \<and> y < a \<and> (g a - g t) * f' y = (f a - f t) * g' y"
using f0 g0 t(1,2) by (intro GMVT') (force intro!: DERIV_isCont)+
- then guess y ..
- from this
- have [arith]: "t < y" "y < a" and D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
+ then obtain y where [arith]: "t < y" "y < a"
+ and D_eq0: "(g a - g t) * f' y = (f a - f t) * g' y"
+ by blast
+ from D_eq0 have D_eq: "(f t - f a) / (g t - g a) = f' y / g' y"
using `g a < g t` g'_neq_0[of y] by (auto simp add: field_simps)
have *: "f t / g t - x = ((f t - f a) / (g t - g a) - x) * (1 - g a / g t) + (f a - x * g a) / g t"