src/HOL/Hyperreal/Integration.thy

 begin
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}
 
 definition
-
   --{*Partitions and tagged partitions etc.*}
 
-  partition :: "[(real*real),nat => real] => bool"
+  partition :: "[(real*real),nat => real] => bool" where
   "partition = (%(a,b) D. D 0 = a &
                          (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
                               (\<forall>n \<ge> N. D(n) = b)))"
 
-  psize :: "(nat => real) => nat"
+definition
+  psize :: "(nat => real) => nat" where
   "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
                       (\<forall>n \<ge> N. D(n) = D(N)))"
 
-  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
+definition
+  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
   "tpart = (%(a,b) (D,p). partition(a,b) D &
                           (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
 
   --{*Gauges and gauge-fine divisions*}
 
-  gauge :: "[real => bool, real => real] => bool"
+definition
+  gauge :: "[real => bool, real => real] => bool" where
   "gauge E g = (\<forall>x. E x --> 0 < g(x))"
 
-  fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
+definition
+  fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
   "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
 
   --{*Riemann sum*}
 
-  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
+definition
+  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where
   "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))"
 
   --{*Gauge integrability (definite)*}
 
-  Integral :: "[(real*real),real=>real,real] => bool"
+definition
+  Integral :: "[(real*real),real=>real,real] => bool" where
   "Integral = (%(a,b) f k. \<forall>e > 0.
                                (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
                                (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
                                          \<bar>rsum(D,p) f - k\<bar> < e)))"