src/HOL/Hyperreal/Lim.thy
author nipkow
Fri, 07 Feb 2003 16:40:23 +0100
changeset 13810 c3fbfd472365
parent 12018 ec054019c910
child 14269 502a7c95de73
permissions -rw-r--r--
(*f -> ( *f because of new comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : Lim.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Description : Theory of limits, continuity and 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
                  differentiation of real=>real functions
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
Lim = SEQ + RealAbs + 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
(*-----------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
    Limits, continuity and differentiation: standard and NS definitions
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
 -----------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    14
constdefs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
  LIM :: [real=>real,real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    16
				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    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
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
			  --> abs(f x + -L) < r)))"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
  NSLIM :: [real=>real,real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    23
			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
  "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
		      x @= hypreal_of_real a -->
13810
c3fbfd472365 (*f -> ( *f because of new comments
nipkow
parents: 12018
diff changeset
    26
		      ( *f* f) x @= hypreal_of_real L))"   
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
  isCont :: [real=>real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
  "isCont f a == (f -- a --> (f a))"        
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    31
  (* NS definition dispenses with limit notions *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    32
  isNSCont :: [real=>real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    33
  "isNSCont f a == (ALL y. y @= hypreal_of_real a --> 
13810
c3fbfd472365 (*f -> ( *f because of new comments
nipkow
parents: 12018
diff changeset
    34
			   ( *f* f) y @= hypreal_of_real (f a))"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
  (* differentiation: D is derivative of function f at x *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    37
  deriv:: [real=>real,real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    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
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    40
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    41
  nsderiv :: [real=>real,real,real] => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    42
			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    43
  "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. 
13810
c3fbfd472365 (*f -> ( *f because of new comments
nipkow
parents: 12018
diff changeset
    44
			(( *f* f)(hypreal_of_real x + h) + 
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    47
  differentiable :: [real=>real,real] => bool   (infixl 60)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    48
  "f differentiable x == (EX D. DERIV f x :> D)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    49
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    50
  NSdifferentiable :: [real=>real,real] => bool   (infixl 60)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    51
  "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    52
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    53
  increment :: [real=>real,real,hypreal] => hypreal
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    54
  "increment f x h == (@inc. f NSdifferentiable x & 
13810
c3fbfd472365 (*f -> ( *f because of new comments
nipkow
parents: 12018
diff changeset
    55
		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    56
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    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
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    60
			    --> abs(f x + -f y) < r)))"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    61
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    62
  isNSUCont :: (real=>real) => bool
13810
c3fbfd472365 (*f -> ( *f because of new comments
nipkow
parents: 12018
diff changeset
    63
  "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    64
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    65
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    66
(*Used in the proof of the Bolzano theorem*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    67
consts
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    68
  Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    69
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    70
primrec
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    71
  "Bolzano_bisect P a b 0 = (a,b)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    72
  "Bolzano_bisect P a b (Suc n) =
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    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
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    76
  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    77
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    78
end
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    79