Examples (2)
m:numから始まる帰納法の原理numm_INDUCTIONを証明し，それを適用するtactic，INDUCTm_TACを定義しましょう．
まずは肩慣らしに，1から始まるものを証明して見ます．
g ( `!P. P 1 /\ (!n. 1 <= n ==> P n ==> P (SUC n) ) ==> (!n. 1 <= n ==> P n)`
);;
e ( STRIP_TAC THEN STRIP_TAC );;
e ( INDUCT_TAC );;
e( ARITH_TAC );;
e( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`] ) );;
e( REWRITE_TAC[ARITH_RULE`1<=SUC n<=>(n=0\/1<=n)`] );;
e( DISCH_THEN(DISJ_CASES_TAC) );;
e( ASM_SIMP_TAC[ARITH] );;
e( ASM_SIMP_TAC[] );;
実行すると
# g ( `!P. P 1 /\ (!n. 1 <= n ==> P n ==> P (SUC n) ) ==> (!n. 1 <= n ==> P n)`
);;
val it : goalstack = 1 subgoal (1 total)`!P. P 1 /\ (!n. 1 <= n ==> P n ==> P (SUC n)) ==> (!n. 1 <= n ==> P n)`
# e ( STRIP_TAC THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`P 1`]
1 [`!n. 1 <= n ==> P n ==> P (SUC n)`]`!n. 1 <= n ==> P n`
# e ( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)0 [`P 1`]
1 [`!n. 1 <= n ==> P n ==> P (SUC n)`]
2 [`1 <= n ==> P n`]`1 <= SUC n ==> P (SUC n)`
0 [`P 1`]
1 [`!n. 1 <= n ==> P n ==> P (SUC n)`]`1 <= 0 ==> P 0`
# e( ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`P 1`]
1 [`!n. 1 <= n ==> P n ==> P (SUC n)`]
2 [`1 <= n ==> P n`]`1 <= SUC n ==> P (SUC n)`
# e( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`] ) );;
val it : goalstack = 1 subgoal (1 total)0 [`P 1`]
1 [`1 <= n ==> P n`]
2 [`1 <= n ==> P n ==> P (SUC n)`]`1 <= SUC n ==> P (SUC n)`
# e( REWRITE_TAC[ARITH_RULE`1<=SUC n<=>(n=0\/1<=n)`] );;
val it : goalstack = 1 subgoal (1 total)0 [`P 1`]
1 [`1 <= n ==> P n`]
2 [`1 <= n ==> P n ==> P (SUC n)`]`n = 0 \/ 1 <= n ==> P (SUC n)`
# e( DISCH_THEN(DISJ_CASES_TAC) );;
val it : goalstack = 2 subgoals (2 total)0 [`P 1`]
1 [`1 <= n ==> P n`]
2 [`1 <= n ==> P n ==> P (SUC n)`]
3 [`1 <= n`]`P (SUC n)`
0 [`P 1`]
1 [`1 <= n ==> P n`]
2 [`1 <= n ==> P n ==> P (SUC n)`]
3 [`n = 0`]`P (SUC n)`
# e( ASM_SIMP_TAC[ARITH] );;
val it : goalstack = 1 subgoal (1 total)0 [`P 1`]
1 [`1 <= n ==> P n`]
2 [`1 <= n ==> P n ==> P (SUC n)`]
3 [`1 <= n`]`P (SUC n)`
# e( ASM_SIMP_TAC[] );;
val it : goalstack = No subgoals
まとめると
prove ( `!P. P 1 /\ (!n. 1 <= n ==> P n ==> P (SUC n) ) ==> (!n. 1 <= n ==> P n)` ,
( STRIP_TAC THEN STRIP_TAC ) THEN
( INDUCT_TAC ) THENL
[( ARITH_TAC ) ;
( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`] ) ) THEN
( REWRITE_TAC[ARITH_RULE`1<=SUC n<=>(n=0\/1<=n)`] ) THEN
( DISCH_THEN(DISJ_CASES_TAC) THEN ASM_SIMP_TAC[ARITH] )
] );;
同様に，mから始まる帰納法の原理は
g ( `!m:num. !P. P m /\ (!n. m <= n ==> P n ==> P (SUC n) ) ==> (!n. m <= n ==> P n)` );;
e ( STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC );;
e ( INDUCT_TAC );;
e ( ASM_MESON_TAC[LE;ARITH] );;
e ( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`]) );;
e ( REWRITE_TAC[ARITH_RULE`m<=SUC n<=>(m=SUC n\/m<=n)`] );;
e ( DISCH_THEN(DISJ_CASES_TAC) );;
e ( ASM_MESON_TAC );;
e ( ASM_MESON_TAC );;
実行すると
# g ( `!m:num. !P. P m /\ (!n. m <= n ==> P n ==> P (SUC n) ) ==> (!n. m <= n =
=> P n)` );;
val it : goalstack = 1 subgoal (1 total)`!m P. P m /\ (!n. m <= n ==> P n ==> P (SUC n)) ==> (!n. m <= n ==> P n)`
# e ( STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`P m`]
1 [`!n. m <= n ==> P n ==> P (SUC n)`]`!n. m <= n ==> P n`
# e ( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)0 [`P m`]
1 [`!n. m <= n ==> P n ==> P (SUC n)`]
2 [`m <= n ==> P n`]`m <= SUC n ==> P (SUC n)`
0 [`P m`]
1 [`!n. m <= n ==> P n ==> P (SUC n)`]`m <= 0 ==> P 0`
# e ( ASM_MESON_TAC[LE;ARITH] );;
0..0..16..95..566..solved at 576
val it : goalstack = 1 subgoal (1 total)0 [`P m`]
1 [`!n. m <= n ==> P n ==> P (SUC n)`]
2 [`m <= n ==> P n`]`m <= SUC n ==> P (SUC n)`
# e ( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`]) );;
val it : goalstack = 1 subgoal (1 total)0 [`P m`]
1 [`m <= n ==> P n`]
2 [`m <= n ==> P n ==> P (SUC n)`]`m <= SUC n ==> P (SUC n)`
# e ( REWRITE_TAC[ARITH_RULE`m<=SUC n<=>(m=SUC n\/m<=n)`] );;
val it : goalstack = 1 subgoal (1 total)0 [`P m`]
1 [`m <= n ==> P n`]
2 [`m <= n ==> P n ==> P (SUC n)`]`m = SUC n \/ m <= n ==> P (SUC n)`
# e ( DISCH_THEN(DISJ_CASES_TAC) );;
val it : goalstack = 2 subgoals (2 total)0 [`P m`]
1 [`m <= n ==> P n`]
2 [`m <= n ==> P n ==> P (SUC n)`]
3 [`m <= n`]`P (SUC n)`
0 [`P m`]
1 [`m <= n ==> P n`]
2 [`m <= n ==> P n ==> P (SUC n)`]
3 [`m = SUC n`]`P (SUC n)`
# e ( ASM_MESON_TAC );;
0..0..solved at 3
0..0..solved at 3
0..0..solved at 4
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
val it : goalstack = 1 subgoal (1 total)0 [`P m`]
1 [`m <= n ==> P n`]
2 [`m <= n ==> P n ==> P (SUC n)`]
3 [`m <= n`]`P (SUC n)`
# e ( ASM_MESON_TAC );;
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val it : goalstack = No subgoals
まとめると
# let numm_INDUCTION = prove ( `!m:num. !P. P m /\ (!n. m <= n ==> P n ==> P (SUC n) ) ==> (!n. m <= n ==> P n)` ,
( STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC ) THEN
( INDUCT_TAC ) THENL
[( ASM_MESON_TAC[LE;ARITH] ) ;
( FIRST_X_ASSUM(ASSUME_TAC o SPECL[`n:num`]) ) THEN
( REWRITE_TAC[ARITH_RULE`m<=SUC n<=>(m=SUC n\/m<=n)`] ) THEN
( DISCH_THEN(DISJ_CASES_TAC) THEN ASM_MESON_TAC[] )
] );;
0..0..16..95..566..solved at 576
0..0..solved at 3
0..0..solved at 3
0..0..solved at 4
0..0..solved at 2
0..0..solved at 3
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
0..0..solved at 2
val numm_INDUCTION : thm =
|- !m P. P m /\ (!n. m <= n ==> P n ==> P (SUC n)) ==> (!n. m <= n ==> P n)# let INDUCTm_TAC = MATCH_MP_TAC numm_INDUCTION THEN CONJ_TAC THENL [ ALL_TAC ; GEN_TAC THEN DISCH_TAC THEN DISCH_TAC] ;;
val ( INDUCTm_TAC ) : tactic =
となります．
なお，numm_INDUCTION の後半の処理は ASM_MESON_TAC 任せにして
# prove
(`!P m. P m /\ (!n. m <= n /\ P n ==> P (SUC n)) ==> (!n. m <= n ==> P n)`,
STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
INDUCT_TAC THEN
ASM_MESON_TAC [LE]);;
0..0..1..2..5..solved at 11
0..0..2..4..11..25..solved at 44
0..0..1..2..6..13..29..56..solved at 77
val it : thm =
|- !P m. P m /\ (!n. m <= n /\ P n ==> P (SUC n)) ==> (!n. m <= n ==> P n)
とすることも出来ます．
