2 Author : Jacques D. Fleuriot
3 Copyright : 1998 University of Cambridge
4 Description : Theory of limits, continuity and
5 differentiation of real=>real functions
10 (*-----------------------------------------------------------------------
11 Limits, continuity and differentiation: standard and NS definitions
12 -----------------------------------------------------------------------*)
15 LIM :: [real=>real,real,real] => bool
16 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
18 ALL r. Numeral0 < r -->
19 (EX s. Numeral0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
20 --> abs(f x + -L) < r)))"
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))"
28 isCont :: [real=>real,real] => bool
29 "isCont f a == (f -- a --> (f a))"
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))"
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) -- Numeral0 --> D)"
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)"
47 differentiable :: [real=>real,real] => bool (infixl 60)
48 "f differentiable x == (EX D. DERIV f x :> D)"
50 NSdifferentiable :: [real=>real,real] => bool (infixl 60)
51 "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
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))"
57 isUCont :: (real=>real) => bool
58 "isUCont f == (ALL r. Numeral0 < r -->
59 (EX s. Numeral0 < s & (ALL x y. abs(x + -y) < s
60 --> abs(f x + -f y) < r)))"
62 isNSUCont :: (real=>real) => bool
63 "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
66 (*Used in the proof of the Bolzano theorem*)
68 Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
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)