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