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