我正在阅读具体语义的第五章。
我在处理这个玩具示例证明时遇到了一些错误：
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反而。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
