Example (24.7)

　tagged division用のlemmaを幾つか用意すれば，区分求積の公式が証明できます．

g`(!n. n < N
     ==> (if n < N then &n / &N else &1) <
         (if n + 1 < N then &(n + 1) / &N else &1)) /\
(!n. n >= N ==> (if n < N then &n / &N else &1) = &1)`;;
e(REPEAT STRIP_TAC);;
e(ASM_CASES_TAC`n + 1 < N` THEN ASM_SIMP_TAC[prove(`!n N. n < N ==> &n / &N < &(n + 1) / &N /\ &n / &N < &1`,
REPEAT STRIP_TAC THEN MP_TAC(UNDISCH(ARITH_RULE `n < N ==> 0 < N /\ n < N`;)) THEN SIMP_TAC[GSYM REAL_LT; GSYM REAL_ADD] THEN CONV_TAC REAL_SOSFIELD)]);;
e(ASM_SIMP_TAC[ARITH_RULE `n >= N:num ==> ~(n < N)`]);;
let tdiv_lemma1 = top_thm();;

g`(?N'. (!n. n < N'
             ==> (if n < N then &n / &N else &1) <
                 (if n + 1 < N then &(n + 1) / &N else &1)) /\
        (!n. n >= N' ==> (if n < N then &n / &N else &1) = &1))`;;
e(EXISTS_TAC`N:num` THEN SIMP_TAC[tdiv_lemma1]);;
let tdiv_lemma2 = top_thm();;

g`!(z:num->num->real). 1 <= N /\ (!n. if n < N
         then &n / &N <= z N n /\ z N n <= &(n + 1) / &N
         else z N n = &1)
==> (!n. (if n < N then &n / &N else &1) <= z N n /\
      z N n <= (if n + 1 < N then &(n + 1) / &N else &1))`;;
e(REPEAT STRIP_TAC);;
e(ASM_MESON_TAC[REAL_LE_REFL]);;
e(SUBGOAL_TAC""`(z:num->num->real) N n <= &1`[ASM_CASES_TAC`n<N:num`]);;
e(SUBGOAL_TAC""`&1 <= &N /\ &(n + 1) <= &N`[ASM_MESON_TAC[REAL_LE; LE_SUC_LT; ADD1]] THEN FIRST_ASSUM(ASSUME_TAC o (MATCH_MP (REAL_SOSFIELD`&1 <= x /\ y <= x ==> y / x <= &1`))) THEN ASM_MESON_TAC[REAL_LE_TRANS]);;
e(ASM_MESON_TAC[REAL_LE_REFL]);;
e(ASM_MESON_TAC[ARITH_RULE `n + 1 < N ==> n < N`]);;
let tdiv_lemma3 = top_thm();;

g `&0 < g /\ &1 < &N * g /\ 1 <= N
 ==>
(if n + 1 < N then &(n + 1) / &N else &1) -
          (if n < N then &n / &N else &1) < g`;;
e(REPEAT STRIP_TAC THEN SUBGOAL_TAC""`&1 <= &N`[ASM_MESON_TAC[GSYM REAL_LE]]);;
e(ASM_CASES_TAC`n + 1 < N`);;
e(ASM_MESON_TAC[ARITH_RULE `n + 1 < N ==> n < N`; REAL_ADD; REAL_SOSFIELD`&1 < &N * g /\ &1 <= &N ==> (&n + &1) / &N - &n / &N < g`]);;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`~(n + 1 < N) ==> (n = N - 1 \/ ~(n < N))`)));;
e(ASM_MESON_TAC[UNDISCH(ARITH_RULE `1 <= N ==> N - 1 < N`); GSYM REAL_OF_NUM_SUB; REAL_SOSFIELD`&1 < &N * g /\ &1 <= &N ==> &1 - (&N - &1) / &N < g`]);;
e(ASM_MESON_TAC[REAL_SUB_REFL]);;
let fine_lemma = top_thm();;

g`!f N. 1 <= N ==> sum (0,N) f = sum (0..N - 1) f`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPECL[`f:num->real`;`0`;`N:num`]PSUM_SUM_NUMSEG) THEN ASM_SIMP_TAC[LE_1; ADD]);;
let sum_lemma = GSYM(top_thm());;

let dsize_lemma1 = ARITH_RULE`~(N' = N) ==> (N < N' \/ N' < N)`;;
let dsize_lemma1 = ARITH_RULE`~(N:num < N') /\ ~(N' < N) ==> N' = N`;;

g `(!n. n < N'
     ==> (if n < N then &n / &N else &1) <
         (if n + 1 < N then &(n + 1) / &N else &1)) ==> ~(N < N')`;;
e(DISCH_THEN(ASSUME_TAC o (SPEC`N' - 1`)) THEN 
ASM_MESON_TAC[
ARITH_RULE`N < N' ==> N' - 1 < N'`;
ARITH_RULE`N < N' ==> (~(N' - 1 < N) /\ ~((N' - 1) + 1 < N))`;
REAL_ARITH`~(&1 < &1)`;
]);;
let dsize_lemma2 = top_thm();;

g `(!n. n >= N'
            ==> (if n < N then &n / &N else &1) =
                (if N' < N then &N' / &N else &1)) ==> ~(N' < N)`;;
e(DISCH_THEN(ASSUME_TAC o (SPEC`N:num`)) THEN 
ASM_MESON_TAC[
ARITH_RULE`N' < N:num ==> N >= N'`;
ARITH_RULE`~(N < N:num)`;
ARITH_RULE`N' < N ==> 0 < N`;
REAL_LT;
REAL_FIELD`&0 < y /\ x < y ==> ~(&1 = x / y)`;
]);;
let dsize_lemma3 = top_thm();;

(*
MESON[
ARITH_RULE`N' < N ==> 0 < N`;
REAL_LT;
REAL_FIELD`&0 < y /\ x < y ==> ~(&1 = x / y)`;
]`N' < N ==> ~(&1 = &N' / &N)`;;
*)

let dsize_lemma4 = prove( `n < N ==> &n / &N < &(n + 1) / &N /\ &n / &N < &1`,
STRIP_TAC THEN MP_TAC(UNDISCH(ARITH_RULE`n < N ==> 0 < N`)) THEN FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[GSYM REAL_LT; GSYM REAL_ADD] THEN CONV_TAC REAL_SOSFIELD);;

g `!N. 1 <= N
==> (@N'. (!n. n < N'
            ==> (if n < N then &n / &N else &1) <
                (if n + 1 < N then &(n + 1) / &N else &1)) /\
       (!n. n >= N'
            ==> (if n < N then &n / &N else &1) =
                (if N' < N then &N' / &N else &1))) = N`;;
e(REPEAT STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN X_GEN_TAC `N':num` THEN BETA_TAC THEN EQ_TAC);;
e(REPEAT STRIP_TAC THEN MAP_EVERY MP_TAC [dsize_lemma2; dsize_lemma3] THEN ASM_SIMP_TAC[dsize_lemma1]);;
e(STRIP_TAC THEN ASM_MESON_TAC[dsize_lemma4;
ARITH_RULE`n >= N:num ==> ~(n < N)`;
ARITH_RULE`~(N < N:num)`;
]);;
let dsize_lemma5 = top_thm();;

g `!N n. n < N
==>
 (if n + 1 < N then &(n + 1) / &N else &1) -
 (if n < N then &n / &N else &1) = &1 / &N`;;
e(REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`n < N:num ==> n + 1 < N \/ (~(n + 1 < N) /\ N = n + 1)`)));;
e(ASM_SIMP_TAC[GSYM REAL_ADD] THEN REAL_ARITH_TAC);;
e(ASM_SIMP_TAC[GSYM REAL_ADD] THEN CONV_TAC REAL_FIELD);;
let d_lemma1 = top_thm();;

let d_lemma2 = MESON[d_lemma1]`!f (z:num->num->real) N n. n < N
==>
 f (z N n) *
     ((if n + 1 < N then &(n + 1) / &N else &1) -
      (if n < N then &n / &N else &1)) = f (z N n) * &1 / &N`;;

g `!(f:real->real) (z:num->num->real). rintegrable(&0,&1) f /\
         (!N. 1 <= N
                  ==> (!n. if n < N then
                           &n / &N <= z N n /\ z N n <= &(n + 1) / &N
                           else z N n = &1))
         ==>
         (\N. sum (0..N-1) (\n. f (z N n) * &1 / &N)) tends_num_real integral (&0,&1) f`;;
e(ASSUME_TAC REAL_LE_01 THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL[`&0`; `&1`; `f:real->real`]rINTEGRABLE_rdefint) THEN ASM_SIMP_TAC[SEQ; rINTEGRAL_EQ_INTEGRAL] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o (SPEC`e:real`)) THEN ASM_SIMP_TAC[division; tdiv; rsum; dsize] THEN REPEAT STRIP_TAC);;
e(SUBGOAL_THEN`?M. &1 < &M * g`MP_TAC THENL [ASM_MESON_TAC[REAL_ARCH];REPEAT STRIP_TAC]);;
e(SUBGOAL_THEN`!N. N >= M
    ==> abs
        (sum (0..N - 1) (\n. f ((z:num->num->real) N n) * &1 / &N) -
         integral (&0,&1) f) <
        e`ASSUME_TAC);;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_TAC""`&M <= &N`[ASM_MESON_TAC[GE; REAL_LE]]);;
e(SUBGOAL_TAC""`&1 < &N * g`[ASM_MESON_TAC[REAL_SOS`&0 < g /\ &1 < x * g /\ x <= y ==> &1 < y * g`]]);; 
e(ASSUME_TAC(UNDISCH(MESON[REAL_SOS`&1 < x * g ==> ~(&0 = x)`; REAL_INJ; LE_1]`&1 < &N * g ==> 1 <= N`)));;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`N:num`)) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM(ASSUME_TAC o (SPEC`\n:num. if n < N then &n / &N else &1`)));;
e(FIRST_X_ASSUM(MP_TAC o (SPEC`\n. (z:num->num->real) N n`)) THEN BETA_TAC THEN ASM_SIMP_TAC[REAL_DIV_LZERO; ADD1; LE_1]);;
e(ASM_SIMP_TAC[tdiv_lemma2; SPEC`(z:num->num->real)`tdiv_lemma3; fine_lemma; sum_lemma; dsize_lemma5]);;

e(MP_TAC
(SPECL[
`\n. f ((z:num->num->real) N n) *
((if n + 1 < N then &(n + 1) / &N else &1) -
 (if n < N then &n / &N else &1))`;
`\n. f ((z:num->num->real) N n) * &1 / &N`;
`0`;`N:num`]SUM_EQ) THEN BETA_TAC THEN SIMP_TAC[LE_0; ADD_0]);;
e(MESON_TAC[d_lemma2; ]);;
e(ASM_MESON_TAC[]);;
let thm27 = top_thm();;