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