Example (22.7)

　同様に第２の和も表せることの証明です．thm8_2はthm7_2を含んだ形になりました．

g`!n xn k. n < 2 EXP SUC xn /\ 1 <= xn /\ 2 EXP xn + 1 <= k /\ k <= n ==> ?x y. &2 pow xn / &k = &x / &y /\ EVEN x /\ ODD y`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(
prove(`2 EXP xn + 1 <= k /\ k <= n /\ n < 2 EXP SUC xn ==> 1 <= k /\ k < 2 EXP SUC xn /\ ~(k = 2 EXP xn)`,
SIMP_TAC[EXP] THEN MP_TAC(MESON[TWO; ZERO_LESS_EXP]`0 < 2 EXP xn`) THEN CONV_TAC SOS_RULE)
) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC (SPECL[`xn:num`;`k:num`]thm4) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM REAL_MUL; GSYM REAL_OF_NUM_POW; REAL_FIELD`a/(b*c)=(a/b)/c`]);;
e(ASSUME_TAC(ARITH_RULE`~(&2 = &0)`) THEN ASM_SIMP_TAC[REAL_DIV_POW2_ALT; REAL_OF_NUM_POW]);;
e(ASM_MESON_TAC[
MESON[ARITH_RULE`EVEN(2)`; LE_1; EVEN_EXP]`!x. 0 < x ==> EVEN (2 EXP x)`;
ARITH_RULE`a<b <=> 0<b-a`]);;
let thm8_1 = top_thm();;

g`!a b:num->real. !s m. (!k. s <= k /\ k <= m ==> ?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y) ==> ?x y. sum (s..m) (\k. a k / b k) = &x / &y /\ EVEN x /\ ODD y`;;
e(STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC);;
e(INDUCT_TAC);;
e(SIMP_TAC[my; ARITH] THEN DISCH_THEN(MP_TAC o (SPEC`0`)) THEN SIMP_TAC[ARITH_RULE`s <= 0 /\ 0 <= 0 <=> s = 0`] THEN MESON_TAC[REAL_FIELD`&0 = &0 / &1`; ARITH_RULE`EVEN 0 /\ ODD 1`]);;
e(DISJ_CASES_THEN ASSUME_TAC (ARITH_RULE`SUC m < s \/ s <= SUC m`));;
e(ASM_MESON_TAC[SUM_TRIV_NUMSEG; REAL_FIELD`&0 = &0 / &1`; ARITH_RULE`EVEN 0 /\ ODD 1`]);;
let lemma = MESON[ARITH_RULE`k <= m ==> k <= SUC m`; LE_REFL]
    `s <= SUC m /\ (!k. s <= k /\ k <= SUC m
     ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y)) ==>
     (!k. s <= k /\ k <= m
     ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y))
     /\ (?x y. a (SUC m) / b (SUC m) = &x / &y /\ EVEN x /\ ODD y)`;;
e(STRIP_TAC THEN MP_TAC lemma THEN ASM_SIMP_TAC[my; ARITH] THEN STRIP_TAC THEN UNDISCH_TAC `(!k. s <= k /\ k <= m
      ==> (?x y. a k / b k = &x / &y /\ EVEN x /\ ODD y))
 ==> (?x y. sum (s..m) (\k. a k / b k) = &x / &y /\ EVEN x /\ ODD y)` THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(ASM_MESON_TAC[thm6]);;
let thm8_2 = top_thm();;

g`!xn. 1 <= xn /\ n < 2 EXP SUC xn ==> ?x y. sum (2 EXP xn + 1..n) (\k. &2 pow xn / &k)  = &x / &y /\ EVEN x /\ ODD y`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPECL[`\k:num. &2 pow xn`;`\k. &k`;`2 EXP xn + 1`;`n:num`]thm8_2) THEN BETA_TAC THEN ASM_MESON_TAC[thm8_1]);;
let thm8 = top_thm();;