我正在学习具体语义的第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上，我会收到伊莎贝尔(类型检查器？(验证器的投诉：
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在这里解决您的目标的原因是它对案例进行了一些预先简化(如 Isabelle/Isar 参考手册的 §6.5.2 中所述(。这足以使这两种情况在这里自动消失，因为它们显然是不可能的。因此，您的证明状态没有证明义务，Isar 只允许您用您仍然需要证明的show来证明事物。这就是为什么您收到错误消息Failed to refine any pending goal：根本没有待定目标。
您可以使用(no_simp)参数禁用cases的预简化，即
proof (cases (no_simp))
但请注意，cases没有定义?case变量，因为它不会更改目标。只需改用?thesis即可。