src/HOL/Hyperreal/Integration.thy
changeset 13958 c1c67582c9b5
child 15093 49ede01e9ee6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Mon May 05 18:23:40 2003 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +(*  Title       : Integration.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 2000  University of Edinburgh
     1.7 +    Description : Theory of integration (cf. Harrison's HOL development)
     1.8 +*)
     1.9 +
    1.10 +Integration = MacLaurin + 
    1.11 +
    1.12 +
    1.13 +constdefs
    1.14 +
    1.15 +  
    1.16 +(* ------------------------------------------------------------------------ *)
    1.17 +(* Partitions and tagged partitions etc.                                    *)
    1.18 +(* ------------------------------------------------------------------------ *)
    1.19 +
    1.20 +  partition :: "[(real*real),nat => real] => bool"
    1.21 +  "partition == %(a,b) D. ((D 0 = a) & 
    1.22 +                         (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
    1.23 +                            (ALL n. N <= n --> (D(n) = b)))))"
    1.24 +  
    1.25 +  psize :: (nat => real) => nat
    1.26 +  "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
    1.27 +                  (ALL n. N <= n --> (D(n) = D(N)))"
    1.28 +  
    1.29 +  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
    1.30 +  "tpart == %(a,b) (D,p). partition(a,b) D &
    1.31 +                          (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
    1.32 +
    1.33 +(* ------------------------------------------------------------------------ *)
    1.34 +(* Gauges and gauge-fine divisions                                          *)
    1.35 +(* ------------------------------------------------------------------------ *)
    1.36 +  
    1.37 +  gauge :: [real => bool, real => real] => bool
    1.38 +  "gauge E g == ALL x. E x --> 0 < g(x)"
    1.39 +
    1.40 +  fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
    1.41 +  "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
    1.42 +
    1.43 +(* ------------------------------------------------------------------------ *)
    1.44 +(* Riemann sum                                                              *)
    1.45 +(* ------------------------------------------------------------------------ *)
    1.46 +
    1.47 +  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
    1.48 +  "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
    1.49 +
    1.50 +(* ------------------------------------------------------------------------ *)
    1.51 +(* Gauge integrability (definite)                                           *)
    1.52 +(* ------------------------------------------------------------------------ *)
    1.53 +
    1.54 +   Integral :: "[(real*real),real=>real,real] => bool"
    1.55 +   "Integral == %(a,b) f k. ALL e. 0 < e -->
    1.56 +                               (EX g. gauge(%x. a <= x & x <= b) g &
    1.57 +                               (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
    1.58 +                                         abs(rsum(D,p) f - k) < e))"    
    1.59 +end
    1.60 +
    1.61 +