\chapter*{Preface}\markboth{Preface}{Preface} %or Preface ?%%\addcontentsline{toc}{chapter}{Preface} Most theorem provers support a fixed logic, such as first-order orequational logic. They bring sophisticated proof procedures to bear uponthe conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} isan impressive example.{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} eachsupport a fixed logic too. These are higher-order type theories,explicitly concerned with computation and capable of expressingdevelopments in constructive mathematics. They are far removed fromclassical first-order logic.A diverse collection of logics --- type theories, process calculi,$\lambda$-calculi --- may be found in the Computer Science literature.Such logics require proof support. Few proof procedures are known forthem, but the theorem prover can at least automate routine steps.A {\bf generic} theorem prover is one that supports a variety of logics.Some generic provers are noteworthy for their user interfaces\cite{dawson90,mural,sawamura92}. Most of them work by implementing asyntactic framework that can express typical inference rules. Isabelle'sdistinctive feature is its representation of logics within a fragment ofhigher-order logic, called the meta-logic. The proof theory ofhigher-order logic may be used to demonstrate that the representation iscorrect~\cite{paulson89}. The approach has much in common with theEdinburgh Logical Framework~\cite{harper-jacm} and withFelty's~\cite{felty93} use of $\lambda$Prolog to implement logics.An inference rule in Isabelle is a generalized Horn clause. Rules arejoined to make proofs by resolving such clauses. Logical variables ingoals can be instantiated incrementally. But Isabelle is not a resolutiontheorem prover like Otter. Isabelle's clauses are drawn from a richerlanguage and a fully automatic search would be impractical. Isabelle doesnot resolve clauses automatically, but under user direction. You canconduct single-step proofs, use Isabelle's built-in proof procedures, ordevelop new proof procedures using tactics and tacticals.Isabelle's meta-logic is higher-order, based on the simply typed$\lambda$-calculus. So resolution cannot use ordinary unification, buthigher-order unification~\cite{huet75}. This complicated procedure givesIsabelle strong support for many logical formalisms involving variablebinding.The diagram below illustrates some of the logics distributed with Isabelle.These include first-order logic (intuitionistic and classical), the sequentcalculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},a version of Constructive Type Theory~\cite{nordstrom90}, several modallogics, and a Logic for Computable Functions~\cite{paulson87}. Severalexperimental logics are being developed, such as linear logic.\centerline{\epsfbox{gfx/Isa-logics.eps}}\section*{How to read this book}Isabelle is a complex system, but beginners can get by with a few commandsand a basic knowledge of how Isabelle works. Some knowledge ofStandard~\ML{} is essential because \ML{} is Isabelle's user interface.Advanced Isabelle theorem proving can involve writing \ML{} code, possiblywith Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} coversmuch material connected with Isabelle, including a simple theorem prover.The Isabelle documentation is divided into three parts, which servedistinct purposes:\begin{itemize}\item {\em Introduction to Isabelle\/} describes the basic features of Isabelle. This part is intended to be read through. If you are impatient to get started, you might skip the first chapter, which describes Isabelle's meta-logic in some detail. The other chapters present on-line sessions of increasing difficulty. It also explains how to derive rules define theories, and concludes with an extended example: a Prolog interpreter.\item {\em The Isabelle Reference Manual\/} provides detailed information about Isabelle's facilities, excluding the object-logics. This part would make boring reading, though browsing might be useful. Mostly you should use it to locate facts quickly.\item {\em Isabelle's Object-Logics\/} describes the various logics distributed with Isabelle. The chapters are intended for reference only; they overlap somewhat so that each chapter can be read in isolation.\end{itemize}This book should not be read from start to finish. Instead you might reada couple of chapters from {\em Introduction to Isabelle}, then try someexamples referring to the other parts, return to the {\em Introduction},and so forth. Starred sections discuss obscure matters and may be skippedon a first reading.\section*{Releases of Isabelle}Isabelle was first distributed in 1986. The 1987 version introduced ahigher-order meta-logic with an improved treatment of quantifiers. The1988 version added limited polymorphism and support for natural deduction.The 1989 version included a parser and pretty printer generator. The 1992version introduced type classes, to support many-sorted and higher-orderlogics. The 1993 version provides greater support for theories and ismuch faster. Isabelle is still under development. Projects under consideration includebetter support for inductive definitions, some means of recording proofs, agraphical user interface, and developments in the standard object-logics.I hope but cannot promise to maintain upwards compatibility.Isabelle can be downloaded from .\begin{quote}{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/} \end{quote}The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}provides a forum for discussing problems and applications involvingIsabelle. To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.Please notify me of any errors you find in this book.\section*{Acknowledgements} Tobias Nipkow has made immense contributions to Isabelle, including theparser generator, type classes, the simplifier, and several object-logics.He also arranged for several of his students to help. Carsten Clasohmimplemented the theory database; Markus Wenzel implemented macros; SoniaMahjoub and Karin Nimmermann also contributed. Nipkow and his students wrote much of the documentation underlying thisbook. Nipkow wrote the first versions of \S\ref{sec:defining-theories},\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@. CarstenClasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributedto Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation atthe front.David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, NorbertV{\"o}lker and Markus Wenzel suggested changes and corrections to thedocumentation.Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helpedto develop Isabelle's standard object-logics. David Aspinall performedsome useful research into theories and implemented an Isabelle Emacs mode.Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,Poly/{\sc ml}. The research has been funded by numerous SERC grants dating from the Alveyprogramme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects3245: Logical Frameworks and 6453: Types).