isabelle - 如何从 HOL 获取 ML 值？

Question

我有一个像这样的嵌入式机器学习代码:

ML ‹
  val boo = true;
  val num = 1234;
  val rea = 3.14;
  val str = "hi";
›

谁能给我一个从 HOL 获取这些值的代码示例吗？

Answer 1

对于所讨论的值的类型，在 SML 类型(术语的子集)和一些规范的 Isabelle/HOL 类型之间建立同构应该不会太困难。在实践中，它们通常采用从 SML 类型的项到 Isabelle/HOL 中某些类型的项的函数形式。 例如，Isabelle/HOL 的标准库已经为您感兴趣的三种类型提供了至少三个这样的函数:

• Quickcheck_Common.reflect_bool : bool -> term 允许将 SML 的 bool 转换为 Isabelle/HOL 的 bool。
• HOLogic.mk_nat : int -> term 允许将 SML 的 int(适当的子集)转换为 Isabelle/HOL 的 nat.
• HOLogic.mk_string : string -> term 允许将 SML 的字符串转换为 Isabelle/HOL 的字符列表。<

将这些值“引入”Isabelle/HOL 可以通过声明和定义新常量来完成。以下示例展示了如何对常量 boo、num 和 str 执行此操作:

ML‹
val boo = true
val num = 1234
val str = "hi"
›

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
›

ML‹
val boo_t = Quickcheck_Common.reflect_bool boo;
val num_t = HOLogic.mk_nat num;
val str_t = HOLogic.mk_string str;
›

local_setup‹mk_const "num" num_t›
local_setup‹mk_const "boo" boo_t›
local_setup‹mk_const "str" str_t›

lemma "num = 1234"
  unfolding num_def by simp

lemma "boo = True"
  unfolding boo_def by simp

lemma "str = ''hi''"
  unfolding str_def by simp

我不知道用于转换 SML 类型 real 的标准函数，但想出一些东西应该不会太困难(我建议你研究一下函数 HOLogic.mk_nat 和 HOLogic.mk_string)。在这种情况下，可能还值得查看有关 Isabelle 代码生成的文档/出版物。