src/HOL/Hyperreal/Lim.thy
changeset 14477 cc61fd03e589
parent 14387 e96d5c42c4b0
child 15003 6145dd7538d7
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Fri Mar 19 10:50:06 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Mar 19 10:51:03 2004 +0100
     1.3 @@ -1,66 +1,67 @@
     1.4  (*  Title       : Lim.thy
     1.5 +    ID          : $Id$
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 1998  University of Cambridge
     1.8 -    Description : Theory of limits, continuity and 
     1.9 -                  differentiation of real=>real functions
    1.10 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    1.11  *)
    1.12  
    1.13 -Lim = SEQ + RealDef + 
    1.14 +header{*Limits, Continuity and Differentiation*}
    1.15  
    1.16 -(*-----------------------------------------------------------------------
    1.17 -    Limits, continuity and differentiation: standard and NS definitions
    1.18 - -----------------------------------------------------------------------*)
    1.19 +theory Lim = SEQ + RealDef:
    1.20 +
    1.21 +text{*Standard and Nonstandard Definitions*}
    1.22  
    1.23  constdefs
    1.24 -  LIM :: [real=>real,real,real] => bool
    1.25 +  LIM :: "[real=>real,real,real] => bool"
    1.26  				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
    1.27    "f -- a --> L ==
    1.28 -     ALL r. 0 < r --> 
    1.29 -	     (EX s. 0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
    1.30 -			  --> abs(f x + -L) < r)))"
    1.31 +     \<forall>r. 0 < r -->
    1.32 +	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (\<bar>x + -a\<bar> < s)
    1.33 +			  --> \<bar>f x + -L\<bar> < r)))"
    1.34  
    1.35 -  NSLIM :: [real=>real,real,real] => bool
    1.36 +  NSLIM :: "[real=>real,real,real] => bool"
    1.37  			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
    1.38 -  "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & 
    1.39 +  "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
    1.40  		      x @= hypreal_of_real a -->
    1.41 -		      ( *f* f) x @= hypreal_of_real L))"   
    1.42 +		      ( *f* f) x @= hypreal_of_real L))"
    1.43  
    1.44 -  isCont :: [real=>real,real] => bool
    1.45 -  "isCont f a == (f -- a --> (f a))"        
    1.46 +  isCont :: "[real=>real,real] => bool"
    1.47 +  "isCont f a == (f -- a --> (f a))"
    1.48  
    1.49    (* NS definition dispenses with limit notions *)
    1.50 -  isNSCont :: [real=>real,real] => bool
    1.51 -  "isNSCont f a == (ALL y. y @= hypreal_of_real a --> 
    1.52 +  isNSCont :: "[real=>real,real] => bool"
    1.53 +  "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
    1.54  			   ( *f* f) y @= hypreal_of_real (f a))"
    1.55  
    1.56    (* differentiation: D is derivative of function f at x *)
    1.57 -  deriv:: [real=>real,real,real] => bool
    1.58 +  deriv:: "[real=>real,real,real] => bool"
    1.59  			    ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
    1.60 -  "DERIV f x :> D == ((%h. (f(x + h) + -f(x))/h) -- 0 --> D)"
    1.61 +  "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
    1.62  
    1.63 -  nsderiv :: [real=>real,real,real] => bool
    1.64 +  nsderiv :: "[real=>real,real,real] => bool"
    1.65  			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
    1.66 -  "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. 
    1.67 -			(( *f* f)(hypreal_of_real x + h) + 
    1.68 +  "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
    1.69 +			(( *f* f)(hypreal_of_real x + h) +
    1.70  			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"
    1.71  
    1.72 -  differentiable :: [real=>real,real] => bool   (infixl 60)
    1.73 -  "f differentiable x == (EX D. DERIV f x :> D)"
    1.74 +  differentiable :: "[real=>real,real] => bool"   (infixl "differentiable" 60)
    1.75 +  "f differentiable x == (\<exists>D. DERIV f x :> D)"
    1.76  
    1.77 -  NSdifferentiable :: [real=>real,real] => bool   (infixl 60)
    1.78 -  "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
    1.79 +  NSdifferentiable :: "[real=>real,real] => bool"   
    1.80 +                       (infixl "NSdifferentiable" 60)
    1.81 +  "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
    1.82  
    1.83 -  increment :: [real=>real,real,hypreal] => hypreal
    1.84 -  "increment f x h == (@inc. f NSdifferentiable x & 
    1.85 +  increment :: "[real=>real,real,hypreal] => hypreal"
    1.86 +  "increment f x h == (@inc. f NSdifferentiable x &
    1.87  		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    1.88  
    1.89 -  isUCont :: (real=>real) => bool
    1.90 -  "isUCont f ==  (ALL r. 0 < r --> 
    1.91 -		      (EX s. 0 < s & (ALL x y. abs(x + -y) < s
    1.92 -			    --> abs(f x + -f y) < r)))"
    1.93 +  isUCont :: "(real=>real) => bool"
    1.94 +  "isUCont f ==  (\<forall>r. 0 < r -->
    1.95 +		      (\<exists>s. 0 < s & (\<forall>x y. \<bar>x + -y\<bar> < s
    1.96 +			    --> \<bar>f x + -f y\<bar> < r)))"
    1.97  
    1.98 -  isNSUCont :: (real=>real) => bool
    1.99 -  "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   1.100 +  isNSUCont :: "(real=>real) => bool"
   1.101 +  "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   1.102  
   1.103  
   1.104  (*Used in the proof of the Bolzano theorem*)
   1.105 @@ -72,8 +73,2258 @@
   1.106    "Bolzano_bisect P a b (Suc n) =
   1.107        (let (x,y) = Bolzano_bisect P a b n
   1.108         in if P(x, (x+y)/2) then ((x+y)/2, y)
   1.109 -                            else (x, (x+y)/2) )"
   1.110 -  
   1.111 +                            else (x, (x+y)/2))"
   1.112 +
   1.113 +
   1.114 +
   1.115 +section{*Some Purely Standard Proofs*}
   1.116 +
   1.117 +lemma LIM_eq:
   1.118 +     "f -- a --> L =
   1.119 +     (\<forall>r. 0<r --> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))"
   1.120 +by (simp add: LIM_def diff_minus)
   1.121 +
   1.122 +lemma LIM_D:
   1.123 +     "[| f -- a --> L; 0<r |]
   1.124 +      ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
   1.125 +by (simp add: LIM_eq)
   1.126 +
   1.127 +lemma LIM_const: "(%x. k) -- x --> k"
   1.128 +by (simp add: LIM_def)
   1.129 +declare LIM_const [simp]
   1.130 +
   1.131 +lemma LIM_add:
   1.132 +  assumes f: "f -- a --> L" and g: "g -- a --> M"
   1.133 +  shows "(%x. f x + g(x)) -- a --> (L + M)"
   1.134 +proof (simp add: LIM_eq, clarify)
   1.135 +  fix r :: real
   1.136 +  assume r: "0<r"
   1.137 +  from LIM_D [OF f half_gt_zero [OF r]]
   1.138 +  obtain fs
   1.139 +    where fs:    "0 < fs"
   1.140 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x - L\<bar> < r/2"
   1.141 +  by blast
   1.142 +  from LIM_D [OF g half_gt_zero [OF r]]
   1.143 +  obtain gs
   1.144 +    where gs:    "0 < gs"
   1.145 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
   1.146 +  by blast
   1.147 +  show "\<exists>s. 0 < s \<and>
   1.148 +            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r)"
   1.149 +  proof (intro exI conjI strip)
   1.150 +    show "0 < min fs gs"  by (simp add: fs gs)
   1.151 +    fix x :: real
   1.152 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
   1.153 +    with fs_lt gs_lt
   1.154 +    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by (auto simp add: fs_lt)
   1.155 +    hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
   1.156 +    thus "\<bar>f x + g x - (L + M)\<bar> < r"
   1.157 +      by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
   1.158 +  qed
   1.159 +qed
   1.160 +
   1.161 +lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   1.162 +apply (simp add: LIM_eq)
   1.163 +apply (subgoal_tac "\<forall>x. \<bar>- f x + L\<bar> = \<bar>f x - L\<bar>")
   1.164 +apply (simp_all add: abs_if)
   1.165 +done
   1.166 +
   1.167 +lemma LIM_add_minus:
   1.168 +    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   1.169 +by (blast dest: LIM_add LIM_minus)
   1.170 +
   1.171 +lemma LIM_diff:
   1.172 +    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
   1.173 +by (simp add: diff_minus LIM_add_minus) 
   1.174 +
   1.175 +
   1.176 +lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
   1.177 +proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
   1.178 +  assume k: "k < L"
   1.179 +  show "\<exists>r. 0 < r \<and>
   1.180 +        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
   1.181 +  proof (intro exI conjI strip)
   1.182 +    show "0 < L-k" by (simp add: k)
   1.183 +    fix s :: real
   1.184 +    assume s: "0<s"
   1.185 +    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
   1.186 +     next
   1.187 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if) 
   1.188 +     next
   1.189 +      from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
   1.190 +  qed
   1.191 +next
   1.192 +  assume k: "L < k"
   1.193 +  show "\<exists>r. 0 < r \<and>
   1.194 +        (\<forall>s. 0 < s \<longrightarrow> (\<exists>x. (x < a \<or> a < x) \<and> \<bar>x-a\<bar> < s) \<and> \<not> \<bar>k-L\<bar> < r)"
   1.195 +  proof (intro exI conjI strip)
   1.196 +    show "0 < k-L" by (simp add: k)
   1.197 +    fix s :: real
   1.198 +    assume s: "0<s"
   1.199 +    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
   1.200 +     next
   1.201 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if) 
   1.202 +     next
   1.203 +      from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
   1.204 +  qed
   1.205 +qed
   1.206 +
   1.207 +lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
   1.208 +apply (rule ccontr)
   1.209 +apply (blast dest: LIM_const_not_eq) 
   1.210 +done
   1.211 +
   1.212 +lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M"
   1.213 +apply (drule LIM_diff, assumption) 
   1.214 +apply (auto dest!: LIM_const_eq)
   1.215 +done
   1.216 +
   1.217 +lemma LIM_mult_zero:
   1.218 +  assumes f: "f -- a --> 0" and g: "g -- a --> 0"
   1.219 +  shows "(%x. f(x) * g(x)) -- a --> 0"
   1.220 +proof (simp add: LIM_eq, clarify)
   1.221 +  fix r :: real
   1.222 +  assume r: "0<r"
   1.223 +  from LIM_D [OF f zero_less_one]
   1.224 +  obtain fs
   1.225 +    where fs:    "0 < fs"
   1.226 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x\<bar> < 1"
   1.227 +  by auto
   1.228 +  from LIM_D [OF g r]
   1.229 +  obtain gs
   1.230 +    where gs:    "0 < gs"
   1.231 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x\<bar> < r"
   1.232 +  by auto
   1.233 +  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x\<bar> * \<bar>g x\<bar> < r)"
   1.234 +  proof (intro exI conjI strip)
   1.235 +    show "0 < min fs gs"  by (simp add: fs gs)
   1.236 +    fix x :: real
   1.237 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
   1.238 +    with fs_lt gs_lt
   1.239 +    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
   1.240 +    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less) 
   1.241 +    thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
   1.242 +  qed
   1.243 +qed
   1.244 +
   1.245 +lemma LIM_self: "(%x. x) -- a --> a"
   1.246 +by (auto simp add: LIM_def)
   1.247 +
   1.248 +text{*Limits are equal for functions equal except at limit point*}
   1.249 +lemma LIM_equal:
   1.250 +     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   1.251 +by (simp add: LIM_def)
   1.252 +
   1.253 +text{*Two uses in Hyperreal/Transcendental.ML*}
   1.254 +lemma LIM_trans:
   1.255 +     "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
   1.256 +apply (drule LIM_add, assumption)
   1.257 +apply (auto simp add: add_assoc)
   1.258 +done
   1.259 +
   1.260 +
   1.261 +subsection{*Relationships Between Standard and Nonstandard Concepts*}
   1.262 +
   1.263 +text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
   1.264 +lemma LIM_NSLIM:
   1.265 +      "f -- x --> L ==> f -- x --NS> L"
   1.266 +apply (simp add: LIM_def NSLIM_def approx_def)
   1.267 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   1.268 +apply (rule_tac z = xa in eq_Abs_hypreal)
   1.269 +apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def hypreal_add)
   1.270 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify) 
   1.271 +apply (drule_tac x = u in spec, clarify)
   1.272 +apply (drule_tac x = s in spec, clarify)
   1.273 +apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u")
   1.274 +prefer 2 apply blast
   1.275 +apply (drule FreeUltrafilterNat_all, ultra)
   1.276 +done
   1.277 +
   1.278 +(*---------------------------------------------------------------------
   1.279 +    Limit: NS definition ==> standard definition
   1.280 + ---------------------------------------------------------------------*)
   1.281 +
   1.282 +lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
   1.283 +         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
   1.284 +      ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
   1.285 +              \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
   1.286 +apply clarify
   1.287 +apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
   1.288 +done
   1.289 +
   1.290 +lemma lemma_skolemize_LIM2:
   1.291 +     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
   1.292 +         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
   1.293 +      ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
   1.294 +                \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
   1.295 +apply (drule lemma_LIM)
   1.296 +apply (drule choice, blast)
   1.297 +done
   1.298 +
   1.299 +lemma lemma_simp: "\<forall>n. X n \<noteq> x &
   1.300 +          \<bar>X n + - x\<bar> < inverse (real(Suc n)) &
   1.301 +          r \<le> abs (f (X n) + - L) ==>
   1.302 +          \<forall>n. \<bar>X n + - x\<bar> < inverse (real(Suc n))"
   1.303 +by auto
   1.304 +
   1.305 +
   1.306 +(*-------------------
   1.307 +    NSLIM => LIM
   1.308 + -------------------*)
   1.309 +
   1.310 +lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
   1.311 +apply (simp add: LIM_def NSLIM_def approx_def)
   1.312 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
   1.313 +apply (rule ccontr, simp)  
   1.314 +apply (simp add: linorder_not_less)
   1.315 +apply (drule lemma_skolemize_LIM2, safe)
   1.316 +apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
   1.317 +apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
   1.318 +apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
   1.319 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
   1.320 +apply (drule spec, drule mp, assumption)
   1.321 +apply (drule FreeUltrafilterNat_all, ultra)
   1.322 +done
   1.323 +
   1.324 +
   1.325 +(**** Key result ****)
   1.326 +lemma LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   1.327 +by (blast intro: LIM_NSLIM NSLIM_LIM)
   1.328 +
   1.329 +(*-------------------------------------------------------------------*)
   1.330 +(*   Proving properties of limits using nonstandard definition and   *)
   1.331 +(*   hence, the properties hold for standard limits as well          *)
   1.332 +(*-------------------------------------------------------------------*)
   1.333 +(*------------------------------------------------
   1.334 +      NSLIM_mult and hence (trivially) LIM_mult
   1.335 + ------------------------------------------------*)
   1.336 +
   1.337 +lemma NSLIM_mult:
   1.338 +     "[| f -- x --NS> l; g -- x --NS> m |]
   1.339 +      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
   1.340 +apply (simp add: NSLIM_def)
   1.341 +apply (auto intro!: approx_mult_HFinite)
   1.342 +done
   1.343 +
   1.344 +lemma LIM_mult2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
   1.345 +by (simp add: LIM_NSLIM_iff NSLIM_mult)
   1.346 +
   1.347 +(*----------------------------------------------
   1.348 +      NSLIM_add and hence (trivially) LIM_add
   1.349 +      Note the much shorter proof
   1.350 + ----------------------------------------------*)
   1.351 +lemma NSLIM_add:
   1.352 +     "[| f -- x --NS> l; g -- x --NS> m |]
   1.353 +      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
   1.354 +apply (simp add: NSLIM_def)
   1.355 +apply (auto intro!: approx_add)
   1.356 +done
   1.357 +
   1.358 +lemma LIM_add2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
   1.359 +by (simp add: LIM_NSLIM_iff NSLIM_add)
   1.360 +
   1.361 +
   1.362 +lemma NSLIM_const: "(%x. k) -- x --NS> k"
   1.363 +by (simp add: NSLIM_def)
   1.364 +
   1.365 +declare NSLIM_const [simp]
   1.366 +
   1.367 +lemma LIM_const2: "(%x. k) -- x --> k"
   1.368 +by (simp add: LIM_NSLIM_iff)
   1.369 +
   1.370 +
   1.371 +lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
   1.372 +by (simp add: NSLIM_def)
   1.373 +
   1.374 +lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
   1.375 +by (simp add: LIM_NSLIM_iff NSLIM_minus)
   1.376 +
   1.377 +
   1.378 +lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
   1.379 +by (blast dest: NSLIM_add NSLIM_minus)
   1.380 +
   1.381 +lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
   1.382 +by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
   1.383 +
   1.384 +
   1.385 +lemma NSLIM_inverse:
   1.386 +     "[| f -- a --NS> L;  L \<noteq> 0 |]
   1.387 +      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
   1.388 +apply (simp add: NSLIM_def, clarify)
   1.389 +apply (drule spec)
   1.390 +apply (auto simp add: hypreal_of_real_approx_inverse)
   1.391 +done
   1.392 +
   1.393 +lemma LIM_inverse: "[| f -- a --> L; L \<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"
   1.394 +by (simp add: LIM_NSLIM_iff NSLIM_inverse)
   1.395 +
   1.396 +
   1.397 +lemma NSLIM_zero:
   1.398 +  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
   1.399 +proof -;
   1.400 +  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
   1.401 +    by (rule NSLIM_add_minus [OF f NSLIM_const]) 
   1.402 +  thus ?thesis by simp
   1.403 +qed
   1.404 +
   1.405 +lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
   1.406 +by (simp add: LIM_NSLIM_iff NSLIM_zero)
   1.407 +
   1.408 +lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
   1.409 +apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
   1.410 +apply (auto simp add: diff_minus add_assoc)
   1.411 +done
   1.412 +
   1.413 +lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
   1.414 +apply (drule_tac g = "%x. l" and M = l in LIM_add)
   1.415 +apply (auto simp add: diff_minus add_assoc)
   1.416 +done
   1.417 +
   1.418 +
   1.419 +
   1.420 +lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
   1.421 +apply (simp add: NSLIM_def)
   1.422 +apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
   1.423 +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   1.424 +            simp add: hypreal_epsilon_not_zero)
   1.425 +done
   1.426 +
   1.427 +lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
   1.428 +apply (simp add: NSLIM_def)
   1.429 +apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
   1.430 +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
   1.431 +            simp add: hypreal_epsilon_not_zero)
   1.432 +done
   1.433 +
   1.434 +lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
   1.435 +apply (rule ccontr)
   1.436 +apply (blast dest: NSLIM_const_not_eq) 
   1.437 +done
   1.438 +
   1.439 +(* can actually be proved more easily by unfolding def! *)
   1.440 +lemma NSLIM_unique: "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M"
   1.441 +apply (drule NSLIM_minus)
   1.442 +apply (drule NSLIM_add, assumption)
   1.443 +apply (auto dest!: NSLIM_const_eq [symmetric])
   1.444 +done
   1.445 +
   1.446 +lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M"
   1.447 +by (simp add: LIM_NSLIM_iff NSLIM_unique)
   1.448 +
   1.449 +
   1.450 +lemma NSLIM_mult_zero: "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   1.451 +by (drule NSLIM_mult, auto)
   1.452 +
   1.453 +(* we can use the corresponding thm LIM_mult2 *)
   1.454 +(* for standard definition of limit           *)
   1.455 +
   1.456 +lemma LIM_mult_zero2: "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
   1.457 +by (drule LIM_mult2, auto)
   1.458 +
   1.459 +
   1.460 +lemma NSLIM_self: "(%x. x) -- a --NS> a"
   1.461 +by (simp add: NSLIM_def)
   1.462 +
   1.463 +
   1.464 +(*-----------------------------------------------------------------------------
   1.465 +   Derivatives and Continuity - NS and Standard properties
   1.466 + -----------------------------------------------------------------------------*)
   1.467 +text{*Continuity*}
   1.468 +
   1.469 +lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
   1.470 +by (simp add: isNSCont_def)
   1.471 +
   1.472 +lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
   1.473 +by (simp add: isNSCont_def NSLIM_def)
   1.474 +
   1.475 +lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
   1.476 +apply (simp add: isNSCont_def NSLIM_def, auto)
   1.477 +apply (rule_tac Q = "y = hypreal_of_real a" in excluded_middle [THEN disjE], auto)
   1.478 +done
   1.479 +
   1.480 +(*-----------------------------------------------------
   1.481 +    NS continuity can be defined using NS Limit in
   1.482 +    similar fashion to standard def of continuity
   1.483 + -----------------------------------------------------*)
   1.484 +lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
   1.485 +by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   1.486 +
   1.487 +(*----------------------------------------------
   1.488 +  Hence, NS continuity can be given
   1.489 +  in terms of standard limit
   1.490 + ---------------------------------------------*)
   1.491 +lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
   1.492 +by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   1.493 +
   1.494 +(*-----------------------------------------------
   1.495 +  Moreover, it's trivial now that NS continuity
   1.496 +  is equivalent to standard continuity
   1.497 + -----------------------------------------------*)
   1.498 +lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
   1.499 +apply (simp add: isCont_def)
   1.500 +apply (rule isNSCont_LIM_iff)
   1.501 +done
   1.502 +
   1.503 +(*----------------------------------------
   1.504 +  Standard continuity ==> NS continuity
   1.505 + ----------------------------------------*)
   1.506 +lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
   1.507 +by (erule isNSCont_isCont_iff [THEN iffD2])
   1.508 +
   1.509 +(*----------------------------------------
   1.510 +  NS continuity ==> Standard continuity
   1.511 + ----------------------------------------*)
   1.512 +lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
   1.513 +by (erule isNSCont_isCont_iff [THEN iffD1])
   1.514 +
   1.515 +text{*Alternative definition of continuity*}
   1.516 +(* Prove equivalence between NS limits - *)
   1.517 +(* seems easier than using standard def  *)
   1.518 +lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
   1.519 +apply (simp add: NSLIM_def, auto)
   1.520 +apply (drule_tac x = "hypreal_of_real a + x" in spec)
   1.521 +apply (drule_tac [2] x = "-hypreal_of_real a + x" in spec, safe, simp)
   1.522 +apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
   1.523 +apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
   1.524 + prefer 3 apply (simp add: add_commute) 
   1.525 +apply (rule_tac [2] z = x in eq_Abs_hypreal)
   1.526 +apply (rule_tac [4] z = x in eq_Abs_hypreal)
   1.527 +apply (auto simp add: starfun hypreal_of_real_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
   1.528 +done
   1.529 +
   1.530 +lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   1.531 +by (rule NSLIM_h_iff)
   1.532 +
   1.533 +lemma LIM_isCont_iff: "(f -- a --> f a) = ((%h. f(a + h)) -- 0 --> f(a))"
   1.534 +by (simp add: LIM_NSLIM_iff NSLIM_isCont_iff)
   1.535 +
   1.536 +lemma isCont_iff: "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))"
   1.537 +by (simp add: isCont_def LIM_isCont_iff)
   1.538 +
   1.539 +(*--------------------------------------------------------------------------
   1.540 +   Immediate application of nonstandard criterion for continuity can offer
   1.541 +   very simple proofs of some standard property of continuous functions
   1.542 + --------------------------------------------------------------------------*)
   1.543 +text{*sum continuous*}
   1.544 +lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"
   1.545 +by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
   1.546 +
   1.547 +text{*mult continuous*}
   1.548 +lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
   1.549 +by (auto intro!: starfun_mult_HFinite_approx 
   1.550 +            simp del: starfun_mult [symmetric] 
   1.551 +            simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
   1.552 +
   1.553 +(*-------------------------------------------
   1.554 +     composition of continuous functions
   1.555 +     Note very short straightforard proof!
   1.556 + ------------------------------------------*)
   1.557 +lemma isCont_o: "[| isCont f a; isCont g (f a) |] ==> isCont (g o f) a"
   1.558 +by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric])
   1.559 +
   1.560 +lemma isCont_o2: "[| isCont f a; isCont g (f a) |] ==> isCont (%x. g (f x)) a"
   1.561 +by (auto dest: isCont_o simp add: o_def)
   1.562 +
   1.563 +lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
   1.564 +by (simp add: isNSCont_def)
   1.565 +
   1.566 +lemma isCont_minus: "isCont f a ==> isCont (%x. - f x) a"
   1.567 +by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
   1.568 +
   1.569 +lemma isCont_inverse:
   1.570 +      "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
   1.571 +apply (simp add: isCont_def)
   1.572 +apply (blast intro: LIM_inverse)
   1.573 +done
   1.574 +
   1.575 +lemma isNSCont_inverse: "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
   1.576 +by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
   1.577 +
   1.578 +lemma isCont_diff:
   1.579 +      "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"
   1.580 +apply (simp add: diff_minus)
   1.581 +apply (auto intro: isCont_add isCont_minus)
   1.582 +done
   1.583 +
   1.584 +lemma isCont_const: "isCont (%x. k) a"
   1.585 +by (simp add: isCont_def)
   1.586 +declare isCont_const [simp]
   1.587 +
   1.588 +lemma isNSCont_const: "isNSCont (%x. k) a"
   1.589 +by (simp add: isNSCont_def)
   1.590 +declare isNSCont_const [simp]
   1.591 +
   1.592 +lemma isNSCont_rabs: "isNSCont abs a"
   1.593 +apply (simp add: isNSCont_def)
   1.594 +apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
   1.595 +done
   1.596 +declare isNSCont_rabs [simp]
   1.597 +
   1.598 +lemma isCont_rabs: "isCont abs a"
   1.599 +by (auto simp add: isNSCont_isCont_iff [symmetric])
   1.600 +declare isCont_rabs [simp]
   1.601 +
   1.602 +(****************************************************************
   1.603 +(%* Leave as commented until I add topology theory or remove? *%)
   1.604 +(%*------------------------------------------------------------
   1.605 +  Elementary topology proof for a characterisation of
   1.606 +  continuity now: a function f is continuous if and only
   1.607 +  if the inverse image, {x. f(x) \<in> A}, of any open set A
   1.608 +  is always an open set
   1.609 + ------------------------------------------------------------*%)
   1.610 +Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
   1.611 +               ==> isNSopen {x. f x \<in> A}"
   1.612 +by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
   1.613 +by (dtac (mem_monad_approx RS approx_sym);
   1.614 +by (dres_inst_tac [("x","a")] spec 1);
   1.615 +by (dtac isNSContD 1 THEN assume_tac 1)
   1.616 +by (dtac bspec 1 THEN assume_tac 1)
   1.617 +by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
   1.618 +by (blast_tac (claset() addIs [starfun_mem_starset]);
   1.619 +qed "isNSCont_isNSopen";
   1.620 +
   1.621 +Goalw [isNSCont_def]
   1.622 +          "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
   1.623 +\              ==> isNSCont f x";
   1.624 +by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
   1.625 +     (approx_minus_iff RS iffD2)],simpset() addsimps
   1.626 +      [Infinitesimal_def,SReal_iff]));
   1.627 +by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
   1.628 +by (etac (isNSopen_open_interval RSN (2,impE));
   1.629 +by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
   1.630 +by (dres_inst_tac [("x","x")] spec 1);
   1.631 +by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
   1.632 +    simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
   1.633 +qed "isNSopen_isNSCont";
   1.634 +
   1.635 +Goal "(\<forall>x. isNSCont f x) = \
   1.636 +\     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
   1.637 +by (blast_tac (claset() addIs [isNSCont_isNSopen,
   1.638 +    isNSopen_isNSCont]);
   1.639 +qed "isNSCont_isNSopen_iff";
   1.640 +
   1.641 +(%*------- Standard version of same theorem --------*%)
   1.642 +Goal "(\<forall>x. isCont f x) = \
   1.643 +\         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
   1.644 +by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
   1.645 +              simpset() addsimps [isNSopen_isopen_iff RS sym,
   1.646 +              isNSCont_isCont_iff RS sym]));
   1.647 +qed "isCont_isopen_iff";
   1.648 +*******************************************************************)
   1.649 +
   1.650 +text{*Uniform continuity*}
   1.651 +lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
   1.652 +by (simp add: isNSUCont_def)
   1.653 +
   1.654 +lemma isUCont_isCont: "isUCont f ==> isCont f x"
   1.655 +by (simp add: isUCont_def isCont_def LIM_def, meson)
   1.656 +
   1.657 +lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
   1.658 +apply (simp add: isNSUCont_def isUCont_def approx_def)
   1.659 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   1.660 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.661 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.662 +apply (auto simp add: starfun hypreal_minus hypreal_add)
   1.663 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
   1.664 +apply (drule_tac x = u in spec, clarify)
   1.665 +apply (drule_tac x = s in spec, clarify)
   1.666 +apply (subgoal_tac "\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u")
   1.667 +prefer 2 apply blast
   1.668 +apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
   1.669 +apply (drule FreeUltrafilterNat_all, ultra)
   1.670 +done
   1.671 +
   1.672 +lemma lemma_LIMu: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
   1.673 +      ==> \<forall>n::nat. \<exists>z y.
   1.674 +               \<bar>z + -y\<bar> < inverse(real(Suc n)) &
   1.675 +               r \<le> \<bar>f z + -f y\<bar>"
   1.676 +apply clarify
   1.677 +apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
   1.678 +done
   1.679 +
   1.680 +lemma lemma_skolemize_LIM2u: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
   1.681 +      ==> \<exists>X Y. \<forall>n::nat.
   1.682 +               abs(X n + -(Y n)) < inverse(real(Suc n)) &
   1.683 +               r \<le> abs(f (X n) + -f (Y n))"
   1.684 +apply (drule lemma_LIMu)
   1.685 +apply (drule choice, safe)
   1.686 +apply (drule choice, blast)
   1.687 +done
   1.688 +
   1.689 +lemma lemma_simpu: "\<forall>n. \<bar>X n + -Y n\<bar> < inverse (real(Suc n)) &
   1.690 +          r \<le> abs (f (X n) + - f(Y n)) ==>
   1.691 +          \<forall>n. \<bar>X n + - Y n\<bar> < inverse (real(Suc n))"
   1.692 +apply auto
   1.693 +done
   1.694 +
   1.695 +lemma isNSUCont_isUCont:
   1.696 +     "isNSUCont f ==> isUCont f"
   1.697 +apply (simp add: isNSUCont_def isUCont_def approx_def)
   1.698 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
   1.699 +apply (rule ccontr, simp) 
   1.700 +apply (simp add: linorder_not_less)
   1.701 +apply (drule lemma_skolemize_LIM2u, safe)
   1.702 +apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
   1.703 +apply (drule_tac x = "Abs_hypreal (hyprel``{Y}) " in spec)
   1.704 +apply (simp add: starfun hypreal_minus hypreal_add, auto)
   1.705 +apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
   1.706 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
   1.707 +apply (rotate_tac 2)
   1.708 +apply (drule_tac x = r in spec, clarify)
   1.709 +apply (drule FreeUltrafilterNat_all, ultra)
   1.710 +done
   1.711 +
   1.712 +text{*Derivatives*}
   1.713 +lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)"
   1.714 +by (simp add: deriv_def)
   1.715 +
   1.716 +lemma DERIV_NS_iff:
   1.717 +      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"
   1.718 +by (simp add: deriv_def LIM_NSLIM_iff)
   1.719 +
   1.720 +lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"
   1.721 +by (simp add: deriv_def)
   1.722 +
   1.723 +lemma NS_DERIV_D: "DERIV f x :> D ==>
   1.724 +           (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"
   1.725 +by (simp add: deriv_def LIM_NSLIM_iff)
   1.726 +
   1.727 +subsubsection{*Uniqueness*}
   1.728 +
   1.729 +lemma DERIV_unique:
   1.730 +      "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
   1.731 +apply (simp add: deriv_def)
   1.732 +apply (blast intro: LIM_unique)
   1.733 +done
   1.734 +
   1.735 +lemma NSDeriv_unique:
   1.736 +     "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"
   1.737 +apply (simp add: nsderiv_def)
   1.738 +apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero)
   1.739 +apply (auto dest!: bspec [where x=epsilon] 
   1.740 +            intro!: inj_hypreal_of_real [THEN injD] 
   1.741 +            dest: approx_trans3)
   1.742 +done
   1.743 +
   1.744 +subsubsection{*Differentiable*}
   1.745 +
   1.746 +lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
   1.747 +by (simp add: differentiable_def)
   1.748 +
   1.749 +lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
   1.750 +by (force simp add: differentiable_def)
   1.751 +
   1.752 +lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
   1.753 +by (simp add: NSdifferentiable_def)
   1.754 +
   1.755 +lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
   1.756 +by (force simp add: NSdifferentiable_def)
   1.757 +
   1.758 +subsubsection{*Alternative definition for differentiability*}
   1.759 +
   1.760 +lemma LIM_I:
   1.761 +     "(!!r. 0<r ==> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))
   1.762 +      ==> f -- a --> L"
   1.763 +by (simp add: LIM_eq)
   1.764 +
   1.765 +lemma DERIV_LIM_iff:
   1.766 +     "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
   1.767 +      ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
   1.768 +proof (intro iffI LIM_I)
   1.769 +  fix r::real
   1.770 +  assume r: "0<r"
   1.771 +  assume "(\<lambda>h. (f (a + h) - f a) / h) -- 0 --> D"
   1.772 +  from LIM_D [OF this r]
   1.773 +  obtain s
   1.774 +    where s:    "0 < s"
   1.775 +      and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
   1.776 +  by auto
   1.777 +  show "\<exists>s. 0 < s \<and>
   1.778 +            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>(f x - f a) / (x-a) - D\<bar> < r)"
   1.779 +  proof (intro exI conjI strip)
   1.780 +    show "0 < s"  by (rule s)
   1.781 +  next
   1.782 +    fix x::real
   1.783 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s"
   1.784 +    with s_lt [THEN spec [where x="x-a"]]
   1.785 +    show "\<bar>(f x - f a) / (x-a) - D\<bar> < r" by auto
   1.786 +  qed
   1.787 +next
   1.788 +  fix r::real
   1.789 +  assume r: "0<r"
   1.790 +  assume "(\<lambda>x. (f x - f a) / (x-a)) -- a --> D"
   1.791 +  from LIM_D [OF this r]
   1.792 +  obtain s
   1.793 +    where s:    "0 < s"
   1.794 +      and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
   1.795 +  by auto
   1.796 +  show "\<exists>s. 0 < s \<and>
   1.797 +            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r)"
   1.798 +  proof (intro exI conjI strip)
   1.799 +    show "0 < s"  by (rule s)
   1.800 +  next
   1.801 +    fix x::real
   1.802 +    assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s"
   1.803 +    with s_lt [THEN spec [where x="x+a"]]
   1.804 +    show "\<bar>(f (a + x) - f a) / x - D\<bar> < r" by (auto simp add: add_ac)
   1.805 +  qed
   1.806 +qed
   1.807 +
   1.808 +lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
   1.809 +by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
   1.810 +
   1.811 +
   1.812 +subsection{*Equivalence of NS and standard definitions of differentiation*}
   1.813 +
   1.814 +text{*First NSDERIV in terms of NSLIM*}
   1.815 +
   1.816 +(*--- first equivalence ---*)
   1.817 +lemma NSDERIV_NSLIM_iff:
   1.818 +      "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"
   1.819 +apply (simp add: nsderiv_def NSLIM_def, auto)
   1.820 +apply (drule_tac x = xa in bspec)
   1.821 +apply (rule_tac [3] ccontr)
   1.822 +apply (drule_tac [3] x = h in spec)
   1.823 +apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
   1.824 +done
   1.825 +
   1.826 +(*--- second equivalence ---*)
   1.827 +lemma NSDERIV_NSLIM_iff2:
   1.828 +     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
   1.829 +by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric] 
   1.830 +              LIM_NSLIM_iff [symmetric])
   1.831 +
   1.832 +(* while we're at it! *)
   1.833 +lemma NSDERIV_iff2:
   1.834 +     "(NSDERIV f x :> D) =
   1.835 +      (\<forall>w.
   1.836 +        w \<noteq> hypreal_of_real x & w \<approx> hypreal_of_real x -->
   1.837 +        ( *f* (%z. (f z - f x) / (z-x))) w \<approx> hypreal_of_real D)"
   1.838 +by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
   1.839 +
   1.840 +(*FIXME DELETE*)
   1.841 +lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))"
   1.842 +by (auto dest: hypreal_eq_minus_iff [THEN iffD2])
   1.843 +
   1.844 +lemma NSDERIVD5:
   1.845 +  "(NSDERIV f x :> D) ==>
   1.846 +   (\<forall>u. u \<approx> hypreal_of_real x -->
   1.847 +     ( *f* (%z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
   1.848 +apply (auto simp add: NSDERIV_iff2)
   1.849 +apply (case_tac "u = hypreal_of_real x", auto)
   1.850 +apply (drule_tac x = u in spec, auto)
   1.851 +apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
   1.852 +apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
   1.853 +apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
   1.854 +apply (auto simp add: diff_minus
   1.855 +	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
   1.856 +		     Infinitesimal_subset_HFinite [THEN subsetD])
   1.857 +done
   1.858 +
   1.859 +lemma NSDERIVD4:
   1.860 +     "(NSDERIV f x :> D) ==>
   1.861 +      (\<forall>h \<in> Infinitesimal.
   1.862 +               (( *f* f)(hypreal_of_real x + h) -
   1.863 +                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
   1.864 +apply (auto simp add: nsderiv_def)
   1.865 +apply (case_tac "h = (0::hypreal) ")
   1.866 +apply (auto simp add: diff_minus)
   1.867 +apply (drule_tac x = h in bspec)
   1.868 +apply (drule_tac [2] c = h in approx_mult1)
   1.869 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.870 +            simp add: diff_minus)
   1.871 +done
   1.872 +
   1.873 +lemma NSDERIVD3:
   1.874 +     "(NSDERIV f x :> D) ==>
   1.875 +      (\<forall>h \<in> Infinitesimal - {0}.
   1.876 +               (( *f* f)(hypreal_of_real x + h) -
   1.877 +                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
   1.878 +apply (auto simp add: nsderiv_def)
   1.879 +apply (rule ccontr, drule_tac x = h in bspec)
   1.880 +apply (drule_tac [2] c = h in approx_mult1)
   1.881 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.882 +            simp add: mult_assoc diff_minus)
   1.883 +done
   1.884 +
   1.885 +text{*Now equivalence between NSDERIV and DERIV*}
   1.886 +lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
   1.887 +by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
   1.888 +
   1.889 +(*---------------------------------------------------
   1.890 +         Differentiability implies continuity
   1.891 +         nice and simple "algebraic" proof
   1.892 + --------------------------------------------------*)
   1.893 +lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
   1.894 +apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
   1.895 +apply (drule approx_minus_iff [THEN iffD1])
   1.896 +apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
   1.897 +apply (drule_tac x = "-hypreal_of_real x + xa" in bspec)
   1.898 + prefer 2 apply (simp add: add_assoc [symmetric]) 
   1.899 +apply (auto simp add: mem_infmal_iff [symmetric] hypreal_add_commute)
   1.900 +apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1)
   1.901 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
   1.902 +            simp add: mult_assoc)
   1.903 +apply (drule_tac x3=D in
   1.904 +           HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
   1.905 +             THEN mem_infmal_iff [THEN iffD1]])
   1.906 +apply (auto simp add: mult_commute 
   1.907 +            intro: approx_trans approx_minus_iff [THEN iffD2])
   1.908 +done
   1.909 +
   1.910 +text{*Now Sandard proof*}
   1.911 +lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x"
   1.912 +by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric] 
   1.913 +              NSDERIV_isNSCont)
   1.914 +
   1.915 +
   1.916 +(*----------------------------------------------------------------------------
   1.917 +      Differentiation rules for combinations of functions
   1.918 +      follow from clear, straightforard, algebraic
   1.919 +      manipulations
   1.920 + ----------------------------------------------------------------------------*)
   1.921 +text{*Constant function*}
   1.922 +
   1.923 +(* use simple constant nslimit theorem *)
   1.924 +lemma NSDERIV_const: "(NSDERIV (%x. k) x :> 0)"
   1.925 +by (simp add: NSDERIV_NSLIM_iff)
   1.926 +declare NSDERIV_const [simp]
   1.927 +
   1.928 +lemma DERIV_const: "(DERIV (%x. k) x :> 0)"
   1.929 +by (simp add: NSDERIV_DERIV_iff [symmetric])
   1.930 +declare DERIV_const [simp]
   1.931 +
   1.932 +(*-----------------------------------------------------
   1.933 +    Sum of functions- proved easily
   1.934 + ----------------------------------------------------*)
   1.935 +
   1.936 +
   1.937 +lemma NSDERIV_add: "[| NSDERIV f x :> Da;  NSDERIV g x :> Db |]
   1.938 +      ==> NSDERIV (%x. f x + g x) x :> Da + Db"
   1.939 +apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   1.940 +apply (auto simp add: add_divide_distrib dest!: spec)
   1.941 +apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add)
   1.942 +apply (auto simp add: add_ac)
   1.943 +done
   1.944 +
   1.945 +(* Standard theorem *)
   1.946 +lemma DERIV_add: "[| DERIV f x :> Da; DERIV g x :> Db |]
   1.947 +      ==> DERIV (%x. f x + g x) x :> Da + Db"
   1.948 +apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric])
   1.949 +done
   1.950 +
   1.951 +(*-----------------------------------------------------
   1.952 +  Product of functions - Proof is trivial but tedious
   1.953 +  and long due to rearrangement of terms
   1.954 + ----------------------------------------------------*)
   1.955 +
   1.956 +lemma lemma_nsderiv1: "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"
   1.957 +by (simp add: right_distrib)
   1.958 +
   1.959 +lemma lemma_nsderiv2: "[| (x + y) / z = hypreal_of_real D + yb; z \<noteq> 0;
   1.960 +         z \<in> Infinitesimal; yb \<in> Infinitesimal |]
   1.961 +      ==> x + y \<approx> 0"
   1.962 +apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
   1.963 +apply (erule_tac V = " (x + y) / z = hypreal_of_real D + yb" in thin_rl)
   1.964 +apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
   1.965 +            simp add: hypreal_mult_assoc mem_infmal_iff [symmetric])
   1.966 +apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   1.967 +done
   1.968 +
   1.969 +
   1.970 +lemma NSDERIV_mult: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
   1.971 +      ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
   1.972 +apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   1.973 +apply (auto dest!: spec
   1.974 +	    simp add: starfun_lambda_cancel lemma_nsderiv1)
   1.975 +apply (simp (no_asm) add: add_divide_distrib)
   1.976 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   1.977 +apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
   1.978 +apply (drule_tac D = Db in lemma_nsderiv2)
   1.979 +apply (drule_tac [4]
   1.980 +     approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) 
   1.981 +apply (auto intro!: approx_add_mono1 
   1.982 +            simp add: left_distrib right_distrib mult_commute add_assoc)
   1.983 +apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)" 
   1.984 +         in add_commute [THEN subst])
   1.985 +apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] 
   1.986 +                    Infinitesimal_add Infinitesimal_mult 
   1.987 +                    Infinitesimal_hypreal_of_real_mult 
   1.988 +                    Infinitesimal_hypreal_of_real_mult2
   1.989 +          simp add: add_assoc [symmetric])
   1.990 +done
   1.991 +
   1.992 +lemma DERIV_mult:
   1.993 +     "[| DERIV f x :> Da; DERIV g x :> Db |] 
   1.994 +      ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
   1.995 +by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
   1.996 +
   1.997 +text{*Multiplying by a constant*}
   1.998 +lemma NSDERIV_cmult: "NSDERIV f x :> D
   1.999 +      ==> NSDERIV (%x. c * f x) x :> c*D"
  1.1000 +apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 
  1.1001 +                  minus_mult_right right_distrib [symmetric])
  1.1002 +apply (erule NSLIM_const [THEN NSLIM_mult])
  1.1003 +done
  1.1004 +
  1.1005 +(* let's do the standard proof though theorem *)
  1.1006 +(* LIM_mult2 follows from a NS proof          *)
  1.1007 +
  1.1008 +lemma DERIV_cmult:
  1.1009 +      "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
  1.1010 +apply (simp only: deriv_def times_divide_eq_right [symmetric] 
  1.1011 +                  NSDERIV_NSLIM_iff minus_mult_right right_distrib [symmetric])
  1.1012 +apply (erule LIM_const [THEN LIM_mult2])
  1.1013 +done
  1.1014 +
  1.1015 +text{*Negation of function*}
  1.1016 +lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
  1.1017 +proof (simp add: NSDERIV_NSLIM_iff)
  1.1018 +  assume "(\<lambda>h. (f (x + h) + - f x) / h) -- 0 --NS> D"
  1.1019 +  hence deriv: "(\<lambda>h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D" 
  1.1020 +    by (rule NSLIM_minus)
  1.1021 +  have "\<forall>h. - ((f (x + h) + - f x) / h) = (- f (x + h) + f x) / h"
  1.1022 +    by (simp add: minus_divide_left) 
  1.1023 +  with deriv
  1.1024 +  show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
  1.1025 +qed
  1.1026 +
  1.1027 +
  1.1028 +lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. -(f x)) x :> -D"
  1.1029 +by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric])
  1.1030 +
  1.1031 +text{*Subtraction*}
  1.1032 +lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"
  1.1033 +by (blast dest: NSDERIV_add NSDERIV_minus)
  1.1034 +
  1.1035 +lemma DERIV_add_minus: "[| DERIV f x :> Da; DERIV g x :> Db |] ==> DERIV (%x. f x + -g x) x :> Da + -Db"
  1.1036 +by (blast dest: DERIV_add DERIV_minus)
  1.1037 +
  1.1038 +lemma NSDERIV_diff:
  1.1039 +     "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
  1.1040 +      ==> NSDERIV (%x. f x - g x) x :> Da-Db"
  1.1041 +apply (simp add: diff_minus)
  1.1042 +apply (blast intro: NSDERIV_add_minus)
  1.1043 +done
  1.1044 +
  1.1045 +lemma DERIV_diff:
  1.1046 +     "[| DERIV f x :> Da; DERIV g x :> Db |]
  1.1047 +       ==> DERIV (%x. f x - g x) x :> Da-Db"
  1.1048 +apply (simp add: diff_minus)
  1.1049 +apply (blast intro: DERIV_add_minus)
  1.1050 +done
  1.1051 +
  1.1052 +(*---------------------------------------------------------------
  1.1053 +                     (NS) Increment
  1.1054 + ---------------------------------------------------------------*)
  1.1055 +lemma incrementI:
  1.1056 +      "f NSdifferentiable x ==>
  1.1057 +      increment f x h = ( *f* f) (hypreal_of_real(x) + h) +
  1.1058 +      -hypreal_of_real (f x)"
  1.1059 +by (simp add: increment_def)
  1.1060 +
  1.1061 +lemma incrementI2: "NSDERIV f x :> D ==>
  1.1062 +     increment f x h = ( *f* f) (hypreal_of_real(x) + h) +
  1.1063 +     -hypreal_of_real (f x)"
  1.1064 +apply (erule NSdifferentiableI [THEN incrementI])
  1.1065 +done
  1.1066 +
  1.1067 +(* The Increment theorem -- Keisler p. 65 *)
  1.1068 +lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
  1.1069 +      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
  1.1070 +apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
  1.1071 +apply (drule bspec, auto)
  1.1072 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) 
  1.1073 +apply (frule_tac b1 = "hypreal_of_real (D) + y" 
  1.1074 +        in hypreal_mult_right_cancel [THEN iffD2])
  1.1075 +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.1076 +apply assumption
  1.1077 +apply (simp add: times_divide_eq_right [symmetric] del: times_divide_eq_right)
  1.1078 +apply (auto simp add: left_distrib)
  1.1079 +done
  1.1080 + 
  1.1081 +lemma increment_thm2:
  1.1082 +     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
  1.1083 +      ==> \<exists>e \<in> Infinitesimal. increment f x h =
  1.1084 +              hypreal_of_real(D)*h + e*h"
  1.1085 +by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
  1.1086 +
  1.1087 +
  1.1088 +lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
  1.1089 +      ==> increment f x h \<approx> 0"
  1.1090 +apply (drule increment_thm2, 
  1.1091 +       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
  1.1092 +apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
  1.1093 +done
  1.1094 +
  1.1095 +text{*  Similarly to the above, the chain rule admits an entirely
  1.1096 +   straightforward derivation. Compare this with Harrison's
  1.1097 +   HOL proof of the chain rule, which proved to be trickier and
  1.1098 +   required an alternative characterisation of differentiability-
  1.1099 +   the so-called Carathedory derivative. Our main problem is
  1.1100 +   manipulation of terms.*}
  1.1101 +
  1.1102 +
  1.1103 +(* lemmas *)
  1.1104 +lemma NSDERIV_zero:
  1.1105 +      "[| NSDERIV g x :> D;
  1.1106 +               ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);
  1.1107 +               xa \<in> Infinitesimal;
  1.1108 +               xa \<noteq> 0
  1.1109 +            |] ==> D = 0"
  1.1110 +apply (simp add: nsderiv_def)
  1.1111 +apply (drule bspec, auto)
  1.1112 +done
  1.1113 +
  1.1114 +(* can be proved differently using NSLIM_isCont_iff *)
  1.1115 +lemma NSDERIV_approx:
  1.1116 +     "[| NSDERIV f x :> D;  h \<in> Infinitesimal;  h \<noteq> 0 |]
  1.1117 +      ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \<approx> 0"
  1.1118 +apply (simp add: nsderiv_def)
  1.1119 +apply (simp add: mem_infmal_iff [symmetric])
  1.1120 +apply (rule Infinitesimal_ratio)
  1.1121 +apply (rule_tac [3] approx_hypreal_of_real_HFinite, auto)
  1.1122 +done
  1.1123 +
  1.1124 +(*---------------------------------------------------------------
  1.1125 +   from one version of differentiability
  1.1126 +
  1.1127 +                f(x) - f(a)
  1.1128 +              --------------- \<approx> Db
  1.1129 +                  x - a
  1.1130 + ---------------------------------------------------------------*)
  1.1131 +lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
  1.1132 +         ( *f* g) (hypreal_of_real(x) + xa) \<noteq> hypreal_of_real (g x);
  1.1133 +         ( *f* g) (hypreal_of_real(x) + xa) \<approx> hypreal_of_real (g x)
  1.1134 +      |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa))
  1.1135 +                   + - hypreal_of_real (f (g x)))
  1.1136 +              / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x))
  1.1137 +             \<approx> hypreal_of_real(Da)"
  1.1138 +by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric])
  1.1139 +
  1.1140 +(*--------------------------------------------------------------
  1.1141 +   from other version of differentiability
  1.1142 +
  1.1143 +                f(x + h) - f(x)
  1.1144 +               ----------------- \<approx> Db
  1.1145 +                       h
  1.1146 + --------------------------------------------------------------*)
  1.1147 +lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
  1.1148 +      ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa
  1.1149 +          \<approx> hypreal_of_real(Db)"
  1.1150 +by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
  1.1151 +
  1.1152 +lemma lemma_chain: "(z::hypreal) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
  1.1153 +by auto
  1.1154 +
  1.1155 +(*------------------------------------------------------
  1.1156 +  This proof uses both definitions of differentiability.
  1.1157 + ------------------------------------------------------*)
  1.1158 +lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
  1.1159 +      ==> NSDERIV (f o g) x :> Da * Db"
  1.1160 +apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
  1.1161 +                mem_infmal_iff [symmetric])
  1.1162 +apply clarify
  1.1163 +apply (frule_tac f = g in NSDERIV_approx)
  1.1164 +apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
  1.1165 +apply (case_tac "( *f* g) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ")
  1.1166 +apply (drule_tac g = g in NSDERIV_zero)
  1.1167 +apply (auto simp add: divide_inverse)
  1.1168 +apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa) + -hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst])
  1.1169 +apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
  1.1170 +apply (rule approx_mult_hypreal_of_real)
  1.1171 +apply (simp_all add: divide_inverse [symmetric])
  1.1172 +apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
  1.1173 +apply (blast intro: NSDERIVD2)
  1.1174 +done
  1.1175 +
  1.1176 +(* standard version *)
  1.1177 +lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
  1.1178 +by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
  1.1179 +
  1.1180 +lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
  1.1181 +by (auto dest: DERIV_chain simp add: o_def)
  1.1182 +
  1.1183 +text{*Differentiation of natural number powers*}
  1.1184 +lemma NSDERIV_Id: "NSDERIV (%x. x) x :> 1"
  1.1185 +by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def starfun_Id)
  1.1186 +declare NSDERIV_Id [simp]
  1.1187 +
  1.1188 +(*derivative of the identity function*)
  1.1189 +lemma DERIV_Id: "DERIV (%x. x) x :> 1"
  1.1190 +by (simp add: NSDERIV_DERIV_iff [symmetric])
  1.1191 +declare DERIV_Id [simp]
  1.1192 +
  1.1193 +lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
  1.1194 +
  1.1195 +(*derivative of linear multiplication*)
  1.1196 +lemma DERIV_cmult_Id: "DERIV (op * c) x :> c"
  1.1197 +by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
  1.1198 +declare DERIV_cmult_Id [simp]
  1.1199 +
  1.1200 +lemma NSDERIV_cmult_Id: "NSDERIV (op * c) x :> c"
  1.1201 +by (simp add: NSDERIV_DERIV_iff)
  1.1202 +declare NSDERIV_cmult_Id [simp]
  1.1203 +
  1.1204 +lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
  1.1205 +apply (induct_tac "n")
  1.1206 +apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
  1.1207 +apply (auto simp add: real_of_nat_Suc left_distrib)
  1.1208 +apply (case_tac "0 < n")
  1.1209 +apply (drule_tac x = x in realpow_minus_mult)
  1.1210 +apply (auto simp add: real_mult_assoc real_add_commute)
  1.1211 +done
  1.1212 +
  1.1213 +(* NS version *)
  1.1214 +lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
  1.1215 +by (simp add: NSDERIV_DERIV_iff DERIV_pow)
  1.1216 +
  1.1217 +(*---------------------------------------------------------------
  1.1218 +                    Power of -1
  1.1219 + ---------------------------------------------------------------*)
  1.1220 +
  1.1221 +(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
  1.1222 +lemma NSDERIV_inverse:
  1.1223 +     "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
  1.1224 +apply (simp add: nsderiv_def)
  1.1225 +apply (rule ballI, simp, clarify) 
  1.1226 +apply (frule Infinitesimal_add_not_zero)
  1.1227 +prefer 2 apply (simp add: add_commute) 
  1.1228 +apply (auto simp add: starfun_inverse_inverse realpow_two 
  1.1229 +        simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
  1.1230 +apply (simp add: inverse_add inverse_mult_distrib [symmetric]
  1.1231 +              inverse_minus_eq [symmetric] add_ac mult_ac
  1.1232 +            del: inverse_mult_distrib inverse_minus_eq 
  1.1233 +                 minus_mult_left [symmetric] minus_mult_right [symmetric])
  1.1234 +apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
  1.1235 +            del: minus_mult_left [symmetric] minus_mult_right [symmetric])
  1.1236 +apply (rule_tac y = " inverse (- hypreal_of_real x * hypreal_of_real x) " in approx_trans)
  1.1237 +apply (rule inverse_add_Infinitesimal_approx2)
  1.1238 +apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal 
  1.1239 +            simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
  1.1240 +apply (rule Infinitesimal_HFinite_mult2, auto)
  1.1241 +done
  1.1242 +
  1.1243 +
  1.1244 +
  1.1245 +
  1.1246 +lemma DERIV_inverse: "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
  1.1247 +by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc)
  1.1248 +
  1.1249 +text{*Derivative of inverse*}
  1.1250 +lemma DERIV_inverse_fun: "[| DERIV f x :> d; f(x) \<noteq> 0 |]
  1.1251 +      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
  1.1252 +apply (simp only: mult_commute [of d] minus_mult_left power_inverse)
  1.1253 +apply (fold o_def)
  1.1254 +apply (blast intro!: DERIV_chain DERIV_inverse)
  1.1255 +done
  1.1256 +
  1.1257 +lemma NSDERIV_inverse_fun: "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
  1.1258 +      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
  1.1259 +by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc)
  1.1260 +
  1.1261 +text{*Derivative of quotient*}
  1.1262 +lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
  1.1263 +       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"
  1.1264 +apply (drule_tac f = g in DERIV_inverse_fun)
  1.1265 +apply (drule_tac [2] DERIV_mult)
  1.1266 +apply (assumption+)
  1.1267 +apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
  1.1268 +                 mult_ac 
  1.1269 +     del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
  1.1270 +done
  1.1271 +
  1.1272 +lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
  1.1273 +       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
  1.1274 +                            + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"
  1.1275 +by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
  1.1276 +
  1.1277 +(* ------------------------------------------------------------------------ *)
  1.1278 +(* Caratheodory formulation of derivative at a point: standard proof        *)
  1.1279 +(* ------------------------------------------------------------------------ *)
  1.1280 +
  1.1281 +lemma CARAT_DERIV:
  1.1282 +     "(DERIV f x :> l) =
  1.1283 +      (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
  1.1284 +      (is "?lhs = ?rhs")
  1.1285 +proof
  1.1286 +  assume der: "DERIV f x :> l"
  1.1287 +  show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
  1.1288 +  proof (intro exI conjI)
  1.1289 +    let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
  1.1290 +    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
  1.1291 +    show "isCont ?g x" using der 
  1.1292 +      by (simp add: isCont_iff DERIV_iff diff_minus 
  1.1293 +               cong: LIM_equal [rule_format])
  1.1294 +    show "?g x = l" by simp
  1.1295 +  qed
  1.1296 +next
  1.1297 +  assume "?rhs"
  1.1298 +  then obtain g where 
  1.1299 +    "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
  1.1300 +  thus "(DERIV f x :> l)" 
  1.1301 +     by (auto simp add: isCont_iff DERIV_iff diff_minus 
  1.1302 +               cong: LIM_equal [rule_format])
  1.1303 +qed
  1.1304 +
  1.1305 +
  1.1306 +lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
  1.1307 +      \<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isNSCont g x & g x = l"
  1.1308 +by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV)
  1.1309 +
  1.1310 +lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
  1.1311 +by auto
  1.1312 +
  1.1313 +lemma CARAT_DERIVD:
  1.1314 +  assumes all: "\<forall>z. f z - f x = g z * (z-x)"
  1.1315 +      and nsc: "isNSCont g x"
  1.1316 +  shows "NSDERIV f x :> g x"
  1.1317 +proof -
  1.1318 +  from nsc
  1.1319 +  have "\<forall>w. w \<noteq> hypreal_of_real x \<and> w \<approx> hypreal_of_real x \<longrightarrow>
  1.1320 +         ( *f* g) w * (w - hypreal_of_real x) / (w - hypreal_of_real x) \<approx>
  1.1321 +         hypreal_of_real (g x)" 
  1.1322 +    by (simp add: diff_minus isNSCont_def)
  1.1323 +  thus ?thesis using all
  1.1324 +    by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) 
  1.1325 +qed
  1.1326 +
  1.1327 +(*--------------------------------------------------------------------------*)
  1.1328 +(* Lemmas about nested intervals and proof by bisection (cf.Harrison)       *)
  1.1329 +(* All considerably tidied by lcp                                           *)
  1.1330 +(*--------------------------------------------------------------------------*)
  1.1331 +
  1.1332 +lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
  1.1333 +apply (induct_tac "no")
  1.1334 +apply (auto intro: order_trans)
  1.1335 +done
  1.1336 +
  1.1337 +lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
  1.1338 +         \<forall>n. g(Suc n) \<le> g(n);
  1.1339 +         \<forall>n. f(n) \<le> g(n) |]
  1.1340 +      ==> Bseq f"
  1.1341 +apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
  1.1342 +apply (induct_tac "n")
  1.1343 +apply (auto intro: order_trans)
  1.1344 +apply (rule_tac y = "g (Suc na) " in order_trans)
  1.1345 +apply (induct_tac [2] "na")
  1.1346 +apply (auto intro: order_trans)
  1.1347 +done
  1.1348 +
  1.1349 +lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
  1.1350 +         \<forall>n. g(Suc n) \<le> g(n);
  1.1351 +         \<forall>n. f(n) \<le> g(n) |]
  1.1352 +      ==> Bseq g"
  1.1353 +apply (subst Bseq_minus_iff [symmetric])
  1.1354 +apply (rule_tac g = "%x. - (f x) " in f_inc_g_dec_Beq_f)
  1.1355 +apply auto
  1.1356 +done
  1.1357 +
  1.1358 +lemma f_inc_imp_le_lim: "[| \<forall>n. f n \<le> f (Suc n);  convergent f |] ==> f n \<le> lim f"
  1.1359 +apply (rule linorder_not_less [THEN iffD1])
  1.1360 +apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
  1.1361 +apply (drule real_less_sum_gt_zero)
  1.1362 +apply (drule_tac x = "f n + - lim f" in spec, safe)
  1.1363 +apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
  1.1364 +apply (subgoal_tac "lim f \<le> f (no + n) ")
  1.1365 +apply (induct_tac [2] "no")
  1.1366 +apply (auto intro: order_trans simp add: diff_minus real_abs_def)
  1.1367 +apply (drule_tac no=no and m=n in lemma_f_mono_add)
  1.1368 +apply (auto simp add: add_commute)
  1.1369 +done
  1.1370 +
  1.1371 +lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)"
  1.1372 +apply (rule LIMSEQ_minus [THEN limI])
  1.1373 +apply (simp add: convergent_LIMSEQ_iff)
  1.1374 +done
  1.1375 +
  1.1376 +lemma g_dec_imp_lim_le: "[| \<forall>n. g(Suc n) \<le> g(n);  convergent g |] ==> lim g \<le> g n"
  1.1377 +apply (subgoal_tac "- (g n) \<le> - (lim g) ")
  1.1378 +apply (cut_tac [2] f = "%x. - (g x) " in f_inc_imp_le_lim)
  1.1379 +apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
  1.1380 +done
  1.1381 +
  1.1382 +lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
  1.1383 +         \<forall>n. g(Suc n) \<le> g(n);
  1.1384 +         \<forall>n. f(n) \<le> g(n) |]
  1.1385 +      ==> \<exists>l m. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
  1.1386 +                            ((\<forall>n. m \<le> g(n)) & g ----> m)"
  1.1387 +apply (subgoal_tac "monoseq f & monoseq g")
  1.1388 +prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
  1.1389 +apply (subgoal_tac "Bseq f & Bseq g")
  1.1390 +prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g)
  1.1391 +apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff)
  1.1392 +apply (rule_tac x = "lim f" in exI)
  1.1393 +apply (rule_tac x = "lim g" in exI)
  1.1394 +apply (auto intro: LIMSEQ_le)
  1.1395 +apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff)
  1.1396 +done
  1.1397 +
  1.1398 +lemma lemma_nest_unique: "[| \<forall>n. f(n) \<le> f(Suc n);
  1.1399 +         \<forall>n. g(Suc n) \<le> g(n);
  1.1400 +         \<forall>n. f(n) \<le> g(n);
  1.1401 +         (%n. f(n) - g(n)) ----> 0 |]
  1.1402 +      ==> \<exists>l. ((\<forall>n. f(n) \<le> l) & f ----> l) &
  1.1403 +                ((\<forall>n. l \<le> g(n)) & g ----> l)"
  1.1404 +apply (drule lemma_nest, auto)
  1.1405 +apply (subgoal_tac "l = m")
  1.1406 +apply (drule_tac [2] X = f in LIMSEQ_diff)
  1.1407 +apply (auto intro: LIMSEQ_unique)
  1.1408 +done
  1.1409 +
  1.1410 +text{*The universal quantifiers below are required for the declaration
  1.1411 +  of @{text Bolzano_nest_unique} below.*}
  1.1412 +
  1.1413 +lemma Bolzano_bisect_le:
  1.1414 + "a \<le> b ==> \<forall>n. fst (Bolzano_bisect P a b n) \<le> snd (Bolzano_bisect P a b n)"
  1.1415 +apply (rule allI)
  1.1416 +apply (induct_tac "n")
  1.1417 +apply (auto simp add: Let_def split_def)
  1.1418 +done
  1.1419 +
  1.1420 +lemma Bolzano_bisect_fst_le_Suc: "a \<le> b ==>
  1.1421 +   \<forall>n. fst(Bolzano_bisect P a b n) \<le> fst (Bolzano_bisect P a b (Suc n))"
  1.1422 +apply (rule allI)
  1.1423 +apply (induct_tac "n")
  1.1424 +apply (auto simp add: Bolzano_bisect_le Let_def split_def)
  1.1425 +done
  1.1426 +
  1.1427 +lemma Bolzano_bisect_Suc_le_snd: "a \<le> b ==>
  1.1428 +   \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
  1.1429 +apply (rule allI)
  1.1430 +apply (induct_tac "n")
  1.1431 +apply (auto simp add: Bolzano_bisect_le Let_def split_def)
  1.1432 +done
  1.1433 +
  1.1434 +lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
  1.1435 +apply auto
  1.1436 +apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
  1.1437 +apply auto
  1.1438 +done
  1.1439 +
  1.1440 +lemma Bolzano_bisect_diff:
  1.1441 +     "a \<le> b ==>
  1.1442 +      snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
  1.1443 +      (b-a) / (2 ^ n)"
  1.1444 +apply (induct_tac "n")
  1.1445 +apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def)
  1.1446 +apply (auto simp add: add_ac Bolzano_bisect_le diff_minus)
  1.1447 +done
  1.1448 +
  1.1449 +lemmas Bolzano_nest_unique =
  1.1450 +    lemma_nest_unique
  1.1451 +    [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le]
  1.1452 +
  1.1453 +
  1.1454 +lemma not_P_Bolzano_bisect:
  1.1455 +  assumes P:    "!!a b c. [| P(a,b); P(b,c); a \<le> b; b \<le> c|] ==> P(a,c)"
  1.1456 +      and notP: "~ P(a,b)"
  1.1457 +      and le:   "a \<le> b"
  1.1458 +  shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
  1.1459 +proof (induct n)
  1.1460 +  case 0 thus ?case by simp
  1.1461 + next
  1.1462 +  case (Suc n)
  1.1463 +  thus ?case
  1.1464 + by (auto simp del: surjective_pairing [symmetric] 
  1.1465 +             simp add: Let_def split_def Bolzano_bisect_le [OF le] 
  1.1466 +     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"]) 
  1.1467 +qed
  1.1468 +
  1.1469 +(*Now we re-package P_prem as a formula*)
  1.1470 +lemma not_P_Bolzano_bisect':
  1.1471 +     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
  1.1472 +         ~ P(a,b);  a \<le> b |] ==>
  1.1473 +      \<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
  1.1474 +by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE])
  1.1475 +
  1.1476 +
  1.1477 +
  1.1478 +lemma lemma_BOLZANO:
  1.1479 +     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
  1.1480 +         \<forall>x. \<exists>d::real. 0 < d &
  1.1481 +                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
  1.1482 +         a \<le> b |]
  1.1483 +      ==> P(a,b)"
  1.1484 +apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
  1.1485 +apply (rule LIMSEQ_minus_cancel)
  1.1486 +apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
  1.1487 +apply (rule ccontr)
  1.1488 +apply (drule not_P_Bolzano_bisect', assumption+)
  1.1489 +apply (rename_tac "l")
  1.1490 +apply (drule_tac x = l in spec, clarify)
  1.1491 +apply (simp add: LIMSEQ_def)
  1.1492 +apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
  1.1493 +apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
  1.1494 +apply (drule real_less_half_sum, auto) 
  1.1495 +apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec)
  1.1496 +apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
  1.1497 +apply safe
  1.1498 +apply (simp_all (no_asm_simp))
  1.1499 +apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l) " in order_le_less_trans)
  1.1500 +apply (simp (no_asm_simp) add: abs_if)
  1.1501 +apply (rule real_sum_of_halves [THEN subst])
  1.1502 +apply (rule add_strict_mono)
  1.1503 +apply (simp_all add: diff_minus [symmetric])
  1.1504 +done
  1.1505 +
  1.1506 +
  1.1507 +lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
  1.1508 +       (\<forall>x. \<exists>d::real. 0 < d &
  1.1509 +                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b))))
  1.1510 +      --> (\<forall>a b. a \<le> b --> P(a,b))"
  1.1511 +apply clarify
  1.1512 +apply (blast intro: lemma_BOLZANO)
  1.1513 +done
  1.1514 +
  1.1515 +
  1.1516 +subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
  1.1517 +
  1.1518 +lemma IVT: "[| f(a) \<le> y; y \<le> f(b);
  1.1519 +         a \<le> b;
  1.1520 +         (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
  1.1521 +      ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
  1.1522 +apply (rule contrapos_pp, assumption)
  1.1523 +apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2)
  1.1524 +apply safe
  1.1525 +apply simp_all
  1.1526 +apply (simp add: isCont_iff LIM_def)
  1.1527 +apply (rule ccontr)
  1.1528 +apply (subgoal_tac "a \<le> x & x \<le> b")
  1.1529 + prefer 2
  1.1530 + apply simp 
  1.1531 + apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
  1.1532 +apply (drule_tac x = x in spec)+
  1.1533 +apply simp
  1.1534 +apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar> " in spec)
  1.1535 +apply safe
  1.1536 +apply simp
  1.1537 +apply (drule_tac x = s in spec, clarify)
  1.1538 +apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
  1.1539 +apply (drule_tac x = "ba-x" in spec)
  1.1540 +apply (simp_all add: abs_if)
  1.1541 +apply (drule_tac x = "aa-x" in spec)
  1.1542 +apply (case_tac "x \<le> aa", simp_all)
  1.1543 +apply (drule_tac x = x and y = aa in order_antisym)
  1.1544 +apply (assumption, simp)
  1.1545 +done
  1.1546 +
  1.1547 +lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
  1.1548 +         a \<le> b;
  1.1549 +         (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
  1.1550 +      |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
  1.1551 +apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify) 
  1.1552 +apply (drule IVT [where f = "%x. - f x"], assumption)
  1.1553 +apply (auto intro: isCont_minus)
  1.1554 +done
  1.1555 +
  1.1556 +(*HOL style here: object-level formulations*)
  1.1557 +lemma IVT_objl: "(f(a) \<le> y & y \<le> f(b) & a \<le> b &
  1.1558 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
  1.1559 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
  1.1560 +apply (blast intro: IVT)
  1.1561 +done
  1.1562 +
  1.1563 +lemma IVT2_objl: "(f(b) \<le> y & y \<le> f(a) & a \<le> b &
  1.1564 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
  1.1565 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
  1.1566 +apply (blast intro: IVT2)
  1.1567 +done
  1.1568 +
  1.1569 +(*---------------------------------------------------------------------------*)
  1.1570 +(* By bisection, function continuous on closed interval is bounded above     *)
  1.1571 +(*---------------------------------------------------------------------------*)
  1.1572 +
  1.1573 +
  1.1574 +lemma isCont_bounded:
  1.1575 +     "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
  1.1576 +      ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
  1.1577 +apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M) " in lemma_BOLZANO2)
  1.1578 +apply safe
  1.1579 +apply simp_all
  1.1580 +apply (rename_tac x xa ya M Ma)
  1.1581 +apply (cut_tac x = M and y = Ma in linorder_linear, safe)
  1.1582 +apply (rule_tac x = Ma in exI, clarify)
  1.1583 +apply (cut_tac x = xb and y = xa in linorder_linear, force)
  1.1584 +apply (rule_tac x = M in exI, clarify)
  1.1585 +apply (cut_tac x = xb and y = xa in linorder_linear, force)
  1.1586 +apply (case_tac "a \<le> x & x \<le> b")
  1.1587 +apply (rule_tac [2] x = 1 in exI)
  1.1588 +prefer 2 apply force
  1.1589 +apply (simp add: LIM_def isCont_iff)
  1.1590 +apply (drule_tac x = x in spec, auto)
  1.1591 +apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
  1.1592 +apply (drule_tac x = 1 in spec, auto)
  1.1593 +apply (rule_tac x = s in exI, clarify)
  1.1594 +apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
  1.1595 +apply (drule_tac x = "xa-x" in spec)
  1.1596 +apply (auto simp add: abs_ge_self, arith+)
  1.1597 +done
  1.1598 +
  1.1599 +(*----------------------------------------------------------------------------*)
  1.1600 +(* Refine the above to existence of least upper bound                         *)
  1.1601 +(*----------------------------------------------------------------------------*)
  1.1602 +
  1.1603 +lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
  1.1604 +      (\<exists>t. isLub UNIV S t)"
  1.1605 +apply (blast intro: reals_complete)
  1.1606 +done
  1.1607 +
  1.1608 +lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
  1.1609 +         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
  1.1610 +                   (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
  1.1611 +apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x) " in lemma_reals_complete)
  1.1612 +apply auto
  1.1613 +apply (drule isCont_bounded, assumption)
  1.1614 +apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
  1.1615 +apply (rule exI, auto)
  1.1616 +apply (auto dest!: spec simp add: linorder_not_less) 
  1.1617 +done
  1.1618 +
  1.1619 +(*----------------------------------------------------------------------------*)
  1.1620 +(* Now show that it attains its upper bound                                   *)
  1.1621 +(*----------------------------------------------------------------------------*)
  1.1622 +
  1.1623 +lemma isCont_eq_Ub:
  1.1624 +  assumes le: "a \<le> b"
  1.1625 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
  1.1626 +  shows "\<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
  1.1627 +             (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
  1.1628 +proof -
  1.1629 +  from isCont_has_Ub [OF le con]
  1.1630 +  obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
  1.1631 +             and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x"  by blast
  1.1632 +  show ?thesis
  1.1633 +  proof (intro exI, intro conjI)
  1.1634 +    show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
  1.1635 +    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M" 
  1.1636 +    proof (rule ccontr)
  1.1637 +      assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
  1.1638 +      with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
  1.1639 +        by (auto simp add: linorder_not_le [symmetric] intro: order_antisym)
  1.1640 +      hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
  1.1641 +        by (auto simp add: isCont_inverse isCont_diff con)
  1.1642 +      from isCont_bounded [OF le this]
  1.1643 +      obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
  1.1644 +      have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
  1.1645 +        by (simp add: M3) 
  1.1646 +      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k 
  1.1647 +        by (auto intro: order_le_less_trans [of _ k]) 
  1.1648 +      with Minv 
  1.1649 +      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))" 
  1.1650 +        by (intro strip less_imp_inverse_less, simp_all)
  1.1651 +      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x" 
  1.1652 +        by simp
  1.1653 +      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le 
  1.1654 +        by (simp, arith)
  1.1655 +      from M2 [OF this]
  1.1656 +      obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
  1.1657 +      thus False using invlt [of x] by force
  1.1658 +    qed
  1.1659 +  qed
  1.1660 +qed
  1.1661 +
  1.1662 +
  1.1663 +
  1.1664 +(*----------------------------------------------------------------------------*)
  1.1665 +(* Same theorem for lower bound                                               *)
  1.1666 +(*----------------------------------------------------------------------------*)
  1.1667 +
  1.1668 +lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
  1.1669 +         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
  1.1670 +                   (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
  1.1671 +apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
  1.1672 +prefer 2 apply (blast intro: isCont_minus)
  1.1673 +apply (drule_tac f = " (%x. - (f x))" in isCont_eq_Ub)
  1.1674 +apply safe
  1.1675 +apply auto
  1.1676 +done
  1.1677 +
  1.1678 +
  1.1679 +(* ------------------------------------------------------------------------- *)
  1.1680 +(* Another version.                                                          *)
  1.1681 +(* ------------------------------------------------------------------------- *)
  1.1682 +
  1.1683 +lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
  1.1684 +      ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
  1.1685 +          (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
  1.1686 +apply (frule isCont_eq_Lb)
  1.1687 +apply (frule_tac [2] isCont_eq_Ub)
  1.1688 +apply (assumption+, safe)
  1.1689 +apply (rule_tac x = "f x" in exI)
  1.1690 +apply (rule_tac x = "f xa" in exI, simp, safe)
  1.1691 +apply (cut_tac x = x and y = xa in linorder_linear, safe)
  1.1692 +apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl)
  1.1693 +apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe)
  1.1694 +apply (rule_tac [2] x = xb in exI)
  1.1695 +apply (rule_tac [4] x = xb in exI, simp_all)
  1.1696 +done
  1.1697 +
  1.1698 +(*----------------------------------------------------------------------------*)
  1.1699 +(* If f'(x) > 0 then x is locally strictly increasing at the right            *)
  1.1700 +(*----------------------------------------------------------------------------*)
  1.1701 +
  1.1702 +lemma DERIV_left_inc:
  1.1703 +    "[| DERIV f x :> l;  0 < l |]
  1.1704 +     ==> \<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
  1.1705 +apply (simp add: deriv_def LIM_def)
  1.1706 +apply (drule spec, auto)
  1.1707 +apply (rule_tac x = s in exI, auto)
  1.1708 +apply (subgoal_tac "0 < l*h")
  1.1709 + prefer 2 apply (simp add: zero_less_mult_iff)
  1.1710 +apply (drule_tac x = h in spec)
  1.1711 +apply (simp add: real_abs_def pos_le_divide_eq pos_less_divide_eq 
  1.1712 +            split add: split_if_asm)
  1.1713 +done
  1.1714 +
  1.1715 +lemma DERIV_left_dec:
  1.1716 +  assumes der: "DERIV f x :> l"
  1.1717 +      and l:   "l < 0"
  1.1718 +  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x-h))"
  1.1719 +proof -
  1.1720 +  from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
  1.1721 +  have "\<exists>s. 0 < s \<and>
  1.1722 +              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
  1.1723 +    by (simp add: diff_minus)
  1.1724 +  then obtain s
  1.1725 +        where s:   "0 < s" 
  1.1726 +          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
  1.1727 +    by auto
  1.1728 +  thus ?thesis
  1.1729 +  proof (intro exI conjI strip)
  1.1730 +    show "0<s" .
  1.1731 +    fix h::real
  1.1732 +    assume "0 < h \<and> h < s"
  1.1733 +    with all [of "-h"] show "f x < f (x-h)" 
  1.1734 +    proof (simp add: real_abs_def pos_less_divide_eq diff_minus [symmetric] 
  1.1735 +		split add: split_if_asm)
  1.1736 +      assume "~ l \<le> - ((f (x-h) - f x) / h)" and h: "0 < h" 
  1.1737 +      with l 
  1.1738 +      have "0 < (f (x-h) - f x) / h" by arith
  1.1739 +      thus "f x < f (x-h)"
  1.1740 +	by (simp add: pos_less_divide_eq h)
  1.1741 +    qed
  1.1742 +  qed
  1.1743 +qed
  1.1744 +
  1.1745 +lemma DERIV_local_max: 
  1.1746 +  assumes der: "DERIV f x :> l"
  1.1747 +      and d:   "0 < d"
  1.1748 +      and le:  "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
  1.1749 +  shows "l = 0"
  1.1750 +proof (cases rule: linorder_cases [of l 0])
  1.1751 +  case equal show ?thesis .
  1.1752 +next
  1.1753 +  case less
  1.1754 +  from DERIV_left_dec [OF der less]
  1.1755 +  obtain d' where d': "0 < d'"
  1.1756 +             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
  1.1757 +  from real_lbound_gt_zero [OF d d']
  1.1758 +  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
  1.1759 +  with lt le [THEN spec [where x="x-e"]] 
  1.1760 +  show ?thesis by (auto simp add: abs_if)
  1.1761 +next
  1.1762 +  case greater
  1.1763 +  from DERIV_left_inc [OF der greater]
  1.1764 +  obtain d' where d': "0 < d'"
  1.1765 +             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x + h)" by blast
  1.1766 +  from real_lbound_gt_zero [OF d d']
  1.1767 +  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
  1.1768 +  with lt le [THEN spec [where x="x+e"]]
  1.1769 +  show ?thesis by (auto simp add: abs_if)
  1.1770 +qed
  1.1771 +
  1.1772 +
  1.1773 +text{*Similar theorem for a local minimum*}
  1.1774 +lemma DERIV_local_min:
  1.1775 +     "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) \<le> f(y) |] ==> l = 0"
  1.1776 +by (drule DERIV_minus [THEN DERIV_local_max], auto)
  1.1777 +
  1.1778 +
  1.1779 +text{*In particular, if a function is locally flat*}
  1.1780 +lemma DERIV_local_const:
  1.1781 +     "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
  1.1782 +by (auto dest!: DERIV_local_max)
  1.1783 +
  1.1784 +text{*Lemma about introducing open ball in open interval*}
  1.1785 +lemma lemma_interval_lt:
  1.1786 +     "[| a < x;  x < b |] 
  1.1787 +      ==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
  1.1788 +apply (simp add: abs_interval_iff)
  1.1789 +apply (insert linorder_linear [of "x-a" "b-x"], safe)
  1.1790 +apply (rule_tac x = "x-a" in exI)
  1.1791 +apply (rule_tac [2] x = "b-x" in exI, auto)
  1.1792 +done
  1.1793 +
  1.1794 +lemma lemma_interval: "[| a < x;  x < b |] ==>
  1.1795 +        \<exists>d::real. 0 < d &  (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
  1.1796 +apply (drule lemma_interval_lt, auto)
  1.1797 +apply (auto intro!: exI)
  1.1798 +done
  1.1799 +
  1.1800 +text{*Rolle's Theorem.
  1.1801 +   If @{term f} is defined and continuous on the closed interval 
  1.1802 +   @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, 
  1.1803 +   and @{term "f(a) = f(b)"},
  1.1804 +   then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}*}
  1.1805 +theorem Rolle: 
  1.1806 +  assumes lt: "a < b"
  1.1807 +      and eq: "f(a) = f(b)"
  1.1808 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
  1.1809 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
  1.1810 +  shows "\<exists>z. a < z & z < b & DERIV f z :> 0"
  1.1811 +proof -
  1.1812 +  have le: "a \<le> b" using lt by simp
  1.1813 +  from isCont_eq_Ub [OF le con]
  1.1814 +  obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" 
  1.1815 +             and alex: "a \<le> x" and xleb: "x \<le> b" 
  1.1816 +    by blast
  1.1817 +  from isCont_eq_Lb [OF le con]
  1.1818 +  obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" 
  1.1819 +              and alex': "a \<le> x'" and x'leb: "x' \<le> b" 
  1.1820 +    by blast
  1.1821 +  show ?thesis
  1.1822 +  proof cases
  1.1823 +    assume axb: "a < x & x < b"
  1.1824 +        --{*@{term f} attains its maximum within the interval*}
  1.1825 +    hence ax: "a<x" and xb: "x<b" by auto
  1.1826 +    from lemma_interval [OF ax xb]
  1.1827 +    obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
  1.1828 +      by blast
  1.1829 +    hence bound': "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> f y \<le> f x" using x_max
  1.1830 +      by blast
  1.1831 +    from differentiableD [OF dif [OF axb]]
  1.1832 +    obtain l where der: "DERIV f x :> l" ..
  1.1833 +    have "l=0" by (rule DERIV_local_max [OF der d bound']) 
  1.1834 +        --{*the derivative at a local maximum is zero*}
  1.1835 +    thus ?thesis using ax xb der by auto
  1.1836 +  next
  1.1837 +    assume notaxb: "~ (a < x & x < b)"
  1.1838 +    hence xeqab: "x=a | x=b" using alex xleb by arith
  1.1839 +    hence fb_eq_fx: "f b = f x" by (auto simp add: eq) 
  1.1840 +    show ?thesis
  1.1841 +    proof cases
  1.1842 +      assume ax'b: "a < x' & x' < b"
  1.1843 +        --{*@{term f} attains its minimum within the interval*}
  1.1844 +      hence ax': "a<x'" and x'b: "x'<b" by auto
  1.1845 +      from lemma_interval [OF ax' x'b]
  1.1846 +      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
  1.1847 +	by blast
  1.1848 +      hence bound': "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min
  1.1849 +	by blast
  1.1850 +      from differentiableD [OF dif [OF ax'b]]
  1.1851 +      obtain l where der: "DERIV f x' :> l" ..
  1.1852 +      have "l=0" by (rule DERIV_local_min [OF der d bound']) 
  1.1853 +        --{*the derivative at a local minimum is zero*}
  1.1854 +      thus ?thesis using ax' x'b der by auto
  1.1855 +    next
  1.1856 +      assume notax'b: "~ (a < x' & x' < b)"
  1.1857 +        --{*@{term f} is constant througout the interval*}
  1.1858 +      hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith
  1.1859 +      hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) 
  1.1860 +      from dense [OF lt]
  1.1861 +      obtain r where ar: "a < r" and rb: "r < b" by blast
  1.1862 +      from lemma_interval [OF ar rb]
  1.1863 +      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
  1.1864 +	by blast
  1.1865 +      have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b" 
  1.1866 +      proof (clarify) 
  1.1867 +        fix z::real
  1.1868 +        assume az: "a \<le> z" and zb: "z \<le> b"
  1.1869 +        show "f z = f b"
  1.1870 +        proof (rule order_antisym)
  1.1871 +          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb) 
  1.1872 +          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb) 
  1.1873 +        qed
  1.1874 +      qed
  1.1875 +      have bound': "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> f r = f y"
  1.1876 +      proof (intro strip)
  1.1877 +        fix y::real
  1.1878 +        assume lt: "\<bar>r-y\<bar> < d"
  1.1879 +        hence "f y = f b" by (simp add: eq_fb bound) 
  1.1880 +        thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le)
  1.1881 +      qed
  1.1882 +      from differentiableD [OF dif [OF conjI [OF ar rb]]]
  1.1883 +      obtain l where der: "DERIV f r :> l" ..
  1.1884 +      have "l=0" by (rule DERIV_local_const [OF der d bound']) 
  1.1885 +        --{*the derivative of a constant function is zero*}
  1.1886 +      thus ?thesis using ar rb der by auto
  1.1887 +    qed
  1.1888 +  qed
  1.1889 +qed
  1.1890 +
  1.1891 +
  1.1892 +subsection{*Mean Value Theorem*}
  1.1893 +
  1.1894 +lemma lemma_MVT:
  1.1895 +     "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
  1.1896 +proof cases
  1.1897 +  assume "a=b" thus ?thesis by simp
  1.1898 +next
  1.1899 +  assume "a\<noteq>b" 
  1.1900 +  hence ba: "b-a \<noteq> 0" by arith
  1.1901 +  show ?thesis
  1.1902 +    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
  1.1903 +        simp add: right_diff_distrib, simp add: left_diff_distrib)
  1.1904 +qed
  1.1905 +
  1.1906 +theorem MVT: 
  1.1907 +  assumes lt:  "a < b"
  1.1908 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
  1.1909 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
  1.1910 +  shows "\<exists>l z. a < z & z < b & DERIV f z :> l &
  1.1911 +                   (f(b) - f(a) = (b-a) * l)"
  1.1912 +proof -
  1.1913 +  let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
  1.1914 +  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
  1.1915 +    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id) 
  1.1916 +  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
  1.1917 +  proof (clarify)
  1.1918 +    fix x::real
  1.1919 +    assume ax: "a < x" and xb: "x < b"
  1.1920 +    from differentiableD [OF dif [OF conjI [OF ax xb]]]
  1.1921 +    obtain l where der: "DERIV f x :> l" ..
  1.1922 +    show "?F differentiable x"
  1.1923 +      by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
  1.1924 +          blast intro: DERIV_diff DERIV_cmult_Id der) 
  1.1925 +  qed  
  1.1926 +  from Rolle [where f = ?F, OF lt lemma_MVT contF difF]
  1.1927 +  obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0" 
  1.1928 +    by blast
  1.1929 +  have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)"
  1.1930 +    by (rule DERIV_cmult_Id)
  1.1931 +  hence derF: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z 
  1.1932 +                   :> 0 + (f b - f a) / (b - a)"
  1.1933 +    by (rule DERIV_add [OF der])
  1.1934 +  show ?thesis  
  1.1935 +  proof (intro exI conjI)
  1.1936 +    show "a < z" .
  1.1937 +    show "z < b" .
  1.1938 +    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by simp
  1.1939 +    show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
  1.1940 +  qed
  1.1941 +qed
  1.1942 +
  1.1943 +
  1.1944 +text{*A function is constant if its derivative is 0 over an interval.*}
  1.1945 +
  1.1946 +lemma DERIV_isconst_end: "[| a < b;
  1.1947 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
  1.1948 +         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
  1.1949 +        ==> (f b = f a)"
  1.1950 +apply (drule MVT, assumption)
  1.1951 +apply (blast intro: differentiableI)
  1.1952 +apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
  1.1953 +done
  1.1954 +
  1.1955 +lemma DERIV_isconst1: "[| a < b;
  1.1956 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
  1.1957 +         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
  1.1958 +        ==> \<forall>x. a \<le> x & x \<le> b --> f x = f a"
  1.1959 +apply safe
  1.1960 +apply (drule_tac x = a in order_le_imp_less_or_eq, safe)
  1.1961 +apply (drule_tac b = x in DERIV_isconst_end, auto)
  1.1962 +done
  1.1963 +
  1.1964 +lemma DERIV_isconst2: "[| a < b;
  1.1965 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
  1.1966 +         \<forall>x. a < x & x < b --> DERIV f x :> 0;
  1.1967 +         a \<le> x; x \<le> b |]
  1.1968 +        ==> f x = f a"
  1.1969 +apply (blast dest: DERIV_isconst1)
  1.1970 +done
  1.1971 +
  1.1972 +lemma DERIV_isconst_all: "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)"
  1.1973 +apply (rule linorder_cases [of x y])
  1.1974 +apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+
  1.1975 +done
  1.1976 +
  1.1977 +lemma DERIV_const_ratio_const:
  1.1978 +     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k"
  1.1979 +apply (rule linorder_cases [of a b], auto)
  1.1980 +apply (drule_tac [!] f = f in MVT)
  1.1981 +apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
  1.1982 +apply (auto dest: DERIV_unique simp add: left_distrib diff_minus)
  1.1983 +done
  1.1984 +
  1.1985 +lemma DERIV_const_ratio_const2:
  1.1986 +     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
  1.1987 +apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
  1.1988 +apply (auto dest!: DERIV_const_ratio_const simp add: real_mult_assoc)
  1.1989 +done
  1.1990 +
  1.1991 +lemma real_average_minus_first: "((a + b) /2 - a) = (b-a)/(2::real)"
  1.1992 +by auto
  1.1993 +declare real_average_minus_first [simp]
  1.1994 +
  1.1995 +lemma real_average_minus_second: "((b + a)/2 - a) = (b-a)/(2::real)"
  1.1996 +by auto
  1.1997 +declare real_average_minus_second [simp]
  1.1998 +
  1.1999 +text{*Gallileo's "trick": average velocity = av. of end velocities*}
  1.2000 +
  1.2001 +lemma DERIV_const_average:
  1.2002 +  assumes neq: "a \<noteq> (b::real)"
  1.2003 +      and der: "\<forall>x. DERIV v x :> k"
  1.2004 +  shows "v ((a + b)/2) = (v a + v b)/2"
  1.2005 +proof (cases rule: linorder_cases [of a b])
  1.2006 +  case equal with neq show ?thesis by simp
  1.2007 +next
  1.2008 +  case less
  1.2009 +  have "(v b - v a) / (b - a) = k"
  1.2010 +    by (rule DERIV_const_ratio_const2 [OF neq der])
  1.2011 +  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp 
  1.2012 +  moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k"
  1.2013 +    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
  1.2014 +  ultimately show ?thesis using neq by force
  1.2015 +next
  1.2016 +  case greater
  1.2017 +  have "(v b - v a) / (b - a) = k"
  1.2018 +    by (rule DERIV_const_ratio_const2 [OF neq der])
  1.2019 +  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp 
  1.2020 +  moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k"
  1.2021 +    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
  1.2022 +  ultimately show ?thesis using neq by (force simp add: add_commute) 
  1.2023 +qed
  1.2024 +
  1.2025 +
  1.2026 +text{*Dull lemma: an continuous injection on an interval must have a
  1.2027 +strict maximum at an end point, not in the middle.*}
  1.2028 +
  1.2029 +lemma lemma_isCont_inj:
  1.2030 +  assumes d: "0 < d"
  1.2031 +      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
  1.2032 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
  1.2033 +  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
  1.2034 +proof (rule ccontr)
  1.2035 +  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
  1.2036 +  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto 
  1.2037 +  show False
  1.2038 +  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
  1.2039 +    case le
  1.2040 +    from d cont all [of "x+d"]
  1.2041 +    have flef: "f(x+d) \<le> f x" 
  1.2042 +     and xlex: "x - d \<le> x" 
  1.2043 +     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z" 
  1.2044 +       by (auto simp add: abs_if)
  1.2045 +    from IVT [OF le flef xlex cont']
  1.2046 +    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
  1.2047 +    moreover
  1.2048 +    hence "g(f x') = g (f(x+d))" by simp
  1.2049 +    ultimately show False using d inj [of x'] inj [of "x+d"]
  1.2050 +      by (simp add: abs_le_interval_iff)
  1.2051 +  next
  1.2052 +    case ge
  1.2053 +    from d cont all [of "x-d"]
  1.2054 +    have flef: "f(x-d) \<le> f x" 
  1.2055 +     and xlex: "x \<le> x+d" 
  1.2056 +     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" 
  1.2057 +       by (auto simp add: abs_if)
  1.2058 +    from IVT2 [OF ge flef xlex cont']
  1.2059 +    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
  1.2060 +    moreover
  1.2061 +    hence "g(f x') = g (f(x-d))" by simp
  1.2062 +    ultimately show False using d inj [of x'] inj [of "x-d"]
  1.2063 +      by (simp add: abs_le_interval_iff)
  1.2064 +  qed
  1.2065 +qed
  1.2066 +
  1.2067 +
  1.2068 +text{*Similar version for lower bound.*}
  1.2069 +
  1.2070 +lemma lemma_isCont_inj2:
  1.2071 +     "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
  1.2072 +        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
  1.2073 +      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
  1.2074 +apply (insert lemma_isCont_inj
  1.2075 +          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
  1.2076 +apply (simp add: isCont_minus linorder_not_le) 
  1.2077 +done
  1.2078 +
  1.2079 +text{*Show there's an interval surrounding @{term "f(x)"} in 
  1.2080 +@{text "f[[x - d, x + d]]"} .*}
  1.2081 +
  1.2082 +lemma isCont_inj_range: 
  1.2083 +  assumes d: "0 < d"
  1.2084 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
  1.2085 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
  1.2086 +  shows "\<exists>e. 0<e & (\<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y))"
  1.2087 +proof -
  1.2088 +  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
  1.2089 +    by (auto simp add: abs_le_interval_iff)
  1.2090 +  from isCont_Lb_Ub [OF this]
  1.2091 +  obtain L M 
  1.2092 +  where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
  1.2093 +    and all2 [rule_format]:
  1.2094 +           "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
  1.2095 +    by auto
  1.2096 +  with d have "L \<le> f x & f x \<le> M" by simp
  1.2097 +  moreover have "L \<noteq> f x"
  1.2098 +  proof -
  1.2099 +    from lemma_isCont_inj2 [OF d inj cont]
  1.2100 +    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
  1.2101 +    thus ?thesis using all1 [of u] by arith
  1.2102 +  qed
  1.2103 +  moreover have "f x \<noteq> M"
  1.2104 +  proof -
  1.2105 +    from lemma_isCont_inj [OF d inj cont]
  1.2106 +    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
  1.2107 +    thus ?thesis using all1 [of u] by arith
  1.2108 +  qed
  1.2109 +  ultimately have "L < f x & f x < M" by arith
  1.2110 +  hence "0 < f x - L" "0 < M - f x" by arith+
  1.2111 +  from real_lbound_gt_zero [OF this]
  1.2112 +  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
  1.2113 +  thus ?thesis
  1.2114 +  proof (intro exI conjI)
  1.2115 +    show "0<e" .
  1.2116 +    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
  1.2117 +    proof (intro strip)
  1.2118 +      fix y::real
  1.2119 +      assume "\<bar>y - f x\<bar> \<le> e"
  1.2120 +      with e have "L \<le> y \<and> y \<le> M" by arith
  1.2121 +      from all2 [OF this]
  1.2122 +      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
  1.2123 +      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
  1.2124 +        by (force simp add: abs_le_interval_iff)
  1.2125 +    qed
  1.2126 +  qed
  1.2127 +qed
  1.2128 +
  1.2129 +
  1.2130 +text{*Continuity of inverse function*}
  1.2131 +
  1.2132 +lemma isCont_inverse_function:
  1.2133 +  assumes d: "0 < d"
  1.2134 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
  1.2135 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
  1.2136 +  shows "isCont g (f x)"
  1.2137 +proof (simp add: isCont_iff LIM_eq)
  1.2138 +  show "\<forall>r. 0 < r \<longrightarrow>
  1.2139 +         (\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r))"
  1.2140 +  proof (intro strip)
  1.2141 +    fix r::real
  1.2142 +    assume r: "0<r"
  1.2143 +    from real_lbound_gt_zero [OF r d]
  1.2144 +    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
  1.2145 +    with inj cont
  1.2146 +    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z" 
  1.2147 +                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
  1.2148 +    from isCont_inj_range [OF e this]
  1.2149 +    obtain e' where e': "0 < e'" 
  1.2150 +        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
  1.2151 +          by blast
  1.2152 +    show "\<exists>s. 0<s \<and> (\<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
  1.2153 +    proof (intro exI conjI)
  1.2154 +      show "0<e'" .
  1.2155 +      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
  1.2156 +      proof (intro strip)
  1.2157 +        fix z::real
  1.2158 +        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
  1.2159 +        with e e_lt e_simps all [rule_format, of "f x + z"]
  1.2160 +        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
  1.2161 +      qed
  1.2162 +    qed
  1.2163 +  qed
  1.2164 +qed  
  1.2165 +
  1.2166 +ML
  1.2167 +{*
  1.2168 +val LIM_def = thm"LIM_def";
  1.2169 +val NSLIM_def = thm"NSLIM_def";
  1.2170 +val isCont_def = thm"isCont_def";
  1.2171 +val isNSCont_def = thm"isNSCont_def";
  1.2172 +val deriv_def = thm"deriv_def";
  1.2173 +val nsderiv_def = thm"nsderiv_def";
  1.2174 +val differentiable_def = thm"differentiable_def";
  1.2175 +val NSdifferentiable_def = thm"NSdifferentiable_def";
  1.2176 +val increment_def = thm"increment_def";
  1.2177 +val isUCont_def = thm"isUCont_def";
  1.2178 +val isNSUCont_def = thm"isNSUCont_def";
  1.2179 +
  1.2180 +val half_gt_zero_iff = thm "half_gt_zero_iff";
  1.2181 +val half_gt_zero = thms "half_gt_zero";
  1.2182 +val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
  1.2183 +val LIM_eq = thm "LIM_eq";
  1.2184 +val LIM_D = thm "LIM_D";
  1.2185 +val LIM_const = thm "LIM_const";
  1.2186 +val LIM_add = thm "LIM_add";
  1.2187 +val LIM_minus = thm "LIM_minus";
  1.2188 +val LIM_add_minus = thm "LIM_add_minus";
  1.2189 +val LIM_diff = thm "LIM_diff";
  1.2190 +val LIM_const_not_eq = thm "LIM_const_not_eq";
  1.2191 +val LIM_const_eq = thm "LIM_const_eq";
  1.2192 +val LIM_unique = thm "LIM_unique";
  1.2193 +val LIM_mult_zero = thm "LIM_mult_zero";
  1.2194 +val LIM_self = thm "LIM_self";
  1.2195 +val LIM_equal = thm "LIM_equal";
  1.2196 +val LIM_trans = thm "LIM_trans";
  1.2197 +val LIM_NSLIM = thm "LIM_NSLIM";
  1.2198 +val NSLIM_LIM = thm "NSLIM_LIM";
  1.2199 +val LIM_NSLIM_iff = thm "LIM_NSLIM_iff";
  1.2200 +val NSLIM_mult = thm "NSLIM_mult";
  1.2201 +val LIM_mult2 = thm "LIM_mult2";
  1.2202 +val NSLIM_add = thm "NSLIM_add";
  1.2203 +val LIM_add2 = thm "LIM_add2";
  1.2204 +val NSLIM_const = thm "NSLIM_const";
  1.2205 +val LIM_const2 = thm "LIM_const2";
  1.2206 +val NSLIM_minus = thm "NSLIM_minus";
  1.2207 +val LIM_minus2 = thm "LIM_minus2";
  1.2208 +val NSLIM_add_minus = thm "NSLIM_add_minus";
  1.2209 +val LIM_add_minus2 = thm "LIM_add_minus2";
  1.2210 +val NSLIM_inverse = thm "NSLIM_inverse";
  1.2211 +val LIM_inverse = thm "LIM_inverse";
  1.2212 +val NSLIM_zero = thm "NSLIM_zero";
  1.2213 +val LIM_zero2 = thm "LIM_zero2";
  1.2214 +val NSLIM_zero_cancel = thm "NSLIM_zero_cancel";
  1.2215 +val LIM_zero_cancel = thm "LIM_zero_cancel";
  1.2216 +val NSLIM_not_zero = thm "NSLIM_not_zero";
  1.2217 +val NSLIM_const_not_eq = thm "NSLIM_const_not_eq";
  1.2218 +val NSLIM_const_eq = thm "NSLIM_const_eq";
  1.2219 +val NSLIM_unique = thm "NSLIM_unique";
  1.2220 +val LIM_unique2 = thm "LIM_unique2";
  1.2221 +val NSLIM_mult_zero = thm "NSLIM_mult_zero";
  1.2222 +val LIM_mult_zero2 = thm "LIM_mult_zero2";
  1.2223 +val NSLIM_self = thm "NSLIM_self";
  1.2224 +val isNSContD = thm "isNSContD";
  1.2225 +val isNSCont_NSLIM = thm "isNSCont_NSLIM";
  1.2226 +val NSLIM_isNSCont = thm "NSLIM_isNSCont";
  1.2227 +val isNSCont_NSLIM_iff = thm "isNSCont_NSLIM_iff";
  1.2228 +val isNSCont_LIM_iff = thm "isNSCont_LIM_iff";
  1.2229 +val isNSCont_isCont_iff = thm "isNSCont_isCont_iff";
  1.2230 +val isCont_isNSCont = thm "isCont_isNSCont";
  1.2231 +val isNSCont_isCont = thm "isNSCont_isCont";
  1.2232 +val NSLIM_h_iff = thm "NSLIM_h_iff";
  1.2233 +val NSLIM_isCont_iff = thm "NSLIM_isCont_iff";
  1.2234 +val LIM_isCont_iff = thm "LIM_isCont_iff";
  1.2235 +val isCont_iff = thm "isCont_iff";
  1.2236 +val isCont_add = thm "isCont_add";
  1.2237 +val isCont_mult = thm "isCont_mult";
  1.2238 +val isCont_o = thm "isCont_o";
  1.2239 +val isCont_o2 = thm "isCont_o2";
  1.2240 +val isNSCont_minus = thm "isNSCont_minus";
  1.2241 +val isCont_minus = thm "isCont_minus";
  1.2242 +val isCont_inverse = thm "isCont_inverse";
  1.2243 +val isNSCont_inverse = thm "isNSCont_inverse";
  1.2244 +val isCont_diff = thm "isCont_diff";
  1.2245 +val isCont_const = thm "isCont_const";
  1.2246 +val isNSCont_const = thm "isNSCont_const";
  1.2247 +val isNSCont_rabs = thm "isNSCont_rabs";
  1.2248 +val isCont_rabs = thm "isCont_rabs";
  1.2249 +val isNSUContD = thm "isNSUContD";
  1.2250 +val isUCont_isCont = thm "isUCont_isCont";
  1.2251 +val isUCont_isNSUCont = thm "isUCont_isNSUCont";
  1.2252 +val isNSUCont_isUCont = thm "isNSUCont_isUCont";
  1.2253 +val DERIV_iff = thm "DERIV_iff";
  1.2254 +val DERIV_NS_iff = thm "DERIV_NS_iff";
  1.2255 +val DERIV_D = thm "DERIV_D";
  1.2256 +val NS_DERIV_D = thm "NS_DERIV_D";
  1.2257 +val DERIV_unique = thm "DERIV_unique";
  1.2258 +val NSDeriv_unique = thm "NSDeriv_unique";
  1.2259 +val differentiableD = thm "differentiableD";
  1.2260 +val differentiableI = thm "differentiableI";
  1.2261 +val NSdifferentiableD = thm "NSdifferentiableD";
  1.2262 +val NSdifferentiableI = thm "NSdifferentiableI";
  1.2263 +val LIM_I = thm "LIM_I";
  1.2264 +val DERIV_LIM_iff = thm "DERIV_LIM_iff";
  1.2265 +val DERIV_iff2 = thm "DERIV_iff2";
  1.2266 +val NSDERIV_NSLIM_iff = thm "NSDERIV_NSLIM_iff";
  1.2267 +val NSDERIV_NSLIM_iff2 = thm "NSDERIV_NSLIM_iff2";
  1.2268 +val NSDERIV_iff2 = thm "NSDERIV_iff2";
  1.2269 +val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
  1.2270 +val NSDERIVD5 = thm "NSDERIVD5";
  1.2271 +val NSDERIVD4 = thm "NSDERIVD4";
  1.2272 +val NSDERIVD3 = thm "NSDERIVD3";
  1.2273 +val NSDERIV_DERIV_iff = thm "NSDERIV_DERIV_iff";
  1.2274 +val NSDERIV_isNSCont = thm "NSDERIV_isNSCont";
  1.2275 +val DERIV_isCont = thm "DERIV_isCont";
  1.2276 +val NSDERIV_const = thm "NSDERIV_const";
  1.2277 +val DERIV_const = thm "DERIV_const";
  1.2278 +val NSDERIV_add = thm "NSDERIV_add";
  1.2279 +val DERIV_add = thm "DERIV_add";
  1.2280 +val NSDERIV_mult = thm "NSDERIV_mult";
  1.2281 +val DERIV_mult = thm "DERIV_mult";
  1.2282 +val NSDERIV_cmult = thm "NSDERIV_cmult";
  1.2283 +val DERIV_cmult = thm "DERIV_cmult";
  1.2284 +val NSDERIV_minus = thm "NSDERIV_minus";
  1.2285 +val DERIV_minus = thm "DERIV_minus";
  1.2286 +val NSDERIV_add_minus = thm "NSDERIV_add_minus";
  1.2287 +val DERIV_add_minus = thm "DERIV_add_minus";
  1.2288 +val NSDERIV_diff = thm "NSDERIV_diff";
  1.2289 +val DERIV_diff = thm "DERIV_diff";
  1.2290 +val incrementI = thm "incrementI";
  1.2291 +val incrementI2 = thm "incrementI2";
  1.2292 +val increment_thm = thm "increment_thm";
  1.2293 +val increment_thm2 = thm "increment_thm2";
  1.2294 +val increment_approx_zero = thm "increment_approx_zero";
  1.2295 +val NSDERIV_zero = thm "NSDERIV_zero";
  1.2296 +val NSDERIV_approx = thm "NSDERIV_approx";
  1.2297 +val NSDERIVD1 = thm "NSDERIVD1";
  1.2298 +val NSDERIVD2 = thm "NSDERIVD2";
  1.2299 +val NSDERIV_chain = thm "NSDERIV_chain";
  1.2300 +val DERIV_chain = thm "DERIV_chain";
  1.2301 +val DERIV_chain2 = thm "DERIV_chain2";
  1.2302 +val NSDERIV_Id = thm "NSDERIV_Id";
  1.2303 +val DERIV_Id = thm "DERIV_Id";
  1.2304 +val isCont_Id = thms "isCont_Id";
  1.2305 +val DERIV_cmult_Id = thm "DERIV_cmult_Id";
  1.2306 +val NSDERIV_cmult_Id = thm "NSDERIV_cmult_Id";
  1.2307 +val DERIV_pow = thm "DERIV_pow";
  1.2308 +val NSDERIV_pow = thm "NSDERIV_pow";
  1.2309 +val NSDERIV_inverse = thm "NSDERIV_inverse";
  1.2310 +val DERIV_inverse = thm "DERIV_inverse";
  1.2311 +val DERIV_inverse_fun = thm "DERIV_inverse_fun";
  1.2312 +val NSDERIV_inverse_fun = thm "NSDERIV_inverse_fun";
  1.2313 +val DERIV_quotient = thm "DERIV_quotient";
  1.2314 +val NSDERIV_quotient = thm "NSDERIV_quotient";
  1.2315 +val CARAT_DERIV = thm "CARAT_DERIV";
  1.2316 +val CARAT_NSDERIV = thm "CARAT_NSDERIV";
  1.2317 +val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
  1.2318 +val starfun_if_eq = thm "starfun_if_eq";
  1.2319 +val CARAT_DERIVD = thm "CARAT_DERIVD";
  1.2320 +val f_inc_g_dec_Beq_f = thm "f_inc_g_dec_Beq_f";
  1.2321 +val f_inc_g_dec_Beq_g = thm "f_inc_g_dec_Beq_g";
  1.2322 +val f_inc_imp_le_lim = thm "f_inc_imp_le_lim";
  1.2323 +val lim_uminus = thm "lim_uminus";
  1.2324 +val g_dec_imp_lim_le = thm "g_dec_imp_lim_le";
  1.2325 +val Bolzano_bisect_le = thm "Bolzano_bisect_le";
  1.2326 +val Bolzano_bisect_fst_le_Suc = thm "Bolzano_bisect_fst_le_Suc";
  1.2327 +val Bolzano_bisect_Suc_le_snd = thm "Bolzano_bisect_Suc_le_snd";
  1.2328 +val eq_divide_2_times_iff = thm "eq_divide_2_times_iff";
  1.2329 +val Bolzano_bisect_diff = thm "Bolzano_bisect_diff";
  1.2330 +val Bolzano_nest_unique = thms "Bolzano_nest_unique";
  1.2331 +val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
  1.2332 +val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
  1.2333 +val lemma_BOLZANO2 = thm "lemma_BOLZANO2";
  1.2334 +val IVT = thm "IVT";
  1.2335 +val IVT2 = thm "IVT2";
  1.2336 +val IVT_objl = thm "IVT_objl";
  1.2337 +val IVT2_objl = thm "IVT2_objl";
  1.2338 +val isCont_bounded = thm "isCont_bounded";
  1.2339 +val isCont_has_Ub = thm "isCont_has_Ub";
  1.2340 +val isCont_eq_Ub = thm "isCont_eq_Ub";
  1.2341 +val isCont_eq_Lb = thm "isCont_eq_Lb";
  1.2342 +val isCont_Lb_Ub = thm "isCont_Lb_Ub";
  1.2343 +val DERIV_left_inc = thm "DERIV_left_inc";
  1.2344 +val DERIV_left_dec = thm "DERIV_left_dec";
  1.2345 +val DERIV_local_max = thm "DERIV_local_max";
  1.2346 +val DERIV_local_min = thm "DERIV_local_min";
  1.2347 +val DERIV_local_const = thm "DERIV_local_const";
  1.2348 +val Rolle = thm "Rolle";
  1.2349 +val MVT = thm "MVT";
  1.2350 +val DERIV_isconst_end = thm "DERIV_isconst_end";
  1.2351 +val DERIV_isconst1 = thm "DERIV_isconst1";
  1.2352 +val DERIV_isconst2 = thm "DERIV_isconst2";
  1.2353 +val DERIV_isconst_all = thm "DERIV_isconst_all";
  1.2354 +val DERIV_const_ratio_const = thm "DERIV_const_ratio_const";
  1.2355 +val DERIV_const_ratio_const2 = thm "DERIV_const_ratio_const2";
  1.2356 +val real_average_minus_first = thm "real_average_minus_first";
  1.2357 +val real_average_minus_second = thm "real_average_minus_second";
  1.2358 +val DERIV_const_average = thm "DERIV_const_average";
  1.2359 +val isCont_inj_range = thm "isCont_inj_range";
  1.2360 +val isCont_inverse_function = thm "isCont_inverse_function";
  1.2361 +*}
  1.2362 +
  1.2363  
  1.2364  end
  1.2365