src/HOL/Deriv.thy
 changeset 56479 91958d4b30f7 parent 56409 36489d77c484 child 56480 093ea91498e6
```     1.1 --- a/src/HOL/Deriv.thy	Tue Apr 08 23:16:00 2014 +0200
1.2 +++ b/src/HOL/Deriv.thy	Wed Apr 09 09:37:47 2014 +0200
1.3 @@ -825,7 +825,7 @@
1.4
1.5  lemma DERIV_mirror:
1.6    "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
1.7 -  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right divide_minus_right
1.8 +  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
1.9                  tendsto_minus_cancel_left field_simps conj_commute)
1.10
1.11  text {* Caratheodory formulation of derivative at a point *}
1.12 @@ -908,8 +908,8 @@
1.13      fix h::real
1.14      assume "0 < h" "h < s"
1.15      with all [of "-h"] show "f x < f (x-h)"
1.17 -      assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
1.19 +      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
1.20        with l
1.21        have "0 < (f (x-h) - f x) / h" by arith
1.22        thus "f x < f (x-h)"
1.23 @@ -1628,8 +1628,7 @@
1.24      ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
1.25    ((\<lambda> x. f x / g x) ---> y) (at_left x)"
1.26    unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
1.27 -  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"])
1.28 -     (auto simp: DERIV_mirror divide_minus_left divide_minus_right)
1.29 +  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
1.30
1.31  lemma lhopital:
1.32    "((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
1.33 @@ -1740,8 +1739,7 @@
1.34      ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
1.35      ((\<lambda> x. f x / g x) ---> y) (at_left x)"
1.36    unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
1.37 -  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"])
1.38 -     (auto simp: divide_minus_left divide_minus_right DERIV_mirror)
1.39 +  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
1.40
1.41  lemma lhopital_at_top:
1.42    "LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
1.43 @@ -1798,7 +1796,7 @@
1.44      unfolding filterlim_at_right_to_top
1.45      apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
1.46      using eventually_ge_at_top[where c="1::real"]
1.47 -    by eventually_elim (simp add: divide_minus_left divide_minus_right)
1.48 +    by eventually_elim simp
1.49  qed
1.50
1.51  end
```