285

1 
\chapter*{Preface}


2 
\markboth{Preface}{Preface} %or Preface ?


3 
\addcontentsline{toc}{chapter}{Preface}


4 


5 
\index{Isabelle!objectlogics supported}


6 


7 
Most theorem provers support a fixed logic, such as firstorder or


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

304

9 
the conjectured formula. The resolution prover Otter~\cite{wosbledsoe} 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 firstorder 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.

285

17 

304

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


24 
higherorder 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{harperjacm} and with

285

27 
Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.


28 


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

304

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 singlestep proofs, use Isabelle's builtin proof procedures, or


36 
develop new proof procedures using tactics and tacticals.

285

37 


38 
Isabelle's metalogic is higherorder, based on the typed


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


40 
higherorder unification~\cite{huet75}. This complicated procedure gives


41 
Isabelle strong support for many logical formalisms involving variable


42 
binding.


43 


44 
The diagram below illustrates some of the logics distributed with Isabelle.


45 
These include firstorder logic (intuitionistic and classical), the sequent


46 
calculus, higherorder logic, ZermeloFraenkel 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


50 
logic.


51 


52 
\centerline{\epsfbox{Isalogics.eps}}


53 


54 


55 
\section*{How to read this book}

304

56 
Isabelle is a complex system, but beginners can get by with a few commands

285

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.


62 


63 
The Isabelle documentation is divided into three parts, which serve


64 
distinct purposes:


65 
\begin{itemize}


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 metalogic in some detail. The other chapters


70 
present online sessions of increasing difficulty. It also explains how


71 
to derive rules define theories, and concludes with an extended example:


72 
a Prolog interpreter.


73 

304

74 
\item {\em The Isabelle Reference Manual\/} provides detailed information


75 
about Isabelle's facilities, excluding the objectlogics. This part


76 
would make boring reading, though browsing might be useful. Mostly you


77 
should use it to locate facts quickly.

285

78 


79 
\item {\em Isabelle's ObjectLogics\/} 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.


82 
\end{itemize}


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


87 
on a first reading.


88 


89 


90 


91 
\section*{Releases of Isabelle}\index{Isabelle!release history}


92 
Isabelle was first distributed in 1986. The 1987 version introduced a


93 
higherorder metalogic 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 manysorted and higherorder


97 
logics. The 1993 version provides greater support for theories and is


98 
much faster.


99 


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


103 
I hope but cannot promise to maintain upwards compatibility.


104 


105 
Isabelle is available by anonymous ftp:


106 
\begin{itemize}


107 
\item University of Cambridge\\


108 
host {\tt ftp.cl.cam.ac.uk}\\


109 
directory {\tt ml}


110 


111 
\item Technical University of Munich\\


112 
host {\tt ftp.informatik.tumuenchen.de}\\


113 
directory {\tt local/lehrstuhl/nipkow}


114 
\end{itemize}


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.


117 


118 

304

119 
\section*{Acknowledgements}

285

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


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


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.


125 


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


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

304

128 
\S\ref{sec:refdefiningtheories}, Chap.\ts\ref{simpchap},


129 
Chap.\ts\ref{DefiningLogics} and App.\ts\ref{app:TheorySyntax}\@. Carsten


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


131 
to Chap.\ts\ref{DefiningLogics}.

285

132 

304

133 
David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and

285

134 
Markus Wenzel suggested changes and corrections to the documentation.


135 


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


137 
to develop Isabelle's standard objectlogics. 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,


140 
Poly/{\sc ml}.


141 


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


145 


146 


147 
\index{ML}
