时间戳

首页 > 解决方案 > 如何在 Isabelle/HOL 的引理之外获取见证实例

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

问题描述

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

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

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)

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

所以看起来我需要弄清楚

还是有更好的方法来做我想做的事情？谢谢！

标签： isabelle

解决方案

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

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

然后用于thm someI_ex显示P my_witness.

推荐阅读