paulson@11408

1 
\chapter*{Preface}

paulson@11408

2 
\markboth{Preface}{Preface}

paulson@11408

3 

paulson@12539

4 
This volume is a selfcontained introduction to interactive proof

nipkow@16306

5 
in higherorder logic (HOL), using the proof assistant Isabelle.

nipkow@16306

6 
It is written for potential users rather

paulson@11408

7 
than for our colleagues in the research world.

paulson@11408

8 

paulson@12539

9 
The book has three parts.

paulson@12539

10 
\begin{itemize}

paulson@12539

11 
\item

wenzelm@12669

12 
The first part, \textbf{Elementary Techniques},

paulson@12539

13 
shows how to model functional programs in higherorder logic. Early

paulson@12539

14 
examples involve lists and the natural numbers. Most proofs

paulson@12539

15 
are two steps long, consisting of induction on a chosen variable

paulson@12539

16 
followed by the \isa{auto} tactic. But even this elementary part

paulson@12539

17 
covers such advanced topics as nested and mutual recursion.

paulson@12539

18 
\item

paulson@12539

19 
The second part, \textbf{Logic and Sets}, presents a collection of

paulson@12539

20 
lowerlevel tactics that you can use to apply rules selectively. It

paulson@12539

21 
also describes Isabelle/HOL's treatment of sets, functions and

paulson@12539

22 
relations and explains how to define sets inductively. One of the

paulson@12539

23 
examples concerns the theory of model checking, and another is drawn

paulson@12539

24 
from a classic textbook on formal languages.

paulson@12539

25 
\item

nipkow@16306

26 
The third part, \textbf{Advanced Material}, describes a variety of other

nipkow@16306

27 
topics. Among these are the real numbers, records and overloading. Advanced

nipkow@16306

28 
techniques for induction and recursion are described. A whole chapter is

nipkow@16306

29 
devoted to an extended example: the verification of a security protocol.

paulson@12539

30 
\end{itemize}

paulson@12539

31 

nipkow@12327

32 
The typesetting relies on Wenzel's theory presentation tools. An

nipkow@12327

33 
annotated source file is run, typesetting the theory

wenzelm@12646

34 
in the form of a \LaTeX\ source file. This book is derived almost entirely

wenzelm@12646

35 
from output generated in this way. The final chapter of Part~I explains how

wenzelm@12646

36 
users may produce their own formal documents in a similar fashion.

paulson@11408

37 

wenzelm@47822

38 
Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains

wenzelm@47822

39 
links to the download area and to documentation and other information.

wenzelm@47822

40 
The classic Isabelle user interface is Proof~General~/ Emacs by David

wenzelm@47822

41 
Aspinall's\index{Aspinall, David}. This book says very little about

wenzelm@47822

42 
Proof General, which has its own documentation.

paulson@12539

43 

paulson@11408

44 
This tutorial owes a lot to the constant discussions with and the valuable

nipkow@11547

45 
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf

nipkow@11547

46 
M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,

paulson@12812

47 
Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan

nipkow@11547

48 
Merz was also kind enough to read and comment on a draft version. We

paulson@14179

49 
received comments from Stefano Bistarelli, Gergely Buday, John Matthews

paulson@14179

50 
and Tanja Vos.

paulson@11408

51 

nipkow@11547

52 
The research has been funded by many sources, including the {\sc dfg} grants

nipkow@16306

53 
NI~491/2, NI~491/3, NI~491/4, NI~491/6, {\sc bmbf} project Verisoft, the {\sc

nipkow@16306

54 
epsrc} grants GR/K57381, GR/K77051, GR/M75440, GR/R01156/01 GR/S57198/01 and

nipkow@16306

55 
by the \textsc{esprit} working groups 21900 and IST199929001 (the

nipkow@16306

56 
\emph{Types} project).
