\chapter*{Preface}

\markboth{Preface}{Preface}

This volume is a self-contained introduction to interactive proof

in higher-order logic (HOL), using the proof assistant Isabelle. 

It is written for potential users rather

than for our colleagues in the research world.

The book has three parts.  

\begin{itemize}

\item 

The first part, \textbf{Elementary Techniques},

shows how to model functional programs in higher-order logic.  Early

examples involve lists and the natural numbers.  Most proofs

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

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

covers such advanced topics as nested and mutual recursion.

\item 

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

lower-level tactics that you can use to apply rules selectively.  It

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

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

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

from a classic textbook on formal languages.

\item 

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

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

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

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

\end{itemize}

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

annotated source file is run, typesetting the theory

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

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

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

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

the download area and to documentation and other information.  Most Isabelle

sessions are now run from within David Aspinall's\index{Aspinall, David}

wonderful user interface, \hfootref{http://proofgeneral.inf.ed.ac.uk/}{Proof

  General}, even together with the

\hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs.  This

book says very little about Proof General, which has its own documentation.

In order to run Isabelle, you will need a Standard ML compiler.  We recommend

\hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best

performance.  The other fully supported compiler is

\hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}.

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

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

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

Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan

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

received comments from Stefano Bistarelli, Gergely Buday, John Matthews

and Tanja Vos.

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

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

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

by the \textsc{esprit} working groups 21900 and IST-1999-29001 (the

\emph{Types} project).