伊莎贝尔未能完成证明，即使这与目标相同

Question

我的代码如下。我希望它能完美地工作，并且确实在最后的 "hence" 行（由 Sledgehammer 发现）的末尾，Isabelle 声称 this 是 ∀y. ∃x. P x y，并且它的目标有一个只有 ∀y. ∃x. P x y 的子目标。这两个表达式是相同的，所以我本以为伊莎贝尔会接受完成的证明。

lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof -
 fix y
 assume "EX x. ALL f. P x f"
 then obtain x where "ALL f. P x f" by blast
 hence "P x y" by blast
 hence "ALL y. EX x. P x y" using `∀f. P x f` by blast
qed

我错过了什么？我是 Isabelle 的初学者，这可能很明显。

Answer 1

命令have和hence只陈述你想证明的中间事实。你必须明确地说，一个陈述应该实现一个目标。为此，您必须使用 show 或 thus 而不是 have 或 hence。因此，如果您将最后一个 hence 替换为 thus，则证明应该成功（模以下的注释）。您还可以在 Output 缓冲区中看到（或者通过将鼠标悬停在 thus 上，您会收到一条消息说 Successful attempt to solve goal by exported rule ...。这表明目标真的被释放了。

顺便说一句，证明不会按预期工作。首先，在你写 proof - 的初始步骤中，你实际上想为全称量词做介绍（因为你在下一步中修复了 y。因此，- 应该是替换为适当的规则应用程序，即 (rule allI)。因此，您的显示语句应该是 EX x. P x y 而不是 ALL y. EX x. P x y。

其次，引理语句中的 assumes 已经将假设添加到上下文中。因此，无需在证明中再次假设。事实上，伊莎贝尔会在show或thus处抱怨无法解决目标。因此，您应该删除 assume ... 部分并将其替换为对假设的引用，例如，使用预定义名称 assms.

伊莎贝尔未能完成证明，即使这与目标相同

Isabelle failed to finish proof even though this is same as goal

isabelle