reorganize sections
authorhuffman
Thu Sep 28 04:03:43 2006 +0200 (2006-09-28)
changeset 20755956a0377a408
parent 20754 9c053a494dc6
child 20756 fec7f5834ffe
reorganize sections
src/HOL/Hyperreal/Lim.thy
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 02:50:07 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 04:03:43 2006 +0200
     1.3 @@ -73,8 +73,9 @@
     1.4                              else (x, (x+y)/2))"
     1.5  
     1.6  
     1.7 +subsection {* Limits of Functions *}
     1.8  
     1.9 -subsection{*Some Purely Standard Proofs*}
    1.10 +subsubsection {* Purely standard proofs *}
    1.11  
    1.12  lemma LIM_eq:
    1.13       "f -- a --> L =
    1.14 @@ -141,7 +142,6 @@
    1.15      "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
    1.16  by (simp only: diff_minus LIM_add LIM_minus)
    1.17  
    1.18 -
    1.19  lemma LIM_const_not_eq:
    1.20    fixes a :: "'a::real_normed_div_algebra"
    1.21    shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
    1.22 @@ -211,8 +211,7 @@
    1.23  apply (auto simp add: add_assoc)
    1.24  done
    1.25  
    1.26 -
    1.27 -subsection{*Relationships Between Standard and Nonstandard Concepts*}
    1.28 +subsubsection {* Purely nonstandard proofs *}
    1.29  
    1.30  lemma NSLIM_I:
    1.31    "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
    1.32 @@ -224,6 +223,92 @@
    1.33     \<Longrightarrow> starfun f x \<approx> star_of L"
    1.34  by (simp add: NSLIM_def)
    1.35  
    1.36 +text{*Proving properties of limits using nonstandard definition.
    1.37 +      The properties hold for standard limits as well!*}
    1.38 +
    1.39 +lemma NSLIM_mult:
    1.40 +  fixes l m :: "'a::real_normed_algebra"
    1.41 +  shows "[| f -- x --NS> l; g -- x --NS> m |]
    1.42 +      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
    1.43 +by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
    1.44 +
    1.45 +lemma NSLIM_add:
    1.46 +     "[| f -- x --NS> l; g -- x --NS> m |]
    1.47 +      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
    1.48 +by (auto simp add: NSLIM_def intro!: approx_add)
    1.49 +
    1.50 +lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
    1.51 +by (simp add: NSLIM_def)
    1.52 +
    1.53 +lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
    1.54 +by (simp add: NSLIM_def)
    1.55 +
    1.56 +lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
    1.57 +by (simp only: NSLIM_add NSLIM_minus)
    1.58 +
    1.59 +lemma NSLIM_inverse:
    1.60 +  fixes L :: "'a::real_normed_div_algebra"
    1.61 +  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
    1.62 +      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
    1.63 +apply (simp add: NSLIM_def, clarify)
    1.64 +apply (drule spec)
    1.65 +apply (auto simp add: star_of_approx_inverse)
    1.66 +done
    1.67 +
    1.68 +lemma NSLIM_zero:
    1.69 +  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
    1.70 +proof -
    1.71 +  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
    1.72 +    by (rule NSLIM_add_minus [OF f NSLIM_const])
    1.73 +  thus ?thesis by simp
    1.74 +qed
    1.75 +
    1.76 +lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
    1.77 +apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
    1.78 +apply (auto simp add: diff_minus add_assoc)
    1.79 +done
    1.80 +
    1.81 +lemma NSLIM_const_not_eq:
    1.82 +  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
    1.83 +  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
    1.84 +apply (simp add: NSLIM_def)
    1.85 +apply (rule_tac x="star_of a + epsilon" in exI)
    1.86 +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
    1.87 +            simp add: hypreal_epsilon_not_zero)
    1.88 +done
    1.89 +
    1.90 +lemma NSLIM_not_zero:
    1.91 +  fixes a :: real
    1.92 +  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
    1.93 +by (rule NSLIM_const_not_eq)
    1.94 +
    1.95 +lemma NSLIM_const_eq:
    1.96 +  fixes a :: real
    1.97 +  shows "(%x. k) -- a --NS> L ==> k = L"
    1.98 +apply (rule ccontr)
    1.99 +apply (blast dest: NSLIM_const_not_eq)
   1.100 +done
   1.101 +
   1.102 +text{* can actually be proved more easily by unfolding the definition!*}
   1.103 +lemma NSLIM_unique:
   1.104 +  fixes a :: real
   1.105 +  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
   1.106 +apply (drule NSLIM_minus)
   1.107 +apply (drule NSLIM_add, assumption)
   1.108 +apply (auto dest!: NSLIM_const_eq [symmetric])
   1.109 +apply (simp add: diff_def [symmetric])
   1.110 +done
   1.111 +
   1.112 +lemma NSLIM_mult_zero:
   1.113 +  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   1.114 +  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   1.115 +by (drule NSLIM_mult, auto)
   1.116 +
   1.117 +lemma NSLIM_self: "(%x. x) -- a --NS> a"
   1.118 +by (simp add: NSLIM_def)
   1.119 +
   1.120 +subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
   1.121 +
   1.122  lemma LIM_NSLIM:
   1.123    assumes f: "f -- a --> L" shows "f -- a --NS> L"
   1.124  proof (rule NSLIM_I)
   1.125 @@ -282,14 +367,7 @@
   1.126  theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   1.127  by (blast intro: LIM_NSLIM NSLIM_LIM)
   1.128  
   1.129 -text{*Proving properties of limits using nonstandard definition.
   1.130 -      The properties hold for standard limits as well!*}
   1.131 -
   1.132 -lemma NSLIM_mult:
   1.133 -  fixes l m :: "'a::real_normed_algebra"
   1.134 -  shows "[| f -- x --NS> l; g -- x --NS> m |]
   1.135 -      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
   1.136 -by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
   1.137 +subsubsection {* Derived theorems about @{term LIM} *}
   1.138  
   1.139  lemma LIM_mult2:
   1.140    fixes l m :: "'a::real_normed_algebra"
   1.141 @@ -297,115 +375,38 @@
   1.142        ==> (%x. f(x) * g(x)) -- x --> (l * m)"
   1.143  by (simp add: LIM_NSLIM_iff NSLIM_mult)
   1.144  
   1.145 -lemma NSLIM_add:
   1.146 -     "[| f -- x --NS> l; g -- x --NS> m |]
   1.147 -      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
   1.148 -by (auto simp add: NSLIM_def intro!: approx_add)
   1.149 -
   1.150  lemma LIM_add2:
   1.151       "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
   1.152  by (simp add: LIM_NSLIM_iff NSLIM_add)
   1.153  
   1.154 -
   1.155 -lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
   1.156 -by (simp add: NSLIM_def)
   1.157 -
   1.158  lemma LIM_const2: "(%x. k) -- x --> k"
   1.159  by (simp add: LIM_NSLIM_iff)
   1.160  
   1.161 -lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
   1.162 -by (simp add: NSLIM_def)
   1.163 -
   1.164  lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   1.165  by (simp add: LIM_NSLIM_iff NSLIM_minus)
   1.166  
   1.167 -
   1.168 -lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
   1.169 -by (blast dest: NSLIM_add NSLIM_minus)
   1.170 -
   1.171  lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   1.172  by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
   1.173  
   1.174 -
   1.175 -lemma NSLIM_inverse:
   1.176 -  fixes L :: "'a::real_normed_div_algebra"
   1.177 -  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
   1.178 -      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
   1.179 -apply (simp add: NSLIM_def, clarify)
   1.180 -apply (drule spec)
   1.181 -apply (auto simp add: star_of_approx_inverse)
   1.182 -done
   1.183 -
   1.184  lemma LIM_inverse:
   1.185    fixes L :: "'a::real_normed_div_algebra"
   1.186    shows "[| f -- a --> L; L \<noteq> 0 |]
   1.187        ==> (%x. inverse(f(x))) -- a --> (inverse L)"
   1.188  by (simp add: LIM_NSLIM_iff NSLIM_inverse)
   1.189  
   1.190 -
   1.191 -lemma NSLIM_zero:
   1.192 -  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
   1.193 -proof -
   1.194 -  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
   1.195 -    by (rule NSLIM_add_minus [OF f NSLIM_const])
   1.196 -  thus ?thesis by simp
   1.197 -qed
   1.198 -
   1.199  lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
   1.200  by (simp add: LIM_NSLIM_iff NSLIM_zero)
   1.201  
   1.202 -lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
   1.203 -apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   1.204 -apply (auto simp add: diff_minus add_assoc)
   1.205 -done
   1.206 -
   1.207  lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
   1.208  apply (drule_tac g = "%x. l" and M = l in LIM_add)
   1.209  apply (auto simp add: diff_minus add_assoc)
   1.210  done
   1.211  
   1.212 -lemma NSLIM_const_not_eq:
   1.213 -  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
   1.214 -  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
   1.215 -apply (simp add: NSLIM_def)
   1.216 -apply (rule_tac x="star_of a + epsilon" in exI)
   1.217 -apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   1.218 -            simp add: hypreal_epsilon_not_zero)
   1.219 -done
   1.220 -
   1.221 -lemma NSLIM_not_zero:
   1.222 -  fixes a :: real
   1.223 -  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
   1.224 -by (rule NSLIM_const_not_eq)
   1.225 -
   1.226 -lemma NSLIM_const_eq:
   1.227 -  fixes a :: real
   1.228 -  shows "(%x. k) -- a --NS> L ==> k = L"
   1.229 -apply (rule ccontr)
   1.230 -apply (blast dest: NSLIM_const_not_eq)
   1.231 -done
   1.232 -
   1.233 -text{* can actually be proved more easily by unfolding the definition!*}
   1.234 -lemma NSLIM_unique:
   1.235 -  fixes a :: real
   1.236 -  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
   1.237 -apply (drule NSLIM_minus)
   1.238 -apply (drule NSLIM_add, assumption)
   1.239 -apply (auto dest!: NSLIM_const_eq [symmetric])
   1.240 -apply (simp add: diff_def [symmetric])
   1.241 -done
   1.242 -
   1.243  lemma LIM_unique2:
   1.244    fixes a :: real
   1.245    shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
   1.246  by (simp add: LIM_NSLIM_iff NSLIM_unique)
   1.247  
   1.248 -
   1.249 -lemma NSLIM_mult_zero:
   1.250 -  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   1.251 -  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   1.252 -by (drule NSLIM_mult, auto)
   1.253 -
   1.254  (* we can use the corresponding thm LIM_mult2 *)
   1.255  (* for standard definition of limit           *)
   1.256  
   1.257 @@ -415,13 +416,7 @@
   1.258  by (drule LIM_mult2, auto)
   1.259  
   1.260  
   1.261 -lemma NSLIM_self: "(%x. x) -- a --NS> a"
   1.262 -by (simp add: NSLIM_def)
   1.263 -
   1.264 -
   1.265 -subsection{* Derivatives and Continuity: NS and Standard properties*}
   1.266 -
   1.267 -subsubsection{*Continuity*}
   1.268 +subsection {* Continuity *}
   1.269  
   1.270  lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
   1.271  by (simp add: isNSCont_def)
   1.272 @@ -592,7 +587,8 @@
   1.273  qed "isCont_isopen_iff";
   1.274  *******************************************************************)
   1.275  
   1.276 -text{*Uniform continuity*}
   1.277 +subsection {* Uniform Continuity *}
   1.278 +
   1.279  lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
   1.280  by (simp add: isNSUCont_def)
   1.281  
   1.282 @@ -654,7 +650,8 @@
   1.283      by transfer
   1.284  qed
   1.285  
   1.286 -text{*Derivatives*}
   1.287 +subsection {* Derivatives *}
   1.288 +
   1.289  lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
   1.290  by (simp add: deriv_def)
   1.291  
   1.292 @@ -668,7 +665,6 @@
   1.293  lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
   1.294  by (simp add: deriv_def LIM_NSLIM_iff)
   1.295  
   1.296 -
   1.297  subsubsection{*Uniqueness*}
   1.298  
   1.299  lemma DERIV_unique:
   1.300 @@ -686,20 +682,6 @@
   1.301              dest: approx_trans3)
   1.302  done
   1.303  
   1.304 -subsubsection{*Differentiable*}
   1.305 -
   1.306 -lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
   1.307 -by (simp add: differentiable_def)
   1.308 -
   1.309 -lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
   1.310 -by (force simp add: differentiable_def)
   1.311 -
   1.312 -lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
   1.313 -by (simp add: NSdifferentiable_def)
   1.314 -
   1.315 -lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
   1.316 -by (force simp add: NSdifferentiable_def)
   1.317 -
   1.318  subsubsection{*Alternative definition for differentiability*}
   1.319  
   1.320  lemma DERIV_LIM_iff:
   1.321 @@ -749,9 +731,9 @@
   1.322  by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
   1.323  
   1.324  
   1.325 -subsection{*Equivalence of NS and standard definitions of differentiation*}
   1.326 +subsubsection{*Equivalence of NS and standard definitions of differentiation*}
   1.327  
   1.328 -subsubsection{*First NSDERIV in terms of NSLIM*}
   1.329 +text {*First NSDERIV in terms of NSLIM*}
   1.330  
   1.331  text{*first equivalence *}
   1.332  lemma NSDERIV_NSLIM_iff:
   1.333 @@ -850,6 +832,7 @@
   1.334  by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
   1.335                NSDERIV_isNSCont)
   1.336  
   1.337 +subsubsection {* Derivatives of various functions *}
   1.338  
   1.339  text{*Differentiation rules for combinations of functions
   1.340        follow from clear, straightforard, algebraic
   1.341 @@ -980,47 +963,6 @@
   1.342  apply (blast intro: DERIV_add_minus)
   1.343  done
   1.344  
   1.345 -text{*(NS) Increment*}
   1.346 -lemma incrementI:
   1.347 -      "f NSdifferentiable x ==>
   1.348 -      increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
   1.349 -      hypreal_of_real (f x)"
   1.350 -by (simp add: increment_def)
   1.351 -
   1.352 -lemma incrementI2: "NSDERIV f x :> D ==>
   1.353 -     increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
   1.354 -     hypreal_of_real (f x)"
   1.355 -apply (erule NSdifferentiableI [THEN incrementI])
   1.356 -done
   1.357 -
   1.358 -(* The Increment theorem -- Keisler p. 65 *)
   1.359 -lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
   1.360 -      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
   1.361 -apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
   1.362 -apply (drule bspec, auto)
   1.363 -apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
   1.364 -apply (frule_tac b1 = "hypreal_of_real (D) + y"
   1.365 -        in hypreal_mult_right_cancel [THEN iffD2])
   1.366 -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)
   1.367 -apply assumption
   1.368 -apply (simp add: times_divide_eq_right [symmetric])
   1.369 -apply (auto simp add: left_distrib)
   1.370 -done
   1.371 -
   1.372 -lemma increment_thm2:
   1.373 -     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
   1.374 -      ==> \<exists>e \<in> Infinitesimal. increment f x h =
   1.375 -              hypreal_of_real(D)*h + e*h"
   1.376 -by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
   1.377 -
   1.378 -
   1.379 -lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
   1.380 -      ==> increment f x h \<approx> 0"
   1.381 -apply (drule increment_thm2,
   1.382 -       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
   1.383 -apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   1.384 -done
   1.385 -
   1.386  text{*  Similarly to the above, the chain rule admits an entirely
   1.387     straightforward derivation. Compare this with Harrison's
   1.388     HOL proof of the chain rule, which proved to be trickier and
   1.389 @@ -1245,6 +1187,114 @@
   1.390      by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
   1.391  qed
   1.392  
   1.393 +subsubsection {* Differentiability predicate *}
   1.394 +
   1.395 +lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
   1.396 +by (simp add: differentiable_def)
   1.397 +
   1.398 +lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
   1.399 +by (force simp add: differentiable_def)
   1.400 +
   1.401 +lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
   1.402 +by (simp add: NSdifferentiable_def)
   1.403 +
   1.404 +lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
   1.405 +by (force simp add: NSdifferentiable_def)
   1.406 +
   1.407 +lemma differentiable_const: "(\<lambda>z. a) differentiable x"
   1.408 +  apply (unfold differentiable_def)
   1.409 +  apply (rule_tac x=0 in exI)
   1.410 +  apply simp
   1.411 +  done
   1.412 +
   1.413 +lemma differentiable_sum:
   1.414 +  assumes "f differentiable x"
   1.415 +  and "g differentiable x"
   1.416 +  shows "(\<lambda>x. f x + g x) differentiable x"
   1.417 +proof -
   1.418 +  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.419 +  then obtain df where "DERIV f x :> df" ..
   1.420 +  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.421 +  then obtain dg where "DERIV g x :> dg" ..
   1.422 +  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
   1.423 +  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
   1.424 +  thus ?thesis by (fold differentiable_def)
   1.425 +qed
   1.426 +
   1.427 +lemma differentiable_diff:
   1.428 +  assumes "f differentiable x"
   1.429 +  and "g differentiable x"
   1.430 +  shows "(\<lambda>x. f x - g x) differentiable x"
   1.431 +proof -
   1.432 +  from prems have "f differentiable x" by simp
   1.433 +  moreover
   1.434 +  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.435 +  then obtain dg where "DERIV g x :> dg" ..
   1.436 +  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
   1.437 +  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
   1.438 +  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
   1.439 +  ultimately 
   1.440 +  show ?thesis
   1.441 +    by (auto simp: real_diff_def dest: differentiable_sum)
   1.442 +qed
   1.443 +
   1.444 +lemma differentiable_mult:
   1.445 +  assumes "f differentiable x"
   1.446 +  and "g differentiable x"
   1.447 +  shows "(\<lambda>x. f x * g x) differentiable x"
   1.448 +proof -
   1.449 +  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.450 +  then obtain df where "DERIV f x :> df" ..
   1.451 +  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.452 +  then obtain dg where "DERIV g x :> dg" ..
   1.453 +  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
   1.454 +  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
   1.455 +  thus ?thesis by (fold differentiable_def)
   1.456 +qed
   1.457 +
   1.458 +subsection {*(NS) Increment*}
   1.459 +lemma incrementI:
   1.460 +      "f NSdifferentiable x ==>
   1.461 +      increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
   1.462 +      hypreal_of_real (f x)"
   1.463 +by (simp add: increment_def)
   1.464 +
   1.465 +lemma incrementI2: "NSDERIV f x :> D ==>
   1.466 +     increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
   1.467 +     hypreal_of_real (f x)"
   1.468 +apply (erule NSdifferentiableI [THEN incrementI])
   1.469 +done
   1.470 +
   1.471 +(* The Increment theorem -- Keisler p. 65 *)
   1.472 +lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
   1.473 +      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
   1.474 +apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
   1.475 +apply (drule bspec, auto)
   1.476 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
   1.477 +apply (frule_tac b1 = "hypreal_of_real (D) + y"
   1.478 +        in hypreal_mult_right_cancel [THEN iffD2])
   1.479 +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)
   1.480 +apply assumption
   1.481 +apply (simp add: times_divide_eq_right [symmetric])
   1.482 +apply (auto simp add: left_distrib)
   1.483 +done
   1.484 +
   1.485 +lemma increment_thm2:
   1.486 +     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
   1.487 +      ==> \<exists>e \<in> Infinitesimal. increment f x h =
   1.488 +              hypreal_of_real(D)*h + e*h"
   1.489 +by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
   1.490 +
   1.491 +
   1.492 +lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
   1.493 +      ==> increment f x h \<approx> 0"
   1.494 +apply (drule increment_thm2,
   1.495 +       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
   1.496 +apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   1.497 +done
   1.498 +
   1.499 +subsection {* Nested Intervals and Bisection *}
   1.500 +
   1.501  text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
   1.502       All considerably tidied by lcp.*}
   1.503  
   1.504 @@ -1436,7 +1486,9 @@
   1.505  done
   1.506  
   1.507  
   1.508 -subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
   1.509 +subsection {* Intermediate Value Theorem *}
   1.510 +
   1.511 +text {*Prove Contrapositive by Bisection*}
   1.512  
   1.513  lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
   1.514           a \<le> b;
   1.515 @@ -1487,7 +1539,7 @@
   1.516  apply (blast intro: IVT2)
   1.517  done
   1.518  
   1.519 -subsection{*By bisection, function continuous on closed interval is bounded above*}
   1.520 +text{*By bisection, function continuous on closed interval is bounded above*}
   1.521  
   1.522  lemma isCont_bounded:
   1.523       "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   1.524 @@ -1605,7 +1657,7 @@
   1.525  done
   1.526  
   1.527  
   1.528 -subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
   1.529 +text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
   1.530  
   1.531  lemma DERIV_left_inc:
   1.532    assumes der: "DERIV f x :> l"
   1.533 @@ -2089,59 +2141,6 @@
   1.534    qed
   1.535  qed
   1.536  
   1.537 -
   1.538 -lemma differentiable_const: "(\<lambda>z. a) differentiable x"
   1.539 -  apply (unfold differentiable_def)
   1.540 -  apply (rule_tac x=0 in exI)
   1.541 -  apply simp
   1.542 -  done
   1.543 -
   1.544 -lemma differentiable_sum:
   1.545 -  assumes "f differentiable x"
   1.546 -  and "g differentiable x"
   1.547 -  shows "(\<lambda>x. f x + g x) differentiable x"
   1.548 -proof -
   1.549 -  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.550 -  then obtain df where "DERIV f x :> df" ..
   1.551 -  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.552 -  then obtain dg where "DERIV g x :> dg" ..
   1.553 -  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
   1.554 -  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
   1.555 -  thus ?thesis by (fold differentiable_def)
   1.556 -qed
   1.557 -
   1.558 -lemma differentiable_diff:
   1.559 -  assumes "f differentiable x"
   1.560 -  and "g differentiable x"
   1.561 -  shows "(\<lambda>x. f x - g x) differentiable x"
   1.562 -proof -
   1.563 -  from prems have "f differentiable x" by simp
   1.564 -  moreover
   1.565 -  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.566 -  then obtain dg where "DERIV g x :> dg" ..
   1.567 -  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
   1.568 -  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
   1.569 -  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
   1.570 -  ultimately 
   1.571 -  show ?thesis
   1.572 -    by (auto simp: real_diff_def dest: differentiable_sum)
   1.573 -qed
   1.574 -
   1.575 -lemma differentiable_mult:
   1.576 -  assumes "f differentiable x"
   1.577 -  and "g differentiable x"
   1.578 -  shows "(\<lambda>x. f x * g x) differentiable x"
   1.579 -proof -
   1.580 -  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.581 -  then obtain df where "DERIV f x :> df" ..
   1.582 -  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.583 -  then obtain dg where "DERIV g x :> dg" ..
   1.584 -  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
   1.585 -  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
   1.586 -  thus ?thesis by (fold differentiable_def)
   1.587 -qed
   1.588 -
   1.589 -
   1.590  theorem GMVT:
   1.591    assumes alb: "a < b"
   1.592    and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"