2

我正在阅读具体语义的第 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 关闭证明。

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

4

1 回答 1

1

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

在这里解决您的目标的原因cases是它对案例进行了一些预先简化（如Isabelle/Isar 参考手册的 §6.5.2 中所述）。这足以让这两种情况在这里自动消失，因为它们显然是不可能的。因此，您的证明状态没有剩余的证明义务，并且 Isar 只允许您证明show您仍然需要证明的事物。这就是您收到错误消息的原因Failed to refine any pending goal：根本没有待定目标。

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

proof (cases (no_simp))

但是请注意，cases它没有定义?case变量，因为它不会改变目标。改用就好?thesis了。

于 2020-05-21T08:00:58.317 回答