Example (24.3)

　の絶対値の積分において，絶対値記号を外に出すには定符号を言えば良いわけです．もし変数変換が使えるならに帰着する道もありそうですが，それらしいthmは見当たりませんので，の偶奇により場合を分けて行きます．

g `!m y. (&2 * &m) * pi <= y /\ y <= (&2 * &m + &1) * pi ==> &0 <= sin y`;;
e(INDUCT_TAC);;
e(REPEAT STRIP_TAC THEN MATCH_MP_TAC SIN_POS_PI_LE THEN ASM_ARITH_TAC);;
e(GEN_TAC THEN FIRST_X_ASSUM(MP_TAC o (SPEC `y - &2 * pi`) o (CONV_RULE(ONCE_REWRITE_CONV[GSYM SIN_PERIODIC]))) THEN SIMP_TAC[REAL; REAL_SUB_ADD] THEN ASM_ARITH_TAC);;
let SIN_POS_PERIODIC = top_thm();;
g `!m y. (&2 * &m - &1) * pi <= y /\ y <= (&2 * &m) * pi ==> &0 <= --sin y`;;
e(REPEAT GEN_TAC THEN MP_TAC(SPECL[`m:num`; `y + pi:real`]SIN_POS_PERIODIC) THEN SIMP_TAC[GSYM SIN_PERIODIC_PI] THEN ASM_ARITH_TAC);;
let SIN_NEG_PERIODIC = top_thm();;

let lemma01 = MESON[REAL_LE; REAL_ARITH `&1 <= &n ==> &0 < &n`; REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; PI_POS; REAL_LE_LMUL_EQ; REAL_MUL_AC]
`1 <= n
==> (&(k - 1) / &n <= x /\ x <= &k / &n
<=> &(k - 1) * pi <= &n * pi * x /\ &n * pi * x <= &k * pi)`;;

g `!n. 1 <= n
 ==> !k. 1 <= k /\ k <= n
 ==> ((!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> &0 <= sin (&n * pi * x)) \/
 (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> &0 <= --sin (&n * pi * x)))`;;
e(REPEAT STRIP_TAC THEN ASM_SIMP_TAC[UNDISCH lemma01; GSYM REAL_OF_NUM_SUB] THEN DISJ_CASES_TAC (SPEC `k:num` EVEN_OR_ODD));;
e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[GSYM REAL_MUL] THEN MESON_TAC[REAL_MUL_AC; SIN_NEG_PERIODIC]);;
e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[ODD_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[ADD1; GSYM REAL_ADD; GSYM REAL_MUL; ] THEN ASM_MESON_TAC[REAL_ADD_AC; REAL_ADD_SUB; REAL_MUL_AC; SIN_POS_PERIODIC]);;
let thm16 = top_thm();;

g `!n. 1 <= n
 ==> !k. 1 <= k /\ k <= n
 ==> !x. &(k - 1) / &n <= x /\ x <= &k / &n
 ==> abs (sin (&n * pi * x))= (-- &1 pow (k + 1) ) * sin (&n * pi * x)`;;
e(STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[UNDISCH lemma01; GSYM REAL_OF_NUM_SUB;] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC (SPEC `k:num` EVEN_OR_ODD));;

e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC);;
e(MP_TAC(SPECL[`m:num`;`&n * pi * x`]SIN_NEG_PERIODIC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC[REAL_MUL] THEN ONCE_ASM_SIMP_TAC[GSYM ABS_NEG] THEN STRIP_TAC);;
e(ASM_SIMP_TAC[real_abs; POW_ADD; POW_MINUS1; POW_1] THEN REAL_ARITH_TAC);;

e(FIRST_X_ASSUM MP_TAC THEN SIMP_TAC[ODD_EXISTS; ADD1; GSYM REAL_ADD] THEN STRIP_TAC);;
e(MP_TAC(SPECL[`m:num`;`&n * pi * x`]SIN_POS_PERIODIC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN SIMP_TAC[REAL_ADD; REAL_MUL] THEN SUBGOAL_TAC""`&(2 * m + 1) - &1 = &(2 * m)`[ASM_MESON_TAC[REAL_OF_NUM_SUB; REAL_ADD_SUB; ADD_SUB;]]);;
e(FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC);; 
e(ASM_SIMP_TAC[real_abs; ARITH_RULE`(2 * m + 1) + 1 = 2 * (m + 1)`; POW_MINUS1] THEN REAL_ARITH_TAC);;
let thm17 = top_thm();;
let thm17 = MESON[thm17]
`!n k x. 1 <= n /\ 1 <= k /\ k <= n /\ &(k - 1) / &n <= x /\ x <= &k / &n
 ==> abs (sin (&n * pi * x))= (-- &1 pow (k + 1) ) * sin (&n * pi * x)`;;