revisions to first Springer draft
authorlcp
Thu Mar 24 18:14:45 1994 +0100 (1994-03-24)
changeset 3045edc4f5e5ebd
parent 303 0746399cfd44
child 305 4c2bbb5de471
revisions to first Springer draft
doc-src/preface.tex
doc-src/springer.tex
     1.1 --- a/doc-src/preface.tex	Thu Mar 24 18:00:11 1994 +0100
     1.2 +++ b/doc-src/preface.tex	Thu Mar 24 18:14:45 1994 +0100
     1.3 @@ -6,36 +6,34 @@
     1.4  
     1.5  Most theorem provers support a fixed logic, such as first-order or
     1.6  equational logic.  They bring sophisticated proof procedures to bear upon
     1.7 -the conjectured formula.  An impressive example is the resolution prover
     1.8 -Otter, which Quaife~\cite{quaife-book} has used to formalize a body of
     1.9 -mathematics.
    1.10 +the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
    1.11 +an impressive example.  ALF~\cite{alf}, Coq~\cite{coq} and
    1.12 +Nuprl~\cite{constable86} each support a fixed logic too, but one far
    1.13 +removed from first-order logic.  They are explicitly concerned with
    1.14 +computation.  A diverse collection of logics --- type theories, process
    1.15 +calculi, $\lambda$-calculi --- may be found in the Computer Science
    1.16 +literature.  Such logics require proof support.  Few proof procedures are
    1.17 +known for them, but the theorem prover can at least automate routine steps.
    1.18  
    1.19 -ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a
    1.20 -fixed logic too, but one far removed from first-order logic.  They are
    1.21 -explicitly concerned with computation.  A diverse collection of logics ---
    1.22 -type theories, process calculi, $\lambda$-calculi --- may be found in the
    1.23 -Computer Science literature.  Such logics require proof support.  Few proof
    1.24 -procedures exist, but the theorem prover can at least check that each
    1.25 -inference is valid.
    1.26 -
    1.27 -A {\bf generic} theorem prover is one that can support many different
    1.28 -logics.  Most of these \cite{dawson90,mural,sawamura92} work by
    1.29 -implementing a syntactic framework that can express the features of typical
    1.30 -inference rules.  Isabelle's distinctive feature is its representation of
    1.31 -logics using a meta-logic.  This meta-logic is just a fragment of
    1.32 -higher-order logic; known proof theory may be used to demonstrate that the
    1.33 -representation is correct~\cite{paulson89}.  The representation has much in
    1.34 -common with the Edinburgh Logical Framework~\cite{harper-jacm} and with 
    1.35 +A {\bf generic} theorem prover is one that can support a variety of logics.
    1.36 +Some generic provers are noteworthy for their user interfaces
    1.37 +\cite{dawson90,mural,sawamura92}.  Most of them work by implementing a
    1.38 +syntactic framework that can express typical inference rules.  Isabelle's
    1.39 +distinctive feature is its representation of logics within a fragment of
    1.40 +higher-order logic, called the meta-logic.  The proof theory of
    1.41 +higher-order logic may be used to demonstrate that the representation is
    1.42 +correct~\cite{paulson89}.  The approach has much in common with the
    1.43 +Edinburgh Logical Framework~\cite{harper-jacm} and with
    1.44  Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
    1.45  
    1.46  An inference rule in Isabelle is a generalized Horn clause.  Rules are
    1.47  joined to make proofs by resolving such clauses.  Logical variables in
    1.48  goals can be instantiated incrementally.  But Isabelle is not a resolution
    1.49 -theorem prover like Otter.  Isabelle's clauses are drawn from a richer,
    1.50 -higher-order language and a fully automatic search would be impractical.
    1.51 -Isabelle does not join clauses automatically, but under strict user
    1.52 -control.  You can conduct single-step proofs, use Isabelle's built-in proof
    1.53 -procedures, or develop new proof procedures using tactics and tacticals.
    1.54 +theorem prover like Otter.  Isabelle's clauses are drawn from a richer
    1.55 +language and a fully automatic search would be impractical.  Isabelle does
    1.56 +not resolve clauses automatically, but under user direction.  You can
    1.57 +conduct single-step proofs, use Isabelle's built-in proof procedures, or
    1.58 +develop new proof procedures using tactics and tacticals.
    1.59  
    1.60  Isabelle's meta-logic is higher-order, based on the typed
    1.61  $\lambda$-calculus.  So resolution cannot use ordinary unification, but
    1.62 @@ -55,7 +53,7 @@
    1.63  
    1.64  
    1.65  \section*{How to read this book}
    1.66 -Isabelle is a large system, but beginners can get by with a few commands
    1.67 +Isabelle is a complex system, but beginners can get by with a few commands
    1.68  and a basic knowledge of how Isabelle works.  Some knowledge of
    1.69  Standard~\ML{} is essential because \ML{} is Isabelle's user interface.
    1.70  Advanced Isabelle theorem proving can involve writing \ML{} code, possibly
    1.71 @@ -73,10 +71,10 @@
    1.72    to derive rules define theories, and concludes with an extended example:
    1.73    a Prolog interpreter.
    1.74  
    1.75 -\item {\em The Isabelle Reference Manual\/} contains information about most
    1.76 -  of the facilities of Isabelle, apart from particular object-logics.  This
    1.77 -  part would make boring reading, though browsing might be useful.  Mostly
    1.78 -  you should use it to locate facts quickly.
    1.79 +\item {\em The Isabelle Reference Manual\/} provides detailed information
    1.80 +  about Isabelle's facilities, excluding the object-logics.  This part
    1.81 +  would make boring reading, though browsing might be useful.  Mostly you
    1.82 +  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 @@ -118,7 +116,7 @@
    1.87  errors you find in this book and your problems or successes with Isabelle.
    1.88  
    1.89  
    1.90 -\subsection*{Acknowledgements} 
    1.91 +\section*{Acknowledgements} 
    1.92  Tobias Nipkow has made immense contributions to Isabelle, including the
    1.93  parser generator, type classes, the simplifier, and several object-logics.
    1.94  He also arranged for several of his students to help.  Carsten Clasohm
    1.95 @@ -127,12 +125,12 @@
    1.96  
    1.97  Nipkow and his students wrote much of the documentation underlying this
    1.98  book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},
    1.99 -Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of
   1.100 -Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}.  Carsten Clasohm
   1.101 -contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed to
   1.102 -Chap.\ts\ref{Defining-Logics}.
   1.103 +\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{simp-chap},
   1.104 +Chap.\ts\ref{Defining-Logics} and App.\ts\ref{app:TheorySyntax}\@.  Carsten
   1.105 +Clasohm contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed
   1.106 +to Chap.\ts\ref{Defining-Logics}.
   1.107  
   1.108 -David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and
   1.109 +David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and
   1.110  Markus Wenzel suggested changes and corrections to the documentation.
   1.111  
   1.112  Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
     2.1 --- a/doc-src/springer.tex	Thu Mar 24 18:00:11 1994 +0100
     2.2 +++ b/doc-src/springer.tex	Thu Mar 24 18:14:45 1994 +0100
     2.3 @@ -1,9 +1,10 @@
     2.4 +%% $ lcp Exp $
     2.5  \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
     2.6 -%%%\includeonly{preface}
     2.7 +%%%\includeonly{Ref/tctical,Ref/thm}
     2.8  %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     2.9  %% run    sedindex springer    to prepare index file
    2.10  
    2.11 -\sloppy%%%????????????????????????????????????????????????????????????????
    2.12 +\sloppy
    2.13  
    2.14  \title{Isabelle\\A Generic Theorem Prover}
    2.15  \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}
    2.16 @@ -15,7 +16,7 @@
    2.17  
    2.18  \underscoreoff
    2.19  
    2.20 -\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1}
    2.21 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}
    2.22  
    2.23  \binperiod     %%%treat . like a binary operator
    2.24  
    2.25 @@ -44,10 +45,11 @@
    2.26  \end{quote}
    2.27  
    2.28  
    2.29 +\index{type classes|see{classes}}
    2.30  \index{definitions|see{rewriting, meta-level}}
    2.31  \index{rewriting!object-level|see{simplification}}
    2.32  \index{rules!meta-level|see{meta-rules}}
    2.33 -\index{scheme variables|see{unknowns}}
    2.34 +\index{variables!schematic|see{unknowns}} 
    2.35  \index{AST|see{trees, abstract syntax}}
    2.36  
    2.37  \part{Introduction to Isabelle}