# HG changeset patch
# User huffman
# Date 1159409023 -7200
# Node ID 956a0377a408e3ccd86206a133af6127fc482ab0
# Parent  9c053a494dc6852b6a52ac36f6e96a289c640db8
reorganize sections

diff -r 9c053a494dc6 -r 956a0377a408 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 02:50:07 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 04:03:43 2006 +0200
@@ -73,8 +73,9 @@
                             else (x, (x+y)/2))"
 
 
+subsection {* Limits of Functions *}
 
-subsection{*Some Purely Standard Proofs*}
+subsubsection {* Purely standard proofs *}
 
 lemma LIM_eq:
      "f -- a --> L =
@@ -141,7 +142,6 @@
     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
 by (simp only: diff_minus LIM_add LIM_minus)
 
-
 lemma LIM_const_not_eq:
   fixes a :: "'a::real_normed_div_algebra"
   shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
@@ -211,8 +211,7 @@
 apply (auto simp add: add_assoc)
 done
 
-
-subsection{*Relationships Between Standard and Nonstandard Concepts*}
+subsubsection {* Purely nonstandard proofs *}
 
 lemma NSLIM_I:
   "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
@@ -224,6 +223,92 @@
    \<Longrightarrow> starfun f x \<approx> star_of L"
 by (simp add: NSLIM_def)
 
+text{*Proving properties of limits using nonstandard definition.
+      The properties hold for standard limits as well!*}
+
+lemma NSLIM_mult:
+  fixes l m :: "'a::real_normed_algebra"
+  shows "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
+by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
+
+lemma NSLIM_add:
+     "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
+by (auto simp add: NSLIM_def intro!: approx_add)
+
+lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
+by (simp add: NSLIM_def)
+
+lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
+by (simp add: NSLIM_def)
+
+lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
+by (simp only: NSLIM_add NSLIM_minus)
+
+lemma NSLIM_inverse:
+  fixes L :: "'a::real_normed_div_algebra"
+  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
+      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
+apply (simp add: NSLIM_def, clarify)
+apply (drule spec)
+apply (auto simp add: star_of_approx_inverse)
+done
+
+lemma NSLIM_zero:
+  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
+proof -
+  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
+    by (rule NSLIM_add_minus [OF f NSLIM_const])
+  thus ?thesis by simp
+qed
+
+lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
+apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
+apply (auto simp add: diff_minus add_assoc)
+done
+
+lemma NSLIM_const_not_eq:
+  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
+  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
+apply (simp add: NSLIM_def)
+apply (rule_tac x="star_of a + epsilon" in exI)
+apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
+            simp add: hypreal_epsilon_not_zero)
+done
+
+lemma NSLIM_not_zero:
+  fixes a :: real
+  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
+by (rule NSLIM_const_not_eq)
+
+lemma NSLIM_const_eq:
+  fixes a :: real
+  shows "(%x. k) -- a --NS> L ==> k = L"
+apply (rule ccontr)
+apply (blast dest: NSLIM_const_not_eq)
+done
+
+text{* can actually be proved more easily by unfolding the definition!*}
+lemma NSLIM_unique:
+  fixes a :: real
+  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
+apply (drule NSLIM_minus)
+apply (drule NSLIM_add, assumption)
+apply (auto dest!: NSLIM_const_eq [symmetric])
+apply (simp add: diff_def [symmetric])
+done
+
+lemma NSLIM_mult_zero:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+by (drule NSLIM_mult, auto)
+
+lemma NSLIM_self: "(%x. x) -- a --NS> a"
+by (simp add: NSLIM_def)
+
+subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
+
 lemma LIM_NSLIM:
   assumes f: "f -- a --> L" shows "f -- a --NS> L"
 proof (rule NSLIM_I)
@@ -282,14 +367,7 @@
 theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
 by (blast intro: LIM_NSLIM NSLIM_LIM)
 
-text{*Proving properties of limits using nonstandard definition.
-      The properties hold for standard limits as well!*}
-
-lemma NSLIM_mult:
-  fixes l m :: "'a::real_normed_algebra"
-  shows "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
-by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
+subsubsection {* Derived theorems about @{term LIM} *}
 
 lemma LIM_mult2:
   fixes l m :: "'a::real_normed_algebra"
@@ -297,115 +375,38 @@
       ==> (%x. f(x) * g(x)) -- x --> (l * m)"
 by (simp add: LIM_NSLIM_iff NSLIM_mult)
 
-lemma NSLIM_add:
-     "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
-by (auto simp add: NSLIM_def intro!: approx_add)
-
 lemma LIM_add2:
      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
 by (simp add: LIM_NSLIM_iff NSLIM_add)
 
-
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
-by (simp add: NSLIM_def)
-
 lemma LIM_const2: "(%x. k) -- x --> k"
 by (simp add: LIM_NSLIM_iff)
 
-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
-by (simp add: NSLIM_def)
-
 lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
 by (simp add: LIM_NSLIM_iff NSLIM_minus)
 
-
-lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
-by (blast dest: NSLIM_add NSLIM_minus)
-
 lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
 by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
 
-
-lemma NSLIM_inverse:
-  fixes L :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
-      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
-apply (simp add: NSLIM_def, clarify)
-apply (drule spec)
-apply (auto simp add: star_of_approx_inverse)
-done
-
 lemma LIM_inverse:
   fixes L :: "'a::real_normed_div_algebra"
   shows "[| f -- a --> L; L \<noteq> 0 |]
       ==> (%x. inverse(f(x))) -- a --> (inverse L)"
 by (simp add: LIM_NSLIM_iff NSLIM_inverse)
 
-
-lemma NSLIM_zero:
-  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
-proof -
-  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
-    by (rule NSLIM_add_minus [OF f NSLIM_const])
-  thus ?thesis by simp
-qed
-
 lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
 by (simp add: LIM_NSLIM_iff NSLIM_zero)
 
-lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
-apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
-apply (auto simp add: diff_minus add_assoc)
-done
-
 lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
 apply (drule_tac g = "%x. l" and M = l in LIM_add)
 apply (auto simp add: diff_minus add_assoc)
 done
 
-lemma NSLIM_const_not_eq:
-  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
-  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
-apply (simp add: NSLIM_def)
-apply (rule_tac x="star_of a + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
-            simp add: hypreal_epsilon_not_zero)
-done
-
-lemma NSLIM_not_zero:
-  fixes a :: real
-  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
-by (rule NSLIM_const_not_eq)
-
-lemma NSLIM_const_eq:
-  fixes a :: real
-  shows "(%x. k) -- a --NS> L ==> k = L"
-apply (rule ccontr)
-apply (blast dest: NSLIM_const_not_eq)
-done
-
-text{* can actually be proved more easily by unfolding the definition!*}
-lemma NSLIM_unique:
-  fixes a :: real
-  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
-apply (drule NSLIM_minus)
-apply (drule NSLIM_add, assumption)
-apply (auto dest!: NSLIM_const_eq [symmetric])
-apply (simp add: diff_def [symmetric])
-done
-
 lemma LIM_unique2:
   fixes a :: real
   shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
 by (simp add: LIM_NSLIM_iff NSLIM_unique)
 
-
-lemma NSLIM_mult_zero:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
-by (drule NSLIM_mult, auto)
-
 (* we can use the corresponding thm LIM_mult2 *)
 (* for standard definition of limit           *)
 
@@ -415,13 +416,7 @@
 by (drule LIM_mult2, auto)
 
 
-lemma NSLIM_self: "(%x. x) -- a --NS> a"
-by (simp add: NSLIM_def)
-
-
-subsection{* Derivatives and Continuity: NS and Standard properties*}
-
-subsubsection{*Continuity*}
+subsection {* Continuity *}
 
 lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
 by (simp add: isNSCont_def)
@@ -592,7 +587,8 @@
 qed "isCont_isopen_iff";
 *******************************************************************)
 
-text{*Uniform continuity*}
+subsection {* Uniform Continuity *}
+
 lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
 by (simp add: isNSUCont_def)
 
@@ -654,7 +650,8 @@
     by transfer
 qed
 
-text{*Derivatives*}
+subsection {* Derivatives *}
+
 lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
 by (simp add: deriv_def)
 
@@ -668,7 +665,6 @@
 lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
 by (simp add: deriv_def LIM_NSLIM_iff)
 
-
 subsubsection{*Uniqueness*}
 
 lemma DERIV_unique:
@@ -686,20 +682,6 @@
             dest: approx_trans3)
 done
 
-subsubsection{*Differentiable*}
-
-lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
-by (simp add: differentiable_def)
-
-lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
-by (force simp add: differentiable_def)
-
-lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
-by (simp add: NSdifferentiable_def)
-
-lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
-by (force simp add: NSdifferentiable_def)
-
 subsubsection{*Alternative definition for differentiability*}
 
 lemma DERIV_LIM_iff:
@@ -749,9 +731,9 @@
 by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
 
 
-subsection{*Equivalence of NS and standard definitions of differentiation*}
+subsubsection{*Equivalence of NS and standard definitions of differentiation*}
 
-subsubsection{*First NSDERIV in terms of NSLIM*}
+text {*First NSDERIV in terms of NSLIM*}
 
 text{*first equivalence *}
 lemma NSDERIV_NSLIM_iff:
@@ -850,6 +832,7 @@
 by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
               NSDERIV_isNSCont)
 
+subsubsection {* Derivatives of various functions *}
 
 text{*Differentiation rules for combinations of functions
       follow from clear, straightforard, algebraic
@@ -980,47 +963,6 @@
 apply (blast intro: DERIV_add_minus)
 done
 
-text{*(NS) Increment*}
-lemma incrementI:
-      "f NSdifferentiable x ==>
-      increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
-      hypreal_of_real (f x)"
-by (simp add: increment_def)
-
-lemma incrementI2: "NSDERIV f x :> D ==>
-     increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
-     hypreal_of_real (f x)"
-apply (erule NSdifferentiableI [THEN incrementI])
-done
-
-(* The Increment theorem -- Keisler p. 65 *)
-lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
-      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
-apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
-apply (drule bspec, auto)
-apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
-apply (frule_tac b1 = "hypreal_of_real (D) + y"
-        in hypreal_mult_right_cancel [THEN iffD2])
-apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
-apply assumption
-apply (simp add: times_divide_eq_right [symmetric])
-apply (auto simp add: left_distrib)
-done
-
-lemma increment_thm2:
-     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
-      ==> \<exists>e \<in> Infinitesimal. increment f x h =
-              hypreal_of_real(D)*h + e*h"
-by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
-
-
-lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
-      ==> increment f x h \<approx> 0"
-apply (drule increment_thm2,
-       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
-apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
-done
-
 text{*  Similarly to the above, the chain rule admits an entirely
    straightforward derivation. Compare this with Harrison's
    HOL proof of the chain rule, which proved to be trickier and
@@ -1245,6 +1187,114 @@
     by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
 qed
 
+subsubsection {* Differentiability predicate *}
+
+lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
+by (simp add: differentiable_def)
+
+lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
+by (force simp add: differentiable_def)
+
+lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
+by (simp add: NSdifferentiable_def)
+
+lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
+by (force simp add: NSdifferentiable_def)
+
+lemma differentiable_const: "(\<lambda>z. a) differentiable x"
+  apply (unfold differentiable_def)
+  apply (rule_tac x=0 in exI)
+  apply simp
+  done
+
+lemma differentiable_sum:
+  assumes "f differentiable x"
+  and "g differentiable x"
+  shows "(\<lambda>x. f x + g x) differentiable x"
+proof -
+  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+  then obtain df where "DERIV f x :> df" ..
+  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
+  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
+  thus ?thesis by (fold differentiable_def)
+qed
+
+lemma differentiable_diff:
+  assumes "f differentiable x"
+  and "g differentiable x"
+  shows "(\<lambda>x. f x - g x) differentiable x"
+proof -
+  from prems have "f differentiable x" by simp
+  moreover
+  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
+  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
+  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
+  ultimately 
+  show ?thesis
+    by (auto simp: real_diff_def dest: differentiable_sum)
+qed
+
+lemma differentiable_mult:
+  assumes "f differentiable x"
+  and "g differentiable x"
+  shows "(\<lambda>x. f x * g x) differentiable x"
+proof -
+  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+  then obtain df where "DERIV f x :> df" ..
+  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
+  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
+  thus ?thesis by (fold differentiable_def)
+qed
+
+subsection {*(NS) Increment*}
+lemma incrementI:
+      "f NSdifferentiable x ==>
+      increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
+      hypreal_of_real (f x)"
+by (simp add: increment_def)
+
+lemma incrementI2: "NSDERIV f x :> D ==>
+     increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
+     hypreal_of_real (f x)"
+apply (erule NSdifferentiableI [THEN incrementI])
+done
+
+(* The Increment theorem -- Keisler p. 65 *)
+lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
+      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
+apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
+apply (drule bspec, auto)
+apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
+apply (frule_tac b1 = "hypreal_of_real (D) + y"
+        in hypreal_mult_right_cancel [THEN iffD2])
+apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
+apply assumption
+apply (simp add: times_divide_eq_right [symmetric])
+apply (auto simp add: left_distrib)
+done
+
+lemma increment_thm2:
+     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
+      ==> \<exists>e \<in> Infinitesimal. increment f x h =
+              hypreal_of_real(D)*h + e*h"
+by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
+
+
+lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
+      ==> increment f x h \<approx> 0"
+apply (drule increment_thm2,
+       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
+apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
+done
+
+subsection {* Nested Intervals and Bisection *}
+
 text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
      All considerably tidied by lcp.*}
 
@@ -1436,7 +1486,9 @@
 done
 
 
-subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
+subsection {* Intermediate Value Theorem *}
+
+text {*Prove Contrapositive by Bisection*}
 
 lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
          a \<le> b;
@@ -1487,7 +1539,7 @@
 apply (blast intro: IVT2)
 done
 
-subsection{*By bisection, function continuous on closed interval is bounded above*}
+text{*By bisection, function continuous on closed interval is bounded above*}
 
 lemma isCont_bounded:
      "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
@@ -1605,7 +1657,7 @@
 done
 
 
-subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
+text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
 
 lemma DERIV_left_inc:
   assumes der: "DERIV f x :> l"
@@ -2089,59 +2141,6 @@
   qed
 qed
 
-
-lemma differentiable_const: "(\<lambda>z. a) differentiable x"
-  apply (unfold differentiable_def)
-  apply (rule_tac x=0 in exI)
-  apply simp
-  done
-
-lemma differentiable_sum:
-  assumes "f differentiable x"
-  and "g differentiable x"
-  shows "(\<lambda>x. f x + g x) differentiable x"
-proof -
-  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
-  then obtain df where "DERIV f x :> df" ..
-  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
-  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
-  thus ?thesis by (fold differentiable_def)
-qed
-
-lemma differentiable_diff:
-  assumes "f differentiable x"
-  and "g differentiable x"
-  shows "(\<lambda>x. f x - g x) differentiable x"
-proof -
-  from prems have "f differentiable x" by simp
-  moreover
-  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
-  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
-  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
-  ultimately 
-  show ?thesis
-    by (auto simp: real_diff_def dest: differentiable_sum)
-qed
-
-lemma differentiable_mult:
-  assumes "f differentiable x"
-  and "g differentiable x"
-  shows "(\<lambda>x. f x * g x) differentiable x"
-proof -
-  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
-  then obtain df where "DERIV f x :> df" ..
-  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
-  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
-  thus ?thesis by (fold differentiable_def)
-qed
-
-
 theorem GMVT:
   assumes alb: "a < b"
   and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"