在HOL中假设一个目标

Question

我在HOL4中声明了以下目标：

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

导致证明状态

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

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

   : proofs

我试图找到一个适当的策略来使用这些假设。我想出了ASM_MESON_TAC：

e (mesonLib.ASM_MESON_TAC [])

它证明了目标：

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

这是这种情况下的标准策略吗？或者，是否有一个更简单的？

Answer 1

e (FIRST_ASSUM ACCEPT_TAC)

可以。

FIRST_ASSUM将参数定理策略应用于假设直到成功。

如果我们提供相同的定理，ACCEPT_TAC只是证明了一个目标。

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

（感谢#hol上的某个人）