author | lcp |

Fri Nov 19 11:31:10 1993 +0100 (1993-11-19) | |

changeset 130 | c035b6b9eafc |

parent 129 | dc50a4b96d7b |

child 131 | bb0caac13eff |

Many edits suggested by Grundy & Thompson

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