1

如果我将括号中的步骤THENL按顺序输入到 HOL 解释器中，则括号中的步骤可以正常工作。但是当我将它们与TAC_PROOFusing结合使用时THENL，出现错误。

THEN我想我理解和THENL （所有子目标与单个子目标）之间的区别。但我找不到区分这两个初始子目标的语法。DISJ1_TAC并且RES_TAC应该只适用于 subgoal1。虽然DISJ2_TAC并且RES_TAC应该只适用于 subgoal2。

我怎样才能解决这个问题？

val constructiveDilemmaRule =
TAC_PROOF (([],``! p q r s .(p==>q) /\ (r==>s) ==> p \/ r ==>q \/s``),
REPEAT STRIP_TAC
THENL [DISJ1_TAC THEN RES_TAC]
THENL [DISJ2_TAC, RES_TAC]);
4

1 回答 1

0

你几乎明白了。ApplyingREPEAT STRIP_TAC给出了两个子目标，因此 list 参数THENL应该包含两种策略：

val g = (([], ``! p q r s .(p ==> q) /\ (r ==> s) ==> p \/ r ==> q \/ s``) : goal);
val tac = (REPEAT STRIP_TAC)
          THENL [DISJ1_TAC THEN RES_TAC,
                 DISJ2_TAC THEN RES_TAC];
val constructiveDilemmaRule = TAC_PROOF (g, tac);

参数列表 ( DISJ1_TAC...) 的第一个元素应用于第一个子目标。参数列表 ( DISJ2_TAC) 的第二个元素应用于第二个子目标。

于 2018-05-10T19:54:50.773 回答