isabelle - 如何从 HOL 获取 ML 值？

Question

我有一个这样的嵌入式 ML 代码：

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 转换为boolIsabelle/HOL 的bool.
• HOLogic.mk_nat : int -> term允许将（适当的）SML'sint转换为 Isabelle/HOL's nat。
• HOLogic.mk_string : string -> term 允许将 SML 转换为stringIsabelle/HOL 的char list.

可以通过声明和定义新常量来将这些值“带入”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 代码生成的文档/出版物。