src/HOL/Hyperreal/Lim.thy
 author wenzelm Fri Oct 05 21:52:39 2001 +0200 (2001-10-05) changeset 11701 3d51fbf81c17 parent 10751 a81ea5d3dd41 child 11704 3c50a2cd6f00 permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
```     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. Numeral0 < r -->
```
```    19 	     (EX s. Numeral0 < 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) -- Numeral0 --> 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. Numeral0 < r -->
```
```    59 		      (EX s. Numeral0 < 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
```