summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Thu, 24 Mar 1994 18:14:45 +0100 | |

changeset 304 | 5edc4f5e5ebd |

parent 303 | 0746399cfd44 |

child 305 | 4c2bbb5de471 |

revisions to first Springer draft

doc-src/preface.tex | file | annotate | diff | comparison | revisions | |

doc-src/springer.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/preface.tex Thu Mar 24 18:00:11 1994 +0100 +++ b/doc-src/preface.tex Thu Mar 24 18:14:45 1994 +0100 @@ -6,36 +6,34 @@ Most theorem provers support a fixed logic, such as first-order or equational logic. They bring sophisticated proof procedures to bear upon -the conjectured formula. An impressive example is the resolution prover -Otter, which Quaife~\cite{quaife-book} has used to formalize a body of -mathematics. +the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is +an impressive example. ALF~\cite{alf}, Coq~\cite{coq} and +Nuprl~\cite{constable86} each support a fixed logic too, but one far +removed from first-order logic. They are explicitly concerned with +computation. A diverse collection of logics --- type theories, process +calculi, $\lambda$-calculi --- may be found in the Computer Science +literature. Such logics require proof support. Few proof procedures are +known for them, but the theorem prover can at least automate routine steps. -ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a -fixed logic too, but one far removed from first-order logic. They are -explicitly concerned with computation. A diverse collection of logics --- -type theories, process calculi, $\lambda$-calculi --- may be found in the -Computer Science literature. Such logics require proof support. Few proof -procedures exist, but the theorem prover can at least check that each -inference is valid. - -A {\bf generic} theorem prover is one that can support many different -logics. Most of these \cite{dawson90,mural,sawamura92} work by -implementing a syntactic framework that can express the features of typical -inference rules. Isabelle's distinctive feature is its representation of -logics using a meta-logic. This meta-logic is just a fragment of -higher-order logic; known proof theory may be used to demonstrate that the -representation is correct~\cite{paulson89}. The representation has much in -common with the Edinburgh Logical Framework~\cite{harper-jacm} and with +A {\bf generic} theorem prover is one that can support a variety of logics. +Some generic provers are noteworthy for their user interfaces +\cite{dawson90,mural,sawamura92}. Most of them work by implementing a +syntactic framework that can express typical inference rules. Isabelle's +distinctive feature is its representation of logics within a fragment of +higher-order logic, called the meta-logic. The proof theory of +higher-order logic may be used to demonstrate that the representation is +correct~\cite{paulson89}. The approach has much in common with the +Edinburgh Logical Framework~\cite{harper-jacm} and with Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. An inference rule in Isabelle is a generalized Horn clause. Rules are joined to make proofs by resolving such clauses. Logical variables in goals can be instantiated incrementally. But Isabelle is not a resolution -theorem prover like Otter. Isabelle's clauses are drawn from a richer, -higher-order language and a fully automatic search would be impractical. -Isabelle does not join clauses automatically, but under strict user -control. You can conduct single-step proofs, use Isabelle's built-in proof -procedures, or develop new proof procedures using tactics and tacticals. +theorem prover like Otter. Isabelle's clauses are drawn from a richer +language and a fully automatic search would be impractical. Isabelle does +not resolve clauses automatically, but under user direction. You can +conduct single-step proofs, use Isabelle's built-in proof procedures, or +develop new proof procedures using tactics and tacticals. Isabelle's meta-logic is higher-order, based on the typed $\lambda$-calculus. So resolution cannot use ordinary unification, but @@ -55,7 +53,7 @@ \section*{How to read this book} -Isabelle is a large system, but beginners can get by with a few commands +Isabelle is a complex system, but beginners can get by with a few commands and a basic knowledge of how Isabelle works. Some knowledge of Standard~\ML{} is essential because \ML{} is Isabelle's user interface. Advanced Isabelle theorem proving can involve writing \ML{} code, possibly @@ -73,10 +71,10 @@ to derive rules define theories, and concludes with an extended example: a Prolog interpreter. -\item {\em The Isabelle Reference Manual\/} contains information about most - of the facilities of Isabelle, apart from particular object-logics. This - part would make boring reading, though browsing might be useful. Mostly - you should use it to locate facts quickly. +\item {\em The Isabelle Reference Manual\/} provides detailed information + about Isabelle's facilities, excluding the object-logics. This part + would make boring reading, though browsing might be useful. Mostly you + should use it to locate facts quickly. \item {\em Isabelle's Object-Logics\/} describes the various logics distributed with Isabelle. Its final chapter explains how to define new @@ -118,7 +116,7 @@ errors you find in this book and your problems or successes with Isabelle. -\subsection*{Acknowledgements} +\section*{Acknowledgements} Tobias Nipkow has made immense contributions to Isabelle, including the parser generator, type classes, the simplifier, and several object-logics. He also arranged for several of his students to help. Carsten Clasohm @@ -127,12 +125,12 @@ Nipkow and his students wrote much of the documentation underlying this book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, -Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of -Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm -contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to -Chap.\ts\ref{Defining-Logics}. +\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{simp-chap}, +Chap.\ts\ref{Defining-Logics} and App.\ts\ref{app:TheorySyntax}\@. Carsten +Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed +to Chap.\ts\ref{Defining-Logics}. -David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and +David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and Markus Wenzel suggested changes and corrections to the documentation. Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped

--- a/doc-src/springer.tex Thu Mar 24 18:00:11 1994 +0100 +++ b/doc-src/springer.tex Thu Mar 24 18:14:45 1994 +0100 @@ -1,9 +1,10 @@ +%% $ lcp Exp $ \documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} -%%%\includeonly{preface} +%%%\includeonly{Ref/tctical,Ref/thm} %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} %% run sedindex springer to prepare index file -\sloppy%%%???????????????????????????????????????????????????????????????? +\sloppy \title{Isabelle\\A Generic Theorem Prover} \author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} @@ -15,7 +16,7 @@ \underscoreoff -\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1} +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1} \binperiod %%%treat . like a binary operator @@ -44,10 +45,11 @@ \end{quote} +\index{type classes|see{classes}} \index{definitions|see{rewriting, meta-level}} \index{rewriting!object-level|see{simplification}} \index{rules!meta-level|see{meta-rules}} -\index{scheme variables|see{unknowns}} +\index{variables!schematic|see{unknowns}} \index{AST|see{trees, abstract syntax}} \part{Introduction to Isabelle}