Getting started: basic Isabelle/jEdit tricks

11 May 2022

As mentioned last time, proof assistants can be daunting, and it’s not just about how to prove theorems. It’s about being aware of all the bells and whistles provided to help you prove theorems. The first modern proof assistant, Edinburgh LCF, provided nothing but a top-level to the ML programming language, designed specifically to the Meta Language for proving theorems. It was a bare-bones environment, but at least it was Turing complete! Nowadays, things work differently. This post is mainly for beginners, but experienced users might learn something too.

Isabelle/jEdit fundamentals

Nothing says daunting like the Isabelle/jEdit reference manual. Everything you want is there, I suppose. More useful to a beginner is the brief tutorial by Christian Sternagel. Let me summarise his main points even more briefly:

This last point can be puzzling if you watch the progress bar on the right and follow the processing of your theory: how does it reach the bottom when there are red blobs (inducating errors) and purple blobs (indicating a proof still running)? You need to watch out for this sort of thing:

a proof of False?

What’s going on? The first lemma, whoops, is actually false but the supplied proof fails to terminate. Isabelle assumes that the proof will succeed eventually, so it continues on and proves False. This strange phenomenon can only happen in interactive mode: the corresponding batch job will run forever. Unfortunately, a student once submitted work containing this error; it was almost entirely incorrect and he had no idea.

More beginner’s points:

Watch those colours

Some colours will be obvious to you: purple, as above, for a running proof method, and red for syntax errors. Other uses of colour are subtler, but still important. Look carefully at the penultimate line below:

have with hanging variables

The variables m and n are shaded. That’s because they aren’t fixed in the lemma statement (either explicitly by fixes or implicitly by being mentioned). Neither are they declared locally in the have line (using for). So although the little fact has been proved, it just refers to some particular m and n that we know nothing about. It’s good for nothing.

Surely we wanted to prove this fact for all m and n. One way is to make them bound variables. They are rendered in green, while free variables are blue.

fact with bound variables

Another way to make m and n universal is via for. Then they are regarded internally as Skolem variables and rendered in orange:

fact with bound variables

If you find yourself working with two versions of a variable, say a free x and a Skolem x, you are in trouble. This can happen in induction proofs that bring the assumptions of the desired theorem into the induction hypotheses.

One last point about colours. We prefer structured proofs, such as you can see in previous posts. If you use “improper commands” such as apply, they’ll be highlighted in red. There are a couple of instances in the proofs for Wetzel’s problem. It’s basically guilt-tripping.

Deep inspecting of your text

You can inspect variables, constants and other elements by holding down CTRL (CMD for Mac users) and then moving the mouse to hover over them. You’ll be offered popups, such as this:

example of popup

You can hover over any symbol and get a description; you can even hover over symbols in the popups themselves, getting another popup!

Finally, having hovered over a symbol, you can click to be taken to its definition. Here is the definition of the operator dvd:

click to definition

If you hover-click over a theorem name, you get taken to its proof. The text is coloured pink to indicate that it’s frozen: this definition was compiled into the Isabelle/HOL image and therefore cannot be modified.

Sometimes a theory file opens with errors. To jump to them quickly, try these shortcuts:

Sadly, you can’t skip to proof steps that are taking forever. That doesn’t count as an error.

Advanced editing features

You can rename a bound or Skolem variable instantly. Simply select it, then press SHIFT-C-RETURN. All visible occurrences of the variable are selected. Then type the new name.

Check out the Edit menu for tonnes of cool things, e.g.

Finally, try some of jEdit’s general text editing features. Search/replace handles regular expressions, and HyperSearch allows you to search entire files or directories. Abbreviations make it easy to type long, formulaic commands by defining your own brief key sequences.

Have fun! Go slowly at first, watching for everything that’s going on.