This directory presents a number of small examples, illustrating various
features of Isabelle/HOL.
- Classical demonstrates the power
of Isabelle's classical reasoner.
- Files mesontest.ML and
mesontest2.ML present an
implementation of the Model Elimination (ME) proof procedure, which is even
more powerful than the classical reasoner but not generic.
- InSort and Qsort are correctness proofs for sorting
- Primrec proves that Ackermann's
function is not primitive recursive.
- Tarski is a proof of Tarski's fixedpoint theorem: the full
version, which states that the fixedpoints of a complete lattice themselves
form a complete lattice. The example demonstrates first-class reasoning about theories.
- NatSum demonstrates the power of permutative rewriting.
Well-known identities about summations are proved using just induction and
- MT is a preliminary version of Jacob Frost's coinduction
example. The full version is on the directory ZF/Coind.
Last modified on $Date$