src/HOL/Hyperreal/Lim.thy
author paulson
Sun Feb 15 10:46:37 2004 +0100 (2004-02-15)
changeset 14387 e96d5c42c4b0
parent 14269 502a7c95de73
child 14477 cc61fd03e589
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
     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 + RealDef + 
     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