如何从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的bool.
• HOLogic.mk_nat : int -> term转换为Isabelle/HOL的nat.
• HOLogic.mk_string : string -> term允许将SML的int转换为Isabelle/HOL的char list.

允许将SML的bool转换为Isabelle/HOL的int

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