Prove a goal with an assumption in HOL

Question

I state the following goal in HOL4:

set_goal([``A:bool``,``B:bool``], ``B:bool``);

resulting in the proof state

val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
    Initial goal:

    B
    ------------------------------------
      0.  B
      1.  A

   : proofs

I tried to find a proper tactic for using the assumptions. I came up with ASM_MESON_TAC:

e (mesonLib.ASM_MESON_TAC [])

and it proved the goal:

OK..
Meson search level: ..
val it =
   Initial goal proved.
    [..] ⊢ B: proof

Is this the standard tactic in such a situation? Or, is there a simpler one?

score 2 · Answer 1 · answered Mar 28 '19 at 15:48

e (FIRST_ASSUM ACCEPT_TAC)

does it.

FIRST_ASSUM applies the argument theorem tactic on assumptions until success.

ACCEPT_TAC simply proves a goal if we supply the same theorem.

ACCEPT_TAC: thm -> tactic
FIRST_ASSUM: (thm -> tactic) -> tactic

(thanks to somebody on #hol)

Prove a goal with an assumption in HOL

1 Answers1