问题描述
在将 Isabelle 2020 的 PDF 教程中的以下证明复制到 IDE 中时（关于康托定理，即从集合到其幂集的函数不能是满射的），我在“从 1 有 2”行上打错了字。
lemma "¬ surj (f :: 'a ⇒ 'a set)"
proof
assume 0: "surj f"
from 0 have 1: "∀ A. ∃ a. A = f a" by(simp add: surj_def )
from 1 have 2: "∃ a. {x. x ∉ f x} = f a" by blast
from 2 show "False" by blast
qed
，以便该行现在读取（使用错误的 forall 量词）
from 1 have 2: "∀ a. {x. x ∉ f x} = f a" by blast
奇怪的是，示例中的原始证明和更改后的版本都有效。 但是更改的版本不正确，不是吗？
我是否遗漏了什么，或者有人可以解释更改后的版本（如下）是如何正确的？
lemma "¬ surj (f :: 'a ⇒ 'a set)"
proof
assume 0: "surj f"
from 0 have 1: "∀ A. ∃ a. A = f a" by(simp add: surj_def )
from 1 have 2: "∀ a. {x. x ∉ f x} = f a" by blast
from 2 show "False" by blast
qed
--- 更新---
为了帮助诊断问题，以下是我将鼠标放在“from 2 show ...”行上时的输出。它提到了一个导出规则，这似乎是要证明的定理。 （我不记得自己导出规则，除了可能在几次试验中不小心把量词弄对了。）
show False
Successful attempt to solve goal by exported rule:
(surj f) ⟹ False
proof (state)
this:
False
goal:
No subgoals!
我只是尝试关闭 Isabelle 并重新打开同一个 .thy 文件，得到了相同的结果。 （如您所见，我是 Isabelle 环境的新手）。当我输入正确的文本时，我是否只是将定理保存在某处？
解决方法
您使用的是哪个 Isabelle 版本？如背景所示，我的爆炸呼叫不会终止（在几秒钟内）：
然而，Isabelle 很乐观：它假设blast 最终会终止（它不会）。因此检查下一步（因为类型不为空，所以这个步骤成立：“∀ a.P a”，然后是“∃ a.P a”）。这可能会给你一种证明正在通过的印象，但事实并非如此。