为什么我不能在Isabelle中明确证明我的案件，但已经给出了证明，但给出了“未能完善任何待解决的目标”错误？

Question

我正在学习具体语义的第5章。

在研究此玩具示例证明时出现了一些错误：

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上，则会收到Isabelle（类型检查器？）验证程序的投诉：

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立即关闭证明。

稍后引用，但我不能使其用于真实证明。

Answer 1

自动生成的证明大纲有时只是错误的。这就是这种情况之一。