author  nipkow 
Fri, 07 Feb 2003 16:40:23 +0100  
changeset 13810  c3fbfd472365 
parent 12018  ec054019c910 
child 14269  502a7c95de73 
permissions  rwrr 
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 == 

12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

18 
ALL r. 0 < r > 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

19 
(EX s. 0 < s & (ALL x. (x ~= a & (abs(x + a) < s) 
10751  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 > 

13810  26 
( *f* f) x @= hypreal_of_real L))" 
10751  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 > 

13810  34 
( *f* f) y @= hypreal_of_real (f a))" 
10751  35 

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

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

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

12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

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

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

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

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

13810  44 
(( *f* f)(hypreal_of_real x + h) + 
10751  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 & 

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

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

12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

58 
"isUCont f == (ALL r. 0 < r > 
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

59 
(EX s. 0 < s & (ALL x y. abs(x + y) < s 
10751  60 
> abs(f x + f y) < r)))" 
61 

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

13810  63 
"isNSUCont f == (ALL x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
10751  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 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

74 
in if P(x, (x+y)/2) then ((x+y)/2, y) 
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

75 
else (x, (x+y)/2) )" 
10751  76 

77 

78 
end 

79 