--- a/src/HOL/Deriv.thy Wed Feb 18 07:24:13 2009 -0800
+++ b/src/HOL/Deriv.thy Wed Feb 18 09:07:36 2009 -0800
@@ -217,9 +217,7 @@
by (cases "n", simp, simp add: DERIV_power_Suc f)
-(* ------------------------------------------------------------------------ *)
-(* Caratheodory formulation of derivative at a point: standard proof *)
-(* ------------------------------------------------------------------------ *)
+text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
"(DERIV f x :> l) =
@@ -307,6 +305,9 @@
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
+lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
+by auto
+
subsection {* Differentiability predicate *}
@@ -655,6 +656,9 @@
apply (blast intro: IVT2)
done
+
+subsection {* Boundedness of continuous functions *}
+
text{*By bisection, function continuous on closed interval is bounded above*}
lemma isCont_bounded:
@@ -773,6 +777,8 @@
done
+subsection {* Local extrema *}
+
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
lemma DERIV_left_inc:
@@ -877,6 +883,9 @@
shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
by (auto dest!: DERIV_local_max)
+
+subsection {* Rolle's Theorem *}
+
text{*Lemma about introducing open ball in open interval*}
lemma lemma_interval_lt:
"[| a < x; x < b |]
@@ -1163,6 +1172,8 @@
qed
+subsection {* Continuous injective functions *}
+
text{*Dull lemma: an continuous injection on an interval must have a
strict maximum at an end point, not in the middle.*}
@@ -1356,6 +1367,9 @@
using neq by (rule LIM_inverse)
qed
+
+subsection {* Generalized Mean Value Theorem *}
+
theorem GMVT:
fixes a b :: real
assumes alb: "a < b"
@@ -1442,9 +1456,6 @@
with g'cdef f'cdef cint show ?thesis by auto
qed
-lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
subsection {* Derivatives of univariate polynomials *}