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