# HG changeset patch # User hoelzl # Date 1354555148 -3600 # Node ID 25b1e8686ce076102d51bee674eec9556fd29186 # Parent bbea2e82871c889a598c76503324aed87039203d tuned proof diff -r bbea2e82871c -r 25b1e8686ce0 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Mon Dec 03 18:19:07 2012 +0100 +++ b/src/HOL/Deriv.thy Mon Dec 03 18:19:08 2012 +0100 @@ -1627,35 +1627,18 @@ and g: "\x. 0 < x \ x < a \ DERIV g x :> (g' x)" unfolding eventually_within eventually_at by (auto simp: dist_real_def) - { fix x assume x: "0 \ x" "x < a" - from `0 \ x` have "isCont f x" - unfolding le_less - proof - assume "0 = x" with `isCont f 0` show "isCont f x" by simp - next - assume "0 < x" with f x show ?thesis by (auto intro!: DERIV_isCont) - qed } - note isCont_f = this - - { fix x assume x: "0 \ x" "x < a" - from `0 \ x` have "isCont g x" - unfolding le_less - proof - assume "0 = x" with `isCont g 0` show "isCont g x" by simp - next - assume "0 < x" with g x show ?thesis by (auto intro!: DERIV_isCont) - qed } - note isCont_g = this - have "\\. \x\{0 <..< a}. 0 < \ x \ \ x < x \ f x / g x = f' (\ x) / g' (\ x)" proof (rule bchoice, rule) fix x assume "x \ {0 <..< a}" then have x[arith]: "0 < x" "x < a" by auto with g'_neq_0 g_neq_0 `g 0 = 0` have g': "\x. 0 < x \ x < a \ 0 \ g' x" "g 0 \ g x" by auto - - have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" - using isCont_f isCont_g f g `x < a` by (intro GMVT') auto + have "\x. 0 \ x \ x < a \ isCont f x" + using `isCont f 0` f by (auto intro: DERIV_isCont simp: le_less) + moreover have "\x. 0 \ x \ x < a \ isCont g x" + using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less) + ultimately have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" + using f g `x < a` by (intro GMVT') auto then guess c .. moreover with g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" @@ -1679,10 +1662,8 @@ from this lim have "((\t. f' (\ t) / g' (\ t)) ---> x) (at_right 0)" by (rule_tac filterlim_compose[of _ _ _ \]) ultimately show "((\t. f t / g t) ---> x) (at_right 0)" - apply (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) - apply (erule_tac eventually_elim1) - apply simp_all - done + by (rule_tac filterlim_cong[THEN iffD1, OF refl refl]) + (auto elim: eventually_elim1) qed lemma lhopital_right_0_at_top: @@ -1709,18 +1690,13 @@ unfolding eventually_within_le by (auto simp: dist_real_def) from Df have - "eventually (\t. t < a) (at_right 0)" - "eventually (\t::real. 0 < t) (at_right 0)" + "eventually (\t. t < a) (at_right 0)" "eventually (\t::real. 0 < t) (at_right 0)" unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def) - moreover - - have "eventually (\t. 0 < g t) (at_right 0)" - using g_0[unfolded filterlim_at_top, rule_format, of "1"] by eventually_elim auto moreover + have "eventually (\t. 0 < g t) (at_right 0)" "eventually (\t. g a < g t) (at_right 0)" + using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top) - have "eventually (\t. g a < g t) (at_right 0)" - using g_0[unfolded filterlim_at_top, rule_format, of "g a + 1"] by eventually_elim auto moreover have inv_g: "((\x. inverse (g x)) ---> 0) (at_right 0)" using tendsto_inverse_0 filterlim_mono[OF g_0 at_top_le_at_infinity order_refl]