paulson@11408: \chapter*{Preface}
paulson@11408: \markboth{Preface}{Preface}
paulson@11408: 
paulson@12539: This volume is a self-contained introduction to interactive proof
paulson@12813: in higher-order logic (HOL), using the proof assistant Isabelle 2002. 
paulson@12539: Compared with existing Isabelle documentation,
paulson@12539: it provides a direct route into higher-order logic, which most people
paulson@12539: prefer these days. It bypasses first-order logic and minimizes
paulson@11408: discussion of meta-theory.  It is written for potential users rather
paulson@11408: than for our colleagues in the research world.
paulson@11408: 
paulson@11450: Another departure from previous documentation is that we describe Markus
paulson@11450: Wenzel's proof script notation instead of ML tactic scripts.  The latter
paulson@11408: make it easier to introduce new tactics on the fly, but hardly anybody
paulson@11408: does that.  Wenzel's dedicated syntax is elegant, replacing for example
paulson@11408: eight simplification tactics with a single method, namely \isa{simp},
paulson@11408: with associated options.
paulson@11408: 
paulson@12539: The book has three parts.  
paulson@12539: \begin{itemize}
paulson@12539: \item 
wenzelm@12669: The first part, \textbf{Elementary Techniques},
paulson@12539: shows how to model functional programs in higher-order logic.  Early
paulson@12539: examples involve lists and the natural numbers.  Most proofs
paulson@12539: are two steps long, consisting of induction on a chosen variable
paulson@12539: followed by the \isa{auto} tactic.  But even this elementary part
paulson@12539: covers such advanced topics as nested and mutual recursion.
paulson@12539: \item 
paulson@12539: The second part, \textbf{Logic and Sets}, presents a collection of
paulson@12539: lower-level tactics that you can use to apply rules selectively.  It
paulson@12539: also describes Isabelle/HOL's treatment of sets, functions and
paulson@12539: relations and explains how to define sets inductively.  One of the
paulson@12539: examples concerns the theory of model checking, and another is drawn
paulson@12539: from a classic textbook on formal languages.
paulson@12539: \item 
paulson@12539: The third part, \textbf{Advanced Material}, describes a variety of
paulson@12539: other topics.  Among these are the real numbers, records and
paulson@12539: overloading.  Esoteric techniques are described involving induction and
paulson@12539: recursion.  A whole chapter is devoted to an extended example: the
paulson@12539: verification of a security protocol.
paulson@12539: \end{itemize}
paulson@12539: 
nipkow@12327: The typesetting relies on Wenzel's theory presentation tools.  An
nipkow@12327: annotated source file is run, typesetting the theory
nipkow@12327: % and any requested Isabelle responses
wenzelm@12646: in the form of a \LaTeX\ source file.  This book is derived almost entirely
wenzelm@12646: from output generated in this way.  The final chapter of Part~I explains how
wenzelm@12646: users may produce their own formal documents in a similar fashion.
paulson@11408: 
wenzelm@12641: Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
wenzelm@12641: the download area and to documentation and other information.  Most Isabelle
wenzelm@12641: sessions are now run from within David Aspinall's\index{Aspinall, David}
wenzelm@12641: wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
wenzelm@12641:   General}, even together with the
wenzelm@13141: \hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs.  This
wenzelm@13141: book says very little about Proof General, which has its own documentation.
wenzelm@13141: In order to run Isabelle, you will need a Standard ML compiler.  We recommend
wenzelm@13141: \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best
wenzelm@13141: performance.  The other fully supported compiler is
wenzelm@12641: \hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
wenzelm@12641:   New Jersey}.
paulson@12539: 
paulson@11408: This tutorial owes a lot to the constant discussions with and the valuable
nipkow@11547: feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
nipkow@11547: M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
paulson@12812: Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan
nipkow@11547: Merz was also kind enough to read and comment on a draft version.  We
paulson@14179: received comments from Stefano Bistarelli, Gergely Buday, John Matthews
paulson@14179: and Tanja Vos.
paulson@11408: 
nipkow@11547: The research has been funded by many sources, including the {\sc dfg} grants
nipkow@11547: Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,
nipkow@11547: GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
nipkow@11547: \textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}
nipkow@11547: project).