doc-src/preface.tex
 author lcp Fri, 15 Apr 1994 18:43:21 +0200 changeset 329 92586a978648 parent 304 5edc4f5e5ebd child 356 2e6545875982 permissions -rw-r--r--
penultimate Springer draft
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 Most theorem provers support a fixed logic, such as first-order or  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  6 equational logic. They bring sophisticated proof procedures to bear upon  304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  7 the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is  329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  8 an impressive example.  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  9 329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  10 {\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  11 support a fixed logic too. These are higher-order type theories,  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  12 explicitly concerned with computation and capable of expressing  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  13 developments in constructive mathematics. They are far removed from  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  14 classical first-order logic.  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  15 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  16 A diverse collection of logics --- type theories, process calculi,  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  17 $\lambda$-calculi --- may be found in the Computer Science literature.  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  18 Such logics require proof support. Few proof procedures are known for  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  19 them, but the theorem prover can at least automate routine steps.  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  20 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  21 A {\bf generic} theorem prover is one that supports a variety of logics.  304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  22 Some generic provers are noteworthy for their user interfaces  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  23 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  24 syntactic framework that can express typical inference rules. Isabelle's  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  25 distinctive feature is its representation of logics within a fragment of  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  26 higher-order logic, called the meta-logic. The proof theory of  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  27 higher-order logic may be used to demonstrate that the representation is  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  28 correct~\cite{paulson89}. The approach has much in common with the  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  29 Edinburgh Logical Framework~\cite{harper-jacm} and with  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  30 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  31 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  32 An inference rule in Isabelle is a generalized Horn clause. Rules are  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  33 joined to make proofs by resolving such clauses. Logical variables in  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  34 goals can be instantiated incrementally. But Isabelle is not a resolution  304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  35 theorem prover like Otter. Isabelle's clauses are drawn from a richer  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  36 language and a fully automatic search would be impractical. Isabelle does  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  37 not resolve clauses automatically, but under user direction. You can  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  38 conduct single-step proofs, use Isabelle's built-in proof procedures, or  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  39 develop new proof procedures using tactics and tacticals.  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  40 329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  41 Isabelle's meta-logic is higher-order, based on the simply typed  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  42 $\lambda$-calculus. So resolution cannot use ordinary unification, but  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  43 higher-order unification~\cite{huet75}. This complicated procedure gives  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  44 Isabelle strong support for many logical formalisms involving variable  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  45 binding.  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  46 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  47 The diagram below illustrates some of the logics distributed with Isabelle.  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  48 These include first-order logic (intuitionistic and classical), the sequent  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal  329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  51 logics, and a Logic for Computable Functions. Several experimental logics  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  52 are being developed, such as linear logic.  285 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}  304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  58 Isabelle is a complex system, but beginners can get by with a few commands  285 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 304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  76 \item {\em The Isabelle Reference Manual\/} provides detailed information  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  77  about Isabelle's facilities, excluding the object-logics. This part  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  78  would make boring reading, though browsing might be useful. Mostly you  5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  79  should use it to locate facts quickly.  285 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  329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  82  distributed with Isabelle. The chapters are intended for reference only;  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  83  they overlap somewhat so that each chapter can be read in isolation.  285 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 329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  93 \section*{Releases of Isabelle}  285 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 304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  121 \section*{Acknowledgements}  285 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},  329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  130 \S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  131 Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@. Carsten  304 5edc4f5e5ebd revisions to first Springer draft lcp parents: 285 diff changeset  132 Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed  329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  133 to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  134 the front.  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  135 329 92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  136 David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  137 V{\"o}lker and Markus Wenzel suggested changes and corrections to the  92586a978648 penultimate Springer draft lcp parents: 304 diff changeset  138 documentation.  285 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  139 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  140 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  141 to develop Isabelle's standard object-logics. David Aspinall performed  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  142 some useful research into theories and implemented an Isabelle Emacs mode.  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  143 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  144 Poly/{\sc ml}.  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  145 fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  146 The research has been funded by numerous SERC grants dating from the Alvey  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  147 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects  fd4a6585e5bf first draft of Springer book lcp parents: diff changeset  148 3245: Logical Frameworks and 6453: Types).