This is a collection of exercises for getting acquainted with the proof assistant Isabelle/HOL. The individual exercises come out of an annual Isabelle/HOL lab course taught at the Technische Universität München. The exercises are arranged theme wise, and as far as possible in order of increasing difficulty. They can be used in conjunction with the online Isabelle/HOL course material or the book Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
Each exercise consists of a [pdf] file containing its description, and a [thy] file that can be used to key in your own solutions in an interactive Isabelle session.
Happy proving!
| 1.1 | cons spelt backwards is ... |
[pdf] | [thy] |
| 1.2 | Replace, reverse and delete | [pdf] | [thy] |
| 1.3 | Quantifying lists | [pdf] | [thy] |
| 1.4 | Searching in lists | [pdf] | [thy] |
| 1.5 | Counting occurrences | [pdf] | [thy] |
| 1.6 | Summation, flattening | [pdf] | [thy] |
| 1.7 | Sets as lists | [pdf] | [thy] |
| 1.8 | Sum of list elements, tail-recursively | [pdf] | [thy] |
| 1.9 | Recursive functions and induction: zip |
[pdf] | [thy] |
| 2.1 | Tree traversal | [pdf] | [thy] |
| 2.2 | Folding lists and trees | [pdf] | [thy] |
| 2.3 | Complete binary trees | [pdf] | [thy] |
| 2.4 | Binary decision diagrams | [pdf] | [thy] |
| 2.5 | Representation of propositional formulae by polynomials | [pdf] | [thy] |
| 3.1 | Power, sum | [pdf] | [thy] |
| 3.2 | Magical methods | [pdf] | [thy] |
| 4.1 | Elimination of connectives | [pdf] | [thy] |
| 4.2 | Propositional logic | [pdf] | [thy] |
| 4.3 | Predicate logic | [pdf] | [thy] |
| 4.4 | A riddle: Rich grandfather | [pdf] | [thy] |
| 4.5 | Context-free grammars | [pdf] | [thy] |
| 5.1 | Sorting with lists and trees | [pdf] | [thy] |
| 5.2 | Merge sort | [pdf] | [thy] |
| 5.3 | Tries | [pdf] | [thy] |
| 5.4 | Interval lists | [pdf] | [thy] |
| 6.1 | The towers of Hanoi | [pdf] | [thy] |
| 6.2 | The Euclidean algorithm - inductively | [pdf] | [thy] |
| 6.3 | Compilation with side effects | [pdf] | [thy] |
| 6.4 | BIGNAT - specification and verification | [pdf] | [thy] |
| 6.5 | Optimizing compilation for a register machine | [pdf] | [thy] |
The solutions to these exercises can be found on the solutions page.
In case you have an interesting Isabelle/HOL exercise of your own, please feel free to send it to us to include on this site. Your contribution will be acknowledged. Furthermore, this may be your chance to win one of the much coveted Isabelle t-shirts.