Get started quick with Isabelle

by Alex Nelson, 15 February 2024

There’s a lot of old and antiquated documentation, tutorials, etc., about Isabelle which is out of date. Here is yet another one, which works for Isabelle2023.

Installation

Installing Isabelle is extraordinarily simple: just download Isabelle, and add it to your path environment variable. Or you could just invoke path/to/Isabelle2023/Isabelle2023 directly to get Isabelle’s jEdit, and path/to/Isabelle2023/bin/isabelle for the tool to create new projects, compile documentation, etc.

Getting Started

Isabelle is a logical framework, which means it implements deductive systems. Unlike, say, Automath, Isabelle uses a fragment of intuitionistic higher-order logic. (This coincides with the spirit of Hilbert’s programme, using an intuitionistic and finitistic metatheory.)

The terminology used in Isabelle is that there is the “metalogic” called “Pure”, and then there is the “object logic” (HOL, FOL, ZF, type theory, etc.) which is implemented in Isabelle. The implementation is called “Isabelle/X” where X = HOL, FOL, ZF, etc.

There are several ways to approach using (or studying) Isabelle:

The most developed object logic with sophisticated tools is Isabelle/HOL. “Morally” HOL = functional programming language + logic. If you thought Haskell was pure, then Isabelle/HOL is the uncut stuff.

If you are a programmer, then you probably want to work with Isabelle/HOL as a programming language. Gerwin Klein and Tobias Nipkow’s Concrete Semantics studies the semantics of a simple imperative programming language using Isabelle/HOL; it’s a great introduction, has a website with useful things like slides from lectures, and is legally and freely available online.

Your first theorem

Getting more to the point, suppose you have ~/src/hack/ be the directory for your exciting new project. You can populate it with all the relevant subdirectories by running:

alex@avocado:~/src/hack/$ ~/src/Isabelle2023/bin/isabelle mkroot -A "Alex Nelson" .

Initializing session "hack" in "/home/alex/src/hack"
  creating "ROOT"
  creating "document/root.tex"

Now use the following command line to build the session:

  isabelle build -D .

alex@avocado:~/src/hack$ ls
document  ROOT

alex@avocado:~/src/hack$ mkdir hack

Now you can open up Isabelle/jEdit by running the command:

alex@avocado:~/src/hack$ ~/src/Isabelle2023/Isabelle2023

Create a new file ~/src/hack/hack/hack.thy which starts a new “theory” file, which is an Isabelle file. Then copy/paste the following into it:

theory hack
  imports Main
begin

end

This is the template for all Isabelle files. The imports tells Isabelle which theories to import — Main refers to the main libraries in Isabelle/HOL.

Now, to double check that everything is working fine, try the following theorem proving concatenating lists is associative:

theorem list_app_assoc: "(xs @ ys) @ zs = xs @ (ys @ zs)"
  apply auto
  done

Just copy/paste this somewhere after begin but before end. If everything works, then you’ll get in the output tab something like:

theorem list_app_assoc: (?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

Again, you’ll probably want to work through the Concrete Semantics book to get up to speed in Isabelle/HOL. There is some loose coding conventions which may be found:

Documenting your code

Documentation is really important, if only to remember what you were in the middle of doing. This can be done writing:

text \<open>
This is an example of some comments I am writing. When I build the
documentation, this will be extracted and pretty-printed in LaTeX.
\<close>

The \<open> and \<close> will be pretty-printed in jEdit as cartouches (the funny angled braces ‹ and ›, respectively).

Depending on what you’re doing, the level of documentation will vary. It has sadly become conventional to have just header documentation for your theory file, when formalizing mathematics or programming with Isabelle/HOL. I don’t know how I feel about this, but my feelings are probably irrelevant anyways.

The entire implementation of Isabelle has a fairly literate documentation assembled from the text blocks of the code implementation.

Example Projects

Consider implementing a proof assistant using Isabelle/HOL.

Consider implementing a different axiomatization of set theory, like Morse-Kelley or helping with the NBG formalization.

Consider formalizing a purely functional programming using Isabelle/HOL, and you could implement an “abstract machine” (virtual machine) for it. Then you could prove properties about its semantics and whatnot.

Examples Implementing new Logics

I’m not going to implement an object logic here, because that could easily take an entire masters or doctoral thesis. But here are a few papers which do exactly that:

Further reading

The documentation is always a good place to turn when you need help, but the proofassistants stackexchange (and the Isabelle zulip chat) are also good.