merged

--- a/src/HOL/Deriv.thy	Wed Feb 18 13:39:16 2009 +0100
+++ b/src/HOL/Deriv.thy	Wed Feb 18 09:08:04 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 *}
 

--- a/src/HOL/ex/ThreeDivides.thy	Wed Feb 18 13:39:16 2009 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Wed Feb 18 09:08:04 2009 -0800
@@ -187,9 +187,8 @@
     "nd = nlen (m div 10) \<Longrightarrow>
     m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
     by blast
-  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
-  then obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
-  then have cdef: "c = m mod 10" by arith
+  obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
+    and cdef: "c = m mod 10" by simp
   show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
   proof -
     from `Suc nd = nlen m`