我试图证明一个定理，但卡在一个子目标上（我更喜欢跳过并稍后证明）。我怎样才能跳过这个并证明其他人？
首先，我尝试了oops和sorry但它们都中止了整个证明（而不是唯一的子目标）。我还尝试将子目标放入虚拟引理（假设用sorry证明）然后使用它（apply (rule [my dummy lemma])），但它将虚拟引理应用于所有其他子目标（不仅是第一个）。
这主要取决于您使用的是古老的（对不起;)）应用样式还是适当结构化的 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移动到前面。