Examples (3)
今回は，分数関数の和の例です．キーとなるthmは，:realの元の和sumについての
# SUM_CLAUSES_NUMSEG;;
val it : thm =
|- (!m. sum (m..0) f = (if m = 0 then f 0 else &0)) /\
(!m n.
sum (m..SUC n) f =
(if m <= SUC n then sum (m..n) f + f (SUC n) else sum (m..n) f))
です．
先に述べたmからの帰納法，INDUCTm_TACを用います．また，よく用いるので
# let REAL_FIELD_TAC = CONV_TAC REAL_FIELD ;;
val ( REAL_FIELD_TAC ) : tactic =
としておきます．
g `!n. 1<=n ==> sum(1..n)(\k. &1/( &k * ( &k+ &1) ) )= &n/( &n+ &1)`;;
e INDUCTm_TAC;;
e (SIMP_TAC[SUM_CLAUSES_NUMSEG;SUM_SING_NUMSEG] THEN ARITH_TAC);;
e (ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;ARITH_RULE`1<=SUC n`]);;
e(SIMP_TAC[GSYM REAL_OF_NUM_SUC]);;
e(REAL_FIELD_TAC);;
実行すると
# g `!n. 1<=n ==> sum(1..n)(\k. &1/( &k * ( &k+ &1) ) )= &n/( &n+ &1)`;;
val it : goalstack = 1 subgoal (1 total)`!n. 1 <= n ==> sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`
# e INDUCTm_TAC;;
val it : goalstack = 2 subgoals (2 total)0 [`1 <= n`]
1 [`sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`]`sum (1..SUC n) (\k. &1 / (&k * (&k + &1))) = &(SUC n) / (&(SUC n) + &1)`
`sum (1..1) (\k. &1 / (&k * (&k + &1))) = &1 / (&1 + &1)`
# e (SIMP_TAC[SUM_CLAUSES_NUMSEG;ARITH_RULE`1..1=1..SUC 0`] THEN ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`1 <= n`]
1 [`sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`]`sum (1..SUC n) (\k. &1 / (&k * (&k + &1))) = &(SUC n) / (&(SUC n) + &1)`
# e (ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;ARITH_RULE`1<=SUC n`]);;
val it : goalstack = 1 subgoal (1 total)0 [`1 <= n`]
1 [`sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`]`&n / (&n + &1) + &1 / (&(SUC n) * (&(SUC n) + &1)) =
&(SUC n) / (&(SUC n) + &1)`# e(SIMP_TAC[MESON[REAL_OF_NUM_SUC]`&(SUC n)= &n+ &1`]);;
0..0..1..2..solved at 6
val it : goalstack = 1 subgoal (1 total)0 [`1 <= n`]
1 [`sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`]`&n / (&n + &1) + &1 / ( (&n + &1) * ( (&n + &1) + &1)) =
(&n + &1) / ( (&n + &1) + &1)`# e(REAL_FIELD_TAC);;
1 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 3 critical pairs
4 basis elements and 5 critical pairs
5 basis elements and 0 critical pairs
val it : goalstack = No subgoals
まとめると
prove
(`!n. 1<=n ==> sum(1..n)(\k. &1/( &k * ( &k+ &1) ) )= &n/( &n+ &1)`,
INDUCTm_TAC THEN
ASM_SIMP_TAC[
SUM_CLAUSES_NUMSEG;
ARITH_RULE`1<=SUC n /\ 1..1=1..SUC 0`;
GSYM REAL_OF_NUM_SUC] THEN
REAL_FIELD_TAC );;
もし
needs "Library/analysis.ml";;
として
# REAL;;
val it : thm = |- !n. &(SUC n) = &n + &1
が使えるなら
# prove
(`!n. 1 <= n ==> sum(1..n)(\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)`,
INDUCTm_TAC THEN
ASM_SIMP_TAC [SUM_SING_NUMSEG;SUM_CLAUSES_NUMSEG;
ARITH_RULE`1 <= SUC n`;REAL] THEN
REAL_FIELD_TAC);;
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 3 critical pairs
4 basis elements and 5 critical pairs
5 basis elements and 0 critical pairs
val it : thm =
|- !n. 1 <= n ==> sum (1..n) (\k. &1 / (&k * (&k + &1))) = &n / (&n + &1)<<
とできます．全く同じ手順で
prove
(`!n. 1<=n ==> sum(1..n)(\k. ( &k + &3)/( &k * ( &k+ &1) * ( &k+ &2) ))= (&5 * &n + &11) * &n /( &4 * ( &n+ &1) * (&n + &2) )`,
INDUCTm_TAC THEN
ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;
SUM_SING_NUMSEG;
ARITH_RULE `1 <= SUC n`;
REAL] THEN
REAL_FIELD_TAC );;
...
val it : thm =
|- !n. 1 <= n
==> sum (1..n) (\k. (&k + &3) / (&k * (&k + &1) * (&k + &2))) =
(&5 * &n + &11) * &n / (&4 * (&n + &1) * (&n + &2))# prove(
`!n. sum(0..n)(\k. (&2 pow k)*(&k pow 2))= (&2 pow (SUC n))*(&n pow 2- &2* &n
- &3)- &6`,
INDUCT_TAC THEN
ASM_SIMP_TAC [SUM_CLAUSES_NUMSEG;REAL;
LE_0;GSYM ADD1;real_pow] THEN
REAL_FIELD_TAC);;
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
val it : thm =
|- !n. sum (0..n) (\k. &2 pow k * &k pow 2) =
&2 pow SUC n * (&n pow 2 - &2 * &n + &3) - &6も得られます．
