src/HOL/Deriv.thy
 changeset 29975 28c5322f0df3 parent 29803 c56a5571f60a child 29982 6ec97eba1ee3
```     1.1 --- a/src/HOL/Deriv.thy	Wed Feb 18 07:24:13 2009 -0800
1.2 +++ b/src/HOL/Deriv.thy	Wed Feb 18 09:07:36 2009 -0800
1.3 @@ -217,9 +217,7 @@
1.4  by (cases "n", simp, simp add: DERIV_power_Suc f)
1.5
1.6
1.7 -(* ------------------------------------------------------------------------ *)
1.8 -(* Caratheodory formulation of derivative at a point: standard proof        *)
1.9 -(* ------------------------------------------------------------------------ *)
1.10 +text {* Caratheodory formulation of derivative at a point *}
1.11
1.12  lemma CARAT_DERIV:
1.13       "(DERIV f x :> l) =
1.14 @@ -307,6 +305,9 @@
1.15         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
1.16  by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
1.17
1.18 +lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
1.19 +by auto
1.20 +
1.21
1.22  subsection {* Differentiability predicate *}
1.23
1.24 @@ -655,6 +656,9 @@
1.25  apply (blast intro: IVT2)
1.26  done
1.27
1.28 +
1.29 +subsection {* Boundedness of continuous functions *}
1.30 +
1.31  text{*By bisection, function continuous on closed interval is bounded above*}
1.32
1.33  lemma isCont_bounded:
1.34 @@ -773,6 +777,8 @@
1.35  done
1.36
1.37
1.38 +subsection {* Local extrema *}
1.39 +
1.40  text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
1.41
1.42  lemma DERIV_left_inc:
1.43 @@ -877,6 +883,9 @@
1.44    shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
1.45  by (auto dest!: DERIV_local_max)
1.46
1.47 +
1.48 +subsection {* Rolle's Theorem *}
1.49 +
1.50  text{*Lemma about introducing open ball in open interval*}
1.51  lemma lemma_interval_lt:
1.52       "[| a < x;  x < b |]
1.53 @@ -1163,6 +1172,8 @@
1.54  qed
1.55
1.56
1.57 +subsection {* Continuous injective functions *}
1.58 +
1.59  text{*Dull lemma: an continuous injection on an interval must have a
1.60  strict maximum at an end point, not in the middle.*}
1.61
1.62 @@ -1356,6 +1367,9 @@
1.63      using neq by (rule LIM_inverse)
1.64  qed
1.65
1.66 +
1.67 +subsection {* Generalized Mean Value Theorem *}
1.68 +
1.69  theorem GMVT:
1.70    fixes a b :: real
1.71    assumes alb: "a < b"
1.72 @@ -1442,9 +1456,6 @@
1.73    with g'cdef f'cdef cint show ?thesis by auto
1.74  qed
1.75
1.76 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
1.77 -by auto
1.78 -
1.79
1.80  subsection {* Derivatives of univariate polynomials *}
1.81
```