当证明已经完成但给出“无法完善任何待定目标”错误时，为什么我不能在 Isabelle 中明确说明我的情况？

我正在阅读具体语义的第五章。

我在处理这个玩具示例证明时遇到了一些错误：

lemma
  shows "¬ ev (Suc 0)"

我知道这超出了需要（因为by cases）神奇地解​​决了所有问题并给出了完整的证明，但我想明确说明这些情况。

我试过这个：

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof (cases)
  case ev0
    then show ?case by blast
  next
    case evSS
    then show ?case sorry
qed

但如果我把鼠标放在?cases我收到伊莎贝尔（类型检查器？）验证者的投诉：

proof (chain)
picking this:

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  HOL.induct_true

这个错误是什么意思？

为什么我不能用以下方式明确证明case这里的语法？即使这是微不足道的？

问题是，如何立即结案？

如果没有需要证明的情况，您可以立即使用 qed 关闭证明。

稍后会引用，但我无法使其适用于真正的证明。

自动生成的校样大纲有时是错误的。这就是一个这样的案例。

之所以cases在这里解决您的目标是它对案例进行了一些预先简化（如 §6.5.2 中所述）伊莎贝尔/伊萨尔参考手册）。这足以使这两种情况在这里自动消失，因为它们显然是不可能的。因此，你的证明状态没有剩下的证明义务，而 Isar 只允许你用show你还需要证明。这就是您收到错误消息的原因Failed to refine any pending goal：根本就没有悬而未决的目标。

您可以禁用预简化cases使用(no_simp)参数，即

proof (cases (no_simp))

但请注意cases没有定义?case变量，因为它不会改变目标。只需使用?thesis反而。