1\chapter*{Preface} 2\markboth{Preface}{Preface} %or Preface ? 3%%\addcontentsline{toc}{chapter}{Preface} 4 5Most theorem provers support a fixed logic, such as first-order or 6equational logic. They bring sophisticated proof procedures to bear upon 7the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is 8an impressive example. 9 10{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each 11support a fixed logic too. These are higher-order type theories, 12explicitly concerned with computation and capable of expressing 13developments in constructive mathematics. They are far removed from 14classical first-order logic. 15 16A diverse collection of logics --- type theories, process calculi, 17$\lambda$-calculi --- may be found in the Computer Science literature. 18Such logics require proof support. Few proof procedures are known for 19them, but the theorem prover can at least automate routine steps. 20 21A {\bf generic} theorem prover is one that supports a variety of logics. 22Some generic provers are noteworthy for their user interfaces 23\cite{dawson90,mural,sawamura92}. Most of them work by implementing a 24syntactic framework that can express typical inference rules. Isabelle's 25distinctive feature is its representation of logics within a fragment of 26higher-order logic, called the meta-logic. The proof theory of 27higher-order logic may be used to demonstrate that the representation is 28correct~\cite{paulson89}. The approach has much in common with the 29Edinburgh Logical Framework~\cite{harper-jacm} and with 30Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. 31 32An inference rule in Isabelle is a generalized Horn clause. Rules are 33joined to make proofs by resolving such clauses. Logical variables in 34goals can be instantiated incrementally. But Isabelle is not a resolution 35theorem prover like Otter. Isabelle's clauses are drawn from a richer 36language and a fully automatic search would be impractical. Isabelle does 37not resolve clauses automatically, but under user direction. You can 38conduct single-step proofs, use Isabelle's built-in proof procedures, or 39develop new proof procedures using tactics and tacticals. 40 41Isabelle's meta-logic is higher-order, based on the simply typed 42$\lambda$-calculus. So resolution cannot use ordinary unification, but 43higher-order unification~\cite{huet75}. This complicated procedure gives 44Isabelle strong support for many logical formalisms involving variable 45binding. 46 47The diagram below illustrates some of the logics distributed with Isabelle. 48These include first-order logic (intuitionistic and classical), the sequent 49calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, 50a version of Constructive Type Theory~\cite{nordstrom90}, several modal 51logics, and a Logic for Computable Functions~\cite{paulson87}. Several 52experimental logics are being developed, such as linear logic. 53 54\centerline{\epsfbox{gfx/Isa-logics.eps}} 55 56 57\section*{How to read this book} 58Isabelle is a complex system, but beginners can get by with a few commands 59and a basic knowledge of how Isabelle works. Some knowledge of 60Standard~\ML{} is essential because \ML{} is Isabelle's user interface. 61Advanced Isabelle theorem proving can involve writing \ML{} code, possibly 62with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers 63much material connected with Isabelle, including a simple theorem prover. 64 65The Isabelle documentation is divided into three parts, which serve 66distinct 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\/} provides detailed information 77 about Isabelle's facilities, excluding the object-logics. This part 78 would make boring reading, though browsing might be useful. Mostly you 79 should use it to locate facts quickly. 80 81\item {\em Isabelle's Object-Logics\/} describes the various logics 82 distributed with Isabelle. The chapters are intended for reference only; 83 they overlap somewhat so that each chapter can be read in isolation. 84\end{itemize} 85This book should not be read from start to finish. Instead you might read 86a couple of chapters from {\em Introduction to Isabelle}, then try some 87examples referring to the other parts, return to the {\em Introduction}, 88and so forth. Starred sections discuss obscure matters and may be skipped 89on a first reading. 90 91 92 93\section*{Releases of Isabelle} 94Isabelle was first distributed in 1986. The 1987 version introduced a 95higher-order meta-logic with an improved treatment of quantifiers. The 961988 version added limited polymorphism and support for natural deduction. 97The 1989 version included a parser and pretty printer generator. The 1992 98version introduced type classes, to support many-sorted and higher-order 99logics. The 1993 version provides greater support for theories and is 100much faster. 101 102Isabelle is still under development. Projects under consideration include 103better support for inductive definitions, some means of recording proofs, a 104graphical user interface, and developments in the standard object-logics. 105I hope but cannot promise to maintain upwards compatibility. 106 107Isabelle can be downloaded from . 108\begin{quote} 109{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/} 110\end{quote} 111The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk} 112provides a forum for discussing problems and applications involving 113Isabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}. 114Please notify me of any errors you find in this book. 115 116\section*{Acknowledgements} 117Tobias Nipkow has made immense contributions to Isabelle, including the 118parser generator, type classes, the simplifier, and several object-logics. 119He also arranged for several of his students to help. Carsten Clasohm 120implemented the theory database; Markus Wenzel implemented macros; Sonia 121Mahjoub and Karin Nimmermann also contributed. 122 123Nipkow and his students wrote much of the documentation underlying this 124book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, 125\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics}, 126Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@. Carsten 127Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed 128to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at 129the front. 130 131David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert 132V{\"o}lker and Markus Wenzel suggested changes and corrections to the 133documentation. 134 135Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped 136to develop Isabelle's standard object-logics. David Aspinall performed 137some useful research into theories and implemented an Isabelle Emacs mode. 138Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, 139Poly/{\sc ml}. 140 141The research has been funded by numerous SERC grants dating from the Alvey 142programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects 1433245: Logical Frameworks and 6453: Types). 144