Isabelle/HOL:在另一个区域设置中访问口译

Question

有一个Isabelle/HOL库，我想用新的定义和证明来构建它。 该库定义了 locale2，我想在此基础上进行构建。 在区域设置 2 中，有对区域设置 1 的解释。

为了在单独的理论中扩展locale2，我定义了locale3 = locale2。 但是，在 locale3 中，我不知道如何访问 locale2 对 locale1 的解释。 我该怎么做？ (我甚至以正确的方式做这件事吗？

下面是一个MWE。 这是库理论，我想要扩展的语言环境：

theory ExistingLibrary
imports Main
begin
(* this is the locale with the function I want *)
locale locale1 = assumes True
begin
fun inc :: "nat ⇒ nat"
where "inc n = n + 1"
end
(* this is the locale that interprets the locale I want *)
locale locale2 = assumes True
begin
interpretation I: locale1
by unfold_locales auto
end
end

这是我的扩展理论。 我的尝试在底部，导致错误：

theory MyExtension
imports ExistingLibrary
begin
locale locale3 = locale2
begin
definition x :: nat
where "x = I.inc 7" (* Undefined constant: "I.inc" *)
end
end

Answer 1

上下文中的解释仅持续到上下文结束。再次输入上下文时，您必须重复解释以使定义和定理可用：

locale 3 = locale2 begin
interpretation I: locale1 <proof>

出于这个原因，我建议将第一个解释步骤分为两个：

1. 具有证明解释步骤目标的名称的引理。
2. interpretation命令本身可以证明by(rule引理)

如果您希望在打开区域设置和解释区域设置时进行解释，则sublocale而不是interpretation可能会更好。