How can I use functions written in ML inside Isabelle?

Question

Apologies if this is considered a dumb question, but how can I make an Isabelle theory recognise ML code? For example, let's say I have an Isabelle file that looks like

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)"

Unfortunately addvec isn't recognised in the lemma. How can I make the function recognised? I've read through How to get ML values from HOL? as well as the Isabelle Cookbook. The former uses a local_setup to assign the constants to Isabelle constants (as far as I can see) using a function called mk_const

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

What do the functions Binding.name and Local_Theory.define do, and what is the local_theory type?

Thanks in advance!

Answer 1

The idea is not to define a function written in ML, it is to define in ML a function that you can use in 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

For example, let us define a function that just calls coord_x:

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

Now we have written the definition, we can bind it a name:

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

local_setup is a keyword to change the theory (so add constants, change the context and so on).

Now obviously you most likely do not want hard coded constants like coord_x.

Some general comments here: I have never used records and I have written a lot of Isabelle. They can be useful (because they are extensible and so on), but they are weird /because they are extensible/. So if you can work on a datatype, do so. It is nicer, it is a proper type (so locales/instances/... just work).