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) -->