Example (24.1)

　まずは，区間の等分です．単調列での分割を帰納法で示した後，を固定した列により等分します．

needs "Library/transc.ml";;

g `!n f x i. (!j k. j <= k /\ k <= n ==> x j <= x k) /\
             (!k. 1 <= k /\ k <= n ==> defint (x (k -1),x k) f (i k))
             ==> defint (x 0,x n) f (sum (1,n) i)`;;
e(INDUCT_TAC);;
e(SIMP_TAC[INTEGRAL_NULL; sum]);;
e(REPEAT STRIP_TAC THEN SIMP_TAC[sum] THEN MATCH_MP_TAC DEFINT_COMBINE);;
e(FIRST_ASSUM(MP_TAC o (SPEC`SUC n`)) THEN SIMP_TAC[LE_REFL; my]);;
e(FIRST_ASSUM(MP_TAC o (SPECL[`n:num`;`SUC n`])) THEN SIMP_TAC[LESS_EQ_SUC_REFL; LE_REFL]);;
e(FIRST_ASSUM(MP_TAC o (SPECL[`0`;`n:num`])) THEN SIMP_TAC[LE_0; LESS_EQ_SUC_REFL; SUC_SUB1; ADD1; ADD_AC]);;
e(FIRST_X_ASSUM(MP_TAC o (SPECL[`f:real->real`;`x:num->real`;`i':num->real`])));;
e(ASM_MESON_TAC[LE_TRANS; LESS_EQ_SUC_REFL]);;
let thm01 = top_thm();;

let thm02 = prove
 (`!n j k. 1 <= n /\ j <= k /\ k <= n ==> &j / &n <= &k / &n`,
  REPEAT GEN_TAC THEN SIMP_TAC[GSYM REAL_LE] THEN CONV_TAC REAL_SOSFIELD);;

let thm03 = SPECL[`n:num`;`f:real->real`;`(\k:num. &k / &n)`;`i:num->real`]thm01;;

g `!n f i. 1 <= n /\ 
          (!k. 1 <= k /\ k <= n ==> defint (&(k - 1) / &n,&k / &n) f (i k))
          ==> defint (&0,&1) f (sum (1,n) i)`;;
e(REPEAT STRIP_TAC THEN MP_TAC thm03);;
e(ASM_MESON_TAC[thm02; REAL_DIV_LZERO; LE_1; REAL_INJ; REAL_DIV_REFL]);;
let thm04 = top_thm();;
let thm04 = 
SPECL[`n:num`;`f:real->real`;`(\k. integral (&(k - 1) / &n,&k / &n) f)`]thm04;;

g `1 <= n ==> 1 <= k /\ k <= n ==> &0 <= &(k - 1) / &n /\  &(k - 1) / &n <= &k / &n /\ &k / &n <= &1`;;
e(SIMP_TAC[GSYM REAL_OF_NUM_SUB; GSYM REAL_LE] THEN CONV_TAC REAL_SOSFIELD);;
let thm05 = top_thm();;

let thm06 = MESON[thm05;INTEGRABLE_CONTINUOUS;INTEGRABLE_SUBINTERVAL;]
`(!x. &0 <= x /\ x <= &1 ==> f contl x)
    ==> integrable (&0,&1) f /\
        (1 <= n
             ==> (!k. 1 <= k /\ k <= n
                      ==> integrable (&(k - 1) / &n,&k / &n) f))`;;

g `1 <= n ==> &(k - 1) / &n <= &k / &n /\ &0 <= &1`;;
e(MP_TAC(ARITH_RULE`k-1<=k`) THEN SIMP_TAC[GSYM REAL_OF_NUM_SUB; GSYM REAL_LE] THEN CONV_TAC REAL_SOSFIELD);;
let thm07 = top_thm();;

g `!f. (!x. &0 <= x /\ x <= &1 ==> f contl x)
       ==> (!n. 1 <= n
                ==> integral (&0,&1) f =
                    sum (1,n) (\k. integral (&(k - 1) / &n,&k / &n) f))`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC thm06 THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(ASM_MESON_TAC[thm04; thm07; INTEGRABLE_DEFINT; DINT_UNIQ]);;
let thm08 = top_thm();;

# thm08;;
val it : thm =
  |- !f. (!x. &0 <= x /\ x <= &1 ==> f contl x)
         ==> (!n. 1 <= n
                  ==> integral (&0,&1) f =
                      sum (1,n) (\k. integral (&(k - 1) / &n,&k / &n) f))

　この定理を適用して，次を得ます．

let thm09 = MESON[DIFF_CONT; DIFF_CONV`\x. sin (&n * pi * x)`]`(\x. sin (&n * pi * x)) contl x`;;

g `f contl x ==> (\x. f x * abs (sin (&n * pi * x))) contl x`;;
e(STRIP_TAC THEN MATCH_MP_TAC CONT_MUL);;
e(ASSUME_TAC(MATCH_MP CONT_ABS thm09) THEN ASM_MESON_TAC[]);;
let thm10 = top_thm();;


g `(!x. &0 <= x /\ x <= &1 ==> f contl x)
          ==> !n. 1 <= n 
          ==> integral (&0,&1) (\x. f x * abs (sin (&n * pi * x))) =
              sum (1,n)
              (\k. integral (&(k - 1) / &n,&k / &n)
                   (\x. f x * abs (sin (&n * pi * x))))`;;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_TAC""`(!x. &0 <= x /\ x <= &1 ==> (\x. f x * abs (sin (&n * pi * x))) contl x)`[ASM_MESON_TAC[thm10]]);;
e(FIRST_X_ASSUM(MP_TAC o (MATCH_MP thm08)) THEN DISCH_THEN(MP_TAC o (SPEC`n:num`)) THEN ASM_SIMP_TAC[]);;
let thm11 = top_thm();;

val thm11 : thm =
  |- (!x. &0 <= x /\ x <= &1 ==> f contl x)
     ==> (!n. 1 <= n
              ==> integral (&0,&1) (\x. f x * abs (sin (&n * pi * x))) =
                  sum (1,n)
                  (\k. integral (&(k - 1) / &n,&k / &n)
                       (\x. f x * abs (sin (&n * pi * x)))))