author paulson Tue Dec 18 16:14:56 2001 +0100 (2001-12-18) changeset 12539 368414099877 parent 12538 150af0a4bb11 child 12540 a5604ff1ef4e
     1.1 --- a/doc-src/TutorialI/preface.tex	Tue Dec 18 16:14:50 2001 +0100
1.2 +++ b/doc-src/TutorialI/preface.tex	Tue Dec 18 16:14:56 2001 +0100
1.3 @@ -1,10 +1,11 @@
1.4  \chapter*{Preface}
1.5  \markboth{Preface}{Preface}
1.6
1.7 -This volume is a self-contained introduction to interactive proof using
1.8 -Isabelle/HOL\@.  Compared with existing Isabelle documentation, it
1.9 -provides a straightforward route into higher-order logic, which most
1.10 -people prefer these days. It bypasses first-order logic and minimizes
1.11 +This volume is a self-contained introduction to interactive proof
1.12 +in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@.
1.13 +Compared with existing Isabelle documentation,
1.14 +it provides a direct route into higher-order logic, which most people
1.15 +prefer these days. It bypasses first-order logic and minimizes
1.16  discussion of meta-theory.  It is written for potential users rather
1.17  than for our colleagues in the research world.
1.18
1.19 @@ -16,20 +17,56 @@
1.20  eight simplification tactics with a single method, namely \isa{simp},
1.21  with associated options.
1.22
1.23 -\REMARK{mention Wenzel once author?}
1.24 +The book has three parts.
1.25 +\begin{itemize}
1.26 +\item
1.27 +The first part, \textbf{Basic Techniques},
1.28 +shows how to model functional programs in higher-order logic.  Early
1.29 +examples involve lists and the natural numbers.  Most proofs
1.30 +are two steps long, consisting of induction on a chosen variable
1.31 +followed by the \isa{auto} tactic.  But even this elementary part
1.32 +covers such advanced topics as nested and mutual recursion.
1.33 +\item
1.34 +The second part, \textbf{Logic and Sets}, presents a collection of
1.35 +lower-level tactics that you can use to apply rules selectively.  It
1.36 +also describes Isabelle/HOL's treatment of sets, functions and
1.37 +relations and explains how to define sets inductively.  One of the
1.38 +examples concerns the theory of model checking, and another is drawn
1.39 +from a classic textbook on formal languages.
1.40 +\item
1.41 +The third part, \textbf{Advanced Material}, describes a variety of
1.42 +other topics.  Among these are the real numbers, records and
1.44 +recursion.  A whole chapter is devoted to an extended example: the
1.45 +verification of a security protocol.
1.46 +\end{itemize}
1.47 +
1.48  The typesetting relies on Wenzel's theory presentation tools.  An
1.49  annotated source file is run, typesetting the theory
1.50  % and any requested Isabelle responses
1.51  in the form of a \TeX\ source file.  This book is
1.52  derived almost entirely from output generated in this way.
1.53
1.54 +Isabelle's
1.55 +\href{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}{web site}
1.57 +information.  Most Isabelle sessions are now run from within David
1.58 +Aspinall's wonderful user interface,
1.59 +\href{http://www.proofgeneral.org/}{Proof General}.  This book says
1.60 +very little about Proof General, which has its own documentation.  In
1.61 +order to run Isabelle, you will need a Standard ML compiler.  We
1.62 +recommend \href{http://www.polyml.org/}{Poly/ML}, which is free and
1.63 +gives the best performance.  The other supported compiler is
1.64 +\href{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
1.65 +ML of New Jersey}.
1.66 +
1.67  This tutorial owes a lot to the constant discussions with and the valuable
1.68  feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
1.69  M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
1.70  Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan
1.71  Merz was also kind enough to read and comment on a draft version.  We