some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
removed historic note about Poly/ML vs. SML/NJ;
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.
6 It is written for potential users rather
7 than for our colleagues in the research world.
9 The book has three parts.
12 The first part, \textbf{Elementary Techniques},
13 shows how to model functional programs in higher-order logic. Early
14 examples involve lists and the natural numbers. Most proofs
15 are two steps long, consisting of induction on a chosen variable
16 followed by the \isa{auto} tactic. But even this elementary part
17 covers such advanced topics as nested and mutual recursion.
19 The second part, \textbf{Logic and Sets}, presents a collection of
20 lower-level tactics that you can use to apply rules selectively. It
21 also describes Isabelle/HOL's treatment of sets, functions and
22 relations and explains how to define sets inductively. One of the
23 examples concerns the theory of model checking, and another is drawn
24 from a classic textbook on formal languages.
26 The third part, \textbf{Advanced Material}, describes a variety of other
27 topics. Among these are the real numbers, records and overloading. Advanced
28 techniques for induction and recursion are described. A whole chapter is
29 devoted to an extended example: the verification of a security protocol.
32 The typesetting relies on Wenzel's theory presentation tools. An
33 annotated source file is run, typesetting the theory
34 in the form of a \LaTeX\ source file. This book is derived almost entirely
35 from output generated in this way. The final chapter of Part~I explains how
36 users may produce their own formal documents in a similar fashion.
38 Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains
39 links to the download area and to documentation and other information.
40 The classic Isabelle user interface is Proof~General~/ Emacs by David
41 Aspinall's\index{Aspinall, David}. This book says very little about
42 Proof General, which has its own documentation.
44 This tutorial owes a lot to the constant discussions with and the valuable
45 feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
46 M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
47 Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan
48 Merz was also kind enough to read and comment on a draft version. We
49 received comments from Stefano Bistarelli, Gergely Buday, John Matthews
52 The research has been funded by many sources, including the {\sc dfg} grants
53 NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc
54 epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and
55 by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the
56 \emph{Types} project).