isabelle - 以应用风格在目标中放下前提

Question

假设我要显示以下引理

lemma "⟦ A; B; C ⟧ ⟹ D"

我有目标

1. A ⟹ B ⟹ C ⟹ D

但是，我不需要 B。我如何将目标转移到类似

1. A ⟹ C ⟹ D

我不想更改原始的 lemma语句，而只是更改应用样式中的当前目标。

Answer 1

您想要的是apply (thin_tac B)。但是，上一次我这样做时，彼得·拉米奇大喊:“天哪，你为什么要这样做!”厌恶并重写了我的证明，以摆脱Thin_TAC。因此，似乎不再鼓励使用这种策略。