HOL中的ACCEPT_TAC异常

Question

我试图通过封装用于证明目标absorptionRule的策略来创建一个名为“!(p:bool) (q:bool). (p==>q) ==> p ==> p /\ q”的定理。但是，我在ACCEPT_TAC上得到了一个例外。当我一个接一个地执行每一种战术时，一切都很好。

val absorptionRule =  
TAC_PROOF(  
([],``!(p:bool) (q:bool).(p ==> q) ==> p ==> p /\ q``),  
REPEAT STRIP_TAC THEN  
ACCEPT_TAC(ASSUME ``p:bool``) THEN  
RES_TAC);  

Answer 1

THEN战术将第二种战术应用于all，即第一种战术(来源)产生的子目标。但是ACCEPT_TAC (ASSUME ``p:bool``)只适用于第一个子目标。当你一个接一个地运用战术时，你不会发现任何问题，因为你从不尝试将ACCEPT_TAC应用于第二个子目标。下面的解决方案使用THENL而不是THEN。

val g1 = (([], ``!(p:bool) (q:bool). (p ==> q) ==> p ==> p /\ q``) : goal);
val absorptionRule =
    TAC_PROOF (g1,
        REPEAT STRIP_TAC
        THENL [ACCEPT_TAC (ASSUME ``p:bool``), RES_TAC]);