Example (25.2)

　これで積分の第一平均値定理が通常の形で証明できます．

let CONT_ATTAINS3 = prove
 (`!f:real->real a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> f contl x)
    ==> (?L. (!x. a <= x /\ x <= b ==> L <= f x) /\
             (?x1. a <= x1 /\ x1 <= b /\ f x1 = L)) /\
        (?M. (!x. a <= x /\ x <= b ==> f x <= M) /\
             (?x2. a <= x2 /\ x2 <= b /\ f x2 = M))`,
  SIMP_TAC[CONT_ATTAINS; CONT_ATTAINS2]);;

g `!f g a b.
    a <= b /\ (!x. a <= x /\ x <= b ==> f contl x)
           /\ (!x. a <= x /\ x <= b ==> g contl x)
           /\ (!x. a <= x /\ x <= b ==> &0 <= g x)
    ==> (?z. a <= z /\ z <= b /\
            integral (a,b) (\x. f x * g x) = f z * integral (a,b) g)`;;
e(REPEAT STRIP_TAC THEN MP_TAC(SPEC_ALL CONT_ATTAINS3) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(SUBGOAL_TAC""`integrable (a,b) g`[ASM_MESON_TAC[INTEGRABLE_CONTINUOUS]]);;

e(SUBGOAL_THEN`L * integral (a,b) g <= integral (a,b) (\x. f x * g x) /\ integral (a,b) (\x. f x * g x) <= M * integral (a,b) g`ASSUME_TAC);;
e(ASM_SIMP_TAC[GSYM INTEGRAL_CMUL]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> (\x. L:real * (g:real->real) x) contl x`[ASM_MESON_TAC[CONT_CONST; INST[`(\x:real. L:real)`,`f:real->real`]CONT_MUL;]]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> (\x. M:real * (g:real->real) x) contl x`[ASM_MESON_TAC[CONT_CONST; INST[`(\x:real. M:real)`,`f:real->real`]CONT_MUL;]]);;
e(SUBGOAL_TAC""`integrable (a,b) (\x. L * g x) /\ integrable (a,b) (\x. f x * g x) /\ integrable (a,b) (\x. M * g x)`[ASM_MESON_TAC[CONT_CONST; CONT_MUL; INTEGRABLE_CONTINUOUS]]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> L * g x <= f x * g x /\ f x * g x <= M * g x`[ASM_MESON_TAC[REAL_LE_RMUL]] THEN ASM_SIMP_TAC[INTEGRAL_LE]);;

e(SUBGOAL_TAC""`&0 <= integral (a,b) g`[ASM_SIMP_TAC[INTEGRAL_POS_LE]] THEN ABBREV_TAC `K = integral (a,b) g`);;
e(DISJ_CASES_TAC(UNDISCH(REAL_ARITH`&0 <= K ==> &0 < K \/ K = &0`)));;

e(MAP_EVERY MP_TAC[
SPECL[`K:real`;`L:real`;`integral (a,b) (\x. f x * g x)`]REAL_LE_RDIV;
SPECL[`K:real`;`integral (a,b) (\x. f x * g x)`;`M:real`]REAL_LE_LDIV] THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC );;
e(DISJ_CASES_TAC(REAL_ARITH`x1 <= x2 \/ x2 <= x1`));;
e(MP_TAC(SPECL[`f:real->real`;`x1:real`;`x2:real`;`integral (a,b) (\x. f x * g x) / K`]IVT) THEN SUBGOAL_TAC""`(!x. x1 <= x /\ x <= x2 ==> f contl x)`[ASM_MESON_TAC[REAL_LE_TRANS]] THEN ASM_SIMP_TAC[REAL_EQ_RDIV_EQ] THEN ASM_MESON_TAC[REAL_LE_TRANS]);;
e(MP_TAC(SPECL[`f:real->real`;`x2:real`;`x1:real`;`integral (a,b) (\x. f x * g x) / K`]IVT2) THEN SUBGOAL_TAC""`(!x. x2 <= x /\ x <= x1 ==> f contl x)`[ASM_MESON_TAC[REAL_LE_TRANS]] THEN ASM_SIMP_TAC[REAL_EQ_RDIV_EQ] THEN ASM_MESON_TAC[REAL_LE_TRANS]);;

e(DISJ_CASES_TAC(UNDISCH(REAL_ARITH`a <= b ==> a = b \/ a < b`)));;

e(ASM_MESON_TAC[REAL_LE_ANTISYM; INTEGRAL_NULL; DEFINT_INTEGRAL; REAL_MUL_RZERO]);;
e(SUBGOAL_TAC""`!x. a <= x /\ x <= b ==> g x = &0`[MATCH_MP_TAC INTEGRAL_POS_EQ_0 THEN ASM_SIMP_TAC[]]);;

e(EXISTS_TAC `a:real` THEN ASM_SIMP_TAC[REAL_LE_REFL; REAL_MUL_RZERO]);;
e(MATCH_MP_TAC DEFINT_INTEGRAL THEN ASM_SIMP_TAC[] THEN MATCH_MP_TAC INTEGRAL_EQ THEN EXISTS_TAC `\x:real. &0` THEN BETA_TAC THEN ASM_SIMP_TAC[DEFINT_0; REAL_MUL_RZERO]);;

let INTEGRAL_MVT_1 = top_thm();;