如何在 Isabelle 中使用用 ML 编写的函数？

Question

抱歉，如果这被认为是一个愚蠢的问题，但我怎样才能让 Isabelle 理论识别 ML 代码？例如，假设我有一个 Isabelle 文件，看起来像

ML ‹
type vec = real * real;

fun addvec ((a,b):vec) ((c,d):vec) : vec = (a+b,c+d); 
›

lemma "addvec (1,2) (3,4) = (4,6)"

很遗憾，addvec 在引理中未被识别。如何使功能被识别？我已经阅读了How to get ML values from HOL? 以及 Isabelle Cookbook。前者使用local_setup 使用名为mk_const 的函数将常量分配给Isabelle 常量（据我所知）

fun mk_const c t =
  let 
    val b = Binding.name c 
    val defb = Binding.name (c ^ "_def")
  in (((b, NoSyn), ((defb, []), t)) |> Local_Theory.define) #> snd end

Binding.name 和 Local_Theory.define 函数有什么作用，local_theory 类型是什么？

提前致谢！

Answer 1

我们的想法不是定义一个用 ML 编写的函数，而是在 ML 中定义一个可以在 Isabelle 中使用的函数。

ML ‹
fun mk_const c t =
  let 
    val b = Binding.name c 
    val defb = Binding.name (c ^ "_def")
  in (((b, NoSyn), ((defb, []), t)) |> Local_Theory.define) #> snd end
›


record point =
  coord_x::int

例如，让我们定义一个只调用coord_x的函数：

ML ‹
val f = Abs ("x", @{typ "point"}, Const( \<^const_name>‹coord_x›, @{typ "point"} --> @{typ int}) $ Bound 0)
›

现在我们已经写好了定义，我们可以给它绑定一个名字：

local_setup‹mk_const "c" f›
thm c_def
(*c ≡ coord_x*)

local_setup是改变理论的关键字（所以添加常量，改变上下文等等）。

现在显然您很可能不想要像 coord_x 这样的硬编码常量。

这里有一些一般的cmets：我从来没有用过唱片，我写了很多伊莎贝尔。它们可能很有用（因为它们是可扩展的等等），但它们很奇怪/因为它们是可扩展的/。因此，如果您可以处理数据类型，请这样做。它更好，它是一个合适的类型（所以 locales/instances/... 可以正常工作）。