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 +
```