author paulson Fri, 22 Nov 1996 17:44:05 +0100 changeset 2219 5687d7dec139 parent 2218 36bb751913c6 child 2220 547d2b58307e
Minor textual improvements; updating of a reference
 doc-src/ind-defs.tex file | annotate | diff | comparison | revisions
--- a/doc-src/ind-defs.tex	Fri Nov 22 17:41:32 1996 +0100
+++ b/doc-src/ind-defs.tex	Fri Nov 22 17:44:05 1996 +0100
@@ -136,7 +136,7 @@
Such data structures are called \defn{datatypes}
below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
Some logics take datatypes as primitive; consider Boyer and Moore's shell
-principle~\cite{bm79} and the Coq type theory~\cite{paulin92}.
+principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.

A datatype is but one example of an \defn{inductive definition}.  This
specifies the least set closed under given rules~\cite{aczel77}.  The
@@ -144,7 +144,7 @@
operational semantics~\cite{hennessy90} is an inductive definition of a
reduction or evaluation relation on programs.  A few theorem provers
provide commands for formalizing inductive definitions; these include
-Coq~\cite{paulin92} and again the \textsc{hol} system~\cite{camilleri92}.
+Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}.

The dual notion is that of a \defn{coinductive definition}.  This specifies
the greatest set closed under given rules.  Important examples include
@@ -246,7 +246,7 @@
\ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
parameters must be identical every time they occur within a definition.  This
would appear to be a serious restriction compared with other systems such as
-Coq~\cite{paulin92}.  For instance, we cannot define the lists of
+Coq~\cite{paulin-tlca}.  For instance, we cannot define the lists of
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
varies.  Section~\ref{listn-sec} describes how to express this set using the
inductive definition package.
@@ -549,7 +549,7 @@

\subsection{Lists of $n$ elements}\label{listn-sec}
This has become a standard example of an inductive definition.  Following
-Paulin-Mohring~\cite{paulin92}, we could attempt to define a new datatype
+Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
But her introduction rules
$\hbox{\tt Niln}\in\listn(A,0) \qquad @@ -735,7 +735,7 @@ all \prec-predecessors of~a, for a\in D. Thus we need an introduction rule of the form \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)}$
-Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
+Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
difficulties for other systems.  Its premise is not acceptable to the
inductive definition package of the Cambridge \textsc{hol}
system~\cite{camilleri92}.  It is also unacceptable to the Isabelle package
@@ -1212,7 +1212,7 @@
\textsc{alf} requires new rules for each definition~\cite{dybjer91}.  With Coq
the situation is subtler still; its underlying Calculus of Constructions can
express inductive definitions~\cite{huet88}, but cannot quite handle datatype
-definitions~\cite{paulin92}.  It seems that researchers tried hard to
+definitions~\cite{paulin-tlca}.  It seems that researchers tried hard to
circumvent these problems before finally extending the Calculus with rule
schemes for strictly positive operators.  Recently Gim{\'e}nez has extended
the Calculus of Constructions with inductive and coinductive
@@ -1414,7 +1414,7 @@
type_intrs {\it introduction rules for type-checking}
type_elims {\it elimination rules for type-checking}
\end{ttbox}
-A coinductive definition is identical save that it starts with the keyword
+A coinductive definition is identical, but starts with the keyword
{\tt coinductive}.

The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
@@ -1549,8 +1549,8 @@
$\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.

These choices should work for all finitely-branching (co)datatype
-  definitions.  For examples of infinitely-branching datatype
-  definitions, see the file {\tt ZF/ex/Brouwer.thy}.
+  definitions.  For examples of infinitely-branching datatypes,
+  see file {\tt ZF/ex/Brouwer.thy}.

\item[\it datatype declaration] has the form
\begin{quote}