isabelle - 如何使用机器学习中的语言环境假设和变量抽象地处理定理和术语？

Question

考虑以下语言环境定义：

locale my_locale =
  fixes a :: nat
  assumes "a > 0"
begin

definition "f n ≡ a + n"
lemma f_pos: "f x > 0"
  sorry

end

在 Isar 中，如果我尝试使用f或 lemma的定义f_pos，则语言环境假设和固定变量对我来说是隐藏的。例如，thm f_def f_pos返回：

f ?n ≡ a + ?n
0 < f ?x

正如预期的那样。

然而，如果我试图在 ML 中推理这些术语，“隐藏的”固定变量就会突然暴露出来。ML {* @{thm f_def} |> prop_of *}，例如，返回：

Const ("==", "nat ⇒ nat ⇒ prop") $
 (Const ("TestSimple.my_locale.f", "nat ⇒ nat ⇒ nat") $
   Free ("a", "nat") $ Var (("n", 0), "nat")) $
 (Const ("Groups.plus_class.plus", "nat ⇒ nat ⇒ nat") $
   Free ("a", "nat") $ Var (("n", 0), "nat"))

其中固定变量a成为函数的参数f。

有没有办法能够在 ML 的语言环境中工作，这样我就不会接触到这样的语言环境变量？

Answer 1

看起来f没有参数的版本a只是命令生成的缩写locale。特别是，打字print_abbrevs显示：

local.f ≡ My_Theory.my_locale.f a

这意味着从用户的角度来看，f似乎没有任何语言环境参数，因为它们隐藏在缩写后面。然而，在幕后，f总是会附加语言环境参数，因此必须对 ML 代码进行编码以显式处理它。