Many edits suggested by Grundy & Thompson
authorlcp
Fri Nov 19 11:31:10 1993 +0100 (1993-11-19)
changeset 130c035b6b9eafc
parent 129 dc50a4b96d7b
child 131 bb0caac13eff
Many edits suggested by Grundy & Thompson
doc-src/ind-defs.tex
     1.1 --- a/doc-src/ind-defs.tex	Fri Nov 19 11:25:36 1993 +0100
     1.2 +++ b/doc-src/ind-defs.tex	Fri Nov 19 11:31:10 1993 +0100
     1.3 @@ -1,9 +1,11 @@
     1.4 -\documentstyle[11pt,a4,proof,lcp,alltt,amssymbols,draft]{article}
     1.5 +\documentstyle[12pt,a4,proof,lcp,alltt,amssymbols]{article}
     1.6 +%CADE version should use 11pt and the Springer style
     1.7  \newif\ifCADE
     1.8  \CADEfalse
     1.9  
    1.10 -\title{A Fixedpoint Approach to Implementing (Co-)Inductive Definitions\\
    1.11 -  DRAFT\thanks{Research funded by the SERC (grants GR/G53279,
    1.12 +\title{A Fixedpoint Approach to Implementing (Co)Inductive
    1.13 +   Definitions\thanks{Jim Grundy and Simon Thompson made detailed comments on
    1.14 +   a draft.  Research funded by the SERC (grants GR/G53279,
    1.15      GR/H40570) and by the ESPRIT Basic Research Action 6453 `Types'.}}
    1.16  
    1.17  \author{{\em Lawrence C. Paulson}\\ 
    1.18 @@ -108,21 +110,22 @@
    1.19    approach, based on fixedpoint definitions.  It is unusually general:
    1.20    it admits all monotone inductive definitions.  It is conceptually simple,
    1.21    which has allowed the easy implementation of mutual recursion and other
    1.22 -  conveniences.  It also handles co-inductive definitions: simply replace
    1.23 +  conveniences.  It also handles coinductive definitions: simply replace
    1.24    the least fixedpoint by a greatest fixedpoint.  This represents the first
    1.25 -  automated support for co-inductive definitions.
    1.26 +  automated support for coinductive definitions.
    1.27 +
    1.28 +  The method has been implemented in Isabelle's formalization of ZF set
    1.29 +  theory.  It should
    1.30 +  be applicable to any logic in which the Knaster-Tarski Theorem can be
    1.31 +  proved.  The paper briefly describes a method of formalizing
    1.32 +  non-well-founded data structures in standard ZF set theory.
    1.33  
    1.34    Examples include lists of $n$ elements, the accessible part of a relation
    1.35    and the set of primitive recursive functions.  One example of a
    1.36 -  co-inductive definition is bisimulations for lazy lists.  \ifCADE\else
    1.37 +  coinductive definition is bisimulations for lazy lists.  \ifCADE\else
    1.38    Recursive datatypes are examined in detail, as well as one example of a
    1.39 -  ``co-datatype'': lazy lists.  The appendices are simple user's manuals
    1.40 +  {\bf codatatype}: lazy lists.  The appendices are simple user's manuals
    1.41    for this Isabelle/ZF package.\fi
    1.42 -
    1.43 -  The method has been implemented in Isabelle's ZF set theory.  It should
    1.44 -  be applicable to any logic in which the Knaster-Tarski Theorem can be
    1.45 -  proved.  The paper briefly describes a method of formalizing
    1.46 -  non-well-founded data structures in standard ZF set theory.
    1.47  \end{abstract}
    1.48  %
    1.49  \begin{center} Copyright \copyright{} \number\year{} by Lawrence C. Paulson
    1.50 @@ -132,7 +135,7 @@
    1.51  
    1.52  \tableofcontents
    1.53  \cleardoublepage
    1.54 -\pagenumbering{arabic}\pagestyle{headings}\DRAFT
    1.55 +\pagenumbering{arabic}\pagestyle{headings}
    1.56  
    1.57  \section{Introduction}
    1.58  Several theorem provers provide commands for formalizing recursive data
    1.59 @@ -141,7 +144,7 @@
    1.60  system~\cite{melham89}.  Such data structures are called {\bf datatypes}
    1.61  below, by analogy with {\tt datatype} definitions in Standard~ML\@.
    1.62  
    1.63 -A datatype is but one example of a {\bf inductive definition}.  This
    1.64 +A datatype is but one example of an {\bf inductive definition}.  This
    1.65  specifies the least set closed under given rules~\cite{aczel77}.  The
    1.66  collection of theorems in a logic is inductively defined.  A structural
    1.67  operational semantics~\cite{hennessy90} is an inductive definition of a
    1.68 @@ -149,30 +152,30 @@
    1.69  provide commands for formalizing inductive definitions; these include
    1.70  Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}.
    1.71  
    1.72 -The dual notion is that of a {\bf co-inductive definition}.  This specifies
    1.73 +The dual notion is that of a {\bf coinductive definition}.  This specifies
    1.74  the greatest set closed under given rules.  Important examples include
    1.75  using bisimulation relations to formalize equivalence of
    1.76  processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}.
    1.77  Other examples include lazy lists and other infinite data structures; these
    1.78 -are called {\bf co-datatypes} below.
    1.79 +are called {\bf codatatypes} below.
    1.80  
    1.81  Most existing implementations of datatype and inductive definitions accept
    1.82 -an artifically narrow class of inputs, and are not easily extended.  The
    1.83 +an artificially narrow class of inputs, and are not easily extended.  The
    1.84  shell principle and Coq's inductive definition rules are built into the
    1.85  underlying logic.  Melham's packages derive datatypes and inductive
    1.86  definitions from specialized constructions in higher-order logic.
    1.87  
    1.88  This paper describes a package based on a fixedpoint approach.  Least
    1.89  fixedpoints yield inductive definitions; greatest fixedpoints yield
    1.90 -co-inductive definitions.  The package is uniquely powerful:
    1.91 +coinductive definitions.  The package is uniquely powerful:
    1.92  \begin{itemize}
    1.93  \item It accepts the largest natural class of inductive definitions, namely
    1.94 -  all monotone inductive definitions.
    1.95 +  all that are provably monotone.
    1.96  \item It accepts a wide class of datatype definitions.
    1.97 -\item It handles co-inductive and co-datatype definitions.  Most of
    1.98 -  the discussion below applies equally to inductive and co-inductive
    1.99 +\item It handles coinductive and codatatype definitions.  Most of
   1.100 +  the discussion below applies equally to inductive and coinductive
   1.101    definitions, and most of the code is shared.  To my knowledge, this is
   1.102 -  the only package supporting co-inductive definitions.
   1.103 +  the only package supporting coinductive definitions.
   1.104  \item Definitions may be mutually recursive.
   1.105  \end{itemize}
   1.106  The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set
   1.107 @@ -182,7 +185,7 @@
   1.108  transforms these rules into a mapping over sets, and attempts to prove that
   1.109  the mapping is monotonic and well-typed.  If successful, the package
   1.110  makes fixedpoint definitions and proves the introduction, elimination and
   1.111 -(co-)induction rules.  The package consists of several Standard ML
   1.112 +(co)induction rules.  The package consists of several Standard ML
   1.113  functors~\cite{paulson91}; it accepts its argument and returns its result
   1.114  as ML structures.
   1.115  
   1.116 @@ -192,13 +195,13 @@
   1.117  the Isabelle/ZF theory provides well-founded recursion and other logical
   1.118  tools to simplify this task~\cite{paulson-set-II}.
   1.119  
   1.120 -\S2 briefly introduces the least and greatest fixedpoint operators.  \S3
   1.121 -discusses the form of introduction rules, mutual recursion and other points
   1.122 -common to inductive and co-inductive definitions.  \S4 discusses induction
   1.123 -and co-induction rules separately.  \S5 presents several examples,
   1.124 -including a co-inductive definition.  \S6 describes datatype definitions,
   1.125 -while \S7 draws brief conclusions.  \ifCADE\else The appendices are simple
   1.126 -user's manuals for this Isabelle/ZF package.\fi
   1.127 +{\bf Outline.}  \S2 briefly introduces the least and greatest fixedpoint
   1.128 +operators.  \S3 discusses the form of introduction rules, mutual recursion and
   1.129 +other points common to inductive and coinductive definitions.  \S4 discusses
   1.130 +induction and coinduction rules separately.  \S5 presents several examples,
   1.131 +including a coinductive definition.  \S6 describes datatype definitions, while
   1.132 +\S7 draws brief conclusions.  \ifCADE\else The appendices are simple user's
   1.133 +manuals for this Isabelle/ZF package.\fi
   1.134  
   1.135  Most of the definitions and theorems shown below have been generated by the
   1.136  package.  I have renamed some variables to improve readability.
   1.137 @@ -210,7 +213,8 @@
   1.138     \lfp(D,h)  & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
   1.139     \gfp(D,h)  & \equiv & \union\{X\sbs D. X\sbs h(X)\}
   1.140  \end{eqnarray*}   
   1.141 -Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and {\bf monotone} if
   1.142 +Let $D$ be a set.  Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and
   1.143 +{\bf monotone below~$D$} if
   1.144  $h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$.  If $h$ is
   1.145  bounded by~$D$ and monotone then both operators yield fixedpoints:
   1.146  \begin{eqnarray*}
   1.147 @@ -225,17 +229,19 @@
   1.148  This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
   1.149  prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
   1.150  also exhibit a bounding set~$D$ for~$h$.  Sometimes this is trivial, as
   1.151 -when a set of ``theorems'' is (co-)inductively defined over some previously
   1.152 +when a set of ``theorems'' is (co)inductively defined over some previously
   1.153  existing set of ``formulae.''  But defining the bounding set for
   1.154 -(co-)datatype definitions requires some effort; see~\S\ref{data-sec} below.
   1.155 +(co)datatype definitions requires some effort; see~\S\ref{univ-sec} below.
   1.156  
   1.157  
   1.158 -\section{Elements of an inductive or co-inductive definition}\label{basic-sec}
   1.159 -Consider a (co-)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
   1.160 +\section{Elements of an inductive or coinductive definition}\label{basic-sec}
   1.161 +Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
   1.162  mutual recursion.  They will be constructed from previously existing sets
   1.163  $D_1$, \ldots,~$D_n$, respectively, which are called their {\bf domains}. 
   1.164  The construction yields not $R_i\sbs D_i$ but $R_i\sbs D_1+\cdots+D_n$, where
   1.165 -$R_i$ is the image of~$D_i$ under an injection~\cite[\S4.5]{paulson-set-II}.
   1.166 +$R_i$ is contained in the image of~$D_i$ under an
   1.167 +injection.  Reasons for this are discussed
   1.168 +elsewhere~\cite[\S4.5]{paulson-set-II}.
   1.169  
   1.170  The definition may involve arbitrary parameters $\vec{p}=p_1$,
   1.171  \ldots,~$p_k$.  Each recursive set then has the form $R_i(\vec{p})$.  The
   1.172 @@ -243,8 +249,8 @@
   1.173  would appear to be a serious restriction compared with other systems such as
   1.174  Coq~\cite{paulin92}.  For instance, we cannot define the lists of
   1.175  $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
   1.176 -varies.  \S\ref{listn-sec} describes how to express this definition using the
   1.177 -package.
   1.178 +varies.  \S\ref{listn-sec} describes how to express this set using the
   1.179 +inductive definition package.
   1.180  
   1.181  To avoid clutter below, the recursive sets are shown as simply $R_i$
   1.182  instead of $R_i(\vec{p})$.
   1.183 @@ -259,17 +265,16 @@
   1.184  The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
   1.185  sets, satisfying the rule 
   1.186  \[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
   1.187 -The inductive definition package must be supplied monotonicity rules for
   1.188 -all such premises.
   1.189 +The user must supply the package with monotonicity rules for all such premises.
   1.190  
   1.191  Because any monotonic $M$ may appear in premises, the criteria for an
   1.192  acceptable definition is semantic rather than syntactic.  A suitable choice
   1.193  of~$M$ and~$t$ can express a lot.  The powerset operator $\pow$ is
   1.194  monotone, and the premise $t\in\pow(R)$ expresses $t\sbs R$; see
   1.195 -\S\ref{acc-sec} for an example.  The `list of' operator is monotone, and
   1.196 -the premise $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$
   1.197 -using mutual recursion; see \S\ref{primrec-sec} and also my earlier
   1.198 -paper~\cite[\S4.4]{paulson-set-II}.
   1.199 +\S\ref{acc-sec} for an example.  The `list of' operator is monotone, as is
   1.200 +easily proved by induction.  The premise $t\in\lst(R)$ avoids having to
   1.201 +encode the effect of~$\lst(R)$ using mutual recursion; see \S\ref{primrec-sec}
   1.202 +and also my earlier paper~\cite[\S4.4]{paulson-set-II}.
   1.203  
   1.204  Introduction rules may also contain {\bf side-conditions}.  These are
   1.205  premises consisting of arbitrary formulae not mentioning the recursive
   1.206 @@ -286,7 +291,7 @@
   1.207      \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)} 
   1.208  \]
   1.209  
   1.210 -The domain for a (co-)inductive definition must be some existing set closed
   1.211 +The domain in a (co)inductive definition must be some existing set closed
   1.212  under the rules.  A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
   1.213  subsets of~$A$.  The package generates the definition
   1.214  \begin{eqnarray*}
   1.215 @@ -295,9 +300,9 @@
   1.216        \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
   1.217                    &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
   1.218    \end{array}
   1.219 -\end{eqnarray*}
   1.220 +\end{eqnarray*} 
   1.221  The contribution of each rule to the definition of $\Fin(A)$ should be
   1.222 -obvious.  A co-inductive definition is similar but uses $\gfp$ instead
   1.223 +obvious.  A coinductive definition is similar but uses $\gfp$ instead
   1.224  of~$\lfp$.
   1.225  
   1.226  The package must prove that the fixedpoint operator is applied to a
   1.227 @@ -306,12 +311,12 @@
   1.228  $t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
   1.229    presence of logical connectives in the fixedpoint's body, the
   1.230    monotonicity proof requires some unusual rules.  These state that the
   1.231 -  connectives $\conj$, $\disj$ and $\exists$ are monotonic with respect to
   1.232 -  the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
   1.233 +  connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
   1.234 +  to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
   1.235    only if $\forall x.P(x)\imp Q(x)$.}
   1.236  
   1.237 -The result structure returns the definitions of the recursive sets as a theorem
   1.238 -list called {\tt defs}.  It also returns, as the theorem {\tt unfold}, a
   1.239 +The result structure contains the definitions of the recursive sets as a theorem
   1.240 +list called {\tt defs}.  It also contains, as the theorem {\tt unfold}, a
   1.241  fixedpoint equation such as 
   1.242  \begin{eqnarray*}
   1.243    \Fin(A) & = &
   1.244 @@ -320,16 +325,16 @@
   1.245               &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
   1.246    \end{array}
   1.247  \end{eqnarray*}
   1.248 -It also returns, as the theorem {\tt dom\_subset}, an inclusion such as 
   1.249 +It also contains, as the theorem {\tt dom\_subset}, an inclusion such as 
   1.250  $\Fin(A)\sbs\pow(A)$.
   1.251  
   1.252  
   1.253  \subsection{Mutual recursion} \label{mutual-sec}
   1.254 -In a mutually recursive definition, the domain for the fixedoint construction
   1.255 +In a mutually recursive definition, the domain of the fixedpoint construction
   1.256  is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
   1.257  \ldots,~$n$.  The package uses the injections of the
   1.258  binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
   1.259 -$h_{1,n}$, \ldots, $h_{n,n}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
   1.260 +$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
   1.261  
   1.262  As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the
   1.263  operator $\Part$ to support mutual recursion.  The set $\Part(A,h)$
   1.264 @@ -341,15 +346,15 @@
   1.265  $n>1$, the package makes $n+1$ definitions.  The first defines a set $R$ using
   1.266  a fixedpoint operator. The remaining $n$ definitions have the form
   1.267  \begin{eqnarray*}
   1.268 -  R_i & \equiv & \Part(R,h_{i,n}), \qquad i=1,\ldots, n.
   1.269 +  R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n.
   1.270  \end{eqnarray*} 
   1.271  It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
   1.272  
   1.273  
   1.274  \subsection{Proving the introduction rules}
   1.275 -The uesr supplies the package with the desired form of the introduction
   1.276 +The user supplies the package with the desired form of the introduction
   1.277  rules.  Once it has derived the theorem {\tt unfold}, it attempts
   1.278 -to prove the introduction rules.  From the user's point of view, this is the
   1.279 +to prove those rules.  From the user's point of view, this is the
   1.280  trickiest stage; the proofs often fail.  The task is to show that the domain 
   1.281  $D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
   1.282  closed under all the introduction rules.  This essentially involves replacing
   1.283 @@ -367,33 +372,39 @@
   1.284  specifically proved for a particular inductive definition; sometimes this is
   1.285  the easiest way to get the definition through!
   1.286  
   1.287 -The package returns the introduction rules as the theorem list {\tt intrs}.
   1.288 +The result structure contains the introduction rules as the theorem list {\tt
   1.289 +intrs}.
   1.290  
   1.291  \subsection{The elimination rule}
   1.292 -The elimination rule, called {\tt elim}, is derived in a straightforward
   1.293 -manner.  Applying the rule performs a case analysis, with one case for each
   1.294 -introduction rule.  Continuing our example, the elimination rule for $\Fin(A)$
   1.295 -is
   1.296 +The elimination rule, called {\tt elim}, performs case analysis: a
   1.297 +case for each introduction rule.  The elimination rule
   1.298 +for $\Fin(A)$ is
   1.299  \[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
   1.300                   & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
   1.301  \]
   1.302 +This rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else
   1.303 +$x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence
   1.304 +of {\tt unfold}.
   1.305 +
   1.306 +\ifCADE\typeout{****Omitting mk_cases from CADE version!}\else
   1.307  The package also returns a function {\tt mk\_cases}, for generating simplified
   1.308  instances of the elimination rule.  However, {\tt mk\_cases} only works for
   1.309  datatypes and for inductive definitions involving datatypes, such as an
   1.310  inductively defined relation between lists.  It instantiates {\tt elim}
   1.311  with a user-supplied term, then simplifies the cases using the freeness of
   1.312  the underlying datatype.
   1.313 -
   1.314 +See \S\ref{mkcases} for an example.
   1.315 +\fi
   1.316  
   1.317 -\section{Induction and co-induction rules}
   1.318 -Here we must consider inductive and co-inductive definitions separately.
   1.319 +\section{Induction and coinduction rules}
   1.320 +Here we must consider inductive and coinductive definitions separately.
   1.321  For an inductive definition, the package returns an induction rule derived
   1.322  directly from the properties of least fixedpoints, as well as a modified
   1.323  rule for mutual recursion and inductively defined relations.  For a
   1.324 -co-inductive definition, the package returns a basic co-induction rule.
   1.325 +coinductive definition, the package returns a basic coinduction rule.
   1.326  
   1.327  \subsection{The basic induction rule}\label{basic-ind-sec}
   1.328 -The basic rule, called simply {\tt induct}, is appropriate in most situations.
   1.329 +The basic rule, called {\tt induct}, is appropriate in most situations.
   1.330  For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
   1.331  datatype definitions (see below), it is just structural induction.  
   1.332  
   1.333 @@ -405,8 +416,8 @@
   1.334  is~$P(t)$.
   1.335  
   1.336  \item The minor premise's eigenvariables are precisely the introduction
   1.337 -rule's free variables that are not parameters of~$R$ --- for instance, $A$
   1.338 -is not an eigenvariable in the $\Fin(A)$ rule below.
   1.339 +rule's free variables that are not parameters of~$R$.  For instance, the
   1.340 +eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
   1.341  
   1.342  \item If the introduction rule has a premise $t\in R_i$, then the minor
   1.343  premise discharges the assumption $t\in R_i$ and the induction
   1.344 @@ -417,7 +428,8 @@
   1.345  occurrence of $P$ gives the effect of an induction hypothesis, which may be
   1.346  exploited by appealing to properties of~$M$.
   1.347  \end{itemize}
   1.348 -The rule for $\Fin(A)$ is
   1.349 +The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
   1.350 +but includes an induction hypothesis:
   1.351  \[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
   1.352          & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
   1.353  \] 
   1.354 @@ -452,37 +464,42 @@
   1.355  relations.  It eliminates the need to express properties of $z_1$,
   1.356  \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
   1.357  
   1.358 -\subsection{Co-induction}\label{co-ind-sec}
   1.359 -A co-inductive definition yields a primitive co-induction rule, with no
   1.360 +\subsection{Coinduction}\label{coind-sec}
   1.361 +A coinductive definition yields a primitive coinduction rule, with no
   1.362  refinements such as those for the induction rules.  (Experience may suggest
   1.363 -refinements later.)  Consider the co-datatype of lazy lists as an example.  For
   1.364 +refinements later.)  Consider the codatatype of lazy lists as an example.  For
   1.365  suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
   1.366  greatest fixedpoint satisfying the rules
   1.367  \[  \LNil\in\llist(A)  \qquad 
   1.368      \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
   1.369  \]
   1.370 -The $(-)$ tag stresses that this is a co-inductive definition.  A suitable
   1.371 +The $(-)$ tag stresses that this is a coinductive definition.  A suitable
   1.372  domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of
   1.373  sum and product for representing infinite data structures
   1.374 -(\S\ref{data-sec}).  Co-inductive definitions use these variant sums and
   1.375 +(see~\S\ref{univ-sec}).  Coinductive definitions use these variant sums and
   1.376  products.
   1.377  
   1.378  The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 
   1.379  Then it proves the theorem {\tt co\_induct}, which expresses that $\llist(A)$
   1.380  is the greatest solution to this equation contained in $\quniv(A)$:
   1.381 -\[ \infer{a\in\llist(A)}{a\in X & X\sbs \quniv(A) &
   1.382 +\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
   1.383      \infer*{z=\LNil\disj \bigl(\exists a\,l.\,
   1.384        \begin{array}[t]{@{}l}
   1.385          z=\LCons(a,l) \conj a\in A \conj{}\\
   1.386          l\in X\un\llist(A) \bigr)
   1.387        \end{array}  }{[z\in X]_z}}
   1.388  \]
   1.389 +This rule complements the introduction rules; it provides a means of showing
   1.390 +$x\in\llist(A)$ when $x$ is infinite.  For instance, if $x=\LCons(0,x)$ then
   1.391 +applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  Here $\nat$
   1.392 +is the set of natural numbers.
   1.393 +
   1.394  Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
   1.395  represents a slight strengthening of the greatest fixedpoint property.  I
   1.396 -discuss several forms of co-induction rules elsewhere~\cite{paulson-coind}.
   1.397 +discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
   1.398  
   1.399  
   1.400 -\section{Examples of inductive and co-inductive definitions}\label{ind-eg-sec}
   1.401 +\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
   1.402  This section presents several examples: the finite set operator,
   1.403  lists of $n$ elements, bisimulations on lazy lists, the well-founded part
   1.404  of a relation, and the primitive recursive functions.
   1.405 @@ -500,7 +517,7 @@
   1.406             "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
   1.407    val monos = [];
   1.408    val con_defs = [];
   1.409 -  val type_intrs = [empty_subsetI, cons_subsetI, PowI]
   1.410 +  val type_intrs = [empty_subsetI, cons_subsetI, PowI];
   1.411    val type_elims = [make_elim PowD]);
   1.412  \end{ttbox}
   1.413  The parent theory is obtained from {\tt Arith.thy} by adding the unary
   1.414 @@ -536,10 +553,11 @@
   1.415    val rec_doms = [("listn", "nat*list(A)")];
   1.416    val sintrs = 
   1.417        ["<0,Nil> : listn(A)",
   1.418 -       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
   1.419 +       "[| a: A;  <n,l> : listn(A) |] ==> 
   1.420 +        <succ(n), Cons(a,l)> : listn(A)"];
   1.421    val monos = [];
   1.422    val con_defs = [];
   1.423 -  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
   1.424 +  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI];
   1.425    val type_elims = [SigmaE2]);
   1.426  \end{verbatim}
   1.427  \end{small}
   1.428 @@ -576,7 +594,7 @@
   1.429  This rule requires the induction formula to be a 
   1.430  unary property of pairs,~$P(\pair{n,l})$.  The alternative rule, {\tt
   1.431  ListN.mutual\_induct}, uses a binary property instead:
   1.432 -\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(\pair{n,l})}
   1.433 +\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)}
   1.434           {P(0,\Nil) &
   1.435            \infer*{P(\succ(n),\Cons(a,l))}
   1.436                  {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
   1.437 @@ -584,13 +602,14 @@
   1.438  It is now a simple matter to prove theorems about $\listn(A)$, such as
   1.439  \[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
   1.440  \[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
   1.441 -This latter result --- here $r``A$ denotes the image of $A$ under $r$
   1.442 +This latter result --- here $r``X$ denotes the image of $X$ under $r$
   1.443  --- asserts that the inductive definition agrees with the obvious notion of
   1.444  $n$-element list.  
   1.445  
   1.446  Unlike in Coq, the definition does not declare a new datatype.  A `list of
   1.447 -$n$ elements' really is a list, and is subject to list operators such
   1.448 -as append.  For example, a trivial induction yields
   1.449 +$n$ elements' really is a list and is subject to list operators such
   1.450 +as append (concatenation).  For example, a trivial induction on
   1.451 +$\pair{m,l}\in\listn(A)$ yields
   1.452  \[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)}
   1.453           {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
   1.454  \]
   1.455 @@ -598,7 +617,7 @@
   1.456  
   1.457  \ifCADE\typeout{****Omitting mk_cases from CADE version!}
   1.458  \else
   1.459 -\subsection{A demonstration of {\tt mk\_cases}}
   1.460 +\subsection{A demonstration of {\tt mk\_cases}}\label{mkcases}
   1.461  The elimination rule, {\tt ListN.elim}, is cumbersome:
   1.462  \[ \infer{Q}{x\in\listn(A) & 
   1.463            \infer*{Q}{[x = \pair{0,\Nil}]} &
   1.464 @@ -609,14 +628,15 @@
   1.465                 \pair{n,l}\in\listn(A)
   1.466                 \end{array} \right]_{a,l,n}}}
   1.467  \]
   1.468 -The function {\tt ListN.mk\_cases} generates simplified instances of this
   1.469 -rule.  It works by freeness reasoning on the list constructors.
   1.470 -If $x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases}
   1.471 -deduces the corresponding form of~$i$.  For example,
   1.472 +The ML function {\tt ListN.mk\_cases} generates simplified instances of this
   1.473 +rule.  It works by freeness reasoning on the list constructors: $\Cons$ is
   1.474 +injective and $\Cons(a,l)\not=\Nil$. If $x$ is $\pair{i,\Nil}$ or
   1.475 +$\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} deduces the corresponding
   1.476 +form of~$i$.  For example,
   1.477  \begin{ttbox}
   1.478  ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)"
   1.479  \end{ttbox}
   1.480 -yields the rule
   1.481 +yields a rule with only two premises:
   1.482  \[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
   1.483            \infer*{Q}
   1.484               {\left[\begin{array}{l}
   1.485 @@ -634,79 +654,78 @@
   1.486                   & \infer*{Q}{[a\in A &l\in\lst(A)]} }
   1.487  \]
   1.488  The most important uses of {\tt mk\_cases} concern inductive definitions of
   1.489 -evaluation relations.  Then {\tt mk\_cases} supports the kind of backward
   1.490 -inference typical of hand proofs, for example to prove that the evaluation
   1.491 -relation is functional.
   1.492 +evaluation relations.  Then {\tt mk\_cases} supports case analysis on
   1.493 +possible evaluations, for example to prove that evaluation is
   1.494 +functional.
   1.495  \fi  %CADE
   1.496  
   1.497 -\subsection{A co-inductive definition: bisimulations on lazy lists}
   1.498 -This example anticipates the definition of the co-datatype $\llist(A)$, which
   1.499 -consists of lazy lists over~$A$.  Its constructors are $\LNil$ and $\LCons$,
   1.500 -satisfying the introduction rules shown in~\S\ref{co-ind-sec}.  
   1.501 +\subsection{A coinductive definition: bisimulations on lazy lists}
   1.502 +This example anticipates the definition of the codatatype $\llist(A)$, which
   1.503 +consists of finite and infinite lists over~$A$.  Its constructors are $\LNil$
   1.504 +and
   1.505 +$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.  
   1.506  Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
   1.507  pairing and injection operators, it contains non-well-founded elements such as
   1.508  solutions to $\LCons(a,l)=l$.
   1.509  
   1.510 -The next step in the development of lazy lists is to define a co-induction
   1.511 +The next step in the development of lazy lists is to define a coinduction
   1.512  principle for proving equalities.  This is done by showing that the equality
   1.513  relation on lazy lists is the greatest fixedpoint of some monotonic
   1.514  operation.  The usual approach~\cite{pitts94} is to define some notion of 
   1.515  bisimulation for lazy lists, define equivalence to be the greatest
   1.516  bisimulation, and finally to prove that two lazy lists are equivalent if and
   1.517 -only if they are equal.  The co-induction rule for equivalence then yields a
   1.518 -co-induction principle for equalities.
   1.519 +only if they are equal.  The coinduction rule for equivalence then yields a
   1.520 +coinduction principle for equalities.
   1.521  
   1.522  A binary relation $R$ on lazy lists is a {\bf bisimulation} provided $R\sbs
   1.523  R^+$, where $R^+$ is the relation
   1.524 -\[ \{\pair{\LNil;\LNil}\} \un 
   1.525 -   \{\pair{\LCons(a,l);\LCons(a,l')} . a\in A \conj \pair{l;l'}\in R\}.
   1.526 +\[ \{\pair{\LNil,\LNil}\} \un 
   1.527 +   \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
   1.528  \]
   1.529 -Variant pairs are used, $\pair{l;l'}$ instead of $\pair{l,l'}$, because this
   1.530 -is a co-inductive definition. 
   1.531  
   1.532  A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation. 
   1.533 -Equivalence can be co-inductively defined as the greatest fixedpoint for the
   1.534 +Equivalence can be coinductively defined as the greatest fixedpoint for the
   1.535  introduction rules
   1.536 -\[  \pair{\LNil;\LNil} \in\lleq(A)  \qquad 
   1.537 -    \infer[(-)]{\pair{\LCons(a,l);\LCons(a,l')} \in\lleq(A)}
   1.538 -          {a\in A & \pair{l;l'}\in \lleq(A)}
   1.539 +\[  \pair{\LNil,\LNil} \in\lleq(A)  \qquad 
   1.540 +    \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
   1.541 +          {a\in A & \pair{l,l'}\in \lleq(A)}
   1.542  \]
   1.543 -To make this co-inductive definition, we invoke \verb|Co_Inductive_Fun|:
   1.544 +To make this coinductive definition, we invoke \verb|CoInductive_Fun|:
   1.545  \begin{ttbox}
   1.546 -structure LList_Eq = Co_Inductive_Fun
   1.547 +structure LList_Eq = CoInductive_Fun
   1.548  (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
   1.549 - val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
   1.550 + val rec_doms = [("lleq", "llist(A) * llist(A)")];
   1.551   val sintrs = 
   1.552 -   ["<LNil; LNil> : lleq(A)",
   1.553 -    "[| a:A; <l;l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')>: lleq(A)"];
   1.554 +   ["<LNil, LNil> : lleq(A)",
   1.555 +    "[| a:A; <l,l'>: lleq(A) |] ==> 
   1.556 +     <LCons(a,l), LCons(a,l')>: lleq(A)"];
   1.557   val monos = [];
   1.558   val con_defs = [];
   1.559 - val type_intrs = LList.intrs@[QSigmaI];
   1.560 - val type_elims = [QSigmaE2]);
   1.561 + val type_intrs = LList.intrs @ [SigmaI];
   1.562 + val type_elims = [SigmaE2]);
   1.563  \end{ttbox}
   1.564  Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. 
   1.565 -The domain of $\lleq(A)$ is $\llist(A)\otimes\llist(A)$, where $\otimes$
   1.566 -denotes the variant Cartesian product.  The type-checking rules include the
   1.567 -introduction rules for lazy lists as well as rules expressinve both
   1.568 -definitions of the equivalence
   1.569 -\[ \pair{a;b}\in A\otimes B \bimp a\in A \conj b\in B. \]
   1.570 +The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
   1.571 +rules include the introduction rules for lazy lists as well as rules
   1.572 +for both directions of the equivalence
   1.573 +$\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$.
   1.574  
   1.575  The package returns the introduction rules and the elimination rule, as
   1.576 -usual.  But instead of induction rules, it returns a co-induction rule.
   1.577 +usual.  But instead of induction rules, it returns a coinduction rule.
   1.578  The rule is too big to display in the usual notation; its conclusion is
   1.579 -$a\in\lleq(A)$ and its premises are $a\in X$, $X\sbs \llist(A)\otimes\llist(A)$
   1.580 -and
   1.581 -\[ \infer*{z=\pair{\LNil;\LNil}\disj \bigl(\exists a\,l\,l'.\,
   1.582 +$x\in\lleq(A)$ and its premises are $x\in X$, 
   1.583 +${X\sbs\llist(A)\times\llist(A)}$ and
   1.584 +\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
   1.585        \begin{array}[t]{@{}l}
   1.586 -        z=\pair{\LCons(a,l);\LCons(a,l')} \conj a\in A \conj{}\\
   1.587 -        \pair{l;l'}\in X\un\lleq(A) \bigr)
   1.588 +        z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
   1.589 +        \pair{l,l'}\in X\un\lleq(A) \bigr)
   1.590        \end{array}  }{[z\in X]_z}
   1.591  \]
   1.592 -Thus if $a\in X$, where $X$ is a bisimulation contained in the
   1.593 -domain of $\lleq(A)$, then $a\in\lleq(A)$.  It is easy to show that
   1.594 +Thus if $x\in X$, where $X$ is a bisimulation contained in the
   1.595 +domain of $\lleq(A)$, then $x\in\lleq(A)$.  It is easy to show that
   1.596  $\lleq(A)$ is reflexive: the equality relation is a bisimulation.  And
   1.597  $\lleq(A)$ is symmetric: its converse is a bisimulation.  But showing that
   1.598 -$\lleq(A)$ coincides with the equality relation takes considerable work.
   1.599 +$\lleq(A)$ coincides with the equality relation takes some work.
   1.600  
   1.601  \subsection{The accessible part of a relation}\label{acc-sec}
   1.602  Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
   1.603 @@ -716,13 +735,12 @@
   1.604  inductively defined to be the least set that contains $a$ if it contains
   1.605  all $\prec$-predecessors of~$a$, for $a\in D$.  Thus we need an
   1.606  introduction rule of the form 
   1.607 -%%%%\[ \infer{a\in\acc(\prec)}{\infer*{y\in\acc(\prec)}{[y\prec a]_y}} \] 
   1.608  \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
   1.609  Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
   1.610  difficulties for other systems.  Its premise does not conform to 
   1.611  the structure of introduction rules for HOL's inductive definition
   1.612  package~\cite{camilleri92}.  It is also unacceptable to Isabelle package
   1.613 -(\S\ref{intro-sec}), but fortunately can be transformed into one of the
   1.614 +(\S\ref{intro-sec}), but fortunately can be transformed into the acceptable
   1.615  form $t\in M(R)$.
   1.616  
   1.617  The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
   1.618 @@ -732,15 +750,16 @@
   1.619  the inverse image of~$\{a\}$ under~$\prec$.
   1.620  
   1.621  The ML invocation below follows this approach.  Here $r$ is~$\prec$ and
   1.622 -$\field(r)$ refers to~$D$, the domain of $\acc(r)$.  Finally $r^{-}``\{a\}$
   1.623 -denotes the inverse image of~$\{a\}$ under~$r$.  The package is supplied
   1.624 -the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic.
   1.625 +$\field(r)$ refers to~$D$, the domain of $\acc(r)$.  (The field of a
   1.626 +relation is the union of its domain and range.)  Finally
   1.627 +$r^{-}``\{a\}$ denotes the inverse image of~$\{a\}$ under~$r$.  The package is
   1.628 +supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic.
   1.629  \begin{ttbox}
   1.630  structure Acc = Inductive_Fun
   1.631   (val thy = WF.thy addconsts [(["acc"],"i=>i")];
   1.632    val rec_doms = [("acc", "field(r)")];
   1.633    val sintrs = 
   1.634 -      ["[| r-``\{a\} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
   1.635 +      ["[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"];
   1.636    val monos = [Pow_mono];
   1.637    val con_defs = [];
   1.638    val type_intrs = [];
   1.639 @@ -766,7 +785,7 @@
   1.640  introduction rules with arbitrary premises of the form $\forall
   1.641  \vec{y}.P(\vec{y})\imp f(\vec{y})\in R$.  The premise can be expressed
   1.642  equivalently as 
   1.643 -\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \] 
   1.644 +\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
   1.645  provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$.  The
   1.646  following section demonstrates another use of the premise $t\in M(R)$,
   1.647  where $M=\lst$. 
   1.648 @@ -811,22 +830,22 @@
   1.649  each operation on primitive recursive functions combined just two functions.
   1.650  
   1.651  \begin{figure}
   1.652 -\begin{ttbox}
   1.653 +\begin{small}\begin{verbatim}
   1.654  structure Primrec = Inductive_Fun
   1.655   (val thy = Primrec0.thy;
   1.656    val rec_doms = [("primrec", "list(nat)->nat")];
   1.657 -  val ext = None
   1.658 +  val ext = None;
   1.659    val sintrs = 
   1.660        ["SC : primrec",
   1.661         "k: nat ==> CONST(k) : primrec",
   1.662         "i: nat ==> PROJ(i) : primrec",
   1.663 -       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
   1.664 -       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
   1.665 +       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
   1.666 +       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"];
   1.667    val monos = [list_mono];
   1.668    val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
   1.669 -  val type_intrs = pr0_typechecks
   1.670 +  val type_intrs = pr0_typechecks;
   1.671    val type_elims = []);
   1.672 -\end{ttbox}
   1.673 +\end{verbatim}\end{small}
   1.674  \hrule
   1.675  \caption{Inductive definition of the primitive recursive functions} 
   1.676  \label{primrec-fig}
   1.677 @@ -842,7 +861,7 @@
   1.678  Due to the use of $\lst$ as a monotone operator, the composition case has
   1.679  an unusual induction hypothesis:
   1.680   \[ \infer*{P(\COMP(g,\fs))}
   1.681 -          {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(x)\})]_{\fs,g}} \]
   1.682 +          {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} \]
   1.683  The hypothesis states that $\fs$ is a list of primitive recursive functions
   1.684  satisfying the induction formula.  Proving the $\COMP$ case typically requires
   1.685  structural induction on lists, yielding two subcases: either $\fs=\Nil$ or
   1.686 @@ -865,20 +884,20 @@
   1.687  tradition.
   1.688  
   1.689  
   1.690 -\section{Datatypes and co-datatypes}\label{data-sec}
   1.691 -A (co-)datatype definition is a (co-)inductive definition with automatically
   1.692 -defined constructors and case analysis operator.  The package proves that the
   1.693 +\section{Datatypes and codatatypes}\label{data-sec}
   1.694 +A (co)datatype definition is a (co)inductive definition with automatically
   1.695 +defined constructors and a case analysis operator.  The package proves that the
   1.696  case operator inverts the constructors, and can also prove freeness theorems
   1.697  involving any pair of constructors.
   1.698  
   1.699  
   1.700 -\subsection{Constructors and their domain}
   1.701 -Conceptually, our two forms of definition are distinct: a (co-)inductive
   1.702 -definition selects a subset of an existing set, but a (co-)datatype
   1.703 +\subsection{Constructors and their domain}\label{univ-sec}
   1.704 +Conceptually, our two forms of definition are distinct: a (co)inductive
   1.705 +definition selects a subset of an existing set, but a (co)datatype
   1.706  definition creates a new set.  But the package reduces the latter to the
   1.707  former.  A set having strong closure properties must serve as the domain
   1.708 -of the (co-)inductive definition.  Constructing this set requires some
   1.709 -theoretical effort.  Consider first datatypes and then co-datatypes.
   1.710 +of the (co)inductive definition.  Constructing this set requires some
   1.711 +theoretical effort.  Consider first datatypes and then codatatypes.
   1.712  
   1.713  Isabelle/ZF defines the standard notion of Cartesian product $A\times B$,
   1.714  containing ordered pairs $\pair{a,b}$.  Now the $m$-tuple
   1.715 @@ -890,7 +909,7 @@
   1.716  A datatype constructor $\Con(x_1,\ldots\,x_m)$ is defined to be
   1.717  $h(\pair{x_1,\ldots\,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
   1.718  In a mutually recursive definition, all constructors for the set~$R_i$ have
   1.719 -the outer form~$h_{i,n}$, where $h_{i,n}$ is the injection described
   1.720 +the outer form~$h_{in}$, where $h_{in}$ is the injection described
   1.721  in~\S\ref{mutual-sec}.  Further nested injections ensure that the
   1.722  constructors for~$R_i$ are pairwise distinct.  
   1.723  
   1.724 @@ -903,30 +922,31 @@
   1.725  
   1.726  The standard pairs and injections can only yield well-founded
   1.727  constructions.  This eases the (manual!) definition of recursive functions
   1.728 -over datatypes.  But they are unsuitable for co-datatypes, which typically
   1.729 +over datatypes.  But they are unsuitable for codatatypes, which typically
   1.730  contain non-well-founded objects.
   1.731  
   1.732 -To support co-datatypes, Isabelle/ZF defines a variant notion of ordered
   1.733 +To support codatatypes, Isabelle/ZF defines a variant notion of ordered
   1.734  pair, written~$\pair{a;b}$.  It also defines the corresponding variant
   1.735  notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
   1.736  and~$\QInr(b)$, and variant disjoint sum $A\oplus B$.  Finally it defines
   1.737  the set $\quniv(A)$, which contains~$A$ and furthermore contains
   1.738  $\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$.  In a
   1.739 -typical co-datatype definition with set parameters $A_1$, \ldots, $A_k$, a
   1.740 -suitable domain is $\quniv(A_1\un\cdots\un A_k)$.  This approach is an
   1.741 -alternative to adopting an Anti-Foundation
   1.742 -Axiom~\cite{aczel88}.\footnote{No reference is available.  Variant pairs
   1.743 -  are defined by $\pair{a;b}\equiv a+b \equiv (\{0\}\times a) \un (\{1\}\times
   1.744 -  b)$, where $\times$ is the Cartesian product for standard ordered pairs.  Now
   1.745 +typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a
   1.746 +suitable domain is $\quniv(A_1\un\cdots\un A_k)$.  This approach using
   1.747 +standard ZF set theory\footnote{No reference is available.  Variant pairs
   1.748 +  are defined by $\pair{a;b}\equiv (a+b) \equiv (\{0\}\times a) \un
   1.749 +  (\{1\}\times b)$, where $\times$ is the Cartesian product for standard
   1.750 +  ordered pairs.  Now
   1.751    $\pair{a;b}$ is injective and monotonic in its two arguments.
   1.752    Non-well-founded constructions, such as infinite lists, are constructed
   1.753    as least fixedpoints; the bounding set typically has the form
   1.754    $\univ(a_1\un\cdots\un a_k)$, where $a_1$, \ldots, $a_k$ are specified
   1.755    elements of the construction.}
   1.756 -
   1.757 +is an alternative to adopting Aczel's Anti-Foundation
   1.758 +Axiom~\cite{aczel88}.
   1.759  
   1.760  \subsection{The case analysis operator}
   1.761 -The (co-)datatype package automatically defines a case analysis operator,
   1.762 +The (co)datatype package automatically defines a case analysis operator,
   1.763  called {\tt$R$\_case}.  A mutually recursive definition still has only
   1.764  one operator, called {\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is
   1.765  analogous to those for products and sums.  
   1.766 @@ -945,9 +965,12 @@
   1.767    R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}),
   1.768      \qquad i = 1, \ldots, k
   1.769  \end{eqnarray*}
   1.770 -Note that if $f$ and $g$ have meta-type $i\To i$ then so do $\split(f)$ and
   1.771 -$\case(f,g)$.  This works because $\split$ and $\case$ operate on their
   1.772 -last argument.  They are easily combined to make complex case analysis
   1.773 +The case operator's definition takes advantage of Isabelle's representation
   1.774 +of syntax in the typed $\lambda$-calculus; it could readily be adapted to a
   1.775 +theorem prover for higher-order logic.  If $f$ and~$g$ have meta-type
   1.776 +$i\To i$ then so do $\split(f)$ and
   1.777 +$\case(f,g)$.  This works because $\split$ and $\case$ operate on their last
   1.778 +argument.  They are easily combined to make complex case analysis
   1.779  operators.  Here are two examples:
   1.780  \begin{itemize}
   1.781  \item $\split(\lambda x.\split(f(x)))$ performs case analysis for
   1.782 @@ -967,13 +990,13 @@
   1.783      & = & g(b)
   1.784  \end{eqnarray*}
   1.785  \end{itemize}
   1.786 -Co-datatype definitions are treated in precisely the same way.  They express
   1.787 +Codatatype definitions are treated in precisely the same way.  They express
   1.788  case operators using those for the variant products and sums, namely
   1.789  $\qsplit$ and~$\qcase$.
   1.790  
   1.791  
   1.792  \ifCADE The package has processed all the datatypes discussed in my earlier
   1.793 -paper~\cite{paulson-set-II} and the co-datatype of lazy lists.  Space
   1.794 +paper~\cite{paulson-set-II} and the codatatype of lazy lists.  Space
   1.795  limitations preclude discussing these examples here, but they are
   1.796  distributed with Isabelle.  
   1.797  \typeout{****Omitting datatype examples from CADE version!} \else
   1.798 @@ -991,12 +1014,12 @@
   1.799            [(["Nil"],    "i"), 
   1.800             (["Cons"],   "[i,i]=>i")])];
   1.801    val rec_styp = "i=>i";
   1.802 -  val ext = None
   1.803 +  val ext = None;
   1.804    val sintrs = 
   1.805        ["Nil : list(A)",
   1.806         "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   1.807    val monos = [];
   1.808 -  val type_intrs = datatype_intrs
   1.809 +  val type_intrs = datatype_intrs;
   1.810    val type_elims = datatype_elims);
   1.811  \end{ttbox}
   1.812  \hrule
   1.813 @@ -1004,29 +1027,29 @@
   1.814  
   1.815  \medskip
   1.816  \begin{ttbox}
   1.817 -structure LList = Co_Datatype_Fun
   1.818 +structure LList = CoDatatype_Fun
   1.819   (val thy = QUniv.thy;
   1.820    val rec_specs = 
   1.821        [("llist", "quniv(A)",
   1.822            [(["LNil"],   "i"), 
   1.823             (["LCons"],  "[i,i]=>i")])];
   1.824    val rec_styp = "i=>i";
   1.825 -  val ext = None
   1.826 +  val ext = None;
   1.827    val sintrs = 
   1.828        ["LNil : llist(A)",
   1.829         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   1.830    val monos = [];
   1.831 -  val type_intrs = co_datatype_intrs
   1.832 -  val type_elims = co_datatype_elims);
   1.833 +  val type_intrs = codatatype_intrs;
   1.834 +  val type_elims = codatatype_elims);
   1.835  \end{ttbox}
   1.836  \hrule
   1.837 -\caption{Defining the co-datatype of lazy lists} \label{llist-fig}
   1.838 +\caption{Defining the codatatype of lazy lists} \label{llist-fig}
   1.839  \end{figure}
   1.840  
   1.841  \subsection{Example: lists and lazy lists}
   1.842  Figures \ref{list-fig} and~\ref{llist-fig} present the ML definitions of
   1.843  lists and lazy lists, respectively.  They highlight the (many) similarities
   1.844 -and (few) differences between datatype and co-datatype definitions.
   1.845 +and (few) differences between datatype and codatatype definitions.
   1.846  
   1.847  Each form of list has two constructors, one for the empty list and one for
   1.848  adding an element to a list.  Each takes a parameter, defining the set of
   1.849 @@ -1039,7 +1062,8 @@
   1.850  QUniv.thy}.
   1.851  \end{itemize}
   1.852  
   1.853 -Since $\lst(A)$ is a datatype, it enjoys a structural rule, {\tt List.induct}:
   1.854 +Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
   1.855 +  List.induct}:
   1.856  \[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
   1.857          & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
   1.858  \] 
   1.859 @@ -1050,8 +1074,8 @@
   1.860  is
   1.861  \[ \rank(l) < \rank(\Cons(a,l)). \]
   1.862  
   1.863 -Since $\llist(A)$ is a co-datatype, it has no induction rule.  Instead it has
   1.864 -the co-induction rule shown in \S\ref{co-ind-sec}.  Since variant pairs and
   1.865 +Since $\llist(A)$ is a codatatype, it has no induction rule.  Instead it has
   1.866 +the coinduction rule shown in \S\ref{coind-sec}.  Since variant pairs and
   1.867  injections are monotonic and need not have greater rank than their
   1.868  components, fixedpoint operators can create cyclic constructions.  For
   1.869  example, the definition
   1.870 @@ -1077,11 +1101,11 @@
   1.871      \lstcase(c, h, \Nil) & = & 
   1.872         \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
   1.873       & = & (\lambda u.c)(\emptyset) \\
   1.874 -     & = & c.\\[1ex]
   1.875 +     & = & c\\[1ex]
   1.876      \lstcase(c, h, \Cons(x,y)) & = & 
   1.877         \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
   1.878       & = & \split(h, \pair{x,y}) \\
   1.879 -     & = & h(x,y).
   1.880 +     & = & h(x,y)
   1.881  \end{eqnarray*} 
   1.882  
   1.883  \begin{figure}
   1.884 @@ -1096,13 +1120,13 @@
   1.885            [(["Fnil"],   "i"),
   1.886             (["Fcons"],  "[i,i]=>i")])];
   1.887    val rec_styp = "i=>i";
   1.888 -  val ext = None
   1.889 +  val ext = None;
   1.890    val sintrs = 
   1.891            ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
   1.892             "Fnil : forest(A)",
   1.893             "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
   1.894    val monos = [];
   1.895 -  val type_intrs = datatype_intrs
   1.896 +  val type_intrs = datatype_intrs;
   1.897    val type_elims = datatype_elims);
   1.898  \end{verbatim}
   1.899  \end{small}
   1.900 @@ -1112,7 +1136,7 @@
   1.901  
   1.902  
   1.903  \subsection{Example: mutual recursion}
   1.904 -In the mutually recursive trees/forests~\cite[\S4.5]{paulson-set-II}, trees
   1.905 +In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
   1.906  have the one constructor $\Tcons$, while forests have the two constructors
   1.907  $\Fnil$ and~$\Fcons$.  Figure~\ref{tf-fig} presents the ML
   1.908  definition.  It has much in common with that of $\lst(A)$, including its
   1.909 @@ -1128,7 +1152,7 @@
   1.910                 \end{array}
   1.911           \right]_{a,f}}
   1.912       & P(\Fnil)
   1.913 -     & \infer*{P(\Fcons(a,l))}
   1.914 +     & \infer*{P(\Fcons(t,f))}
   1.915          {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
   1.916                                  f\in\forest(A) \\ P(f)
   1.917                  \end{array}
   1.918 @@ -1150,7 +1174,7 @@
   1.919                 \end{array}
   1.920           \right]_{a,f}}
   1.921       & Q(\Fnil)
   1.922 -     & \infer*{Q(\Fcons(a,l))}
   1.923 +     & \infer*{Q(\Fcons(t,f))}
   1.924          {\left[\begin{array}{l} t\in\tree(A)   \\ P(t) \\
   1.925                                  f\in\forest(A) \\ Q(f)
   1.926                  \end{array}
   1.927 @@ -1187,14 +1211,14 @@
   1.928             (["Con2"],   "[i,i]=>i"),
   1.929             (["Con3"],   "[i,i,i]=>i")])];
   1.930    val rec_styp = "[i,i]=>i";
   1.931 -  val ext = None
   1.932 +  val ext = None;
   1.933    val sintrs = 
   1.934            ["Con0 : data(A,B)",
   1.935             "[| a: A |] ==> Con1(a) : data(A,B)",
   1.936             "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
   1.937             "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
   1.938    val monos = [];
   1.939 -  val type_intrs = datatype_intrs
   1.940 +  val type_intrs = datatype_intrs;
   1.941    val type_elims = datatype_elims);
   1.942  \end{verbatim}
   1.943  \end{small}
   1.944 @@ -1204,7 +1228,7 @@
   1.945  
   1.946  \subsection{A four-constructor datatype}
   1.947  Finally let us consider a fairly general datatype.  It has four
   1.948 -constructors $\Con_0$, $\Con_1$\ $\Con_2$ and $\Con_3$, with the
   1.949 +constructors $\Con_0$, \ldots, $\Con_3$, with the
   1.950  corresponding arities.  Figure~\ref{data-fig} presents the ML definition. 
   1.951  Because this datatype has two set parameters, $A$ and~$B$, it specifies
   1.952  $\univ(A\un B)$ as its domain.  The structural induction rule has four
   1.953 @@ -1248,11 +1272,8 @@
   1.954  quadratic in size.  It is like the difference between the binary and unary
   1.955  numeral systems. 
   1.956  
   1.957 -The package returns the constructor and case operator definitions as the
   1.958 -theorem list \verb|con_defs|.  The head of this list defines the case
   1.959 -operator and the tail defines the constructors. 
   1.960 -
   1.961 -The package returns the case equations, such as 
   1.962 +The result structure contains the case operator and constructor definitions as
   1.963 +the theorem list \verb|con_defs|. It contains the case equations, such as 
   1.964  \begin{eqnarray*}
   1.965    {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c),
   1.966  \end{eqnarray*}
   1.967 @@ -1280,7 +1301,7 @@
   1.968    \Con_1(a)=c   & \bimp &  c=\Inl(\Inr(a))             \\
   1.969                  & \vdots &                             \\
   1.970    \Inl(a)=\Inl(b)   & \bimp &  a=b                     \\
   1.971 -  \Inl(a)=\Inr(b)   & \bimp &  \bot                    \\
   1.972 +  \Inl(a)=\Inr(b)   & \bimp &  {\tt False}             \\
   1.973    \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
   1.974  \end{eqnarray*}
   1.975  For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
   1.976 @@ -1298,8 +1319,8 @@
   1.977  \fi  %CADE
   1.978  
   1.979  \section{Conclusions and future work}
   1.980 -The fixedpoint approach makes it easy to implement a uniquely powerful
   1.981 -package for inductive and co-inductive definitions.  It is efficient: it
   1.982 +The fixedpoint approach makes it easy to implement a powerful
   1.983 +package for inductive and coinductive definitions.  It is efficient: it
   1.984  processes most definitions in seconds and even a 60-constructor datatype
   1.985  requires only two minutes.  It is also simple: the package consists of
   1.986  under 1100 lines (35K bytes) of Standard ML code.  The first working
   1.987 @@ -1310,11 +1331,11 @@
   1.988  Indeed, Melham's inductive definition package for the HOL
   1.989  system~\cite{camilleri92} implicitly proves this theorem.
   1.990  
   1.991 -Datatype and co-datatype definitions furthermore require a particular set
   1.992 +Datatype and codatatype definitions furthermore require a particular set
   1.993  closed under a suitable notion of ordered pair.  I intend to use the
   1.994  Isabelle/ZF package as the basis for a higher-order logic one, using
   1.995  Isabelle/HOL\@.  The necessary theory is already
   1.996 -mechanizeds~\cite{paulson-coind}.  HOL represents sets by unary predicates;
   1.997 +mechanized~\cite{paulson-coind}.  HOL represents sets by unary predicates;
   1.998  defining the corresponding types may cause complication.
   1.999  
  1.1000  
  1.1001 @@ -1326,9 +1347,9 @@
  1.1002  \else
  1.1003  \newpage
  1.1004  \appendix
  1.1005 -\section{Inductive and co-inductive definitions: users guide}
  1.1006 -The ML functors \verb|Inductive_Fun| and \verb|Co_Inductive_Fun| build
  1.1007 -inductive and co-inductive definitions, respectively.  This section describes
  1.1008 +\section{Inductive and coinductive definitions: users guide}
  1.1009 +The ML functors \verb|Inductive_Fun| and \verb|CoInductive_Fun| build
  1.1010 +inductive and coinductive definitions, respectively.  This section describes
  1.1011  how to invoke them.  
  1.1012  
  1.1013  \subsection{The result structure}
  1.1014 @@ -1356,8 +1377,11 @@
  1.1015  \end{description}
  1.1016  
  1.1017  For an inductive definition, the result structure contains two induction rules,
  1.1018 -{\tt induct} and \verb|mutual_induct|.  For a co-inductive definition, it
  1.1019 -contains the rule \verb|co_induct|.
  1.1020 +{\tt induct} and \verb|mutual_induct|.  For a coinductive definition, it
  1.1021 +contains the rule \verb|coinduct|.
  1.1022 +
  1.1023 +Figure~\ref{def-result-fig} summarizes the two result signatures,
  1.1024 +specifying the types of all these components.
  1.1025  
  1.1026  \begin{figure}
  1.1027  \begin{ttbox}
  1.1028 @@ -1373,18 +1397,14 @@
  1.1029  {\it(Inductive definitions only)} 
  1.1030  val induct       : thm
  1.1031  val mutual_induct: thm
  1.1032 -{\it(Co-inductive definitions only)}
  1.1033 -val co_induct    : thm
  1.1034 +{\it(Coinductive definitions only)}
  1.1035 +val coinduct    : thm
  1.1036  end
  1.1037  \end{ttbox}
  1.1038  \hrule
  1.1039 -\caption{The result of a (co-)inductive definition} \label{def-result-fig}
  1.1040 -\end{figure}
  1.1041 +\caption{The result of a (co)inductive definition} \label{def-result-fig}
  1.1042  
  1.1043 -Figure~\ref{def-result-fig} summarizes the two result signatures,
  1.1044 -specifying the types of all these components.
  1.1045 -
  1.1046 -\begin{figure}
  1.1047 +\medskip
  1.1048  \begin{ttbox}
  1.1049  sig  
  1.1050  val thy          : theory
  1.1051 @@ -1397,11 +1417,11 @@
  1.1052  end
  1.1053  \end{ttbox}
  1.1054  \hrule
  1.1055 -\caption{The argument of a (co-)inductive definition} \label{def-arg-fig}
  1.1056 +\caption{The argument of a (co)inductive definition} \label{def-arg-fig}
  1.1057  \end{figure}
  1.1058  
  1.1059  \subsection{The argument structure}
  1.1060 -Both \verb|Inductive_Fun| and \verb|Co_Inductive_Fun| take the same argument
  1.1061 +Both \verb|Inductive_Fun| and \verb|CoInductive_Fun| take the same argument
  1.1062  structure (Figure~\ref{def-arg-fig}).  Its components are as follows:
  1.1063  \begin{description}
  1.1064  \item[\tt thy] is the definition's parent theory, which {\it must\/}
  1.1065 @@ -1416,9 +1436,9 @@
  1.1066  to a recursive set in the introduction rules.
  1.1067  
  1.1068  \item[\tt con\_defs] contains definitions of constants appearing in the
  1.1069 -introduction rules.  The (co-)datatype package supplies the constructors'
  1.1070 +introduction rules.  The (co)datatype package supplies the constructors'
  1.1071  definitions here.  Most direct calls of \verb|Inductive_Fun| or
  1.1072 -\verb|Co_Inductive_Fun| pass the empty list; one exception is the primitive
  1.1073 +\verb|CoInductive_Fun| pass the empty list; one exception is the primitive
  1.1074  recursive functions example (\S\ref{primrec-sec}).
  1.1075  
  1.1076  \item[\tt type\_intrs] consists of introduction rules for type-checking the
  1.1077 @@ -1448,14 +1468,14 @@
  1.1078  \end{itemize}
  1.1079  
  1.1080  
  1.1081 -\section{Datatype and co-datatype definitions: users guide}
  1.1082 -The ML functors \verb|Datatype_Fun| and \verb|Co_Datatype_Fun| define datatypes
  1.1083 -and co-datatypes, invoking \verb|Datatype_Fun| and
  1.1084 -\verb|Co_Datatype_Fun| to make the underlying (co-)inductive definitions. 
  1.1085 +\section{Datatype and codatatype definitions: users guide}
  1.1086 +The ML functors \verb|Datatype_Fun| and \verb|CoDatatype_Fun| define datatypes
  1.1087 +and codatatypes, invoking \verb|Datatype_Fun| and
  1.1088 +\verb|CoDatatype_Fun| to make the underlying (co)inductive definitions. 
  1.1089  
  1.1090  
  1.1091  \subsection{The result structure}
  1.1092 -The result structure extends that of (co-)inductive definitions
  1.1093 +The result structure extends that of (co)inductive definitions
  1.1094  (Figure~\ref{def-result-fig}) with several additional items:
  1.1095  \begin{ttbox}
  1.1096  val con_thy   : theory
  1.1097 @@ -1468,9 +1488,9 @@
  1.1098  Most of these have been discussed in~\S\ref{data-sec}.  Here is a summary:
  1.1099  \begin{description}
  1.1100  \item[\tt con\_thy] is a new theory containing definitions of the
  1.1101 -(co-)datatype's constructors and case operator.  It also declares the
  1.1102 +(co)datatype's constructors and case operator.  It also declares the
  1.1103  recursive sets as constants, so that it may serve as the parent
  1.1104 -theory for the (co-)inductive definition.
  1.1105 +theory for the (co)inductive definition.
  1.1106  
  1.1107  \item[\tt con\_defs] is a list of definitions: the case operator followed by
  1.1108  the constructors.  This theorem list can be supplied to \verb|mk_cases|, for
  1.1109 @@ -1498,8 +1518,8 @@
  1.1110  \end{description}
  1.1111  
  1.1112  The result structure also inherits everything from the underlying
  1.1113 -(co-)inductive definition, such as the introduction rules, elimination rule,
  1.1114 -and induction/co-induction rule.
  1.1115 +(co)inductive definition, such as the introduction rules, elimination rule,
  1.1116 +and induction/coinduction rule.
  1.1117  
  1.1118  
  1.1119  \begin{figure}
  1.1120 @@ -1516,18 +1536,18 @@
  1.1121  end
  1.1122  \end{ttbox}
  1.1123  \hrule
  1.1124 -\caption{The argument of a (co-)datatype definition} \label{data-arg-fig}
  1.1125 +\caption{The argument of a (co)datatype definition} \label{data-arg-fig}
  1.1126  \end{figure}
  1.1127  
  1.1128  \subsection{The argument structure}
  1.1129 -Both (co-)datatype functors take the same argument structure
  1.1130 -(Figure~\ref{data-arg-fig}).  It does not extend that for (co-)inductive
  1.1131 +Both (co)datatype functors take the same argument structure
  1.1132 +(Figure~\ref{data-arg-fig}).  It does not extend that for (co)inductive
  1.1133  definitions, but shares several components  and passes them uninterpreted to
  1.1134  \verb|Datatype_Fun| or
  1.1135 -\verb|Co_Datatype_Fun|.  The new components are as follows:
  1.1136 +\verb|CoDatatype_Fun|.  The new components are as follows:
  1.1137  \begin{description}
  1.1138 -\item[\tt thy] is the (co-)datatype's parent theory. It {\it must not\/}
  1.1139 -declare constants for the recursive sets.  Recall that (co-)inductive
  1.1140 +\item[\tt thy] is the (co)datatype's parent theory. It {\it must not\/}
  1.1141 +declare constants for the recursive sets.  Recall that (co)inductive
  1.1142  definitions have the opposite restriction.
  1.1143  
  1.1144  \item[\tt rec\_specs] is a list of triples of the form ({\it recursive set\/},
  1.1145 @@ -1550,9 +1570,9 @@
  1.1146  products and disjoint sums \cite[\S4.2]{paulson-set-II}.  In a typical
  1.1147  datatype definition with set parameters $A_1$, \ldots, $A_k$, a suitable
  1.1148  domain for all the recursive sets is $\univ(A_1\un\cdots\un A_k)$.  For a
  1.1149 -co-datatype definition, the set
  1.1150 +codatatype definition, the set
  1.1151  $\quniv(A)$ contains~$A$ and is closed under the variant Cartesian products
  1.1152 -and disjoint sums; the appropropriate domain is
  1.1153 +and disjoint sums; the appropriate domain is
  1.1154  $\quniv(A_1\un\cdots\un A_k)$.
  1.1155  
  1.1156  The {\tt sintrs} specify the introduction rules, which govern the recursive
  1.1157 @@ -1560,7 +1580,7 @@
  1.1158  and side-conditions to express things that go beyond the usual notion of
  1.1159  datatype.  The theorem lists {\tt monos}, {\tt type\_intrs} and {\tt
  1.1160  type\_elims} should contain precisely what is needed for the underlying
  1.1161 -(co-)inductive definition.  Isabelle/ZF defines theorem lists that can be
  1.1162 +(co)inductive definition.  Isabelle/ZF defines theorem lists that can be
  1.1163  defined for the latter two components:
  1.1164  \begin{itemize}
  1.1165  \item {\tt datatype\_intrs} and {\tt datatype\_elims} are type-checking rules