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}