10751

1 
(* Title : Lim.thy


2 
Author : Jacques D. Fleuriot


3 
Copyright : 1998 University of Cambridge


4 
Description : Theory of limits, continuity and


5 
differentiation of real=>real functions


6 
*)


7 


8 
Lim = SEQ + RealAbs +


9 


10 
(*


11 
Limits, continuity and differentiation: standard and NS definitions


12 
*)


13 


14 
constdefs


15 
LIM :: [real=>real,real,real] => bool


16 
("((_)/  (_)/ > (_))" [60, 0, 60] 60)


17 
"f  a > L ==


18 
ALL r. #0 < r >


19 
(EX s. #0 < s & (ALL x. (x ~= a & (abs(x + a) < s)


20 
> abs(f x + L) < r)))"


21 


22 
NSLIM :: [real=>real,real,real] => bool


23 
("((_)/  (_)/ NS> (_))" [60, 0, 60] 60)


24 
"f  a NS> L == (ALL x. (x ~= hypreal_of_real a &


25 
x @= hypreal_of_real a >


26 
(*f* f) x @= hypreal_of_real L))"


27 


28 
isCont :: [real=>real,real] => bool


29 
"isCont f a == (f  a > (f a))"


30 


31 
(* NS definition dispenses with limit notions *)


32 
isNSCont :: [real=>real,real] => bool


33 
"isNSCont f a == (ALL y. y @= hypreal_of_real a >


34 
(*f* f) y @= hypreal_of_real (f a))"


35 


36 
(* differentiation: D is derivative of function f at x *)


37 
deriv:: [real=>real,real,real] => bool


38 
("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)


39 
"DERIV f x :> D == ((%h. (f(x + h) + f(x))/h)  #0 > D)"


40 


41 
nsderiv :: [real=>real,real,real] => bool


42 
("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)


43 
"NSDERIV f x :> D == (ALL h: Infinitesimal  {0}.


44 
((*f* f)(hypreal_of_real x + h) +


45 
 hypreal_of_real (f x))/h @= hypreal_of_real D)"


46 


47 
differentiable :: [real=>real,real] => bool (infixl 60)


48 
"f differentiable x == (EX D. DERIV f x :> D)"


49 


50 
NSdifferentiable :: [real=>real,real] => bool (infixl 60)


51 
"f NSdifferentiable x == (EX D. NSDERIV f x :> D)"


52 


53 
increment :: [real=>real,real,hypreal] => hypreal


54 
"increment f x h == (@inc. f NSdifferentiable x &


55 
inc = (*f* f)(hypreal_of_real x + h) + hypreal_of_real (f x))"


56 


57 
isUCont :: (real=>real) => bool


58 
"isUCont f == (ALL r. #0 < r >


59 
(EX s. #0 < s & (ALL x y. abs(x + y) < s


60 
> abs(f x + f y) < r)))"


61 


62 
isNSUCont :: (real=>real) => bool


63 
"isNSUCont f == (ALL x y. x @= y > (*f* f) x @= (*f* f) y)"


64 


65 


66 
(*Used in the proof of the Bolzano theorem*)


67 
consts


68 
Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"


69 


70 
primrec


71 
"Bolzano_bisect P a b 0 = (a,b)"


72 
"Bolzano_bisect P a b (Suc n) =


73 
(let (x,y) = Bolzano_bisect P a b n


74 
in if P(x, (x+y)/#2) then ((x+y)/#2, y)


75 
else (x, (x+y)/#2) )"


76 


77 


78 
end


79 
