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.16 -    proof (simp add: abs_if pos_less_divide_eq divide_minus_right split add: split_if_asm)
    1.17 -      assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
    1.18 +    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
    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