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