在 Isabelle 中证明时跳过子目标

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 移到前面。