src/HOL/Hyperreal/Integration.thy
author paulson
Mon May 05 18:23:40 2003 +0200 (2003-05-05)
changeset 13958 c1c67582c9b5
child 15093 49ede01e9ee6
permissions -rw-r--r--
New material on integration, etc. Moving Hyperreal/ex
to directory Complex
paulson@13958
     1
(*  Title       : Integration.thy
paulson@13958
     2
    Author      : Jacques D. Fleuriot
paulson@13958
     3
    Copyright   : 2000  University of Edinburgh
paulson@13958
     4
    Description : Theory of integration (cf. Harrison's HOL development)
paulson@13958
     5
*)
paulson@13958
     6
paulson@13958
     7
Integration = MacLaurin + 
paulson@13958
     8
paulson@13958
     9
paulson@13958
    10
constdefs
paulson@13958
    11
paulson@13958
    12
  
paulson@13958
    13
(* ------------------------------------------------------------------------ *)
paulson@13958
    14
(* Partitions and tagged partitions etc.                                    *)
paulson@13958
    15
(* ------------------------------------------------------------------------ *)
paulson@13958
    16
paulson@13958
    17
  partition :: "[(real*real),nat => real] => bool"
paulson@13958
    18
  "partition == %(a,b) D. ((D 0 = a) & 
paulson@13958
    19
                         (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
paulson@13958
    20
                            (ALL n. N <= n --> (D(n) = b)))))"
paulson@13958
    21
  
paulson@13958
    22
  psize :: (nat => real) => nat
paulson@13958
    23
  "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
paulson@13958
    24
                  (ALL n. N <= n --> (D(n) = D(N)))"
paulson@13958
    25
  
paulson@13958
    26
  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
paulson@13958
    27
  "tpart == %(a,b) (D,p). partition(a,b) D &
paulson@13958
    28
                          (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
paulson@13958
    29
paulson@13958
    30
(* ------------------------------------------------------------------------ *)
paulson@13958
    31
(* Gauges and gauge-fine divisions                                          *)
paulson@13958
    32
(* ------------------------------------------------------------------------ *)
paulson@13958
    33
  
paulson@13958
    34
  gauge :: [real => bool, real => real] => bool
paulson@13958
    35
  "gauge E g == ALL x. E x --> 0 < g(x)"
paulson@13958
    36
paulson@13958
    37
  fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
paulson@13958
    38
  "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
paulson@13958
    39
paulson@13958
    40
(* ------------------------------------------------------------------------ *)
paulson@13958
    41
(* Riemann sum                                                              *)
paulson@13958
    42
(* ------------------------------------------------------------------------ *)
paulson@13958
    43
paulson@13958
    44
  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
paulson@13958
    45
  "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
paulson@13958
    46
paulson@13958
    47
(* ------------------------------------------------------------------------ *)
paulson@13958
    48
(* Gauge integrability (definite)                                           *)
paulson@13958
    49
(* ------------------------------------------------------------------------ *)
paulson@13958
    50
paulson@13958
    51
   Integral :: "[(real*real),real=>real,real] => bool"
paulson@13958
    52
   "Integral == %(a,b) f k. ALL e. 0 < e -->
paulson@13958
    53
                               (EX g. gauge(%x. a <= x & x <= b) g &
paulson@13958
    54
                               (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
paulson@13958
    55
                                         abs(rsum(D,p) f - k) < e))"    
paulson@13958
    56
end
paulson@13958
    57
paulson@13958
    58