Isabelle/HOL is an interative theorem prover. To be extremely precise Isabelle is a distribution of a the theorem prover and HOL is an object logic embedded in the ambient logic. If this is confusing don’t sweat about it, it’s only to make the next distinction a little clearer.

I have recently started a project using Isabelle/ML, the part of the Isabelle distribution where you write Standard ML code to extend what Isabelle can do on the logic side. These are small tips that made me more productive because the experience of using Isabelle/ML is really subpar to using Isabelle and Isabelle/HOL.

Can’t click X

Isabelle has a neat feature where you can Ctrl-Click anything and it will bring you to where it is defined. This does not work as well in Isabelle/ML, especially with the output buffer. This breaks the flows a lot because I cannot find my way to a type or a module fast.

Let’s see an example where we want to see the type of Object_Logic.atomize. In my theory file I write the following.

ML_val <
  Object_Logic.atomize
>

In the output buffer I can then read the following but I cannot click anything. I can copy this signature to the previous block and click it though.

val it = fn : Proof.context -> conv

In general though if you know where you want to go there are two ways to get there fast. For types it is easy to define a newtype and the right-hand-side will be clickable, for modules it is always possible to open them.

ML_val <
  type A = Proof.context;
  open Proof;
>

Syntax and type errors

Everybody starts with the /embedded ML/ because it is easy. The errors though could be better. The syntax and type errors may mix though making it hard to understand what is the problem and how do you fix it.

As always the way out is kind of boring and obvious when you think about it.

Always start with a complete ML expression which produces no syntax error and then start adding stuff.

The following snippet is an example of many things that could go wrong. Are getting an error because there is a type mismatch or because the term is not parsable? I cannot tell.

ML_val <
let
  val an_id : a_type_signature = an_expression
>

Small incremental steps instead bring you there. First a parsable term

ML_ <
let
in
  ()
end
>

Then a name and type for your binding.

ML_ <
let
  val a_name : a_type = error "TODO"
in
  ()
end
>

Then a body for your binding.

ML_ <
let
  val a_name : a_type = error "TODO"
in
  body
end
>

Then a value

ML_ <
let
  val a_name : a_type = a_value
in
  body
end
>

Each small step is either a syntax error or a type error and you can always tell.

Error is surprisingly useful

Just like you would use undefined in your inner syntax to have a hole you can fill in later I think error is a fantastic hole for your ML sources.

Finding other stuff

We do not have access to find_theorems and find_consts so the way forward is textual seach. Lucky us that this is already available.

Where to find stuff

We have stuff already

The Isabelle distribution comes with a bunch of stuff already. You most likely know that Isabelle/HOL is defined in the HOL directory of the Isabelle distribution. There are other developments there such as FOL, LCF, Pure, ZF.

I like to interactively explore this root directory using the builtin search.

I always start with filtering out the ML files because I am looking for examples of how to use the outer syntax. If I am looking for examples of Isabelle/ML I also start with the theory files because it’s likely that I am reinventing the wheel.

Then when I’m done with theory files I start searching through the ML sources.

The Archive of Formal Proofs

The AFP is another good source of examples you should comb. Instead of looking at the web frontend you should download it and use the builtin search as described before.