Исключение для ACCEPT_TAC после THEN в HOL

Question

Я пытаюсь создать теорему под названием «поглощение» путем объединения тактики, используемой для доказательства цели !(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]);