src/HOL/Hyperreal/Integration.thy
 changeset 21404 eb85850d3eb7 parent 20792 add17d26151b child 22998 97e1f9c2cc46
```     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -13,38 +13,43 @@
1.4  text{*We follow John Harrison in formalizing the Gauge integral.*}
1.5
1.6  definition
1.7 -
1.8    --{*Partitions and tagged partitions etc.*}
1.9
1.10 -  partition :: "[(real*real),nat => real] => bool"
1.11 +  partition :: "[(real*real),nat => real] => bool" where
1.12    "partition = (%(a,b) D. D 0 = a &
1.13                           (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
1.14                                (\<forall>n \<ge> N. D(n) = b)))"
1.15
1.16 -  psize :: "(nat => real) => nat"
1.17 +definition
1.18 +  psize :: "(nat => real) => nat" where
1.19    "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
1.20                        (\<forall>n \<ge> N. D(n) = D(N)))"
1.21
1.22 -  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
1.23 +definition
1.24 +  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
1.25    "tpart = (%(a,b) (D,p). partition(a,b) D &
1.26                            (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
1.27
1.28    --{*Gauges and gauge-fine divisions*}
1.29
1.30 -  gauge :: "[real => bool, real => real] => bool"
1.31 +definition
1.32 +  gauge :: "[real => bool, real => real] => bool" where
1.33    "gauge E g = (\<forall>x. E x --> 0 < g(x))"
1.34
1.35 -  fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
1.36 +definition
1.37 +  fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
1.38    "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
1.39
1.40    --{*Riemann sum*}
1.41
1.42 -  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
1.43 +definition
1.44 +  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where
1.45    "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))"
1.46
1.47    --{*Gauge integrability (definite)*}
1.48
1.49 -  Integral :: "[(real*real),real=>real,real] => bool"
1.50 +definition
1.51 +  Integral :: "[(real*real),real=>real,real] => bool" where
1.52    "Integral = (%(a,b) f k. \<forall>e > 0.
1.53                                 (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
1.54                                 (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
```