如何在 Isabelle/HOL 的引理之外获取见证实例

Posted 2023-03-28

【中文标题】如何在 Isabelle/HOL 的引理之外获取见证实例

【英文标题】：How to obtain witness instances outside a lemma in Isabelle/HOL

【发布时间】：2020-05-13 21:55:52

【问题描述】：

我正在使用 Isabelle/HOL，试图证明声明 Q。在证明Q 的路上，我已经证明了满足P::"nat=>bool" 的自然数的存在。如何创建满足P 的实例x::nat，以便在后续引理中引用它？

在任何给定的引理中，我都可以使用获取命令来完成。但是，我想在许多不同的引理中引用相同的见证实例，因此我需要一种方法来在任何引理之外执行此操作。我尝试在新的语言环境中使用 fix/assume，如下所示：

locale outerlocale
  fixes a b c ...
begin

definition Q::bool where ...

lemma existence: "EX x. P x"
proof -
  ...
qed

locale innerlocale = outerlocale +
  fixes x::nat
  assumes "P x"
begin


(*lots of lemmas that reference x*)
lemma innerlemma0
  ...
lemma innerlemma7
proof -
  ...
qed

lemma finalinnerlemma: "Q"
proof -
  ...
  ...
qed


end (*innerlocale*)

lemma outerlemma: "Q"
proof -
  (*I don't know what goes here*)
qed

end (*outerlocale)

不幸的是，这只是把罐子踢到了路上。我需要一种方法来使用存在引理将最终的内部引理提取到外部语言环境中。如果我试图解释内部语言环境，我将再次遇到提供证人的问题。我无法解释引理中的语言环境（除非我误解了我得到的错误），而且我不能在引理之外使用获取，所以我被卡住了。

所以看起来我需要弄清楚

如何在引理之外指定见证实例或 如何通过证明语言环境的假设从语言环境中提取引理

或者有没有更好的方法来做我想做的事情？谢谢！

【参考方案1】：

您可以只使用SOME x. P x，例如，在定义中：

definition my_witness :: nat where
   "my_witness = (SOME x. P x)"

然后使用thm someI_ex 显示P my_witness。