# HG changeset patch # User paulson # Date 848681045 -3600 # Node ID 5687d7dec139bb8409f8c8f3a648f4d5e26b9a9a # Parent 36bb751913c6bf808ec3f32e30e97388b0353081 Minor textual improvements; updating of a reference diff -r 36bb751913c6 -r 5687d7dec139 doc-src/ind-defs.tex --- 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}