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