This is a set of possible solutions for the online Isabelle/HOL exercises.
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] |
| 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 we do not currently have? Do you think your solution to be 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. Furthermore, this may be your chance to win one of the much coveted Isabelle t-shirts.