src/HOL/Real/Hyperreal/Lim.thy
changeset 10045 c76b73e16711
child 10607 352f6f209775
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Lim.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +(*  Title       : Lim.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Theory of limits, continuity and 
     1.8 +                  differentiation of real=>real functions
     1.9 +*)
    1.10 +
    1.11 +Lim = SEQ + RealAbs + 
    1.12 +
    1.13 +     (*-----------------------------------------------------------------------
    1.14 +         Limits, continuity and differentiation: standard and NS definitions
    1.15 +      -----------------------------------------------------------------------*)
    1.16 +constdefs
    1.17 +      LIM :: [real=>real,real,real] => bool    ("((_)/ -- (_)/ --> (_))" 60)
    1.18 +      "f -- a --> L == (ALL r. #0 < r --> 
    1.19 +                          (EX s. #0 < s & (ALL x. (#0 < abs(x + -a) & (abs(x + -a) < s)
    1.20 +                                --> abs(f x + -L) < r))))"
    1.21 +
    1.22 +      NSLIM :: [real=>real,real,real] => bool  ("((_)/ -- (_)/ --NS> (_))" 60)
    1.23 +      "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & 
    1.24 +                          x @= hypreal_of_real a --> (*f* f) x @= hypreal_of_real L))"   
    1.25 +
    1.26 +      isCont :: [real=>real,real] => bool
    1.27 +      "isCont f a == (f -- a --> (f a))"        
    1.28 +
    1.29 +      (* NS definition dispenses with limit notions *)
    1.30 +      isNSCont :: [real=>real,real] => bool
    1.31 +      "isNSCont f a == (ALL y. y @= hypreal_of_real a --> 
    1.32 +                               (*f* f) y @= hypreal_of_real (f a))"
    1.33 +      
    1.34 +      (* differentiation: D is derivative of function f at x *)
    1.35 +      deriv:: [real=>real,real,real] => bool   ("(DERIV (_)/ (_)/ :> (_))" 60)
    1.36 +      "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*rinv(h)) -- #0 --> D)"
    1.37 +
    1.38 +      nsderiv :: [real=>real,real,real] => bool   ("(NSDERIV (_)/ (_)/ :> (_))" 60)
    1.39 +      "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. 
    1.40 +                            ((*f* f)(hypreal_of_real x + h) + 
    1.41 +                             -hypreal_of_real (f x))*hrinv(h) @= hypreal_of_real D)"
    1.42 +
    1.43 +      differentiable :: [real=>real,real] => bool   (infixl 60)
    1.44 +      "f differentiable x == (EX D. DERIV f x :> D)"
    1.45 +
    1.46 +      NSdifferentiable :: [real=>real,real] => bool   (infixl 60)
    1.47 +      "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
    1.48 +
    1.49 +      increment :: [real=>real,real,hypreal] => hypreal
    1.50 +      "increment f x h == (@inc. f NSdifferentiable x & 
    1.51 +                           inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    1.52 +
    1.53 +      isUCont :: (real=>real) => bool
    1.54 +      "isUCont f ==  (ALL r. #0 < r --> 
    1.55 +                          (EX s. #0 < s & (ALL x y. abs(x + -y) < s
    1.56 +                                --> abs(f x + -f y) < r)))"
    1.57 +
    1.58 +      isNSUCont :: (real=>real) => bool
    1.59 +      "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
    1.60 +end
    1.61 +