|
1 \chapter*{Preface} |
|
2 \markboth{Preface}{Preface} %or Preface ? |
|
3 \addcontentsline{toc}{chapter}{Preface} |
|
4 |
|
5 \index{Isabelle!object-logics supported} |
|
6 |
|
7 Most theorem provers support a fixed logic, such as first-order or |
|
8 equational logic. They bring sophisticated proof procedures to bear upon |
|
9 the conjectured formula. An impressive example is the resolution prover |
|
10 Otter, which Quaife~\cite{quaife-book} has used to formalize a body of |
|
11 mathematics. |
|
12 |
|
13 ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a |
|
14 fixed logic too, but one far removed from first-order logic. They are |
|
15 explicitly concerned with computation. A diverse collection of logics --- |
|
16 type theories, process calculi, $\lambda$-calculi --- may be found in the |
|
17 Computer Science literature. Such logics require proof support. Few proof |
|
18 procedures exist, but the theorem prover can at least check that each |
|
19 inference is valid. |
|
20 |
|
21 A {\bf generic} theorem prover is one that can support many different |
|
22 logics. Most of these \cite{dawson90,mural,sawamura92} work by |
|
23 implementing a syntactic framework that can express the features of typical |
|
24 inference rules. Isabelle's distinctive feature is its representation of |
|
25 logics using a meta-logic. This meta-logic is just a fragment of |
|
26 higher-order logic; known proof theory may be used to demonstrate that the |
|
27 representation is correct~\cite{paulson89}. The representation has much in |
|
28 common with the Edinburgh Logical Framework~\cite{harper-jacm} and with |
|
29 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. |
|
30 |
|
31 An inference rule in Isabelle is a generalized Horn clause. Rules are |
|
32 joined to make proofs by resolving such clauses. Logical variables in |
|
33 goals can be instantiated incrementally. But Isabelle is not a resolution |
|
34 theorem prover like Otter. Isabelle's clauses are drawn from a richer, |
|
35 higher-order language and a fully automatic search would be impractical. |
|
36 Isabelle does not join clauses automatically, but under strict user |
|
37 control. You can conduct single-step proofs, use Isabelle's built-in proof |
|
38 procedures, or develop new proof procedures using tactics and tacticals. |
|
39 |
|
40 Isabelle's meta-logic is higher-order, based on the typed |
|
41 $\lambda$-calculus. So resolution cannot use ordinary unification, but |
|
42 higher-order unification~\cite{huet75}. This complicated procedure gives |
|
43 Isabelle strong support for many logical formalisms involving variable |
|
44 binding. |
|
45 |
|
46 The diagram below illustrates some of the logics distributed with Isabelle. |
|
47 These include first-order logic (intuitionistic and classical), the sequent |
|
48 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, |
|
49 a version of Constructive Type Theory~\cite{nordstrom90}, several modal |
|
50 logics, and a Logic for Computable Functions. Several experimental |
|
51 logics are also available, such a term assignment calculus for linear |
|
52 logic. |
|
53 |
|
54 \centerline{\epsfbox{Isa-logics.eps}} |
|
55 |
|
56 |
|
57 \section*{How to read this book} |
|
58 Isabelle is a large system, but beginners can get by with a few commands |
|
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 |
|
76 \item {\em The Isabelle Reference Manual\/} contains information about most |
|
77 of the facilities of Isabelle, apart from particular object-logics. This |
|
78 part would make boring reading, though browsing might be useful. Mostly |
|
79 you should use it to locate facts quickly. |
|
80 |
|
81 \item {\em Isabelle's Object-Logics\/} describes the various logics |
|
82 distributed with Isabelle. Its final chapter explains how to define new |
|
83 logics. The other chapters are intended for reference only. |
|
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 |
|
93 \section*{Releases of Isabelle}\index{Isabelle!release history} |
|
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 |
|
107 Isabelle is available by anonymous ftp: |
|
108 \begin{itemize} |
|
109 \item University of Cambridge\\ |
|
110 host {\tt ftp.cl.cam.ac.uk}\\ |
|
111 directory {\tt ml} |
|
112 |
|
113 \item Technical University of Munich\\ |
|
114 host {\tt ftp.informatik.tu-muenchen.de}\\ |
|
115 directory {\tt local/lehrstuhl/nipkow} |
|
116 \end{itemize} |
|
117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any |
|
118 errors you find in this book and your problems or successes with Isabelle. |
|
119 |
|
120 |
|
121 \subsection*{Acknowledgements} |
|
122 Tobias Nipkow has made immense contributions to Isabelle, including the |
|
123 parser generator, type classes, the simplifier, and several object-logics. |
|
124 He also arranged for several of his students to help. Carsten Clasohm |
|
125 implemented the theory database; Markus Wenzel implemented macros; Sonia |
|
126 Mahjoub and Karin Nimmermann also contributed. |
|
127 |
|
128 Nipkow and his students wrote much of the documentation underlying this |
|
129 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, |
|
130 Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of |
|
131 Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm |
|
132 contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to |
|
133 Chap.\ts\ref{Defining-Logics}. |
|
134 |
|
135 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and |
|
136 Markus Wenzel suggested changes and corrections to the documentation. |
|
137 |
|
138 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped |
|
139 to develop Isabelle's standard object-logics. David Aspinall performed |
|
140 some useful research into theories and implemented an Isabelle Emacs mode. |
|
141 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, |
|
142 Poly/{\sc ml}. |
|
143 |
|
144 The research has been funded by numerous SERC grants dating from the Alvey |
|
145 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects |
|
146 3245: Logical Frameworks and 6453: Types). |
|
147 |
|
148 |
|
149 \index{ML} |