How to get ML values from HOL?

Question

I have an embedded ML code like this:

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

Can anyone give me an example of code that gets those values from HOL?

Answer 1

For the types of the values in question, it should not be too difficult to establish isomorphisms between (the subsets of the terms of) the SML types and some canonical Isabelle/HOL types. In practice, they would normally take the form of a function from the terms of an SML type to the terms of some type in Isabelle/HOL. For example, the standard library of Isabelle/HOL already provides at least three such functions for three of the types that you are interested in:

• Quickcheck_Common.reflect_bool : bool -> term allows for the conversion of the SML's bool to the Isabelle/HOL's bool.
• HOLogic.mk_nat : int -> term allows for the conversion of the (appropriate subset of the) SML's int to the Isabelle/HOL's nat.
• HOLogic.mk_string : string -> term allows for the conversion of the SML's string to the Isabelle/HOL's char list.

Bringing such values 'into' Isabelle/HOL can be done by declaring and defining new constants. The following example shows how this can be done for the constants boo, num and 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

I am not aware of a standard function for the conversion of the SML's type real, but it should not be too difficult to come up with something (I suggest for you to study the implementation of the functions HOLogic.mk_nat and HOLogic.mk_string). In this context, it may also be worth looking at the documentation/publications about the code generation for Isabelle.