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 firstorder or


6 
equational logic. They bring sophisticated proof procedures to bear upon

304

7 
the conjectured formula. The resolution prover Otter~\cite{wosbledsoe} 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 higherorder type theories,


12 
explicitly concerned with computation and capable of expressing


13 
developments in constructive mathematics. They are far removed from


14 
classical firstorder 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 
higherorder logic, called the metalogic. The proof theory of


27 
higherorder 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{harperjacm} 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 singlestep proofs, use Isabelle's builtin proof procedures, or


39 
develop new proof procedures using tactics and tacticals.

285

40 

329

41 
Isabelle's metalogic is higherorder, based on the simply typed

285

42 
$\lambda$calculus. So resolution cannot use ordinary unification, but


43 
higherorder 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 firstorder logic (intuitionistic and classical), the sequent


49 
calculus, higherorder logic, ZermeloFraenkel 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/Isalogics.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 metalogic in some detail. The other chapters


72 
present online 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 objectlogics. 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 ObjectLogics\/} 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 
higherorder metalogic 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 manysorted and higherorder


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 objectlogics.


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.tumuenchen.de}\\


115 
directory {\tt local/lehrstuhl/nipkow}


116 
\end{itemize}

356

117 
The electronic distribution list {\tt isabelleusers\at cl.cam.ac.uk}


118 
provides a forum for discussing problems and applications involving


119 
Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.


120 
Please notify me of any errors you find in this book.

285

121 

304

122 
\section*{Acknowledgements}

285

123 
Tobias Nipkow has made immense contributions to Isabelle, including the


124 
parser generator, type classes, the simplifier, and several objectlogics.


125 
He also arranged for several of his students to help. Carsten Clasohm


126 
implemented the theory database; Markus Wenzel implemented macros; Sonia


127 
Mahjoub and Karin Nimmermann also contributed.


128 


129 
Nipkow and his students wrote much of the documentation underlying this


130 
book. Nipkow wrote the first versions of \S\ref{sec:definingtheories},

329

131 
\S\ref{sec:refdefiningtheories}, Chap.\ts\ref{DefiningLogics},


132 
Chap.\ts\ref{simpchap} and App.\ts\ref{app:TheorySyntax}\@. Carsten

304

133 
Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed

329

134 
to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at


135 
the front.

285

136 

329

137 
David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert


138 
V{\"o}lker and Markus Wenzel suggested changes and corrections to the


139 
documentation.

285

140 


141 
Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped


142 
to develop Isabelle's standard objectlogics. David Aspinall performed


143 
some useful research into theories and implemented an Isabelle Emacs mode.


144 
Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,


145 
Poly/{\sc ml}.


146 


147 
The research has been funded by numerous SERC grants dating from the Alvey


148 
programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects


149 
3245: Logical Frameworks and 6453: Types).
