11 Wellfounded induction
通常の帰納法の原理
# num_INDUCTION;;
val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)
を用いて，Wellfounded induction（整礎帰納法）の原理
# num_WF;;
val it : thm = |- !P. (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)
を証明して見ましょう．なお，num_WFに P 0 が無いように見えますが，m<0を満たすm:numはないので
# ARITH_RULE`!m. m < 0 ==> P m`;;
val it : thm = |- !m. m < 0 ==> P m
# MESON[it]`( (!m. m < 0 ==> P m) ==> P 0 ) <=> P 0`;;
0..0..2..solved at 5
0..0..solved at 2
0..0..solved at 2
val it : thm = |- (!m. m < 0 ==> P m) ==> P 0 <=> P 0
なので，P 0 も含まれています．
num_WFのような複数のステップを仮定する帰納法の原理の証明のポイントは，目標を連言，或いは，その拡張である全称量化の形にしたものを証明し，得られた結果から当初の目標部分のみを利用する点にあります．
実際の証明では，上記の
# ARITH_RULE `m<0 <=> F`;;
val it : thm = |- m < 0 <=> F
および
# ARITH_RULE `(m < SUC n) <=> (m=n \/ m < n)`;;
val it : thm = |- m < SUC n <=> m = n \/ m < n
が重要な働きをしますが，これは
# LT;;
val it : thm = |- (!m. m < 0 <=> F) /\ (!m n. m < SUC n <=> m = n \/ m < n)
に他なりません．
では
# num_WF;;
val it : thm = |- !P. (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)
の結論を取り出して，改めて証明します．
# g( concl it );;
val it : goalstack = 1 subgoal (1 total)`!P. (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)`
# e( REPEAT STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`!n. (!m. m < n ==> P m) ==> P n`]
`P n`
この仮定 0 は任意のnに対して，`(!m. m < n ==> P m) ==> P n` となるということですが，一般に`A ==> B` は `A ==> (A/\B)`と等価なので，これは`(!m. m < n ==> P m) ==> (!m. m < n+1 ==> P m)`
と等価です．
# MESON[LT] ` *1 `;;
0..0..3..solved at 6
0..0..2..5..11..23..46..107..267..solved at 397
0..0..3..solved at 6
0..0..2..6..solved at 11
val it : thm =
|- (!m. m < n ==> P m) ==> P n <=>
(!m. m < n ==> P m) ==> (!m. m < SUC n ==> P m)
従って，中間目標のsubgoalとして `!n. (!m. m
# e( SUBGOAL_THEN `!n. (!m. m
P m)` ASSUME_TAC );;
val it : goalstack = 2 subgoals (2 total)0 [`!n. (!m. m < n ==> P m) ==> P n`]
1 [`!n m. m < n ==> P m`]`P n`
0 [`!n. (!m. m < n ==> P m) ==> P n`]
`!n m. m < n ==> P m`
新たに設けたsubgoalは上記の通り，帰納法で処理できるはずですが
# e( INDUCT_TAC );;
val it : goalstack = 2 subgoals (3 total)0 [`!n. (!m. m < n ==> P m) ==> P n`]
1 [`!m. m < n ==> P m`]`!m. m < SUC n ==> P m`
0 [`!n. (!m. m < n ==> P m) ==> P n`]
`!m. m < 0 ==> P m`
のように，見るからにLTが要りそうですから
# e( ASM_MESON_TAC[LT] );;
0..0..solved at 2
val it : goalstack = 1 subgoal (2 total)0 [`!n. (!m. m < n ==> P m) ==> P n`]
1 [`!m. m < n ==> P m`]`!m. m < SUC n ==> P m`
更に
# e( ASM_MESON_TAC[LT] );;
0..0..2..8..21..48..97..228..574..1455..3845..solved at 7234
val it : goalstack = 1 subgoal (1 total)0 [`!n. (!m. m < n ==> P m) ==> P n`]
1 [`!n m. m < n ==> P m`]`P n`
まで進みます．導入された仮定1は結論を含んでいます．実際，m，nをそれぞれn，SUC nとすればよいのですが，SPECLを用いるまでもなく
# e( ASM_MESON_TAC[] );;
0..0..1..5..13..solved at 24
val it : goalstack = No subgoals
と処理できます．
以上のうち，INDUCT_TAC THEN tac とすると帰納法の2つのsubgoalsに同時にtacを作用させることができ
# prove(
`!P. (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!n. (!m. mP m)` ASSUME_TAC THENL
[ INDUCT_TAC THEN ASM_MESON_TAC[LT] ; ASM_MESON_TAC[]
] );;
0..0..solved at 2
0..0..2..8..21..48..97..228..574..1455..3845..solved at 7234
0..0..1..5..13..solved at 24
val it : thm = |- !P. (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)
となります．
そして，2ステップの仮定をとる帰納法の原理も
# let num2_INDUCTION = prove(
`!P. P 0 /\ P 1 /\ (!n. P n /\ P (SUC n) ==> P (SUC (SUC n)) ) ==> (!n
. P n)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!n. P n /\ P (SUC n)` ASSUME_TAC THENL
[ INDUCT_TAC THEN ASM_SIMP_TAC[ARITH] ; ASM_SIMP_TAC[]
] );;
val num2_INDUCTION : thm =
|- !P. P 0 /\ P 1 /\ (!n. P n /\ P (SUC n) ==> P (SUC (SUC n)))
==> (!n. P n)
と証明できます．ここで，ARITHは:numの定理集（NUM_REDUCE_CONVよりの非力ながら，thmなので*_TAC[]での参照には便利）です．また，2つ目のASM_SIMP_TACはASM_MESON_TACでも構いません．
*1:!m. m < n ==> P m) ==> P n)<=>((!m. m < n ==> P m) ==> (!m. m < SUC n ==> P m
