use DERIV_intros
authorhoelzl
Tue Dec 21 15:00:59 2010 +0100 (2010-12-21)
changeset 413688afa26855137
parent 41367 1b65137d598c
child 41369 177f91b9f8e7
use DERIV_intros
src/HOL/Deriv.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Dec 21 14:50:53 2010 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Tue Dec 21 15:00:59 2010 +0100
     1.3 @@ -879,14 +879,14 @@
     1.4    fixes f :: "real => real"
     1.5    shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
     1.6    apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
     1.7 -  apply (auto simp add: DERIV_minus) 
     1.8 +  apply (auto simp add: DERIV_minus)
     1.9    done
    1.10  
    1.11  lemma DERIV_neg_dec_right:
    1.12    fixes f :: "real => real"
    1.13    shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
    1.14    apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
    1.15 -  apply (auto simp add: DERIV_minus) 
    1.16 +  apply (auto simp add: DERIV_minus)
    1.17    done
    1.18  
    1.19  lemma DERIV_local_max:
    1.20 @@ -1554,21 +1554,8 @@
    1.21    then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
    1.22  
    1.23    from cdef have "DERIV ?h c :> l" by auto
    1.24 -  moreover
    1.25 -  {
    1.26 -    have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
    1.27 -      apply (insert DERIV_const [where k="f b - f a"])
    1.28 -      apply (drule meta_spec [of _ c])
    1.29 -      apply (drule DERIV_mult [OF _ g'cdef])
    1.30 -      by simp
    1.31 -    moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
    1.32 -      apply (insert DERIV_const [where k="g b - g a"])
    1.33 -      apply (drule meta_spec [of _ c])
    1.34 -      apply (drule DERIV_mult [OF _ f'cdef])
    1.35 -      by simp
    1.36 -    ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
    1.37 -      by (simp add: DERIV_diff)
    1.38 -  }
    1.39 +  moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
    1.40 +    using g'cdef f'cdef by (auto intro!: DERIV_intros)
    1.41    ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
    1.42  
    1.43    {