1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/preface.tex Mon Mar 21 10:51:28 1994 +0100
1.3 @@ -0,0 +1,149 @@
1.4 +\chapter*{Preface}
1.5 +\markboth{Preface}{Preface} %or Preface ?
1.6 +\addcontentsline{toc}{chapter}{Preface}
1.7 +
1.8 +\index{Isabelle!object-logics supported}
1.9 +
1.10 +Most theorem provers support a fixed logic, such as first-order or
1.11 +equational logic. They bring sophisticated proof procedures to bear upon
1.12 +the conjectured formula. An impressive example is the resolution prover
1.13 +Otter, which Quaife~\cite{quaife-book} has used to formalize a body of
1.14 +mathematics.
1.15 +
1.16 +ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a
1.17 +fixed logic too, but one far removed from first-order logic. They are
1.18 +explicitly concerned with computation. A diverse collection of logics ---
1.19 +type theories, process calculi, $\lambda$-calculi --- may be found in the
1.20 +Computer Science literature. Such logics require proof support. Few proof
1.21 +procedures exist, but the theorem prover can at least check that each
1.22 +inference is valid.
1.23 +
1.24 +A {\bf generic} theorem prover is one that can support many different
1.25 +logics. Most of these \cite{dawson90,mural,sawamura92} work by
1.26 +implementing a syntactic framework that can express the features of typical
1.27 +inference rules. Isabelle's distinctive feature is its representation of
1.28 +logics using a meta-logic. This meta-logic is just a fragment of
1.29 +higher-order logic; known proof theory may be used to demonstrate that the
1.30 +representation is correct~\cite{paulson89}. The representation has much in
1.31 +common with the Edinburgh Logical Framework~\cite{harper-jacm} and with
1.32 +Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
1.33 +
1.34 +An inference rule in Isabelle is a generalized Horn clause. Rules are
1.35 +joined to make proofs by resolving such clauses. Logical variables in
1.36 +goals can be instantiated incrementally. But Isabelle is not a resolution
1.37 +theorem prover like Otter. Isabelle's clauses are drawn from a richer,
1.38 +higher-order language and a fully automatic search would be impractical.
1.39 +Isabelle does not join clauses automatically, but under strict user
1.40 +control. You can conduct single-step proofs, use Isabelle's built-in proof
1.41 +procedures, or develop new proof procedures using tactics and tacticals.
1.42 +
1.43 +Isabelle's meta-logic is higher-order, based on the typed
1.44 +$\lambda$-calculus. So resolution cannot use ordinary unification, but
1.45 +higher-order unification~\cite{huet75}. This complicated procedure gives
1.46 +Isabelle strong support for many logical formalisms involving variable
1.47 +binding.
1.48 +
1.49 +The diagram below illustrates some of the logics distributed with Isabelle.
1.50 +These include first-order logic (intuitionistic and classical), the sequent
1.51 +calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
1.52 +a version of Constructive Type Theory~\cite{nordstrom90}, several modal
1.53 +logics, and a Logic for Computable Functions. Several experimental
1.54 +logics are also available, such a term assignment calculus for linear
1.55 +logic.
1.56 +
1.57 +\centerline{\epsfbox{Isa-logics.eps}}
1.58 +
1.59 +
1.60 +\section*{How to read this book}
1.61 +Isabelle is a large system, but beginners can get by with a few commands
1.62 +and a basic knowledge of how Isabelle works. Some knowledge of
1.63 +Standard~\ML{} is essential because \ML{} is Isabelle's user interface.
1.64 +Advanced Isabelle theorem proving can involve writing \ML{} code, possibly
1.65 +with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers
1.66 +much material connected with Isabelle, including a simple theorem prover.
1.67 +
1.68 +The Isabelle documentation is divided into three parts, which serve
1.69 +distinct purposes:
1.70 +\begin{itemize}
1.71 +\item {\em Introduction to Isabelle\/} describes the basic features of
1.72 + Isabelle. This part is intended to be read through. If you are
1.73 + impatient to get started, you might skip the first chapter, which
1.74 + describes Isabelle's meta-logic in some detail. The other chapters
1.75 + present on-line sessions of increasing difficulty. It also explains how
1.76 + to derive rules define theories, and concludes with an extended example:
1.77 + a Prolog interpreter.
1.78 +
1.79 +\item {\em The Isabelle Reference Manual\/} contains information about most
1.80 + of the facilities of Isabelle, apart from particular object-logics. This
1.81 + part would make boring reading, though browsing might be useful. Mostly
1.82 + you should use it to locate facts quickly.
1.83 +
1.84 +\item {\em Isabelle's Object-Logics\/} describes the various logics
1.85 + distributed with Isabelle. Its final chapter explains how to define new
1.86 + logics. The other chapters are intended for reference only.
1.87 +\end{itemize}
1.88 +This book should not be read from start to finish. Instead you might read
1.89 +a couple of chapters from {\em Introduction to Isabelle}, then try some
1.90 +examples referring to the other parts, return to the {\em Introduction},
1.91 +and so forth. Starred sections discuss obscure matters and may be skipped
1.92 +on a first reading.
1.93 +
1.94 +
1.95 +
1.96 +\section*{Releases of Isabelle}\index{Isabelle!release history}
1.97 +Isabelle was first distributed in 1986. The 1987 version introduced a
1.98 +higher-order meta-logic with an improved treatment of quantifiers. The
1.99 +1988 version added limited polymorphism and support for natural deduction.
1.100 +The 1989 version included a parser and pretty printer generator. The 1992
1.101 +version introduced type classes, to support many-sorted and higher-order
1.102 +logics. The 1993 version provides greater support for theories and is
1.103 +much faster.
1.104 +
1.105 +Isabelle is still under development. Projects under consideration include
1.106 +better support for inductive definitions, some means of recording proofs, a
1.107 +graphical user interface, and developments in the standard object-logics.
1.108 +I hope but cannot promise to maintain upwards compatibility.
1.109 +
1.110 +Isabelle is available by anonymous ftp:
1.111 +\begin{itemize}
1.112 +\item University of Cambridge\\
1.113 + host {\tt ftp.cl.cam.ac.uk}\\
1.114 + directory {\tt ml}
1.115 +
1.116 +\item Technical University of Munich\\
1.117 + host {\tt ftp.informatik.tu-muenchen.de}\\
1.118 + directory {\tt local/lehrstuhl/nipkow}
1.119 +\end{itemize}
1.120 +My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any
1.121 +errors you find in this book and your problems or successes with Isabelle.
1.122 +
1.123 +
1.124 +\subsection*{Acknowledgements}
1.125 +Tobias Nipkow has made immense contributions to Isabelle, including the
1.126 +parser generator, type classes, the simplifier, and several object-logics.
1.127 +He also arranged for several of his students to help. Carsten Clasohm
1.128 +implemented the theory database; Markus Wenzel implemented macros; Sonia
1.129 +Mahjoub and Karin Nimmermann also contributed.
1.130 +
1.131 +Nipkow and his students wrote much of the documentation underlying this
1.132 +book. Nipkow wrote the first versions of \S\ref{sec:defining-theories},
1.133 +Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of
1.134 +Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm
1.135 +contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to
1.136 +Chap.\ts\ref{Defining-Logics}.
1.137 +
1.138 +David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and
1.139 +Markus Wenzel suggested changes and corrections to the documentation.
1.140 +
1.141 +Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
1.142 +to develop Isabelle's standard object-logics. David Aspinall performed
1.143 +some useful research into theories and implemented an Isabelle Emacs mode.
1.144 +Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
1.145 +Poly/{\sc ml}.
1.146 +
1.147 +The research has been funded by numerous SERC grants dating from the Alvey
1.148 +programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects
1.149 +3245: Logical Frameworks and 6453: Types).
1.150 +
1.151 +
1.152 +\index{ML}