| author | paulson |
| Mon, 02 Aug 1999 11:31:04 +0200 | |
| changeset 7146 | 3c664fbb2910 |
| parent 3279 | 815ef5848324 |
| child 11444 | b24017251fc1 |
| permissions | -rw-r--r-- |
| paulson@3123 | 1 |
<!-- $Id$ --> |
| wenzelm@3279 | 2 |
<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY> |
| paulson@3123 | 3 |
|
| paulson@3123 | 4 |
<H2>ex--Miscellaneous Examples</H2> |
| paulson@3123 | 5 |
|
| paulson@3123 | 6 |
<P>This directory presents a number of small examples, illustrating various |
| paulson@3123 | 7 |
features of Isabelle/HOL. |
| paulson@3123 | 8 |
|
| paulson@3123 | 9 |
<UL> |
| paulson@3123 | 10 |
<LI>Files <KBD>cla.ML</KBD> demonstrates the |
| paulson@3123 | 11 |
power of Isabelle's classical reasoner. |
| paulson@3123 | 12 |
|
| paulson@3123 | 13 |
<LI>Files <KBD>meson.ML</KBD> and <KBD>mesontest.ML</KBD> present an |
| paulson@3123 | 14 |
implementation of the Model Elimination (ME) proof procedure, which is even |
| paulson@3123 | 15 |
more powerful than the classical reasoner but not generic. |
| paulson@3123 | 16 |
|
| paulson@3123 | 17 |
<LI><KBD>InSort</KBD> and <KBD>Qsort</KBD> are correctness proofs for sorting |
| paulson@3123 | 18 |
functions. |
| paulson@3123 | 19 |
|
| paulson@3123 | 20 |
<LI><KBD>Primes</KBD> is a theory of the <EM>divides</EM> relation, the |
| paulson@3123 | 21 |
greatest common divisor and Euclid's algorithm. |
| paulson@3123 | 22 |
|
| paulson@7146 | 23 |
<LI><KBD>Fib</KBD> proves some theorems (some rather difficult) about the |
| paulson@7146 | 24 |
Fibonacci function. |
| paulson@7146 | 25 |
|
| paulson@7146 | 26 |
<LI><KBD>Tarski</KBD> is a proof of Tarski's fixedpoint theorem: the full |
| paulson@7146 | 27 |
version, which states that the fixedpoints of a complete lattice themselves |
| paulson@7146 | 28 |
form a complete lattice. The example demonstrates first-class reasoning about theories. |
| paulson@7146 | 29 |
|
| paulson@3123 | 30 |
<LI><KBD>NatSum</KBD> demonstrates the power of permutative rewriting. |
| paulson@3123 | 31 |
Well-known identities about summations are proved using just induction and |
| paulson@3123 | 32 |
rewriting. |
| paulson@3123 | 33 |
|
| paulson@3123 | 34 |
<LI><KBD>MT</KBD> is a preliminary version of Jacob Frost's coinduction |
| paulson@3123 | 35 |
example. The full version is on the directory <KBD>ZF/Coind</KBD>. |
| paulson@3123 | 36 |
</UL> |
| paulson@3123 | 37 |
|
| paulson@3123 | 38 |
<HR> |
| paulson@7146 | 39 |
<P>Last modified on $Date$ |
| paulson@3123 | 40 |
|
| paulson@3123 | 41 |
<ADDRESS> |
| paulson@3123 | 42 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
| paulson@3123 | 43 |
</ADDRESS> |
| paulson@3123 | 44 |
</BODY></HTML> |