【发布时间】：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)
不幸的是，这只是把罐子踢到了路上。我需要一种方法来使用存在引理将最终的内部引理提取到外部语言环境中。如果我试图解释内部语言环境，我将再次遇到提供证人的问题。我无法解释引理中的语言环境（除非我误解了我得到的错误），而且我不能在引理之外使用获取，所以我被卡住了。
所以看起来我需要弄清楚
- 如何在引理之外指定见证实例或
- 如何通过证明语言环境的假设从语言环境中提取引理
或者有没有更好的方法来做我想做的事情？谢谢！
【问题讨论】：
标签： isabelle