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