author | lcp |

Mon Mar 21 10:51:28 1994 +0100 (1994-03-21) | |

changeset 285 | fd4a6585e5bf |

parent 284 | 1072b18b2caa |

child 286 | e7efbf03562b |

first draft of Springer book

doc-src/Ref/theory-syntax.tex | file | annotate | diff | revisions | |

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

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

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/doc-src/Ref/theory-syntax.tex Mon Mar 21 10:51:28 1994 +0100 1.3 @@ -0,0 +1,83 @@ 1.4 +%% $Id$ 1.5 + 1.6 +\appendix 1.7 +\newlinechar=-1 %mathsing.sty sets \newlinechar=`\|, which would cause mayhem 1.8 + 1.9 +\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax} 1.10 +\begin{itemize} 1.11 +\item {\tt Typewriter font} denotes terminal symbols. 1.12 +\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of 1.13 + identifiers, type identifiers, natural numbers, \ML\ strings (with their 1.14 + quotation marks) and arbitrary \ML\ text. The first three are fully defined 1.15 + in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}. 1.16 +\end{itemize} 1.17 + 1.18 +\begin{rail} 1.19 + 1.20 +theoryDef : id '=' (name + '+') ('+' extension | ()); 1.21 + 1.22 +name: id | string; 1.23 + 1.24 +extension : classes default types arities consts trans rules 'end' ml 1.25 + ; 1.26 + 1.27 +classes : () 1.28 + | 'classes' ( ( id ( () 1.29 + | '<' (id + ',') 1.30 + ) 1.31 + ) + ) 1.32 + ; 1.33 + 1.34 +default : () 1.35 + | 'default' sort 1.36 + ; 1.37 + 1.38 +sort : id 1.39 + | '\{' (id * ',') '\}' 1.40 + ; 1.41 + 1.42 +types : () 1.43 + | 'types' ( ( type ( () | '(' infix ')' ) ) + ) 1.44 + ; 1.45 + 1.46 +type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string ); 1.47 + 1.48 +infix : ( 'infixr' | 'infixl' ) nat; 1.49 + 1.50 + 1.51 +arities : () 1.52 + | 'arities' ((( name + ',' ) '::' arity ) + ) 1.53 + ; 1.54 + 1.55 +arity : ( () 1.56 + | '(' (sort + ',') ')' 1.57 + ) id 1.58 + ; 1.59 + 1.60 + 1.61 +consts : () 1.62 + | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) 1.63 + ; 1.64 + 1.65 +constDecl : ( name + ',') '::' string ; 1.66 + 1.67 + 1.68 +mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) 1.69 + | infix 1.70 + | 'binder' string nat ; 1.71 + 1.72 +trans : () 1.73 + | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) 1.74 + ; 1.75 + 1.76 +pat : ( () | ( '(' id ')' ) ) string; 1.77 + 1.78 +rules : () 1.79 + | 'rules' (( id string ) + ) 1.80 + ; 1.81 + 1.82 +ml : () 1.83 + | 'ML' text 1.84 + ; 1.85 + 1.86 +\end{rail}

2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 2.2 +++ b/doc-src/preface.tex Mon Mar 21 10:51:28 1994 +0100 2.3 @@ -0,0 +1,149 @@ 2.4 +\chapter*{Preface} 2.5 +\markboth{Preface}{Preface} %or Preface ? 2.6 +\addcontentsline{toc}{chapter}{Preface} 2.7 + 2.8 +\index{Isabelle!object-logics supported} 2.9 + 2.10 +Most theorem provers support a fixed logic, such as first-order or 2.11 +equational logic. They bring sophisticated proof procedures to bear upon 2.12 +the conjectured formula. An impressive example is the resolution prover 2.13 +Otter, which Quaife~\cite{quaife-book} has used to formalize a body of 2.14 +mathematics. 2.15 + 2.16 +ALF~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each support a 2.17 +fixed logic too, but one far removed from first-order logic. They are 2.18 +explicitly concerned with computation. A diverse collection of logics --- 2.19 +type theories, process calculi, $\lambda$-calculi --- may be found in the 2.20 +Computer Science literature. Such logics require proof support. Few proof 2.21 +procedures exist, but the theorem prover can at least check that each 2.22 +inference is valid. 2.23 + 2.24 +A {\bf generic} theorem prover is one that can support many different 2.25 +logics. Most of these \cite{dawson90,mural,sawamura92} work by 2.26 +implementing a syntactic framework that can express the features of typical 2.27 +inference rules. Isabelle's distinctive feature is its representation of 2.28 +logics using a meta-logic. This meta-logic is just a fragment of 2.29 +higher-order logic; known proof theory may be used to demonstrate that the 2.30 +representation is correct~\cite{paulson89}. The representation has much in 2.31 +common with the Edinburgh Logical Framework~\cite{harper-jacm} and with 2.32 +Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics. 2.33 + 2.34 +An inference rule in Isabelle is a generalized Horn clause. Rules are 2.35 +joined to make proofs by resolving such clauses. Logical variables in 2.36 +goals can be instantiated incrementally. But Isabelle is not a resolution 2.37 +theorem prover like Otter. Isabelle's clauses are drawn from a richer, 2.38 +higher-order language and a fully automatic search would be impractical. 2.39 +Isabelle does not join clauses automatically, but under strict user 2.40 +control. You can conduct single-step proofs, use Isabelle's built-in proof 2.41 +procedures, or develop new proof procedures using tactics and tacticals. 2.42 + 2.43 +Isabelle's meta-logic is higher-order, based on the typed 2.44 +$\lambda$-calculus. So resolution cannot use ordinary unification, but 2.45 +higher-order unification~\cite{huet75}. This complicated procedure gives 2.46 +Isabelle strong support for many logical formalisms involving variable 2.47 +binding. 2.48 + 2.49 +The diagram below illustrates some of the logics distributed with Isabelle. 2.50 +These include first-order logic (intuitionistic and classical), the sequent 2.51 +calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, 2.52 +a version of Constructive Type Theory~\cite{nordstrom90}, several modal 2.53 +logics, and a Logic for Computable Functions. Several experimental 2.54 +logics are also available, such a term assignment calculus for linear 2.55 +logic. 2.56 + 2.57 +\centerline{\epsfbox{Isa-logics.eps}} 2.58 + 2.59 + 2.60 +\section*{How to read this book} 2.61 +Isabelle is a large system, but beginners can get by with a few commands 2.62 +and a basic knowledge of how Isabelle works. Some knowledge of 2.63 +Standard~\ML{} is essential because \ML{} is Isabelle's user interface. 2.64 +Advanced Isabelle theorem proving can involve writing \ML{} code, possibly 2.65 +with Isabelle's sources at hand. My book on~\ML{}~\cite{paulson91} covers 2.66 +much material connected with Isabelle, including a simple theorem prover. 2.67 + 2.68 +The Isabelle documentation is divided into three parts, which serve 2.69 +distinct purposes: 2.70 +\begin{itemize} 2.71 +\item {\em Introduction to Isabelle\/} describes the basic features of 2.72 + Isabelle. This part is intended to be read through. If you are 2.73 + impatient to get started, you might skip the first chapter, which 2.74 + describes Isabelle's meta-logic in some detail. The other chapters 2.75 + present on-line sessions of increasing difficulty. It also explains how 2.76 + to derive rules define theories, and concludes with an extended example: 2.77 + a Prolog interpreter. 2.78 + 2.79 +\item {\em The Isabelle Reference Manual\/} contains information about most 2.80 + of the facilities of Isabelle, apart from particular object-logics. This 2.81 + part would make boring reading, though browsing might be useful. Mostly 2.82 + you should use it to locate facts quickly. 2.83 + 2.84 +\item {\em Isabelle's Object-Logics\/} describes the various logics 2.85 + distributed with Isabelle. Its final chapter explains how to define new 2.86 + logics. The other chapters are intended for reference only. 2.87 +\end{itemize} 2.88 +This book should not be read from start to finish. Instead you might read 2.89 +a couple of chapters from {\em Introduction to Isabelle}, then try some 2.90 +examples referring to the other parts, return to the {\em Introduction}, 2.91 +and so forth. Starred sections discuss obscure matters and may be skipped 2.92 +on a first reading. 2.93 + 2.94 + 2.95 + 2.96 +\section*{Releases of Isabelle}\index{Isabelle!release history} 2.97 +Isabelle was first distributed in 1986. The 1987 version introduced a 2.98 +higher-order meta-logic with an improved treatment of quantifiers. The 2.99 +1988 version added limited polymorphism and support for natural deduction. 2.100 +The 1989 version included a parser and pretty printer generator. The 1992 2.101 +version introduced type classes, to support many-sorted and higher-order 2.102 +logics. The 1993 version provides greater support for theories and is 2.103 +much faster. 2.104 + 2.105 +Isabelle is still under development. Projects under consideration include 2.106 +better support for inductive definitions, some means of recording proofs, a 2.107 +graphical user interface, and developments in the standard object-logics. 2.108 +I hope but cannot promise to maintain upwards compatibility. 2.109 + 2.110 +Isabelle is available by anonymous ftp: 2.111 +\begin{itemize} 2.112 +\item University of Cambridge\\ 2.113 + host {\tt ftp.cl.cam.ac.uk}\\ 2.114 + directory {\tt ml} 2.115 + 2.116 +\item Technical University of Munich\\ 2.117 + host {\tt ftp.informatik.tu-muenchen.de}\\ 2.118 + directory {\tt local/lehrstuhl/nipkow} 2.119 +\end{itemize} 2.120 +My electronic mail address is {\tt lcp\at cl.cam.ac.uk}. Please report any 2.121 +errors you find in this book and your problems or successes with Isabelle. 2.122 + 2.123 + 2.124 +\subsection*{Acknowledgements} 2.125 +Tobias Nipkow has made immense contributions to Isabelle, including the 2.126 +parser generator, type classes, the simplifier, and several object-logics. 2.127 +He also arranged for several of his students to help. Carsten Clasohm 2.128 +implemented the theory database; Markus Wenzel implemented macros; Sonia 2.129 +Mahjoub and Karin Nimmermann also contributed. 2.130 + 2.131 +Nipkow and his students wrote much of the documentation underlying this 2.132 +book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, 2.133 +Chap.\ts\ref{simp-chap}, Chap.\ts\ref{Defining-Logics} and part of 2.134 +Chap.\ts\ref{theories}, and App.\ts\ref{app:TheorySyntax}. Carsten Clasohm 2.135 +contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed to 2.136 +Chap.\ts\ref{Defining-Logics}. 2.137 + 2.138 +David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert Voelker and 2.139 +Markus Wenzel suggested changes and corrections to the documentation. 2.140 + 2.141 +Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped 2.142 +to develop Isabelle's standard object-logics. David Aspinall performed 2.143 +some useful research into theories and implemented an Isabelle Emacs mode. 2.144 +Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler, 2.145 +Poly/{\sc ml}. 2.146 + 2.147 +The research has been funded by numerous SERC grants dating from the Alvey 2.148 +programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects 2.149 +3245: Logical Frameworks and 6453: Types). 2.150 + 2.151 + 2.152 +\index{ML}

3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 3.2 +++ b/doc-src/springer.tex Mon Mar 21 10:51:28 1994 +0100 3.3 @@ -0,0 +1,96 @@ 3.4 +\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} 3.5 +%%%\includeonly{preface} 3.6 +%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} 3.7 +%% run sedindex springer to prepare index file 3.8 + 3.9 +\sloppy%%%???????????????????????????????????????????????????????????????? 3.10 + 3.11 +\title{Isabelle\\A Generic Theorem Prover} 3.12 +\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} 3.13 + 3.14 +\date{} 3.15 +\makeindex 3.16 +\let\idx=\ttindexbold 3.17 +\def\S{Sect.\thinspace}%This is how Springer like it 3.18 + 3.19 +\underscoreoff 3.20 + 3.21 +\setcounter{secnumdepth}{1} \setcounter{tocdepth}{1} 3.22 + 3.23 +\binperiod %%%treat . like a binary operator 3.24 + 3.25 +\begin{document} 3.26 +\maketitle 3.27 + 3.28 +\pagenumbering{Roman} 3.29 +\include{preface} 3.30 + 3.31 +\tableofcontents 3.32 +\newpage 3.33 + 3.34 +\pagenumbering{arabic} 3.35 + 3.36 +\markboth{}{} 3.37 +\newfont{\sanssi}{cmssi12} 3.38 +\vspace*{2.5cm} 3.39 +\begin{quote} 3.40 +\raggedleft 3.41 +{\sanssi 3.42 +You can only find truth with logic\\ 3.43 +if you have already found truth without it.}\\ 3.44 +\bigskip 3.45 + 3.46 +G.K. Chesterton, {\em The Man who was Orthodox} 3.47 +\end{quote} 3.48 + 3.49 + 3.50 +\index{definitions|see{rewriting, meta-level}} 3.51 +\index{rewriting!object-level|see{simplification}} 3.52 +\index{rules!meta-level|see{meta-rules}} 3.53 +\index{scheme variables|see{unknowns}} 3.54 +\index{AST|see{trees, abstract syntax}} 3.55 + 3.56 +\part{Introduction to Isabelle} 3.57 + 3.58 +\begingroup 3.59 +\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification 3.60 +\newcommand{\nand}{\mathbin{\lnot\&}} 3.61 +\newcommand{\xor}{\mathbin{\#}} 3.62 +\let\part=\chapter 3.63 +\include{Intro/foundations} 3.64 +\include{Intro/getting} 3.65 +\include{Intro/advanced} 3.66 +\endgroup 3.67 + 3.68 +\part{The Isabelle Reference Manual} 3.69 +\include{Ref/introduction} 3.70 +\include{Ref/goals} 3.71 +\include{Ref/tactic} 3.72 +\include{Ref/tctical} 3.73 +\include{Ref/thm} 3.74 +\include{Ref/theories} 3.75 +\include{Ref/substitution} 3.76 +\include{Ref/simplifier} 3.77 +\include{Ref/classical} 3.78 + 3.79 +\part{Isabelle's Object-Logics} 3.80 +\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip 3.81 + \hrule\bigskip} 3.82 +\include{Logics/intro} 3.83 +\include{Logics/FOL} 3.84 +\include{Logics/ZF} 3.85 +\include{Logics/HOL} 3.86 +\include{Logics/LK} 3.87 +\include{Logics/CTT} 3.88 +\include{Logics/defining} 3.89 + 3.90 +\include{Ref/theory-syntax} 3.91 + 3.92 +%%seealso's must be last so that they appear last in the index entries 3.93 +\index{rewriting!meta-level|seealso{tactics, theorems}} 3.94 + 3.95 +\bibliographystyle{springer} \small\raggedright\frenchspacing 3.96 +\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory} 3.97 + 3.98 +\input{springer.ind} 3.99 +\end{document}