1 \chapter*{Preface} |
|
2 \markboth{Preface}{Preface} |
|
3 |
|
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. |
|
8 |
|
9 The book has three parts. |
|
10 \begin{itemize} |
|
11 \item |
|
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. |
|
18 \item |
|
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. |
|
25 \item |
|
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. |
|
30 \end{itemize} |
|
31 |
|
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. |
|
37 |
|
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. |
|
43 |
|
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 |
|
50 and Tanja Vos. |
|
51 |
|
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). |
|