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 |
|