doc-src/preface.tex
author wenzelm
Sat, 22 May 2010 20:10:11 +0200
changeset 37061 026504e21088
parent 14379 ea10a8c3e9cf
permissions -rw-r--r--
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
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 ?
356
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
     3
%%\addcontentsline{toc}{chapter}{Preface} 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     4
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     5
Most theorem provers support a fixed logic, such as first-order or
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     6
equational logic.  They bring sophisticated proof procedures to bear upon
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
     7
the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
     8
an impressive example.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
     9
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    10
{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    11
support a fixed logic too.  These are higher-order type theories,
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    12
explicitly concerned with computation and capable of expressing
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    13
developments in constructive mathematics.  They are far removed from
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    14
classical first-order logic.
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    15
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    16
A diverse collection of logics --- type theories, process calculi,
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    17
$\lambda$-calculi --- may be found in the Computer Science literature.
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    18
Such logics require proof support.  Few proof procedures are known for
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    19
them, but the theorem prover can at least automate routine steps.
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    20
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    21
A {\bf generic} theorem prover is one that supports a variety of logics.
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    22
Some generic provers are noteworthy for their user interfaces
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    23
\cite{dawson90,mural,sawamura92}.  Most of them work by implementing a
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    24
syntactic framework that can express typical inference rules.  Isabelle's
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    25
distinctive feature is its representation of logics within a fragment of
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    26
higher-order logic, called the meta-logic.  The proof theory of
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    27
higher-order logic may be used to demonstrate that the representation is
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    28
correct~\cite{paulson89}.  The approach has much in common with the
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    29
Edinburgh Logical Framework~\cite{harper-jacm} and with
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    30
Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    31
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    32
An inference rule in Isabelle is a generalized Horn clause.  Rules are
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    33
joined to make proofs by resolving such clauses.  Logical variables in
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    34
goals can be instantiated incrementally.  But Isabelle is not a resolution
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    35
theorem prover like Otter.  Isabelle's clauses are drawn from a richer
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    36
language and a fully automatic search would be impractical.  Isabelle does
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    37
not resolve clauses automatically, but under user direction.  You can
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    38
conduct single-step proofs, use Isabelle's built-in proof procedures, or
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    39
develop new proof procedures using tactics and tacticals.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    40
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    41
Isabelle's meta-logic is higher-order, based on the simply typed
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    42
$\lambda$-calculus.  So resolution cannot use ordinary unification, but
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    43
higher-order unification~\cite{huet75}.  This complicated procedure gives
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    44
Isabelle strong support for many logical formalisms involving variable
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    45
binding.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    46
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    47
The diagram below illustrates some of the logics distributed with Isabelle.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    48
These include first-order logic (intuitionistic and classical), the sequent
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    49
calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    50
a version of Constructive Type Theory~\cite{nordstrom90}, several modal
356
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
    51
logics, and a Logic for Computable Functions~\cite{paulson87}.  Several
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
    52
experimental logics are being developed, such as linear logic.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
    53
5374
6ef3742b6153 moved images to gfx dir;
wenzelm
parents: 356
diff changeset
    54
\centerline{\epsfbox{gfx/Isa-logics.eps}}
285
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}
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    58
Isabelle is a complex system, but beginners can get by with a few commands
285
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
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    76
\item {\em The Isabelle Reference Manual\/} provides detailed information
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    77
  about Isabelle's facilities, excluding the object-logics.  This part
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    78
  would make boring reading, though browsing might be useful.  Mostly you
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
    79
  should use it to locate facts quickly.
285
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
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    82
  distributed with Isabelle.  The chapters are intended for reference only;
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    83
  they overlap somewhat so that each chapter can be read in isolation.
285
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
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
    93
\section*{Releases of Isabelle}
285
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
14379
ea10a8c3e9cf updated links to the old ftp site
paulson
parents: 5374
diff changeset
   107
Isabelle can be downloaded from .
ea10a8c3e9cf updated links to the old ftp site
paulson
parents: 5374
diff changeset
   108
\begin{quote}
ea10a8c3e9cf updated links to the old ftp site
paulson
parents: 5374
diff changeset
   109
{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/}  
ea10a8c3e9cf updated links to the old ftp site
paulson
parents: 5374
diff changeset
   110
\end{quote}
356
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
   111
The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
   112
provides a forum for discussing problems and applications involving
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
   113
Isabelle.  To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.
2e6545875982 post-CRC corrections
lcp
parents: 329
diff changeset
   114
Please notify me of any errors you find in this book.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   115
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
   116
\section*{Acknowledgements} 
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   117
Tobias Nipkow has made immense contributions to Isabelle, including the
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   118
parser generator, type classes, the simplifier, and several object-logics.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   119
He also arranged for several of his students to help.  Carsten Clasohm
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   120
implemented the theory database; Markus Wenzel implemented macros; Sonia
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   121
Mahjoub and Karin Nimmermann also contributed.  
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   122
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   123
Nipkow and his students wrote much of the documentation underlying this
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   124
book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   125
\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   126
Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@.  Carsten
304
5edc4f5e5ebd revisions to first Springer draft
lcp
parents: 285
diff changeset
   127
Clasohm contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   128
to Chap.\ts\ref{chap:syntax}.  Nipkow also provided the quotation at
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   129
the front.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   130
329
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   131
David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   132
V{\"o}lker and Markus Wenzel suggested changes and corrections to the
92586a978648 penultimate Springer draft
lcp
parents: 304
diff changeset
   133
documentation.
285
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   134
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   135
Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   136
to develop Isabelle's standard object-logics.  David Aspinall performed
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   137
some useful research into theories and implemented an Isabelle Emacs mode.
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   138
Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   139
Poly/{\sc ml}.  
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   140
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   141
The research has been funded by numerous SERC grants dating from the Alvey
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   142
programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects
fd4a6585e5bf first draft of Springer book
lcp
parents:
diff changeset
   143
3245: Logical Frameworks and 6453: Types).