Screenshots of an example proof

Here, we show one method of proving a simple theorem:

This theorem is used as an one of the examples of Isabelle/Isar.

Note: Isabelle is smart enough that it is able to solve this in fewer steps than shown below. We choose this slightly longer solution to give the reader a basic idea of what is going on.

This is the proof window, where theorems in a particular theory are to be proven.

Select "New Theorem" from the Theory menu to begin a proof.

Give the new theorem a name.

Define the theorem. Currently the user is required to understand Isabelle's theorem syntax. This could be extended: a nice solution might make use of a MathML equation editor. The equation editor Jex (used in OpenOffice) appears to be a good candidate, although it is written in Java.

This is the initial proof state, labelled "Step 0".

The only goal in the initial proof state is the theorem itself.

Here, we apply Isabelle's induction tactic.

The result of the induction step: a new proof state.

Now we have two goals: a base case and an inductive case.

Here we ask Isabelle to simplify the base case.

The result is another proof state, without the base case which has been proven.

Now we ask Isabelle to simplify the induction step.

The last subgoal has been proven, and the proof is complete.