--- a/src/HOL/Deriv.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Deriv.thy Wed Apr 09 09:37:47 2014 +0200
@@ -825,7 +825,7 @@
lemma DERIV_mirror:
"(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
- by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right divide_minus_right
+ by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
text {* Caratheodory formulation of derivative at a point *}
@@ -908,8 +908,8 @@
fix h::real
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq divide_minus_right split add: split_if_asm)
- assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
+ proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l
have "0 < (f (x-h) - f x) / h" by arith
thus "f x < f (x-h)"
@@ -1628,8 +1628,7 @@
((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
((\<lambda> x. f x / g x) ---> y) (at_left x)"
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
- by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"])
- (auto simp: DERIV_mirror divide_minus_left divide_minus_right)
+ by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
lemma lhopital:
"((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
@@ -1740,8 +1739,7 @@
((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
((\<lambda> x. f x / g x) ---> y) (at_left x)"
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
- by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"])
- (auto simp: divide_minus_left divide_minus_right DERIV_mirror)
+ by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
lemma lhopital_at_top:
"LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
@@ -1798,7 +1796,7 @@
unfolding filterlim_at_right_to_top
apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
using eventually_ge_at_top[where c="1::real"]
- by eventually_elim (simp add: divide_minus_left divide_minus_right)
+ by eventually_elim simp
qed
end