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