doc-src/TutorialI/preface.tex
author wenzelm
Fri, 04 Jan 2002 19:23:28 +0100
changeset 12630 6f2951938b66
parent 12561 8cf9d9a3a327
child 12641 140241dc55e6
permissions -rw-r--r--
document preparation overview;
paulson@11408
     1
\chapter*{Preface}
paulson@11408
     2
\markboth{Preface}{Preface}
paulson@11408
     3
paulson@12539
     4
This volume is a self-contained introduction to interactive proof
paulson@12539
     5
in higher-order logic (HOL), using the proof assistant Isabelle/HOL\@. 
paulson@12539
     6
Compared with existing Isabelle documentation,
paulson@12539
     7
it provides a direct route into higher-order logic, which most people
paulson@12539
     8
prefer these days. It bypasses first-order logic and minimizes
paulson@11408
     9
discussion of meta-theory.  It is written for potential users rather
paulson@11408
    10
than for our colleagues in the research world.
paulson@11408
    11
paulson@11450
    12
\index{Wenzel, Markus}%
paulson@11450
    13
Another departure from previous documentation is that we describe Markus
paulson@11450
    14
Wenzel's proof script notation instead of ML tactic scripts.  The latter
paulson@11408
    15
make it easier to introduce new tactics on the fly, but hardly anybody
paulson@11408
    16
does that.  Wenzel's dedicated syntax is elegant, replacing for example
paulson@11408
    17
eight simplification tactics with a single method, namely \isa{simp},
paulson@11408
    18
with associated options.
paulson@11408
    19
paulson@12539
    20
The book has three parts.  
paulson@12539
    21
\begin{itemize}
paulson@12539
    22
\item 
paulson@12539
    23
The first part, \textbf{Basic Techniques},
paulson@12539
    24
shows how to model functional programs in higher-order logic.  Early
paulson@12539
    25
examples involve lists and the natural numbers.  Most proofs
paulson@12539
    26
are two steps long, consisting of induction on a chosen variable
paulson@12539
    27
followed by the \isa{auto} tactic.  But even this elementary part
paulson@12539
    28
covers such advanced topics as nested and mutual recursion.
paulson@12539
    29
\item 
paulson@12539
    30
The second part, \textbf{Logic and Sets}, presents a collection of
paulson@12539
    31
lower-level tactics that you can use to apply rules selectively.  It
paulson@12539
    32
also describes Isabelle/HOL's treatment of sets, functions and
paulson@12539
    33
relations and explains how to define sets inductively.  One of the
paulson@12539
    34
examples concerns the theory of model checking, and another is drawn
paulson@12539
    35
from a classic textbook on formal languages.
paulson@12539
    36
\item 
paulson@12539
    37
The third part, \textbf{Advanced Material}, describes a variety of
paulson@12539
    38
other topics.  Among these are the real numbers, records and
paulson@12539
    39
overloading.  Esoteric techniques are described involving induction and
paulson@12539
    40
recursion.  A whole chapter is devoted to an extended example: the
paulson@12539
    41
verification of a security protocol.
paulson@12539
    42
\end{itemize}
paulson@12539
    43
nipkow@12327
    44
The typesetting relies on Wenzel's theory presentation tools.  An
nipkow@12327
    45
annotated source file is run, typesetting the theory
nipkow@12327
    46
% and any requested Isabelle responses
wenzelm@12630
    47
in the form of a \LaTeX\ source file.  This book is
paulson@11408
    48
derived almost entirely from output generated in this way.
wenzelm@12630
    49
The end of Part~I explains how users may produce their own formal documents in
wenzelm@12630
    50
the same manner.
paulson@11408
    51
paulson@12539
    52
Isabelle's
paulson@12561
    53
\hfootref{http://isabelle.in.tum.de/}{web site}
paulson@12539
    54
contains links to the download area and to documentation and other
paulson@12539
    55
information.  Most Isabelle sessions are now run from within David
paulson@12539
    56
Aspinall's wonderful user interface,
paulson@12561
    57
\hfootref{http://www.proofgeneral.org/}{Proof General}.  This book says
paulson@12539
    58
very little about Proof General, which has its own documentation.  In
paulson@12539
    59
order to run Isabelle, you will need a Standard ML compiler.  We
paulson@12561
    60
recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is free and
wenzelm@12630
    61
gives the best performance.  The other fully supported compiler is
paulson@12561
    62
\hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard
paulson@12539
    63
ML of New Jersey}.
paulson@12539
    64
paulson@11408
    65
This tutorial owes a lot to the constant discussions with and the valuable
nipkow@11547
    66
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf
nipkow@11547
    67
M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
nipkow@11547
    68
Cornelia Pusch, Norbert Schirmer, Martin Strecker and Markus Wenzel. Stephan
nipkow@11547
    69
Merz was also kind enough to read and comment on a draft version.  We
nipkow@11547
    70
received comments from Stefano Bistarelli, Gergely Buday and Tanja
paulson@12539
    71
Vos.
paulson@11408
    72
nipkow@11547
    73
The research has been funded by many sources, including the {\sc dfg} grants
nipkow@11547
    74
Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,
nipkow@11547
    75
GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
nipkow@11547
    76
\textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}
nipkow@11547
    77
project).