doc-src/preface.tex
author wenzelm
Mon Oct 01 21:19:50 2007 +0200 (2007-10-01)
changeset 24803 38577b4b1fde
parent 14379 ea10a8c3e9cf
permissions -rw-r--r--
Norbert Schirmer: record improvements;
lcp@285
     1
\chapter*{Preface}
lcp@285
     2
\markboth{Preface}{Preface}   %or Preface ?
lcp@356
     3
%%\addcontentsline{toc}{chapter}{Preface} 
lcp@285
     4
lcp@285
     5
Most theorem provers support a fixed logic, such as first-order or
lcp@285
     6
equational logic.  They bring sophisticated proof procedures to bear upon
lcp@304
     7
the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
lcp@329
     8
an impressive example.
lcp@285
     9
lcp@329
    10
{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each
lcp@329
    11
support a fixed logic too.  These are higher-order type theories,
lcp@329
    12
explicitly concerned with computation and capable of expressing
lcp@329
    13
developments in constructive mathematics.  They are far removed from
lcp@329
    14
classical first-order logic.
lcp@329
    15
lcp@329
    16
A diverse collection of logics --- type theories, process calculi,
lcp@329
    17
$\lambda$-calculi --- may be found in the Computer Science literature.
lcp@329
    18
Such logics require proof support.  Few proof procedures are known for
lcp@329
    19
them, but the theorem prover can at least automate routine steps.
lcp@329
    20
lcp@329
    21
A {\bf generic} theorem prover is one that supports a variety of logics.
lcp@304
    22
Some generic provers are noteworthy for their user interfaces
lcp@304
    23
\cite{dawson90,mural,sawamura92}.  Most of them work by implementing a
lcp@304
    24
syntactic framework that can express typical inference rules.  Isabelle's
lcp@304
    25
distinctive feature is its representation of logics within a fragment of
lcp@304
    26
higher-order logic, called the meta-logic.  The proof theory of
lcp@304
    27
higher-order logic may be used to demonstrate that the representation is
lcp@304
    28
correct~\cite{paulson89}.  The approach has much in common with the
lcp@304
    29
Edinburgh Logical Framework~\cite{harper-jacm} and with
lcp@285
    30
Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
lcp@285
    31
lcp@285
    32
An inference rule in Isabelle is a generalized Horn clause.  Rules are
lcp@285
    33
joined to make proofs by resolving such clauses.  Logical variables in
lcp@285
    34
goals can be instantiated incrementally.  But Isabelle is not a resolution
lcp@304
    35
theorem prover like Otter.  Isabelle's clauses are drawn from a richer
lcp@304
    36
language and a fully automatic search would be impractical.  Isabelle does
lcp@304
    37
not resolve clauses automatically, but under user direction.  You can
lcp@304
    38
conduct single-step proofs, use Isabelle's built-in proof procedures, or
lcp@304
    39
develop new proof procedures using tactics and tacticals.
lcp@285
    40
lcp@329
    41
Isabelle's meta-logic is higher-order, based on the simply typed
lcp@285
    42
$\lambda$-calculus.  So resolution cannot use ordinary unification, but
lcp@285
    43
higher-order unification~\cite{huet75}.  This complicated procedure gives
lcp@285
    44
Isabelle strong support for many logical formalisms involving variable
lcp@285
    45
binding.
lcp@285
    46
lcp@285
    47
The diagram below illustrates some of the logics distributed with Isabelle.
lcp@285
    48
These include first-order logic (intuitionistic and classical), the sequent
lcp@285
    49
calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
lcp@285
    50
a version of Constructive Type Theory~\cite{nordstrom90}, several modal
lcp@356
    51
logics, and a Logic for Computable Functions~\cite{paulson87}.  Several
lcp@356
    52
experimental logics are being developed, such as linear logic.
lcp@285
    53
wenzelm@5374
    54
\centerline{\epsfbox{gfx/Isa-logics.eps}}
lcp@285
    55
lcp@285
    56
lcp@285
    57
\section*{How to read this book}
lcp@304
    58
Isabelle is a complex system, but beginners can get by with a few commands
lcp@285
    59
and a basic knowledge of how Isabelle works.  Some knowledge of
lcp@285
    60
Standard~\ML{} is essential because \ML{} is Isabelle's user interface.
lcp@285
    61
Advanced Isabelle theorem proving can involve writing \ML{} code, possibly
lcp@285
    62
with Isabelle's sources at hand.  My book on~\ML{}~\cite{paulson91} covers
lcp@285
    63
much material connected with Isabelle, including a simple theorem prover.
lcp@285
    64
lcp@285
    65
The Isabelle documentation is divided into three parts, which serve
lcp@285
    66
distinct purposes:
lcp@285
    67
\begin{itemize}
lcp@285
    68
\item {\em Introduction to Isabelle\/} describes the basic features of
lcp@285
    69
  Isabelle.  This part is intended to be read through.  If you are
lcp@285
    70
  impatient to get started, you might skip the first chapter, which
lcp@285
    71
  describes Isabelle's meta-logic in some detail.  The other chapters
lcp@285
    72
  present on-line sessions of increasing difficulty.  It also explains how
lcp@285
    73
  to derive rules define theories, and concludes with an extended example:
lcp@285
    74
  a Prolog interpreter.
lcp@285
    75
lcp@304
    76
\item {\em The Isabelle Reference Manual\/} provides detailed information
lcp@304
    77
  about Isabelle's facilities, excluding the object-logics.  This part
lcp@304
    78
  would make boring reading, though browsing might be useful.  Mostly you
lcp@304
    79
  should use it to locate facts quickly.
lcp@285
    80
lcp@285
    81
\item {\em Isabelle's Object-Logics\/} describes the various logics
lcp@329
    82
  distributed with Isabelle.  The chapters are intended for reference only;
lcp@329
    83
  they overlap somewhat so that each chapter can be read in isolation.
lcp@285
    84
\end{itemize}
lcp@285
    85
This book should not be read from start to finish.  Instead you might read
lcp@285
    86
a couple of chapters from {\em Introduction to Isabelle}, then try some
lcp@285
    87
examples referring to the other parts, return to the {\em Introduction},
lcp@285
    88
and so forth.  Starred sections discuss obscure matters and may be skipped
lcp@285
    89
on a first reading.
lcp@285
    90
lcp@285
    91
lcp@285
    92
lcp@329
    93
\section*{Releases of Isabelle}
lcp@285
    94
Isabelle was first distributed in 1986.  The 1987 version introduced a
lcp@285
    95
higher-order meta-logic with an improved treatment of quantifiers.  The
lcp@285
    96
1988 version added limited polymorphism and support for natural deduction.
lcp@285
    97
The 1989 version included a parser and pretty printer generator.  The 1992
lcp@285
    98
version introduced type classes, to support many-sorted and higher-order
lcp@285
    99
logics.  The 1993 version provides greater support for theories and is
lcp@285
   100
much faster.  
lcp@285
   101
lcp@285
   102
Isabelle is still under development.  Projects under consideration include
lcp@285
   103
better support for inductive definitions, some means of recording proofs, a
lcp@285
   104
graphical user interface, and developments in the standard object-logics.
lcp@285
   105
I hope but cannot promise to maintain upwards compatibility.
lcp@285
   106
paulson@14379
   107
Isabelle can be downloaded from .
paulson@14379
   108
\begin{quote}
paulson@14379
   109
{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/}  
paulson@14379
   110
\end{quote}
lcp@356
   111
The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
lcp@356
   112
provides a forum for discussing problems and applications involving
lcp@356
   113
Isabelle.  To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.
lcp@356
   114
Please notify me of any errors you find in this book.
lcp@285
   115
lcp@304
   116
\section*{Acknowledgements} 
lcp@285
   117
Tobias Nipkow has made immense contributions to Isabelle, including the
lcp@285
   118
parser generator, type classes, the simplifier, and several object-logics.
lcp@285
   119
He also arranged for several of his students to help.  Carsten Clasohm
lcp@285
   120
implemented the theory database; Markus Wenzel implemented macros; Sonia
lcp@285
   121
Mahjoub and Karin Nimmermann also contributed.  
lcp@285
   122
lcp@285
   123
Nipkow and his students wrote much of the documentation underlying this
lcp@285
   124
book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},
lcp@329
   125
\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},
lcp@329
   126
Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@.  Carsten
lcp@304
   127
Clasohm contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed
lcp@329
   128
to Chap.\ts\ref{chap:syntax}.  Nipkow also provided the quotation at
lcp@329
   129
the front.
lcp@285
   130
lcp@329
   131
David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert
lcp@329
   132
V{\"o}lker and Markus Wenzel suggested changes and corrections to the
lcp@329
   133
documentation.
lcp@285
   134
lcp@285
   135
Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
lcp@285
   136
to develop Isabelle's standard object-logics.  David Aspinall performed
lcp@285
   137
some useful research into theories and implemented an Isabelle Emacs mode.
lcp@285
   138
Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
lcp@285
   139
Poly/{\sc ml}.  
lcp@285
   140
lcp@285
   141
The research has been funded by numerous SERC grants dating from the Alvey
lcp@285
   142
programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects
lcp@285
   143
3245: Logical Frameworks and 6453: Types).