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