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


9 
the conjectured formula. An impressive example is the resolution prover


10 
Otter, which Quaife~\cite{quaifebook} 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 firstorder 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 metalogic. This metalogic is just a fragment of


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


38 
procedures, or develop new proof procedures using tactics and tacticals.


39 


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


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


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


48 
calculus, higherorder logic, ZermeloFraenkel 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{Isalogics.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 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 


76 
\item {\em The Isabelle Reference Manual\/} contains information about most


77 
of the facilities of Isabelle, apart from particular objectlogics. 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 ObjectLogics\/} 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 
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}


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


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:definingtheories},


130 
Chap.\ts\ref{simpchap}, Chap.\ts\ref{DefiningLogics} 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{DefiningLogics}.


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