doc-src/preface.tex
 author lcp Mon, 21 Mar 1994 10:51:28 +0100 changeset 285 fd4a6585e5bf child 304 5edc4f5e5ebd permissions -rw-r--r--
first draft of Springer book
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 1 \chapter*{Preface} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 2 \markboth{Preface}{Preface} %or Preface ? fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 3 \addcontentsline{toc}{chapter}{Preface} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 4 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 5 \index{Isabelle!object-logics supported} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 6 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 7 Most theorem provers support a fixed logic, such as first-order or fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 8 equational logic. They bring sophisticated proof procedures to bear upon fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 9 the conjectured formula. An impressive example is the resolution prover fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 10 Otter, which Quaife~\cite{quaife-book} has used to formalize a body of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 11 mathematics. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 12 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 13 ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 14 fixed logic too, but one far removed from first-order logic. They are fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 15 explicitly concerned with computation. A diverse collection of logics --- fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 16 type theories, process calculi, $\lambda$-calculi --- may be found in the fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 17 Computer Science literature. Such logics require proof support. Few proof fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 18 procedures exist, but the theorem prover can at least check that each fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 19 inference is valid. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 20 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 21 A {\bf generic} theorem prover is one that can support many different fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 22 logics. Most of these \cite{dawson90,mural,sawamura92} work by fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 23 implementing a syntactic framework that can express the features of typical fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 24 inference rules. Isabelle's distinctive feature is its representation of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 25 logics using a meta-logic. This meta-logic is just a fragment of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 26 higher-order logic; known proof theory may be used to demonstrate that the fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 27 representation is correct~\cite{paulson89}. The representation has much in fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 28 common with the Edinburgh Logical Framework~\cite{harper-jacm} and with fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 29 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 30 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 31 An inference rule in Isabelle is a generalized Horn clause. Rules are fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 32 joined to make proofs by resolving such clauses. Logical variables in fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 33 goals can be instantiated incrementally. But Isabelle is not a resolution fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 34 theorem prover like Otter. Isabelle's clauses are drawn from a richer, fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 35 higher-order language and a fully automatic search would be impractical. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 36 Isabelle does not join clauses automatically, but under strict user fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 37 control. You can conduct single-step proofs, use Isabelle's built-in proof fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 38 procedures, or develop new proof procedures using tactics and tacticals. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 39 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 40 Isabelle's meta-logic is higher-order, based on the typed fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 41 $\lambda$-calculus. So resolution cannot use ordinary unification, but fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 42 higher-order unification~\cite{huet75}. This complicated procedure gives fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 43 Isabelle strong support for many logical formalisms involving variable fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 44 binding. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 45 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 46 The diagram below illustrates some of the logics distributed with Isabelle. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 47 These include first-order logic (intuitionistic and classical), the sequent fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 48 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 49 a version of Constructive Type Theory~\cite{nordstrom90}, several modal fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 50 logics, and a Logic for Computable Functions. Several experimental fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 51 logics are also available, such a term assignment calculus for linear fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 52 logic. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 53 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 54 \centerline{\epsfbox{Isa-logics.eps}} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 55 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 56 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 57 \section*{How to read this book} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 58 Isabelle is a large system, but beginners can get by with a few commands fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 59 and a basic knowledge of how Isabelle works. Some knowledge of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 60 Standard~\ML{} is essential because \ML{} is Isabelle's user interface. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 61 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 62 with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 63 much material connected with Isabelle, including a simple theorem prover. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 64 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 65 The Isabelle documentation is divided into three parts, which serve fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 66 distinct purposes: fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 67 \begin{itemize} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 68 \item {\em Introduction to Isabelle\/} describes the basic features of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 69 Isabelle. This part is intended to be read through. If you are fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 70 impatient to get started, you might skip the first chapter, which fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 71 describes Isabelle's meta-logic in some detail. The other chapters fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 72 present on-line sessions of increasing difficulty. It also explains how fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 73 to derive rules define theories, and concludes with an extended example: fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 74 a Prolog interpreter. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 75 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 76 \item {\em The Isabelle Reference Manual\/} contains information about most fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 77 of the facilities of Isabelle, apart from particular object-logics. This fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 78 part would make boring reading, though browsing might be useful. Mostly fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 79 you should use it to locate facts quickly. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 80 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 81 \item {\em Isabelle's Object-Logics\/} describes the various logics fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 82 distributed with Isabelle. Its final chapter explains how to define new fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 83 logics. The other chapters are intended for reference only. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 84 \end{itemize} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 85 This book should not be read from start to finish. Instead you might read fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 86 a couple of chapters from {\em Introduction to Isabelle}, then try some fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 87 examples referring to the other parts, return to the {\em Introduction}, fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 88 and so forth. Starred sections discuss obscure matters and may be skipped fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 89 on a first reading. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 90 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 91 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 92 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 93 \section*{Releases of Isabelle}\index{Isabelle!release history} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 94 Isabelle was first distributed in 1986. The 1987 version introduced a fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 95 higher-order meta-logic with an improved treatment of quantifiers. The fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 96 1988 version added limited polymorphism and support for natural deduction. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 97 The 1989 version included a parser and pretty printer generator. The 1992 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 98 version introduced type classes, to support many-sorted and higher-order fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 99 logics. The 1993 version provides greater support for theories and is fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 100 much faster. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 101 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 102 Isabelle is still under development. Projects under consideration include fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 103 better support for inductive definitions, some means of recording proofs, a fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 104 graphical user interface, and developments in the standard object-logics. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 105 I hope but cannot promise to maintain upwards compatibility. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 106 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 107 Isabelle is available by anonymous ftp: fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 108 \begin{itemize} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 109 \item University of Cambridge\\ fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 110 host {\tt ftp.cl.cam.ac.uk}\\ fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 111 directory {\tt ml} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 112 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 113 \item Technical University of Munich\\ fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 114 host {\tt ftp.informatik.tu-muenchen.de}\\ fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 115 directory {\tt local/lehrstuhl/nipkow} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 116 \end{itemize} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 118 errors you find in this book and your problems or successes with Isabelle. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 119 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 120 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 121 \subsection*{Acknowledgements} fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 122 Tobias Nipkow has made immense contributions to Isabelle, including the fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 123 parser generator, type classes, the simplifier, and several object-logics. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 124 He also arranged for several of his students to help. Carsten Clasohm fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 125 implemented the theory database; Markus Wenzel implemented macros; Sonia fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 126 Mahjoub and Karin Nimmermann also contributed. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 127 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 128 Nipkow and his students wrote much of the documentation underlying this fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 129 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 130 Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 131 Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 132 contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 133 Chap.\ts\ref{Defining-Logics}. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 134 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 135 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 136 Markus Wenzel suggested changes and corrections to the documentation. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 137 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 138 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 139 to develop Isabelle's standard object-logics. David Aspinall performed fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 140 some useful research into theories and implemented an Isabelle Emacs mode. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 141 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 142 Poly/{\sc ml}. fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 143 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 144 The research has been funded by numerous SERC grants dating from the Alvey fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 145 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 146 3245: Logical Frameworks and 6453: Types). fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 147 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 148 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset 149 \index{ML}