sml - 在 HOL 中 THEN 之后的 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战术应用于第一种战术产生的所有子目标（来源）。但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]);