Hacking on Isabelle/ML

This is less a post than a couple of notes to myself; but perhaps they might also be helpful to others when starting out. I may extend or update it later.


General: along with the official Isabelle Homepage there is isabelle.systems, collecting helpful links to other sites.

Specific to Isabelle/ML:

Basic Isabelle/ML

This is just a collection of helpful functions so I’ll have a place to look them up once I inevitably forget about them again.

How to execute code?

Useful antiquotations:

Printing things

Printing any value that can reasonably be printed:

writeln (@{make_string} ...)

Pretty-printing terms (color-coding of variables depends on context):

Pretty.writeln (Syntax.pretty_term @{context} intr)

What are types?

Types are a simple ADT:

datatype typ =
  Type  of string * typ list |
  TFree of string * sort |
  TVar  of indexname * sort

Additionally, there’s also Term.dummyT (which is really Type ("dummy", [])). This is used to leave the type unspecified. Terms using this type may lead to errors if passed to functions which do not expect them (but usually they are resolved during type inference).

Note that there is no extra builtin function type; a ⇒ b is represented simply as Type ("fun", [a,b]).

What are terms?

Terms are also simply an ADT implementing Isabelle’s take on the lambda calculus:

datatype term =
  Const of string * typ |
  Free of string * typ |
  Var of indexname * typ |
  Bound of int |
  Abs of string * typ * term |
  $ of term * term

Truly a lot of ways to represent a variable!

Note that all names must always be qualified by theory name (antiquatations do this automatically — don’t forget to insert theory names when replacing one with a concrete term!).

What are sorts?

There is one important other detail: sorts. These give an extremely simple meta-logic over types: each sort is just a list of strings, and “subsumes” all lists which contain (at least) the same elements.

There is a “top” sort (the empty list), and apart from that sorts are used to implement things like locales (e.g. in a term a < b, the types of a, b should have a sort that contains "Orderings.org").

Most sorts are just ["HOL.Type"]. There is a \<^sort> antiquotation to write them more easily.

How to find things

To find a specific function (especially if it’s a basic, “obvious” function, like some variation of a map/fold), the best way is often to use ripgrep on Isabelle’s src directory with a likely name/type signature.

The best way to find theories/ML files is likewise with fd.

Use bat (or isabat) to browse these quickly; pass -l sml for files ending in .ML to get correct syntax highlighting.

Basic SML functions may be found in contrib/polyml-x.x/src/basis/*; many additional useful (general) functions are in src/Pure/library.ML.

Interactive exploring of ML files

Isabelle/jedit can provide “jump to definition” and similar features for ML (as it does by default for Isabelle theory files), but only does so for files explicitly loaded by some theory.

So to get these features e.g. in inductive.ML, do this:

ML_file ‹~~/src/HOL/Tools/inductive.ML›

(the double tilde is Isabelle’s home directory, value of $ISABELLE_HOME)

Sometimes this leads to errors (e.g. command defined twice); these are safe to ignore.

Layout of ML files

Most ML files in Pure/HOL define a main signature, and everything contained therein is available qualified with that file’s name, but capitalised; e.g. the result type defined in HOL/Tools/inductive.ML is available as Inductive.result.

Sometimes if an ML file is not part of any theory that is in Main; in that case, import the corresponding theory into your own, and that signature will be available.