1
2\chapter{More Examples}
3\label{chap:more-examples}
4
5In addition to the examples already covered in this text, the \holn{}
6distribution comes with a variety of instructive examples in the
7\verb|examples| directory.  There the following examples (among
8others) are to be found:
9
10\begin{description}
11
12\item [\tt autopilot.sml]
13
14  This example is a \holn{} rendition (by Mark Staples) of a PVS
15  example due to Ricky Butler of NASA. The example shows the use of
16  the record-definition package, as well as illustrating some aspects
17  of the automation available in \holn{}.
18
19\item [\tt bmark]
20
21  In this directory, there is a standard HOL benchmark: the proof of
22  correctness of a multiplier circuit, due to Mike Gordon.
23
24\item [\tt euclid.sml]
25
26  This example is the same as that covered in
27  Chapter~\ref{chap:euclid}: a proof of Euclid's theorem on the
28  infinitude of the prime numbers, extracted and modified from a much
29  larger development due to John Harrison. It illustrates the
30  automation of \HOL{} on a classic proof.
31
32\item[\tt ind\_def]
33
34This directory contains some examples of an inductive definition package
35in action. Featured are an operational semantics for a small imperative
36programming language, a small process algebra, and combinatory logic
37with its type system. The files were originally developed by Tom Melham
38and Juanito Camilleri and are extensively commented.  The last is the
39basis for Chapter~\ref{chap:combin}.
40
41Most of the proofs in these theories can now be done much more easily by
42using some of the recently developed proof tools, namely the simplifier
43and the first order prover.
44
45\item [\tt fol.sml]
46
47  This file illustrates John Harrison's implementation of a
48  model-elimination style first order prover.
49
50\item[\tt lambda]
51
52This directory develops theories of a ``de Bruijn'' style lambda calculus,
53and also a name-carrying version. (Both are untyped.) The development
54is a revision of the proofs underlying the paper
55{\it ``5 Axioms of Alpha Conversion'',
56            Andy Gordon and Tom Melham,
57            Proceedings of TPHOLs'96, Springer LNCS 1125}.
58
59\item[\tt parity]
60
61  This sub-directory contains the files used in the parity example of
62  Chapter~\ref{parity}.
63
64\item [\tt MLsyntax]
65
66  This sub-directory contains an extended example of a facility for
67  defining mutually recursive types, due to Elsa Gunter of Bell Labs.
68  In the example, the type of abstract syntax for a small but not
69  totally unrealistic subset of ML is defined, along with a simple
70  mutually recursive function over the syntax.
71
72\item[\tt Thery.sml]
73
74  A very short example due to Laurent Th\'ery, demonstrating a cute
75  inductive proof.
76
77\item[\tt RSA]
78
79       This directory develops some of the mathematics underlying
80       the RSA cryptography scheme. The theories have been
81       produced by Laurent Th\'ery of INRIA Sophia-Antipolis.
82
83\end{description}
84
85
86%%% Local Variables:
87%%% mode: latex
88%%% TeX-master: "tutorial"
89%%% End:
90