doc-src/preface.tex
 changeset 285 fd4a6585e5bf child 304 5edc4f5e5ebd
equal inserted replaced
284:1072b18b2caa 285:fd4a6585e5bf

     1 \chapter*{Preface}

     2 \markboth{Preface}{Preface}   %or Preface ?

     3 \addcontentsline{toc}{chapter}{Preface}

     4

     5 \index{Isabelle!object-logics supported}

     6

     7 Most theorem provers support a fixed logic, such as first-order or

     8 equational logic.  They bring sophisticated proof procedures to bear upon

     9 the conjectured formula.  An impressive example is the resolution prover

    10 Otter, which Quaife~\cite{quaife-book} has used to formalize a body of

    11 mathematics.

    12

    13 ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a

    14 fixed logic too, but one far removed from first-order logic.  They are

    15 explicitly concerned with computation.  A diverse collection of logics ---

    16 type theories, process calculi, $\lambda$-calculi --- may be found in the

    17 Computer Science literature.  Such logics require proof support.  Few proof

    18 procedures exist, but the theorem prover can at least check that each

    19 inference is valid.

    20

    21 A {\bf generic} theorem prover is one that can support many different

    22 logics.  Most of these \cite{dawson90,mural,sawamura92} work by

    23 implementing a syntactic framework that can express the features of typical

    24 inference rules.  Isabelle's distinctive feature is its representation of

    25 logics using a meta-logic.  This meta-logic is just a fragment of

    26 higher-order logic; known proof theory may be used to demonstrate that the

    27 representation is correct~\cite{paulson89}.  The representation has much in

    28 common with the Edinburgh Logical Framework~\cite{harper-jacm} and with

    29 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.

    30

    31 An inference rule in Isabelle is a generalized Horn clause.  Rules are

    32 joined to make proofs by resolving such clauses.  Logical variables in

    33 goals can be instantiated incrementally.  But Isabelle is not a resolution

    34 theorem prover like Otter.  Isabelle's clauses are drawn from a richer,

    35 higher-order language and a fully automatic search would be impractical.

    36 Isabelle does not join clauses automatically, but under strict user

    37 control.  You can conduct single-step proofs, use Isabelle's built-in proof

    38 procedures, or develop new proof procedures using tactics and tacticals.

    39

    40 Isabelle's meta-logic is higher-order, based on the typed

    41 $\lambda$-calculus.  So resolution cannot use ordinary unification, but

    42 higher-order unification~\cite{huet75}.  This complicated procedure gives

    43 Isabelle strong support for many logical formalisms involving variable

    44 binding.

    45

    46 The diagram below illustrates some of the logics distributed with Isabelle.

    47 These include first-order logic (intuitionistic and classical), the sequent

    48 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},

    49 a version of Constructive Type Theory~\cite{nordstrom90}, several modal

    50 logics, and a Logic for Computable Functions.  Several experimental

    51 logics are also available, such a term assignment calculus for linear

    52 logic.

    53

    54 \centerline{\epsfbox{Isa-logics.eps}}

    55

    56

    57 \section*{How to read this book}

    58 Isabelle is a large system, but beginners can get by with a few commands

    59 and a basic knowledge of how Isabelle works.  Some knowledge of

    60 Standard~\ML{} is essential because \ML{} is Isabelle's user interface.

    61 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly

    62 with Isabelle's sources at hand.  My book on~\ML{}~\cite{paulson91} covers

    63 much material connected with Isabelle, including a simple theorem prover.

    64

    65 The Isabelle documentation is divided into three parts, which serve

    66 distinct purposes:

    67 \begin{itemize}

    68 \item {\em Introduction to Isabelle\/} describes the basic features of

    69   Isabelle.  This part is intended to be read through.  If you are

    70   impatient to get started, you might skip the first chapter, which

    71   describes Isabelle's meta-logic in some detail.  The other chapters

    72   present on-line sessions of increasing difficulty.  It also explains how

    73   to derive rules define theories, and concludes with an extended example:

    74   a Prolog interpreter.

    75

    76 \item {\em The Isabelle Reference Manual\/} contains information about most

    77   of the facilities of Isabelle, apart from particular object-logics.  This

    78   part would make boring reading, though browsing might be useful.  Mostly

    79   you should use it to locate facts quickly.

    80

    81 \item {\em Isabelle's Object-Logics\/} describes the various logics

    82   distributed with Isabelle.  Its final chapter explains how to define new

    83   logics.  The other chapters are intended for reference only.

    84 \end{itemize}

    85 This book should not be read from start to finish.  Instead you might read

    86 a couple of chapters from {\em Introduction to Isabelle}, then try some

    87 examples referring to the other parts, return to the {\em Introduction},

    88 and so forth.  Starred sections discuss obscure matters and may be skipped

    89 on a first reading.

    90

    91

    92

    93 \section*{Releases of Isabelle}\index{Isabelle!release history}

    94 Isabelle was first distributed in 1986.  The 1987 version introduced a

    95 higher-order meta-logic with an improved treatment of quantifiers.  The

    96 1988 version added limited polymorphism and support for natural deduction.

    97 The 1989 version included a parser and pretty printer generator.  The 1992

    98 version introduced type classes, to support many-sorted and higher-order

    99 logics.  The 1993 version provides greater support for theories and is

   100 much faster.

   101

   102 Isabelle is still under development.  Projects under consideration include

   103 better support for inductive definitions, some means of recording proofs, a

   104 graphical user interface, and developments in the standard object-logics.

   105 I hope but cannot promise to maintain upwards compatibility.

   106

   107 Isabelle is available by anonymous ftp:

   108 \begin{itemize}

   109 \item University of Cambridge\\

   110         host {\tt ftp.cl.cam.ac.uk}\\

   111         directory {\tt ml}

   112

   113 \item Technical University of Munich\\

   114         host {\tt ftp.informatik.tu-muenchen.de}\\

   115         directory {\tt local/lehrstuhl/nipkow}

   116 \end{itemize}

   117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}.  Please report any

   118 errors you find in this book and your problems or successes with Isabelle.

   119

   120

   121 \subsection*{Acknowledgements}

   122 Tobias Nipkow has made immense contributions to Isabelle, including the

   123 parser generator, type classes, the simplifier, and several object-logics.

   124 He also arranged for several of his students to help.  Carsten Clasohm

   125 implemented the theory database; Markus Wenzel implemented macros; Sonia

   126 Mahjoub and Karin Nimmermann also contributed.

   127

   128 Nipkow and his students wrote much of the documentation underlying this

   129 book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},

   130 Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of

   131 Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}.  Carsten Clasohm

   132 contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed to

   133 Chap.\ts\ref{Defining-Logics}.

   134

   135 David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and

   136 Markus Wenzel suggested changes and corrections to the documentation.

   137

   138 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped

   139 to develop Isabelle's standard object-logics.  David Aspinall performed

   140 some useful research into theories and implemented an Isabelle Emacs mode.

   141 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,

   142 Poly/{\sc ml}.

   143

   144 The research has been funded by numerous SERC grants dating from the Alvey

   145 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects

   146 3245: Logical Frameworks and 6453: Types).

   147

   148

   149 \index{ML}