Example (24.6)

　そして，Kurzweil-Henstock積分ですので，区分求積の為に通常のRiemann積分の理論を自作します．

let rdefint = new_definition
`(!a b f k.
     rdefint (a,b) f k <=>
     (!e. &0 < e
          ==> (?g. &0 < g /\
                   (!D p.
                        ((D 0 = a /\
                          (?N. (!n. n < N ==> D n < D (SUC n)) /\
                               (!n. n >= N ==> D n = b))) /\
                         (!n. D n <= p n /\ p n <= D (SUC n))) /\
                        (!n. n <
                             (@N. (!n. n < N ==> D n < D (SUC n)) /\
                                  (!n. n >= N ==> D n = D N))
                             ==> D (SUC n) - D n < g)
                        ==> abs
                            (sum
                             (0,
                              (@N. (!n. n < N ==> D n < D (SUC n)) /\
                                   (!n. n >= N ==> D n = D N)))
                             (\n. f (p n) * (D (SUC n) - D n)) -
                             k) <
                            e))))`;;

g `!a b f k. rdefint (a,b) f k ==> defint (a,b) f k`;;
e(REPEAT GEN_TAC THEN ASM_SIMP_TAC[rdefint; defint; gauge; GSYM tdiv; fine; GSYM rsum; GSYM division; GSYM dsize;] THEN REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`e:real`)) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN FIRST_X_ASSUM MP_TAC);;
e(ONCE_ASM_SIMP_TAC[UNDISCH(MESON[]`&0 < g ==> (D (SUC n) - D n < g <=> D (SUC n) - D n < (\x:real. g:real) (p n))`)] THEN REPEAT STRIP_TAC);;
e(ASSUME_TAC(UNDISCH(MESON[]`&0 < g ==> (!x. a <= x /\ x <= b ==> &0 < (\x:real. g:real) x)`)));;
e(EXISTS_TAC`(\x:real. g:real)`);;
e(ASM_SIMP_TAC[]);;
let rDEFINT_IMP_DEFINT = top_thm();;

let rintegrable = new_definition
`!a b f. rintegrable (a,b) f <=> (?i. rdefint (a,b) f i)`;;

let rintegral = new_definition
`!a b f. rintegral(a,b) f = @i. rdefint(a,b) f i`;;

let rINTEGRABLE_rDEFINT = prove
 (`!f a b. rintegrable(a,b) f ==> rdefint(a,b) f (rintegral(a,b) f)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[rintegrable; rintegral] THEN
  CONV_TAC(RAND_CONV SELECT_CONV) THEN REWRITE_TAC[]);;

let rDINT_UNIQ = prove
 (`!a b f k1 k2. a <= b /\ rdefint(a,b) f k1 /\ rdefint(a,b) f k2 ==> (k1 = k2)`,
  MESON_TAC[rDEFINT_IMP_DEFINT; DINT_UNIQ]);;

let rDEFINT_rINTEGRAL = prove
 (`!f a b i. a <= b /\ rdefint(a,b) f i ==> rintegral(a,b) f = i`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[rintegral] THEN
  MATCH_MP_TAC SELECT_UNIQUE THEN ASM_MESON_TAC[rDINT_UNIQ]);;

g `!a b f. rintegrable(a,b) f
==>
(!e. &0 < e
     ==> (?g. &0 < g /\
              (!D p.
                   tdiv (a,b) (D,p) /\ (!n. n <
     (@N. (!n. n < N ==> D n < D (SUC n)) /\
          (!n. n >= N ==> D n = D N))
     ==> D (SUC n) - D n < g)
                   ==> abs (rsum (D,p) f - rintegral (a,b) f) < e)))`;;
e(REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(SPEC_ALL rINTEGRABLE_rDEFINT) THEN ASM_SIMP_TAC[rdefint] THEN SIMP_TAC[GSYM division; GSYM tdiv; GSYM dsize; GSYM rsum]);;
let rINTEGRABLE_rdefint = top_thm();;

let rINTEGRAL_EQ_INTEGRAL = MESON[rINTEGRABLE_rDEFINT; rDEFINT_IMP_DEFINT; rDEFINT_rINTEGRAL; DEFINT_INTEGRAL]`!f a b. a <= b /\ rintegrable (a,b) f ==> rintegral (a,b) f = integral (a,b) f`;;