Example (25.1)

　落穂ひろい気味ですが，先のthm15から&0 < integral (a,b) gという仮定を外して，積分の第一平均値定理を得るための補題の証明です．

let INTEGRAL_CONST_LE = prove
 (`!c g a b.
    a <= b /\ integrable (a,b) g /\ (!x. a <= x /\ x <= b ==> c <= g x)
    ==> c * (b - a) <= integral (a,b) g`,
  GEN_TAC THEN MP_TAC(SPEC `\x:real. c:real` INTEGRAL_LE) THEN
  SIMP_TAC[INTEGRABLE_CONST; INTEGRAL_CONST]);;

let INTEGRAL_COMBINE_2 = MESON [DEFINT_COMBINE; INTEGRABLE_COMBINE; INTEGRABLE_DEFINT; DEFINT_INTEGRAL; REAL_LE_TRANS]
`!f a b c. a <= c /\ c <= b /\ integrable (a,c) f /\ integrable (c,b) f
    ==> integral (a,b) f = integral (a,c) f + integral (c,b) f`;;

let INTEGRAL_COMBINE = MESON [INTEGRABLE_SUBINTERVAL_LEFT; INTEGRABLE_SUBINTERVAL_RIGHT; INTEGRAL_COMBINE_2]
`!f a b c. a <= c /\ c <= b /\ integrable (a,b) f
    ==> integral (a,b) f = integral (a,c) f + integral (c,b) f`;;

let INTEGRAL_COMBINE_3 = prove
 (`!f a b c d. a <= b /\ b <= c /\ c <= d /\ integrable (a,d) f
    ==> integral (a,d) f = integral (a,b) f + integral (b,c) f + integral (c,d) f`,
  REPEAT STRIP_TAC THEN 
  SUBGOAL_TAC "" `integral (b,c) f + integral (c,d) f = integral (b,d)f`
   [ASM_MESON_TAC[INTEGRABLE_SUBINTERVAL_RIGHT; INTEGRAL_COMBINE; REAL_LE_TRANS]] THEN
  ASM_MESON_TAC[INTEGRAL_COMBINE; REAL_LE_TRANS]);;

g `!a b f. a < b /\
   (!x. a <= x /\ x <= b ==> &0 <= f x) /\
   (!x. a <= x /\ x <= b ==> f contl x) /\
   integral (a,b) f = &0
   ==> (!x. a <= x /\ x <= b ==> f x = &0)`;;
e(REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC[NOT_FORALL_THM; NOT_IMP] THEN REPEAT STRIP_TAC THEN ABBREV_TAC `m = (f:real->real) x`);;
e(SUBGOAL_TAC""`&0 < m / &2`[ASM_MESON_TAC[REAL_ARITH`~(m = &0) /\ &0 <= m ==> &0 < m / &2`]]);;
(*
e(SUBGOAL_TAC""`&0 < m / &2`[ASM_MESON_TAC[REAL_ABS_NZ; ABS_REFL; REAL_LT_HALF1]]);;
*)
e(SUBGOAL_THEN`f contl x`MP_TAC THENL [ASM_SIMP_TAC[]; SIMP_TAC[CONTL] THEN DISCH_THEN(MP_TAC o UNDISCH o SPEC `m / &2`) THEN STRIP_TAC]);;
e(SUBGOAL_TAC""`integrable (a,b) f`[ASM_SIMP_TAC[INTEGRABLE_CONTINUOUS]]);;
e(ABBREV_TAC `a' = max a (x - d / &2)` THEN ABBREV_TAC `b' = min b (x + d / &2)`);;
e(MP_TAC(REAL_FIELD`a < b /\ a <= x /\ x <= b /\ &0 < d /\ max a (x - d / &2) = a' /\ min b (x + d / &2) = b' ==> a <= a'  /\ a' <= b' /\ a' < b' /\ b' <= b`) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;

e(SUBGOAL_TAC""`!x. a <= x /\ x <= a' ==> &0 <= f x`[ASM_MESON_TAC[REAL_LE_TRANS]]);;
e(SUBGOAL_TAC""`&0 <= integral (a,a') f`[ONCE_REWRITE_TAC[SPEC`a' - a:real`(GSYM REAL_MUL_LZERO)] THEN MATCH_MP_TAC INTEGRAL_CONST_LE THEN ASM_MESON_TAC[INTEGRABLE_SUBINTERVAL_LEFT; REAL_LE_TRANS]]);;

e(SUBGOAL_TAC""`!x'. a' <= x' /\ x' <= b' ==> m / &2 <= f x'`[ASM_MESON_TAC[REAL_FIELD`&0 < d /\ max a (x - d / &2) <= x' /\ x' <= min b (x + d / &2) ==> abs (x' - x) < d`; REAL_FIELD`&0 < m / &2 /\ abs (y - m) < m / &2 ==> m / &2 <= y`]]);;
e(SUBGOAL_TAC""`m / &2 * (b' - a') <= integral (a',b') f`[MATCH_MP_TAC INTEGRAL_CONST_LE THEN ASM_MESON_TAC[INTEGRABLE_SUBINTERVAL]]);;

e(SUBGOAL_TAC""`!x. b' <= x /\ x <= b ==> &0 <= f x`[ASM_MESON_TAC[REAL_LE_TRANS]]);;
e(SUBGOAL_TAC""`&0 <= integral (b',b) f`[ONCE_REWRITE_TAC[SPEC`b - b':real`(GSYM REAL_MUL_LZERO)] THEN MATCH_MP_TAC INTEGRAL_CONST_LE THEN ASM_MESON_TAC[INTEGRABLE_SUBINTERVAL_RIGHT; REAL_LE_TRANS]]);;

e(SUBGOAL_TAC""`&0 < integral (a,b) f`
 [ASM_MESON_TAC
  [INTEGRAL_COMBINE_3;
   (*REAL_SOSFIELD `a < b /\ &0 < m / &2 ==> &0 < &0 + m / &2 * (b - a) + &0`;*)
   SIMP_CONV[REAL_SUB_LT; REAL_ADD_LID; REAL_ADD_RID; REAL_LT_MUL]
    `a' < b' /\ &0 < m / &2 ==> &0 < &0 + m / &2 * (b' - a') + &0`;
   REAL_LE_ADD2; REAL_LTE_TRANS]]);;
e(ASM_MESON_TAC[REAL_LT_REFL]);;
let INTEGRAL_POS_EQ_0 = top_thm();;