2

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);
Ionuț G. Stan
  • 176,118
  • 18
  • 189
  • 202
Tuffie
  • 71
  • 2
  • It may be better to tag your questions with "theorem-proving", since the problem is not so much with SML as with logic and the HOL "library". It's a shame that there isn't a "hol" tag (I don't have enough reputation to create one). – tbrk May 07 '18 at 19:44
  • @tbrk I've created the tag. Let me know if you want to add more info to its page and you don't have edit permissions. – Ionuț G. Stan May 08 '18 at 12:40
  • @IonuțG.Stan Great! Thank you. Are you able to please tag the other HOL [question](https://stackoverflow.com/questions/50121473/theorem-proving-from-first-principles-using-sml-with-hol-inference-rules)? (it's an edit of less than 6 characters). – tbrk May 08 '18 at 13:09
  • @tbrk yup, it's been done. – Ionuț G. Stan May 08 '18 at 13:48
  • @IonuțG.Stan Thank you. – tbrk May 08 '18 at 14:00

1 Answers1

1

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]);
tbrk
  • 1,290
  • 1
  • 13
  • 20