src/HOL/ex/README.html
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 15582 7219facb3fd0
permissions -rw-r--r--
added lemmas
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
paulson@3123
     3
<!-- $Id$ -->
webertj@15582
     4
webertj@15582
     5
<HTML>
webertj@15582
     6
webertj@15582
     7
<HEAD>
webertj@15582
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     9
  <TITLE>HOL/ex/README</TITLE>
webertj@15582
    10
</HEAD>
webertj@15582
    11
webertj@15582
    12
<BODY>
paulson@3123
    13
paulson@3123
    14
<H2>ex--Miscellaneous Examples</H2>
paulson@3123
    15
paulson@3123
    16
<P>This directory presents a number of small examples, illustrating various
paulson@3123
    17
features of Isabelle/HOL.
paulson@3123
    18
paulson@3123
    19
<UL> 
webertj@15167
    20
<LI><A HREF="Classical.thy"><KBD>Classical</KBD></A> demonstrates the power 
webertj@15167
    21
of Isabelle's classical reasoner.
paulson@3123
    22
paulson@11444
    23
<LI>Files <A HREF="mesontest.ML"><KBD>mesontest.ML</KBD></A> and
paulson@11444
    24
<A HREF="mesontest2.ML"><KBD>mesontest2.ML</KBD></A> present an
paulson@3123
    25
implementation of the Model Elimination (ME) proof procedure, which is even
paulson@3123
    26
more powerful than the classical reasoner but not generic.
paulson@3123
    27
paulson@11444
    28
<LI><A HREF="InSort.thy"><KBD>InSort</KBD></A> and <A HREF="Qsort.thy"><KBD>Qsort</KBD></A> are correctness proofs for sorting
paulson@3123
    29
functions.
paulson@3123
    30
paulson@11444
    31
<LI><A HREF="Primrec.thy"><KBD>Primrec</KBD></A> proves that Ackermann's
paulson@11444
    32
function is not primitive recursive.
paulson@3123
    33
paulson@11444
    34
<LI><A HREF="Tarski.thy"><KBD>Tarski</KBD></A> is a proof of Tarski's fixedpoint theorem: the full
paulson@7146
    35
version, which states that the fixedpoints of a complete lattice themselves
paulson@7146
    36
form a complete lattice.  The example demonstrates first-class reasoning about theories.
paulson@7146
    37
paulson@11444
    38
<LI><A HREF="NatSum.thy"><KBD>NatSum</KBD></A> demonstrates the power of permutative rewriting.
paulson@3123
    39
Well-known identities about summations are proved using just induction and
paulson@3123
    40
rewriting.
paulson@3123
    41
paulson@11444
    42
<LI><A HREF="MT.thy"><KBD>MT</KBD></A> is a preliminary version of Jacob Frost's coinduction
paulson@3123
    43
example.  The full version is on the directory <KBD>ZF/Coind</KBD>.
paulson@3123
    44
</UL>
paulson@3123
    45
paulson@3123
    46
<HR>
paulson@7146
    47
<P>Last modified on $Date$
paulson@3123
    48
paulson@3123
    49
<ADDRESS>
paulson@3123
    50
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
paulson@3123
    51
</ADDRESS>
webertj@15582
    52
</BODY>
webertj@15582
    53
</HTML>