This is a set of possible solutions for the online Isabelle/HOL exercises. All theory files were written for Isabelle2012.
Contributing your own solutions is encouraged.
| 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] |
| 5.5 | Register Machine from Hell | (The solution is currently not disclosed.) | |
| 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] |
Have you worked out a solution that is better or more elegant than the one currently posted? Then send it to us for our opinion. If we agree we will post it online. Your contribution will be acknowledged.