proof - 在伊莎贝尔证明时跳过一个子目标

Question

我试图证明一个定理，但陷入了一个子目标（我更愿意跳过并稍后证明）。我怎样才能跳过这个并证明其他人？

首先，我尝试过oops，sorry但他们都中止了整个证明（而不是唯一的子目标）。我还尝试将子目标放入虚拟引理（假设用 证明sorry）然后使用它（apply (rule [my dummy lemma])），但它将虚拟引理应用于所有其他子目标（不仅是第一个子目标）。

Answer 1

这主要取决于您是使用古老的（对不起；））应用风格还是适当结构化的 Isar 来证明。我将举一个小例子来涵盖这两种风格。假设你想证明

lemma "A & B"

在哪里A，B只是作为潜在巨大公式的占位符。

作为结构化证明，您可以执行以下操作：

proof
  show "A" sorry
next
  show "B" sorry
qed

即，在这种风格中，您可以使用sorry省略子目标的证明。

在应用风格中你可以做

apply (rule conjI)
defer -- "moves the first subgoal to the last position"
apply (*proof for subgoal "B"*)
apply (*proof for subgoal "A"*)

还有将子目标移到前面的应用样式prefer n命令n。