author | lcp |

Thu Mar 24 18:14:45 1994 +0100 (1994-03-24) | |

changeset 304 | 5edc4f5e5ebd |

parent 303 | 0746399cfd44 |

child 305 | 4c2bbb5de471 |

revisions to first Springer draft

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

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

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}