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