1

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!

Kookie
  • 328
  • 4
  • 14
  • Short version: you cannot easily. If only because you are allowed to write non-terminating functions in ML and not in Isabelle. What are trying to achieve? – Mathias Fleury Jan 25 '22 at 08:14
  • I even believe that it is impossible in general for functions. You would need reflection in SML to be able to study the structure of the function. – Mathias Fleury Jan 25 '22 at 08:18
  • @MathiasFleury I'm trying to eventually write a function in ML that grabs the field names of a record in Isabelle, then use this function in Isabelle. It's pretty loaded and I'm a complete beginner at ML. – Kookie Jan 25 '22 at 08:21
  • Are you trying to write a function in SML with SML types or are you trying to write a function in SML with Isabelle (aka a "term")? The linked question asks about the former (I don't believe it is possible to translate records from Isabelle to SML). But the latter makes a lot of sense too. – Mathias Fleury Jan 25 '22 at 08:26
  • @MathiasFleury Originally I wanted to write a function in SML with SML types which I can use in Isabelle since record fields are implemented in SML. – Kookie Jan 25 '22 at 08:32
  • What are you trying to achieve? Why are you structure in SML instead of Isabelle? As a side note, without restriction, you can even introduce an inconsistency (use a ref and increment it each time you call the function: `f () = f ()` would be /false/). – Mathias Fleury Jan 25 '22 at 10:08
  • @MathiasFleury I'm trying to eventually write a function in ML that grabs the field names of a record in Isabelle, then use this function in Isabelle. I only asked this question to see if my simple example as described in the question description would act as a proof of concept that my approach will help me get there. I'm using ML because I have been told there is no nicer way of achieving this. Is there something that isn't clear about my goal? – Kookie Jan 25 '22 at 10:23
  • Ah that is very different from what I understood. You want to define the function *with* ML, but not *in ML*. So you can construct the Isabelle version directly -- i.e., get the result of `HOLogic.mk_string` directly instead of writing an ML version. – Mathias Fleury Jan 25 '22 at 10:30
  • @MathiasFleury I believe that sounds like what I'm looking for in technical terms (I'm not very familiar with ML). – Kookie Jan 25 '22 at 10:32

1 Answers1

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

Mathias Fleury
  • 2,221
  • 5
  • 12
  • Yeah, nearly there. I should have specified this earlier, but I also would like `c` to be monomorphic (it's currently `point => int` in Isabelle) so that I can have it in the same set as other fields if they had a different type. eg: if there was a field called `name :: string` in there, then I can get `name` and `c` in the same set. Sorry for the extra holdup. – Kookie Jan 25 '22 at 12:13
  • Specify types more precisely: replace `point` by the type you want, like `string point_scheme`. – Mathias Fleury Jan 25 '22 at 12:19
  • Sorry I don't completely understand. I tried changing the type here `val f = Abs ("x", @{typ "string point_scheme"}, Const( \<^const_name>‹coord_x›, @{typ "string point_scheme"} --> @{typ int}) $ Bound 0)` but `c` is still of type `char list point_scheme => int` which is a problem because that `int` type is attached to it. That means if I have the field `name::string` inside the `point` record, then I can't have both names in the same set if I use the same approach. – Kookie Jan 25 '22 at 12:40
  • Wait, this has nothing to do with monomorphism. Do you want overloading of c such that it works on multiple records? Or just change the type int to string if this is what you want. I need an MWE of what you want, I am confused. – Mathias Fleury Jan 25 '22 at 13:57
  • Going back to your first comment: you want to write a set of elements of different types? this does not work. If you have a finite number of possible types, you can use a datatype, but this is not going work directly. Isabelle is a typed language! I guess we are back to: what do you want to do with that set? – Mathias Fleury Jan 25 '22 at 14:01
  • I've started a chat at https://chat.stackoverflow.com/rooms/241397/room-for-kookie-and-mathias-fleury so this comment section doesn't become too cluttered – Kookie Jan 25 '22 at 17:24