8.1 The goalstack (4)
便利なtheorem-tacticとtheorem-tacticalを幾つか述べます．
■ ASSUME_TAC thmとして仮定を追加する代わりに，LABELTAC_TAC "ラベル" thm とすると，その仮定にラベルが付けられます（というより，LABEL_TAC "" がASSUME_TACの実体です）．
■ また，結論がimpliesのとき，その前件を仮定にまわす際，DISCH_TACの代わりに，DISCH_THEN ( LABEL_TAC "ラベル" ) とすればラベルが付けられます．
# g `a ==> ( a ==> b ) ==> b` ;;
Warning: Free variables in goal: a, b
val it : goalstack = 1 subgoal (1 total)`a ==> (a ==> b) ==> b`
# e ( DISCH_THEN (LABEL_TAC "00") );;
val it : goalstack = 1 subgoal (1 total)0 [`a`] (00)
`(a ==> b) ==> b`
# e ( DISCH_THEN (LABEL_TAC "01") );;
val it : goalstack = 1 subgoal (1 total)0 [`a`] (00)
1 [`a ==> b`] (01)`b`
ラベルの付いた仮定p（のASSUME`p`つまりp|-p）をMP_TACに参照させるには，USE_THEN "ラベル" MP_TAC とします（参照後，仮定を除去するならREMOVE_THEN）．
# e ( USE_THEN "00" MP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`a`] (00)
1 [`a ==> b`] (01)`a ==> b`
# e ( ASM_REWRITE_TAC [] );;
val it : goalstack = No subgoals
このDISCH_THENは，結論がimplesのとき，その前件pを切取り，処理中は仮定に加えながら，p|-pを引数のtheorem-tacticに渡しますが，自身はpを仮定に加えません．従って，pが仮定に入っていなくても
DISCH_THEN ASSUME_TAC（DISCH_TACの実体）やDISCH_THEN MP_TACは失敗しません．
# g ( `1=a ==> a EXP 2 =1` );;
Warning: Free variables in goal: a
val it : goalstack = 1 subgoal (1 total)`1 = a ==> a EXP 2 = 1`
# e ( DISCH_THEN ( ASSUME_TAC o SYM ) ) ;;
val it : goalstack = 1 subgoal (1 total)0 [`a = 1`]
`a EXP 2 = 1`
# e ( ASM_REWRITE_TAC [ ARITH ] );;
val it : goalstack = No subgoals
■ なお，theoremの結論が連言の際，その個々を結論とするtheoremをASSUME_TACやMP_TACのようなtheorem-tacticに与え，THENで結合したtheorem-tacticを作るには，CONJUNCTS_THEN(: thm_tactical =
DISCH_THEN ( CONJUNCTS_THEN ASSUME_TAC )
DISCH_THEN ( CONJUNCTS_THEN MP_TAC )
連言項の個数が３以上なら，REPEATのthm_tactical版である REPEAT_TCL を CONJUNCTS_THEN に適用して
DISCH_THEN ( ( REPEAT_TCL CONJUNCTS_THEN ) ASSUME_TAC )
DISCH_THEN ( ( REPEAT_TCL CONJUNCTS_THEN ) MP_TAC )
とすれば
...
`&0 < x /\ &0 < y /\ &0 < z ==> &0 < x * y * z`# e ( DISCH_THEN ( ( REPEAT_TCL CONJUNCTS_THEN ) ASSUME_TAC ) );;
val it : goalstack = 1 subgoal (1 total)0 [`&0 < x`]
1 [`&0 < y`]
2 [`&0 < z`]`&0 < x * y * z`
そして
...
`&0 < x /\ &0 < y /\ &0 < z ==> &0 < x * y * z`# e ( DISCH_THEN ( ( REPEAT_TCL CONJUNCTS_THEN ) MP_TAC ) );;
val it : goalstack = 1 subgoal (1 total)`&0 < z ==> &0 < y ==> &0 < x ==> &0 < x * y * z`
のようになります．
■ 逆に，仮定pを結論の前件にまわすには
0 [`a`]
1 [`a ==> b`]`b`
# e(UNDISCH_TAC`a==>b`);;
val it : goalstack = 1 subgoal (1 total)0 [`a`]
`(a ==> b) ==> b`
のようにUNDISCH_TAC tmを用います．上の例で`a`を前件にまわしたいならhol_typeも明示してUNDSICH_TAC `a:bool`とします．また，UNDISCH_TACと同様に，UNDISCH_TAC tm の実体は，UNDISCH_THEN tm MP_TACであり，このUNDISCH_THEN(: term -> thm_tactic -> tactic =
0 [`a`]
1 [`a ==> b`]`b`
# e(UNDISCH_THEN`a:bool`ASSUME_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`a ==> b`]
1 [`a`]`b`
のように仮定の並べ替えができます．
■ 8.1 The goalstack (2)で扱ったような対称式の証明には
# search[name"WLOG"];;
val it : (string * thm) list =
[("REAL_WLOG_LE",
|- (!x y. P x y <=> P y x) /\ (!x y. x <= y ==> P x y) ==> (!x y. P x y));
("REAL_WLOG_LT",
|- (!x. P x x) /\ (!x y. P x y <=> P y x) /\ (!x y. x < y ==> P x y)
==> (!x y. P x y));
("WLOG_LE",
|- (!m n. P m n <=> P n m) /\ (!m n. m <= n ==> P m n) ==> (!m n. P m n));
("WLOG_LT",
|- (!m. P m m) /\ (!m n. P m n <=> P n m) /\ (!m n. m < n ==> P m n)
==> (!m y. P m y))]
をtheorem-tactic MATCH_MP_TAC に参照させると，変数が交換されただけのsubgoalに対する処理を繰り返さずに済みます．
# prove(
`!x y. &0 < x * y ==> (&0 < x <=> &0 < y)`,
( MATCH_MP_TAC REAL_WLOG_LE ) THEN
( CONJ_TAC ) THEN ( REPEAT GEN_TAC ) THEN
( MP_TAC (SPECL [`--x`; `y:real`] REAL_LE_MUL) ) THEN
( REAL_ARITH_TAC ) );;
val it : thm = |- !x y. &0 < x * y ==> (&0 < x <=> &0 < y)
ここでREAL_WLOG_LEのP x yにマッチしたのは
&0 < x * y ==> (&0 < x <=> &0 < y)
であり
( MATCH_MP_TAC REAL_WLOG_LE ) THEN
( CONJ_TAC ) THEN ( REPEAT GEN_TAC )
までにより，2subgoals
`x <= y ==> &0 < x * y ==> (&0 < x <=> &0 < y)`
`&0 < x * y ==> (&0 < x <=> &0 < y) <=> &0 < y * x ==> (&0 < y <=> &0 < x)`
に展開されて，下側が対称性，上側がx<=yを仮定した場合のものですが，e 関数の中なので続く
( MP_TAC (SPECL [`--x`; `y:real`] REAL_LE_MUL) ) THEN
( REAL_ARITH_TAC )
は双方のsubgoalに施されます．実際には，下側はREAL_ARITHのみで証明できるので，前回と同じREAL_LE_MULが必要なのは上側だけなのですが
# e( MP_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL) );;
val it : goalstack = 1 subgoal (1 total)`(&0 <= x /\ &0 <= --y ==> &0 <= x * --y)
==> x <= y
==> &0 < x * y
==> (&0 < x <=> &0 < y)`# e ( REAL_ARITH_TAC );;
Exception: Failure "linear_ineqs: no contradiction".
# b();;
val it : goalstack = 1 subgoal (1 total)`x <= y ==> &0 < x * y ==> (&0 < x <=> &0 < y)`
# e( MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) );;
val it : goalstack = 1 subgoal (1 total)`(&0 <= --x /\ &0 <= y ==> &0 <= --x * y)
==> x <= y
==> &0 < x * y
==> (&0 < x <=> &0 < y)`# e ( REAL_ARITH_TAC );;
val it : goalstack = No subgoals
となること，つまり
# REAL_ARITH `(x <= y)
==> (&0 < x ==> &0 < y)`;;
val it : thm = |- x <= y ==> &0 < x ==> &0 < y# REAL_ARITH `(&0 <= --x /\ &0 <= y ==> &0 <= --x * y) ==> &0 < x * y
==> (&0 < y ==> &0 < x)`;;
val it : thm =
|- (&0 <= --x /\ &0 <= y ==> &0 <= --x * y)
==> &0 < x * y
==> &0 < y
==> &0 < x
という点を見通した上で，8.1 The goalstack (2)ではなく(3)のSPECLの変数を選らばねばなりません．
WLOG系の例は
http://www.cl.cam.ac.uk/~jrh13/slides/tphols-19aug09/slides.pdf
http://www.cl.cam.ac.uk/~jrh13/slides/tphols-19aug09/tphols.ml
