CODEWITHSUNDEEP
smltheorem-provinghol
Tuffie
Tuffie

Reputation: 71

Exception on ACCEPT_TAC after THEN in HOL

I am trying to create a theorem named "absorptionRule" by packaging the tactics that are used to prove the goal !(p:bool) (q:bool). (p==>q) ==> p ==> p /\ q. However, I am getting an exception on ACCEPT_TAC. When I execute each tactic one-by-one, everything works fine.

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);

Upvotes: 2

Views: 77

Answers (1)

tbrk
tbrk

Reputation: 1299

The THEN tactical applies the second tactic to all the subgoals produced by the first tactic (source). But ACCEPT_TAC (ASSUME ``p:bool``) only applies to the first subgoal. You do not see any problem when you apply the tactics one-by-one because you never try to apply the ACCEPT_TAC to the second subgoal. The following solution uses THENL instead of 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]);

Upvotes: 1

Related Questions