2 \markboth{Preface}{Preface}
4 This volume is a self-contained introduction to interactive proof
5 in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@.
6 Compared with existing Isabelle documentation,
7 it provides a direct route into higher-order logic, which most people
8 prefer these days. It bypasses first-order logic and minimizes
9 discussion of meta-theory. It is written for potential users rather
10 than for our colleagues in the research world.
12 \index{Wenzel, Markus}%
13 Another departure from previous documentation is that we describe Markus
14 Wenzel's proof script notation instead of ML tactic scripts. The latter
15 make it easier to introduce new tactics on the fly, but hardly anybody
16 does that. Wenzel's dedicated syntax is elegant, replacing for example
17 eight simplification tactics with a single method, namely \isa{simp},
18 with associated options.
20 The book has three parts.
23 The first part, \textbf{Basic Techniques},
24 shows how to model functional programs in higher-order logic. Early
25 examples involve lists and the natural numbers. Most proofs
26 are two steps long, consisting of induction on a chosen variable
27 followed by the \isa{auto} tactic. But even this elementary part
28 covers such advanced topics as nested and mutual recursion.
30 The second part, \textbf{Logic and Sets}, presents a collection of
31 lower-level tactics that you can use to apply rules selectively. It
32 also describes Isabelle/HOL's treatment of sets, functions and
33 relations and explains how to define sets inductively. One of the
34 examples concerns the theory of model checking, and another is drawn
35 from a classic textbook on formal languages.
37 The third part, \textbf{Advanced Material}, describes a variety of
38 other topics. Among these are the real numbers, records and
39 overloading. Esoteric techniques are described involving induction and
40 recursion. A whole chapter is devoted to an extended example: the
41 verification of a security protocol.
44 The typesetting relies on Wenzel's theory presentation tools. An
45 annotated source file is run, typesetting the theory
46 % and any requested Isabelle responses
47 in the form of a \LaTeX\ source file. This book is derived almost entirely
48 from output generated in this way. The final chapter of Part~I explains how
49 users may produce their own formal documents in a similar fashion.
51 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
52 the download area and to documentation and other information. Most Isabelle
53 sessions are now run from within David Aspinall's\index{Aspinall, David}
54 wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
55 General}, even together with the
56 \hfootref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}{X-Symbol} package
57 for XEmacs. This book says very little about Proof General, which has its own
58 documentation. In order to run Isabelle, you will need a Standard ML
59 compiler. We recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is
60 free and gives the best performance. The other fully supported compiler is
61 \hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
64 This tutorial owes a lot to the constant discussions with and the valuable
65 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
66 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
67 Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan
68 Merz was also kind enough to read and comment on a draft version. We
69 received comments from Stefano Bistarelli, Gergely Buday and Tanja
72 The research has been funded by many sources, including the {\sc dfg} grants
73 Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,
74 GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
75 \textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}