1 \documentstyle[a4,proof,iman,extra,12pt]{llncs}
5 \title{A Fixedpoint Approach to Implementing\\
6 (Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed
7 comments; the referees were also helpful. Research funded by
8 SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453
11 \author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}}
12 \institute{Computer Laboratory, University of Cambridge, England}
14 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
16 \newcommand\sbs{\subseteq}
20 \newcommand\pow{{\cal P}}
22 \newcommand\RepFun{\hbox{\tt RepFun}}
23 \newcommand\cons{\hbox{\tt cons}}
24 \def\succ{\hbox{\tt succ}}
25 \newcommand\split{\hbox{\tt split}}
26 \newcommand\fst{\hbox{\tt fst}}
27 \newcommand\snd{\hbox{\tt snd}}
28 \newcommand\converse{\hbox{\tt converse}}
29 \newcommand\domain{\hbox{\tt domain}}
30 \newcommand\range{\hbox{\tt range}}
31 \newcommand\field{\hbox{\tt field}}
32 \newcommand\lfp{\hbox{\tt lfp}}
33 \newcommand\gfp{\hbox{\tt gfp}}
34 \newcommand\id{\hbox{\tt id}}
35 \newcommand\trans{\hbox{\tt trans}}
36 \newcommand\wf{\hbox{\tt wf}}
37 \newcommand\nat{\hbox{\tt nat}}
38 \newcommand\rank{\hbox{\tt rank}}
39 \newcommand\univ{\hbox{\tt univ}}
40 \newcommand\Vrec{\hbox{\tt Vrec}}
41 \newcommand\Inl{\hbox{\tt Inl}}
42 \newcommand\Inr{\hbox{\tt Inr}}
43 \newcommand\case{\hbox{\tt case}}
44 \newcommand\lst{\hbox{\tt list}}
45 \newcommand\Nil{\hbox{\tt Nil}}
46 \newcommand\Cons{\hbox{\tt Cons}}
47 \newcommand\lstcase{\hbox{\tt list\_case}}
48 \newcommand\lstrec{\hbox{\tt list\_rec}}
49 \newcommand\length{\hbox{\tt length}}
50 \newcommand\listn{\hbox{\tt listn}}
51 \newcommand\acc{\hbox{\tt acc}}
52 \newcommand\primrec{\hbox{\tt primrec}}
53 \newcommand\SC{\hbox{\tt SC}}
54 \newcommand\CONST{\hbox{\tt CONST}}
55 \newcommand\PROJ{\hbox{\tt PROJ}}
56 \newcommand\COMP{\hbox{\tt COMP}}
57 \newcommand\PREC{\hbox{\tt PREC}}
59 \newcommand\quniv{\hbox{\tt quniv}}
60 \newcommand\llist{\hbox{\tt llist}}
61 \newcommand\LNil{\hbox{\tt LNil}}
62 \newcommand\LCons{\hbox{\tt LCons}}
63 \newcommand\lconst{\hbox{\tt lconst}}
64 \newcommand\lleq{\hbox{\tt lleq}}
65 \newcommand\map{\hbox{\tt map}}
66 \newcommand\term{\hbox{\tt term}}
67 \newcommand\Apply{\hbox{\tt Apply}}
68 \newcommand\termcase{\hbox{\tt term\_case}}
69 \newcommand\rev{\hbox{\tt rev}}
70 \newcommand\reflect{\hbox{\tt reflect}}
71 \newcommand\tree{\hbox{\tt tree}}
72 \newcommand\forest{\hbox{\tt forest}}
73 \newcommand\Part{\hbox{\tt Part}}
74 \newcommand\TF{\hbox{\tt tree\_forest}}
75 \newcommand\Tcons{\hbox{\tt Tcons}}
76 \newcommand\Fcons{\hbox{\tt Fcons}}
77 \newcommand\Fnil{\hbox{\tt Fnil}}
78 \newcommand\TFcase{\hbox{\tt TF\_case}}
79 \newcommand\Fin{\hbox{\tt Fin}}
80 \newcommand\QInl{\hbox{\tt QInl}}
81 \newcommand\QInr{\hbox{\tt QInr}}
82 \newcommand\qsplit{\hbox{\tt qsplit}}
83 \newcommand\qcase{\hbox{\tt qcase}}
84 \newcommand\Con{\hbox{\tt Con}}
85 \newcommand\data{\hbox{\tt data}}
87 \binperiod %%%treat . like a binary operator
94 This paper presents a fixedpoint approach to inductive definitions.
95 Instead of using a syntactic test such as `strictly positive,' the
96 approach lets definitions involve any operators that have been proved
97 monotone. It is conceptually simple, which has allowed the easy
98 implementation of mutual recursion and other conveniences. It also
99 handles coinductive definitions: simply replace the least fixedpoint by a
100 greatest fixedpoint. This represents the first automated support for
101 coinductive definitions.
103 The method has been implemented in two of Isabelle's logics, ZF set theory
104 and higher-order logic. It should be applicable to any logic in which
105 the Knaster-Tarski Theorem can be proved. Examples include lists of $n$
106 elements, the accessible part of a relation and the set of primitive
107 recursive functions. One example of a coinductive definition is
108 bisimulations for lazy lists. \ifCADE\else Recursive datatypes are
109 examined in detail, as well as one example of a {\bf codatatype}: lazy
110 lists. The appendices are simple user's manuals for this Isabelle
114 \bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
115 \thispagestyle{empty}
117 \tableofcontents\cleardoublepage\pagestyle{plain}
119 \section{Introduction}
120 Several theorem provers provide commands for formalizing recursive data
121 structures, like lists and trees. Examples include Boyer and Moore's shell
122 principle~\cite{bm79} and Melham's recursive type package for the Cambridge HOL
123 system~\cite{melham89}. Such data structures are called {\bf datatypes}
124 below, by analogy with {\tt datatype} definitions in Standard~ML\@.
126 A datatype is but one example of an {\bf inductive definition}. This
127 specifies the least set closed under given rules~\cite{aczel77}. The
128 collection of theorems in a logic is inductively defined. A structural
129 operational semantics~\cite{hennessy90} is an inductive definition of a
130 reduction or evaluation relation on programs. A few theorem provers
131 provide commands for formalizing inductive definitions; these include
132 Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}.
134 The dual notion is that of a {\bf coinductive definition}. This specifies
135 the greatest set closed under given rules. Important examples include
136 using bisimulation relations to formalize equivalence of
137 processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}.
138 Other examples include lazy lists and other infinite data structures; these
139 are called {\bf codatatypes} below.
141 Not all inductive definitions are meaningful. {\bf Monotone} inductive
142 definitions are a large, well-behaved class. Monotonicity can be enforced
143 by syntactic conditions such as `strictly positive,' but this could lead to
144 monotone definitions being rejected on the grounds of their syntactic form.
145 More flexible is to formalize monotonicity within the logic and allow users
148 This paper describes a package based on a fixedpoint approach. Least
149 fixedpoints yield inductive definitions; greatest fixedpoints yield
150 coinductive definitions. The package has several advantages:
152 \item It allows reference to any operators that have been proved monotone.
153 Thus it accepts all provably monotone inductive definitions, including
154 iterated definitions.
155 \item It accepts a wide class of datatype definitions, including those with
157 \item It handles coinductive and codatatype definitions. Most of
158 the discussion below applies equally to inductive and coinductive
159 definitions, and most of the code is shared. To my knowledge, this is
160 the only package supporting coinductive definitions.
161 \item Definitions may be mutually recursive.
163 The package has been implemented in Isabelle~\cite{isabelle-intro} using ZF
164 set theory \cite{paulson-set-I,paulson-set-II}; part of it has since been
165 ported to Isabelle's higher-order logic. However, the fixedpoint approach is
166 independent of Isabelle. The recursion equations are specified as
167 introduction rules for the mutually recursive sets. The package transforms
168 these rules into a mapping over sets, and attempts to prove that the
169 mapping is monotonic and well-typed. If successful, the package makes
170 fixedpoint definitions and proves the introduction, elimination and
171 (co)induction rules. The package consists of several Standard ML
172 functors~\cite{paulson91}; it accepts its argument and returns its result
173 as ML structures.\footnote{This use of ML modules is not essential; the
174 package could also be implemented as a function on records.}
176 Most datatype packages equip the new datatype with some means of expressing
177 recursive functions. This is the main omission from my package. Its
178 fixedpoint operators define only recursive sets. To define recursive
179 functions, the Isabelle/ZF theory provides well-founded recursion and other
180 logical tools~\cite{paulson-set-II}.
182 {\bf Outline.} Section~2 introduces the least and greatest fixedpoint
183 operators. Section~3 discusses the form of introduction rules, mutual
184 recursion and other points common to inductive and coinductive definitions.
185 Section~4 discusses induction and coinduction rules separately. Section~5
186 presents several examples, including a coinductive definition. Section~6
187 describes datatype definitions. Section~7 presents related work.
188 Section~8 draws brief conclusions. \ifCADE\else The appendices are simple
189 user's manuals for this Isabelle package.\fi
191 Most of the definitions and theorems shown below have been generated by the
192 package. I have renamed some variables to improve readability.
194 \section{Fixedpoint operators}
195 In set theory, the least and greatest fixedpoint operators are defined as
198 \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
199 \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\}
201 Let $D$ be a set. Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and
202 {\bf monotone below~$D$} if
203 $h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is
204 bounded by~$D$ and monotone then both operators yield fixedpoints:
206 \lfp(D,h) & = & h(\lfp(D,h)) \\
207 \gfp(D,h) & = & h(\gfp(D,h))
209 These equations are instances of the Knaster-Tarski Theorem, which states
210 that every monotonic function over a complete lattice has a
211 fixedpoint~\cite{davey&priestley}. It is obvious from their definitions
212 that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
214 This fixedpoint theory is simple. The Knaster-Tarski Theorem is easy to
215 prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must
216 also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as
217 when a set of `theorems' is (co)inductively defined over some previously
218 existing set of `formulae.' Isabelle/ZF provides a suitable bounding set
219 for finitely branching (co)datatype definitions; see~\S\ref{univ-sec}
220 below. Bounding sets are also called {\bf domains}.
222 The powerset operator is monotone, but by Cantor's Theorem there is no
223 set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because
224 there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates
225 that~$\pow$ is still useful in inductive definitions.
227 \section{Elements of an inductive or coinductive definition}\label{basic-sec}
228 Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
229 mutual recursion. They will be constructed from domains $D_1$,
230 \ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but
231 $R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$
232 under an injection. Reasons for this are discussed
233 elsewhere~\cite[\S4.5]{paulson-set-II}.
235 The definition may involve arbitrary parameters $\vec{p}=p_1$,
236 \ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The
237 parameters must be identical every time they occur within a definition. This
238 would appear to be a serious restriction compared with other systems such as
239 Coq~\cite{paulin92}. For instance, we cannot define the lists of
240 $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
241 varies. Section~\ref{listn-sec} describes how to express this set using the
242 inductive definition package.
244 To avoid clutter below, the recursive sets are shown as simply $R_i$
245 instead of $R_i(\vec{p})$.
247 \subsection{The form of the introduction rules}\label{intro-sec}
248 The body of the definition consists of the desired introduction rules,
249 specified as strings. The conclusion of each rule must have the form $t\in
250 R_i$, where $t$ is any term. Premises typically have the same form, but
251 they can have the more general form $t\in M(R_i)$ or express arbitrary
254 The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
255 sets, satisfying the rule
256 \[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
257 The user must supply the package with monotonicity rules for all such premises.
259 The ability to introduce new monotone operators makes the approach
260 flexible. A suitable choice of~$M$ and~$t$ can express a lot. The
261 powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$
262 expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The `list of'
263 operator is monotone, as is easily proved by induction. The premise
264 $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual
265 recursion; see \S\ref{primrec-sec} and also my earlier
266 paper~\cite[\S4.4]{paulson-set-II}.
268 Introduction rules may also contain {\bf side-conditions}. These are
269 premises consisting of arbitrary formulae not mentioning the recursive
270 sets. Side-conditions typically involve type-checking. One example is the
271 premise $a\in A$ in the following rule from the definition of lists:
272 \[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
274 \subsection{The fixedpoint definitions}
275 The package translates the list of desired introduction rules into a fixedpoint
276 definition. Consider, as a running example, the finite powerset operator
277 $\Fin(A)$: the set of all finite subsets of~$A$. It can be
278 defined as the least set closed under the rules
279 \[ \emptyset\in\Fin(A) \qquad
280 \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)}
283 The domain in a (co)inductive definition must be some existing set closed
284 under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
285 subsets of~$A$. The package generates the definition
287 \Fin(A) & \equiv & \lfp(\pow(A), \;
288 \begin{array}[t]{r@{\,}l}
289 \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
290 &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
293 The contribution of each rule to the definition of $\Fin(A)$ should be
294 obvious. A coinductive definition is similar but uses $\gfp$ instead
297 The package must prove that the fixedpoint operator is applied to a
298 monotonic function. If the introduction rules have the form described
299 above, and if the package is supplied a monotonicity theorem for every
300 $t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
301 presence of logical connectives in the fixedpoint's body, the
302 monotonicity proof requires some unusual rules. These state that the
303 connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
304 to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
305 only if $\forall x.P(x)\imp Q(x)$.}
307 The package returns its result as an ML structure, which consists of named
308 components; we may regard it as a record. The result structure contains
309 the definitions of the recursive sets as a theorem list called {\tt defs}.
310 It also contains, as the theorem {\tt unfold}, a fixedpoint equation such
314 \begin{array}[t]{r@{\,}l}
315 \{z\in\pow(A). & z=\emptyset \disj{} \\
316 &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
319 It also contains, as the theorem {\tt dom\_subset}, an inclusion such as
320 $\Fin(A)\sbs\pow(A)$.
323 \subsection{Mutual recursion} \label{mutual-sec}
324 In a mutually recursive definition, the domain of the fixedpoint construction
325 is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
326 \ldots,~$n$. The package uses the injections of the
327 binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
328 $h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
330 As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/ZF defines the
331 operator $\Part$ to support mutual recursion. The set $\Part(A,h)$
332 contains those elements of~$A$ having the form~$h(z)$:
334 \Part(A,h) & \equiv & \{x\in A. \exists z. x=h(z)\}.
336 For mutually recursive sets $R_1$, \ldots,~$R_n$ with
337 $n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using
338 a fixedpoint operator. The remaining $n$ definitions have the form
340 R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n.
342 It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
345 \subsection{Proving the introduction rules}
346 The user supplies the package with the desired form of the introduction
347 rules. Once it has derived the theorem {\tt unfold}, it attempts
348 to prove those rules. From the user's point of view, this is the
349 trickiest stage; the proofs often fail. The task is to show that the domain
350 $D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
351 closed under all the introduction rules. This essentially involves replacing
352 each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
353 attempting to prove the result.
355 Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$
356 in the rules, the package must prove
357 \[ \emptyset\in\pow(A) \qquad
358 \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)}
360 Such proofs can be regarded as type-checking the definition.\footnote{The
361 Isabelle/HOL version does not require these proofs, as HOL has implicit
362 type-checking.} The user supplies the package with type-checking rules to
363 apply. Usually these are general purpose rules from the ZF theory. They
364 could however be rules specifically proved for a particular inductive
365 definition; sometimes this is the easiest way to get the definition
368 The result structure contains the introduction rules as the theorem list {\tt
371 \subsection{The case analysis rule}
372 The elimination rule, called {\tt elim}, performs case analysis. There is one
373 case for each introduction rule. The elimination rule
375 \[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
376 & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
378 The subscripted variables $a$ and~$b$ above the third premise are
379 eigenvariables, subject to the usual `not free in \ldots' proviso.
380 The rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else
381 $x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence
384 The package also returns a function for generating simplified instances of
385 the case analysis rule. It works for datatypes and for inductive
386 definitions involving datatypes, such as an inductively defined relation
387 between lists. It instantiates {\tt elim} with a user-supplied term then
388 simplifies the cases using freeness of the underlying datatype. The
389 simplified rules perform `rule inversion' on the inductive definition.
390 Section~\S\ref{mkcases} presents an example.
393 \section{Induction and coinduction rules}
394 Here we must consider inductive and coinductive definitions separately.
395 For an inductive definition, the package returns an induction rule derived
396 directly from the properties of least fixedpoints, as well as a modified
397 rule for mutual recursion and inductively defined relations. For a
398 coinductive definition, the package returns a basic coinduction rule.
400 \subsection{The basic induction rule}\label{basic-ind-sec}
401 The basic rule, called {\tt induct}, is appropriate in most situations.
402 For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
403 datatype definitions (see below), it is just structural induction.
405 The induction rule for an inductively defined set~$R$ has the following form.
406 The major premise is $x\in R$. There is a minor premise for each
409 \item If the introduction rule concludes $t\in R_i$, then the minor premise
412 \item The minor premise's eigenvariables are precisely the introduction
413 rule's free variables that are not parameters of~$R$. For instance, the
414 eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
416 \item If the introduction rule has a premise $t\in R_i$, then the minor
417 premise discharges the assumption $t\in R_i$ and the induction
418 hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$
419 then the minor premise discharges the single assumption
420 \[ t\in M(\{z\in R_i. P(z)\}). \]
421 Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The
422 occurrence of $P$ gives the effect of an induction hypothesis, which may be
423 exploited by appealing to properties of~$M$.
425 The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
426 but includes an induction hypothesis:
427 \[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
428 & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
430 Stronger induction rules often suggest themselves. We can derive a rule
431 for $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in
432 b$. The Isabelle/ZF theory defines the {\bf rank} of a
433 set~\cite[\S3.4]{paulson-set-II}, which supports well-founded induction and
434 recursion over datatypes. The package proves a rule for mutual induction
435 and inductive relations.
437 \subsection{Mutual induction}
438 The mutual induction rule is called {\tt
439 mutual\_induct}. It differs from the basic rule in several respects:
441 \item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
442 \ldots,~$P_n$: one for each recursive set.
444 \item There is no major premise such as $x\in R_i$. Instead, the conclusion
445 refers to all the recursive sets:
446 \[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
447 (\forall z.z\in R_n\imp P_n(z))
449 Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
452 \item If the domain of some $R_i$ is the Cartesian product
453 $A_1\times\cdots\times A_m$ (associated to the right), then the
454 corresponding predicate $P_i$ takes $m$ arguments and the corresponding
455 conjunct of the conclusion is
456 \[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m))
459 The last point above simplifies reasoning about inductively defined
460 relations. It eliminates the need to express properties of $z_1$,
461 \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
463 \subsection{Coinduction}\label{coind-sec}
464 A coinductive definition yields a primitive coinduction rule, with no
465 refinements such as those for the induction rules. (Experience may suggest
466 refinements later.) Consider the codatatype of lazy lists as an example. For
467 suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
468 greatest fixedpoint satisfying the rules
469 \[ \LNil\in\llist(A) \qquad
470 \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
472 The $(-)$ tag stresses that this is a coinductive definition. A suitable
473 domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of
474 sum and product for representing infinite data structures
475 (see~\S\ref{univ-sec}). Coinductive definitions use these variant sums and
478 The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$.
479 Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
480 is the greatest solution to this equation contained in $\quniv(A)$:
481 \[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
482 \infer*{z=\LNil\disj \bigl(\exists a\,l.\,
483 z=\LCons(a,l) \conj a\in A \conj l\in X\un\llist(A) \bigr)}
485 % \begin{array}[t]{@{}l}
486 % z=\LCons(a,l) \conj a\in A \conj{}\\
487 % l\in X\un\llist(A) \bigr)
488 % \end{array} }{[z\in X]_z}}
490 This rule complements the introduction rules; it provides a means of showing
491 $x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then
492 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$
493 is the set of natural numbers.)
495 Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
496 represents a slight strengthening of the greatest fixedpoint property. I
497 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
500 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
501 This section presents several examples: the finite powerset operator,
502 lists of $n$ elements, bisimulations on lazy lists, the well-founded part
503 of a relation, and the primitive recursive functions.
505 \subsection{The finite powerset operator}
506 This operator has been discussed extensively above. Here is the
507 corresponding invocation in an Isabelle theory file. Note that
508 $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF.
513 domains "Fin(A)" <= "Pow(A)"
516 consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
517 type_intrs "[empty_subsetI, cons_subsetI, PowI]"
518 type_elims "[make_elim PowD]"
521 Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
522 unary function symbol~$\Fin$, which is defined inductively. Its domain is
523 specified as $\pow(A)$, where $A$ is the parameter appearing in the
524 introduction rules. For type-checking, we supply two introduction
526 \[ \emptyset\sbs A \qquad
527 \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
529 A further introduction rule and an elimination rule express the two
530 directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking
531 involves mostly introduction rules.
533 Like all Isabelle theory files, this one yields a structure containing the
534 new theory as an \ML{} value. Structure {\tt Finite} also has a
535 substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we
536 can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
537 or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
538 rule is {\tt Fin.induct}.
541 \subsection{Lists of $n$ elements}\label{listn-sec}
542 This has become a standard example of an inductive definition. Following
543 Paulin-Mohring~\cite{paulin92}, we could attempt to define a new datatype
544 $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
545 But her introduction rules
546 \[ \hbox{\tt Niln}\in\listn(A,0) \qquad
547 \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
548 {n\in\nat & a\in A & l\in\listn(A,n)}
550 are not acceptable to the inductive definition package:
551 $\listn$ occurs with three different parameter lists in the definition.
553 The Isabelle version of this example suggests a general treatment of
554 varying parameters. Here, we use the existing datatype definition of
555 $\lst(A)$, with constructors $\Nil$ and~$\Cons$. Then incorporate the
556 parameter~$n$ into the inductive set itself, defining $\listn(A)$ as a
557 relation. It consists of pairs $\pair{n,l}$ such that $n\in\nat$
558 and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the
559 converse of the length function on~$\lst(A)$. The Isabelle/ZF introduction
561 \[ \pair{0,\Nil}\in\listn(A) \qquad
562 \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
563 {a\in A & \pair{n,l}\in\listn(A)}
565 The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
566 We declare the constant~$\listn$ and supply an inductive definition,
567 specifying the domain as $\nat\times\lst(A)$:
570 consts listn ::"i=>i"
572 domains "listn(A)" <= "nat*list(A)"
574 NilI "<0,Nil> : listn(A)"
575 ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
576 type_intrs "nat_typechecks @ list.intrs"
579 The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
580 Because $\listn(A)$ is a set of pairs, type-checking requires the
581 equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$; the
582 package always includes the necessary rules.
584 The package returns introduction, elimination and induction rules for
585 $\listn$. The basic induction rule, {\tt ListN.induct}, is
586 \[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) &
587 \infer*{P(\pair{\succ(n),\Cons(a,l)})}
588 {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}}
590 This rule requires the induction formula to be a
591 unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt
592 ListN.mutual\_induct}, uses a binary property instead:
593 \[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)}
595 \infer*{P(\succ(n),\Cons(a,l))}
596 {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
598 It is now a simple matter to prove theorems about $\listn(A)$, such as
599 \[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
600 \[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
601 This latter result --- here $r``X$ denotes the image of $X$ under $r$
602 --- asserts that the inductive definition agrees with the obvious notion of
605 Unlike in Coq, the definition does not declare a new datatype. A `list of
606 $n$ elements' really is a list and is subject to list operators such
607 as append (concatenation). For example, a trivial induction on
608 $\pair{m,l}\in\listn(A)$ yields
609 \[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)}
610 {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)}
612 where $+$ here denotes addition on the natural numbers and @ denotes append.
614 \subsection{A demonstration of rule inversion}\label{mkcases}
615 The elimination rule, {\tt ListN.elim}, is cumbersome:
616 \[ \infer{Q}{x\in\listn(A) &
617 \infer*{Q}{[x = \pair{0,\Nil}]} &
619 {\left[\begin{array}{l}
620 x = \pair{\succ(n),\Cons(a,l)} \\
622 \pair{n,l}\in\listn(A)
623 \end{array} \right]_{a,l,n}}}
625 The ML function {\tt ListN.mk\_cases} generates simplified instances of
626 this rule. It works by freeness reasoning on the list constructors:
627 $\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If
628 $x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases}
629 deduces the corresponding form of~$i$; this is called rule inversion. For
632 ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)"
634 yields a rule with only two premises:
635 \[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) &
637 {\left[\begin{array}{l}
638 i = \succ(n) \\ a\in A \\ \pair{n,l}\in\listn(A)
639 \end{array} \right]_{n}}}
641 The package also has built-in rules for freeness reasoning about $0$
642 and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
643 ListN.mk\_cases} can similarly deduce the corresponding form of~$l$.
645 The function {\tt mk\_cases} is also useful with datatype definitions. The
646 instance from the definition of lists, namely {\tt List.mk\_cases}, can
648 \[ \infer{Q}{\Cons(a,l)\in\lst(A) &
649 & \infer*{Q}{[a\in A &l\in\lst(A)]} }
651 A typical use of {\tt mk\_cases} concerns inductive definitions of
652 evaluation relations. Then rule inversion yields case analysis on possible
653 evaluations. For example, the Isabelle/ZF theory includes a short proof
654 of the diamond property for parallel contraction on combinators.
656 \subsection{A coinductive definition: bisimulations on lazy lists}
657 This example anticipates the definition of the codatatype $\llist(A)$, which
658 consists of finite and infinite lists over~$A$. Its constructors are $\LNil$
660 $\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.
661 Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
662 pairing and injection operators, it contains non-well-founded elements such as
663 solutions to $\LCons(a,l)=l$.
665 The next step in the development of lazy lists is to define a coinduction
666 principle for proving equalities. This is done by showing that the equality
667 relation on lazy lists is the greatest fixedpoint of some monotonic
668 operation. The usual approach~\cite{pitts94} is to define some notion of
669 bisimulation for lazy lists, define equivalence to be the greatest
670 bisimulation, and finally to prove that two lazy lists are equivalent if and
671 only if they are equal. The coinduction rule for equivalence then yields a
672 coinduction principle for equalities.
674 A binary relation $R$ on lazy lists is a {\bf bisimulation} provided $R\sbs
675 R^+$, where $R^+$ is the relation
676 \[ \{\pair{\LNil,\LNil}\} \un
677 \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
680 A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation.
681 Equivalence can be coinductively defined as the greatest fixedpoint for the
683 \[ \pair{\LNil,\LNil} \in\lleq(A) \qquad
684 \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
685 {a\in A & \pair{l,l'}\in \lleq(A)}
687 To make this coinductive definition, the theory file includes (after the
688 declaration of $\llist(A)$) the following lines:
690 consts lleq :: "i=>i"
692 domains "lleq(A)" <= "llist(A) * llist(A)"
694 LNil "<LNil, LNil> : lleq(A)"
695 LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
696 type_intrs "llist.intrs"
698 Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory.
699 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking
700 rules include the introduction rules for $\llist(A)$, whose
701 declaration is discussed below (\S\ref{lists-sec}).
703 The package returns the introduction rules and the elimination rule, as
704 usual. But instead of induction rules, it returns a coinduction rule.
705 The rule is too big to display in the usual notation; its conclusion is
706 $x\in\lleq(A)$ and its premises are $x\in X$,
707 ${X\sbs\llist(A)\times\llist(A)}$ and
708 \[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
709 z=\pair{\LCons(a,l),\LCons(a,l')} \conj
710 a\in A \conj\pair{l,l'}\in X\un\lleq(A) \bigr)
711 % \begin{array}[t]{@{}l}
712 % z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
713 % \pair{l,l'}\in X\un\lleq(A) \bigr)
717 Thus if $x\in X$, where $X$ is a bisimulation contained in the
718 domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that
719 $\lleq(A)$ is reflexive: the equality relation is a bisimulation. And
720 $\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that
721 $\lleq(A)$ coincides with the equality relation takes some work.
723 \subsection{The accessible part of a relation}\label{acc-sec}
724 Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
725 The {\bf accessible} or {\bf well-founded} part of~$\prec$, written
726 $\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
727 no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is
728 inductively defined to be the least set that contains $a$ if it contains
729 all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an
730 introduction rule of the form
731 \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
732 Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
733 difficulties for other systems. Its premise is not acceptable to the
734 inductive definition package of the Cambridge HOL
735 system~\cite{camilleri92}. It is also unacceptable to Isabelle package
736 (recall \S\ref{intro-sec}), but fortunately can be transformed into the
737 acceptable form $t\in M(R)$.
739 The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
740 $t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To
741 express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
742 term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is
743 the inverse image of~$\{a\}$ under~$\prec$.
745 The theory file below follows this approach. Here $r$ is~$\prec$ and
746 $\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a
747 relation is the union of its domain and range.) Finally $r^{-}``\{a\}$
748 denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt
749 Pow\_mono}, which asserts that $\pow$ is monotonic.
754 domains "acc(r)" <= "field(r)"
756 vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
760 The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For
761 instance, $\prec$ is well-founded if and only if its field is contained in
764 As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
765 gives rise to an unusual induction hypothesis. Let us examine the
766 induction rule, {\tt Acc.induct}:
767 \[ \infer{P(x)}{x\in\acc(r) &
768 \infer*{P(a)}{[r^{-}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) &
771 The strange induction hypothesis is equivalent to
772 $\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
773 Therefore the rule expresses well-founded induction on the accessible part
776 The use of inverse image is not essential. The Isabelle package can accept
777 introduction rules with arbitrary premises of the form $\forall
778 \vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed
780 \[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \]
781 provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The
782 following section demonstrates another use of the premise $t\in M(R)$,
785 \subsection{The primitive recursive functions}\label{primrec-sec}
786 The primitive recursive functions are traditionally defined inductively, as
787 a subset of the functions over the natural numbers. One difficulty is that
788 functions of all arities are taken together, but this is easily
789 circumvented by regarding them as functions on lists. Another difficulty,
790 the notion of composition, is less easily circumvented.
792 Here is a more precise definition. Letting $\vec{x}$ abbreviate
793 $x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
794 $[y+1,\vec{x}]$, etc. A function is {\bf primitive recursive} if it
795 belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
797 \item The {\bf successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
798 \item All {\bf constant} functions $\CONST(k)$, such that
799 $\CONST(k)[\vec{x}]=k$.
800 \item All {\bf projection} functions $\PROJ(i)$, such that
801 $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$.
802 \item All {\bf compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$,
803 where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
806 \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] & = &
807 g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]].
810 \item All {\bf recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
813 \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
814 \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
817 Composition is awkward because it combines not two functions, as is usual,
818 but $m+1$ functions. In her proof that Ackermann's function is not
819 primitive recursive, Nora Szasz was unable to formalize this definition
820 directly~\cite{szasz93}. So she generalized primitive recursion to
821 tuple-valued functions. This modified the inductive definition such that
822 each operation on primitive recursive functions combined just two functions.
832 SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
835 domains "primrec" <= "list(nat)->nat"
838 CONST "k: nat ==> CONST(k) : primrec"
839 PROJ "i: nat ==> PROJ(i) : primrec"
840 COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
841 PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
843 con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
844 type_intrs "nat_typechecks @ list.intrs @ \ttback
845 \ttback [lam_type, list_case_type, drop_type, map_type, \ttback
846 \ttback apply_type, rec_type]"
850 \caption{Inductive definition of the primitive recursive functions}
854 Szasz was using ALF, but Coq and HOL would also have problems accepting
855 this definition. Isabelle's package accepts it easily since
856 $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
857 $\lst$ is monotonic. There are five introduction rules, one for each of
858 the five forms of primitive recursive function. Let us examine the one for
860 \[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
861 The induction rule for $\primrec$ has one case for each introduction rule.
862 Due to the use of $\lst$ as a monotone operator, the composition case has
863 an unusual induction hypothesis:
864 \[ \infer*{P(\COMP(g,\fs))}
865 {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} \]
866 The hypothesis states that $\fs$ is a list of primitive recursive functions
867 satisfying the induction formula. Proving the $\COMP$ case typically requires
868 structural induction on lists, yielding two subcases: either $\fs=\Nil$ or
869 else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and $\fs'$ is
870 another list of primitive recursive functions satisfying~$P$.
872 Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec}
873 defines the constants $\SC$, $\CONST$, etc. These are not constructors of
874 a new datatype, but functions over lists of numbers. Their definitions,
875 most of which are omitted, consist of routine list programming. In
876 Isabelle/ZF, the primitive recursive functions are defined as a subset of
877 the function set $\lst(\nat)\to\nat$.
879 The Isabelle theory goes on to formalize Ackermann's function and prove
880 that it is not primitive recursive, using the induction rule {\tt
881 Primrec.induct}. The proof follows Szasz's excellent account.
884 \section{Datatypes and codatatypes}\label{data-sec}
885 A (co)datatype definition is a (co)inductive definition with automatically
886 defined constructors and a case analysis operator. The package proves that
887 the case operator inverts the constructors and can prove freeness theorems
888 involving any pair of constructors.
891 \subsection{Constructors and their domain}\label{univ-sec}
892 Conceptually, our two forms of definition are distinct. A (co)inductive
893 definition selects a subset of an existing set; a (co)datatype definition
894 creates a new set. But the package reduces the latter to the former. A
895 set having strong closure properties must serve as the domain of the
896 (co)inductive definition. Constructing this set requires some theoretical
897 effort, which must be done anyway to show that (co)datatypes exist. It is
898 not obvious that standard set theory is suitable for defining codatatypes.
900 Isabelle/ZF defines the standard notion of Cartesian product $A\times B$,
901 containing ordered pairs $\pair{a,b}$. Now the $m$-tuple
902 $\pair{x_1,\ldots,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply
903 $x_1$ if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.
904 Isabelle/ZF also defines the disjoint sum $A+B$, containing injections
905 $\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$.
907 A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be
908 $h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
909 In a mutually recursive definition, all constructors for the set~$R_i$ have
910 the outer form~$h_{in}$, where $h_{in}$ is the injection described
911 in~\S\ref{mutual-sec}. Further nested injections ensure that the
912 constructors for~$R_i$ are pairwise distinct.
914 Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and
915 furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
916 $b\in\univ(A)$. In a typical datatype definition with set parameters
917 $A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
918 $\univ(A_1\un\cdots\un A_k)$. This solves the problem for
919 datatypes~\cite[\S4.2]{paulson-set-II}.
921 The standard pairs and injections can only yield well-founded
922 constructions. This eases the (manual!) definition of recursive functions
923 over datatypes. But they are unsuitable for codatatypes, which typically
924 contain non-well-founded objects.
926 To support codatatypes, Isabelle/ZF defines a variant notion of ordered
927 pair, written~$\pair{a;b}$. It also defines the corresponding variant
928 notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
929 and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines
930 the set $\quniv(A)$, which contains~$A$ and furthermore contains
931 $\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a
932 typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a
933 suitable domain is $\quniv(A_1\un\cdots\un A_k)$. This approach using
934 standard ZF set theory~\cite{paulson-final} is an alternative to adopting
935 Aczel's Anti-Foundation Axiom~\cite{aczel88}.
937 \subsection{The case analysis operator}
938 The (co)datatype package automatically defines a case analysis operator,
939 called {\tt$R$\_case}. A mutually recursive definition still has only one
940 operator, whose name combines those of the recursive sets: it is called
941 {\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those
942 for products and sums.
944 Datatype definitions employ standard products and sums, whose operators are
945 $\split$ and $\case$ and satisfy the equations
947 \split(f,\pair{x,y}) & = & f(x,y) \\
948 \case(f,g,\Inl(x)) & = & f(x) \\
949 \case(f,g,\Inr(y)) & = & g(y)
951 Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then
952 its case operator takes $k+1$ arguments and satisfies an equation for each
955 R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) & = & f_i(\vec{x}),
956 \qquad i = 1, \ldots, k
958 The case operator's definition takes advantage of Isabelle's representation
959 of syntax in the typed $\lambda$-calculus; it could readily be adapted to a
960 theorem prover for higher-order logic. If $f$ and~$g$ have meta-type
961 $i\To i$ then so do $\split(f)$ and
962 $\case(f,g)$. This works because $\split$ and $\case$ operate on their last
963 argument. They are easily combined to make complex case analysis
964 operators. Here are two examples:
966 \item $\split(\lambda x.\split(f(x)))$ performs case analysis for
967 $A\times (B\times C)$, as is easily verified:
969 \split(\lambda x.\split(f(x)), \pair{a,b,c})
970 & = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\
971 & = & \split(f(a), \pair{b,c}) \\
975 \item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us
976 verify one of the three equations:
978 \case(f,\case(g,h), \Inr(\Inl(b)))
979 & = & \case(g,h,\Inl(b)) \\
983 Codatatype definitions are treated in precisely the same way. They express
984 case operators using those for the variant products and sums, namely
985 $\qsplit$ and~$\qcase$.
989 \ifCADE The package has processed all the datatypes discussed in
990 my earlier paper~\cite{paulson-set-II} and the codatatype of lazy lists.
991 Space limitations preclude discussing these examples here, but they are
992 distributed with Isabelle. \typeout{****Omitting datatype examples from
995 To see how constructors and the case analysis operator are defined, let us
996 examine some examples. These include lists and trees/forests, which I have
997 discussed extensively in another paper~\cite{paulson-set-II}.
1000 \subsection{Example: lists and lazy lists}\label{lists-sec}
1001 Here is a theory file that declares the datatype of lists:
1004 consts list :: "i=>i"
1005 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
1008 And here is the theory file that declares the codatatype of lazy lists:
1011 consts llist :: "i=>i"
1012 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
1015 They highlight the (many) similarities and (few) differences between
1016 datatype and codatatype definitions.\footnote{The real theory files contain
1017 many more declarations, mainly of functions over lists; the declaration
1018 of lazy lists is followed by the coinductive definition of lazy list
1021 Each form of list has two constructors, one for the empty list and one for
1022 adding an element to a list. Each takes a parameter, defining the set of
1023 lists over a given set~$A$. Each uses the appropriate domain from a
1026 \item $\lst(A)$ requires the parent theory {\tt Univ}. The package
1027 automatically uses the domain $\univ(A)$ (the default choice can be
1030 \item $\llist(A)$ requires the parent theory {\tt QUniv}. The package
1031 automatically uses the domain $\quniv(A)$.
1034 Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
1036 \[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
1037 & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
1039 Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this,
1040 Isabelle/ZF defines the rank of a set and proves that the standard pairs and
1041 injections have greater rank than their components. An immediate consequence,
1042 which justifies structural recursion on lists \cite[\S4.3]{paulson-set-II},
1044 \[ \rank(l) < \rank(\Cons(a,l)). \]
1046 Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has
1047 the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and
1048 injections are monotonic and need not have greater rank than their
1049 components, fixedpoint operators can create cyclic constructions. For
1050 example, the definition
1052 \lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l))
1054 yields $\lconst(a) = \LCons(a,\lconst(a))$.
1057 It may be instructive to examine the definitions of the constructors and
1058 case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar.
1059 The list constructors are defined as follows:
1061 \Nil & = & \Inl(\emptyset) \\
1062 \Cons(a,l) & = & \Inr(\pair{a,l})
1064 The operator $\lstcase$ performs case analysis on these two alternatives:
1066 \lstcase(c,h) & \equiv & \case(\lambda u.c, \split(h))
1068 Let us verify the two equations:
1070 \lstcase(c, h, \Nil) & = &
1071 \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
1072 & = & (\lambda u.c)(\emptyset) \\
1074 \lstcase(c, h, \Cons(x,y)) & = &
1075 \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
1076 & = & \split(h, \pair{x,y}) \\
1081 \subsection{Example: mutual recursion}
1082 In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
1083 have the one constructor $\Tcons$, while forests have the two constructors
1084 $\Fnil$ and~$\Fcons$:
1087 consts tree, forest, tree_forest :: "i=>i"
1088 datatype "tree(A)" = Tcons ("a: A", "f: forest(A)")
1089 and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
1092 The three introduction rules define the mutual recursion. The
1093 distinguishing feature of this example is its two induction rules.
1095 The basic induction rule is called {\tt TF.induct}:
1096 \[ \infer{P(x)}{x\in\TF(A) &
1097 \infer*{P(\Tcons(a,f))}
1098 {\left[\begin{array}{l} a\in A \\
1099 f\in\forest(A) \\ P(f)
1103 & \infer*{P(\Fcons(t,f))}
1104 {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
1105 f\in\forest(A) \\ P(f)
1109 This rule establishes a single predicate for $\TF(A)$, the union of the
1112 Although such reasoning is sometimes useful
1113 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
1114 separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this
1115 rule {\tt TF.mutual\_induct}. Observe the usage of $P$ and $Q$ in the
1116 induction hypotheses:
1117 \[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
1118 (\forall z. z\in\forest(A)\imp Q(z))}
1119 {\infer*{P(\Tcons(a,f))}
1120 {\left[\begin{array}{l} a\in A \\
1121 f\in\forest(A) \\ Q(f)
1125 & \infer*{Q(\Fcons(t,f))}
1126 {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
1127 f\in\forest(A) \\ Q(f)
1131 As mentioned above, the package does not define a structural recursion
1132 operator. I have described elsewhere how this is done
1133 \cite[\S4.5]{paulson-set-II}.
1135 Both forest constructors have the form $\Inr(\cdots)$,
1136 while the tree constructor has the form $\Inl(\cdots)$. This pattern would
1137 hold regardless of how many tree or forest constructors there were.
1139 \Tcons(a,l) & = & \Inl(\pair{a,l}) \\
1140 \Fnil & = & \Inr(\Inl(\emptyset)) \\
1141 \Fcons(a,l) & = & \Inr(\Inr(\pair{a,l}))
1143 There is only one case operator; it works on the union of the trees and
1146 {\tt tree\_forest\_case}(f,c,g) & \equiv &
1147 \case(\split(f),\, \case(\lambda u.c, \split(g)))
1151 \subsection{A four-constructor datatype}
1152 Finally let us consider a fairly general datatype. It has four
1153 constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities.
1156 consts data :: "[i,i] => i"
1157 datatype "data(A,B)" = Con0
1159 | Con2 ("a: A", "b: B")
1160 | Con3 ("a: A", "b: B", "d: data(A,B)")
1163 Because this datatype has two set parameters, $A$ and~$B$, the package
1164 automatically supplies $\univ(A\un B)$ as its domain. The structural
1165 induction rule has four minor premises, one per constructor:
1166 \[ \infer{P(x)}{x\in\data(A,B) &
1168 \infer*{P(\Con_1(a))}{[a\in A]_a} &
1169 \infer*{P(\Con_2(a,b))}
1170 {\left[\begin{array}{l} a\in A \\ b\in B \end{array}
1172 \infer*{P(\Con_3(a,b,d))}
1173 {\left[\begin{array}{l} a\in A \\ b\in B \\
1174 d\in\data(A,B) \\ P(d)
1179 The constructor definitions are
1181 \Con_0 & = & \Inl(\Inl(\emptyset)) \\
1182 \Con_1(a) & = & \Inl(\Inr(a)) \\
1183 \Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\
1184 \Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})).
1186 The case operator is
1188 {\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv &
1189 \case(\begin{array}[t]{@{}l}
1190 \case(\lambda u.f_0,\; f_1),\, \\
1191 \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
1194 This may look cryptic, but the case equations are trivial to verify.
1196 In the constructor definitions, the injections are balanced. A more naive
1197 approach is to define $\Con_3(a,b,c)$ as
1198 $\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two
1199 injections. The difference here is small. But the ZF examples include a
1200 60-element enumeration type, where each constructor has 5 or~6 injections.
1201 The naive approach would require 1 to~59 injections; the definitions would be
1202 quadratic in size. It is like the difference between the binary and unary
1205 The result structure contains the case operator and constructor definitions as
1206 the theorem list \verb|con_defs|. It contains the case equations, such as
1208 {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c),
1210 as the theorem list \verb|case_eqns|. There is one equation per constructor.
1212 \subsection{Proving freeness theorems}
1213 There are two kinds of freeness theorems:
1215 \item {\bf injectiveness} theorems, such as
1216 \[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
1218 \item {\bf distinctness} theorems, such as
1219 \[ \Con_1(a) \not= \Con_2(a',b') \]
1221 Since the number of such theorems is quadratic in the number of constructors,
1222 the package does not attempt to prove them all. Instead it returns tools for
1223 proving desired theorems --- either explicitly or `on the fly' during
1224 simplification or classical reasoning.
1226 The theorem list \verb|free_iffs| enables the simplifier to perform freeness
1227 reasoning. This works by incremental unfolding of constructors that appear in
1228 equations. The theorem list contains logical equivalences such as
1230 \Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\
1231 \Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\
1233 \Inl(a)=\Inl(b) & \bimp & a=b \\
1234 \Inl(a)=\Inr(b) & \bimp & {\tt False} \\
1235 \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
1237 For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
1239 The theorem list \verb|free_SEs| enables the classical
1240 reasoner to perform similar replacements. It consists of elimination rules
1241 to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
1244 Such incremental unfolding combines freeness reasoning with other proof
1245 steps. It has the unfortunate side-effect of unfolding definitions of
1246 constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
1247 be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs}
1248 restores the defined constants.
1251 \section{Related work}\label{related}
1252 The use of least fixedpoints to express inductive definitions seems
1253 obvious. Why, then, has this technique so seldom been implemented?
1255 Most automated logics can only express inductive definitions by asserting
1256 new axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if
1257 their shell principle were removed. With ALF the situation is more
1258 complex; earlier versions of Martin-L\"of's type theory could (using
1259 wellordering types) express datatype definitions, but the version
1260 underlying ALF requires new rules for each definition~\cite{dybjer91}.
1261 With Coq the situation is subtler still; its underlying Calculus of
1262 Constructions can express inductive definitions~\cite{huet88}, but cannot
1263 quite handle datatype definitions~\cite{paulin92}. It seems that
1264 researchers tried hard to circumvent these problems before finally
1265 extending the Calculus with rule schemes for strictly positive operators.
1267 Higher-order logic can express inductive definitions through quantification
1268 over unary predicates. The following formula expresses that~$i$ belongs to the
1269 least set containing~0 and closed under~$\succ$:
1270 \[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \]
1271 This technique can be used to prove the Knaster-Tarski Theorem, but it is
1272 little used in the Cambridge HOL system. Melham~\cite{melham89} clearly
1273 describes the development. The natural numbers are defined as shown above,
1274 but lists are defined as functions over the natural numbers. Unlabelled
1275 trees are defined using G\"odel numbering; a labelled tree consists of an
1276 unlabelled tree paired with a list of labels. Melham's datatype package
1277 expresses the user's datatypes in terms of labelled trees. It has been
1278 highly successful, but a fixedpoint approach might have yielded greater
1279 functionality with less effort.
1281 Melham's inductive definition package~\cite{camilleri92} uses
1282 quantification over predicates, which is implicitly a fixedpoint approach.
1283 Instead of formalizing the notion of monotone function, it requires
1284 definitions to consist of finitary rules, a syntactic form that excludes
1285 many monotone inductive definitions.
1287 The earliest use of least fixedpoints is probably Robin Milner's datatype
1288 package for Edinburgh LCF~\cite{milner-ind}. Brian Monahan extended this
1289 package considerably~\cite{monahan84}, as did I in unpublished
1290 work.\footnote{The datatype package described in my LCF
1291 book~\cite{paulson87} does {\it not\/} make definitions, but merely
1293 LCF is a first-order logic of domain theory; the relevant fixedpoint
1294 theorem is not Knaster-Tarski but concerns fixedpoints of continuous
1295 functions over domains. LCF is too weak to express recursive predicates.
1296 Thus it would appear that the Isabelle package is the first to be based
1297 on the Knaster-Tarski Theorem.
1300 \section{Conclusions and future work}
1301 Higher-order logic and set theory are both powerful enough to express
1302 inductive definitions. A growing number of theorem provers implement one
1303 of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive
1304 definition package to write is one that asserts new axioms, not one that
1305 makes definitions and proves theorems about them. But asserting axioms
1306 could introduce unsoundness.
1308 The fixedpoint approach makes it fairly easy to implement a package for
1309 (co)inductive definitions that does not assert axioms. It is efficient: it
1310 processes most definitions in seconds and even a 60-constructor datatype
1311 requires only two minutes. It is also simple: the package consists of
1312 under 1100 lines (35K bytes) of Standard ML code. The first working
1313 version took under a week to code.
1315 In set theory, care is required to ensure that the inductive definition
1316 yields a set (rather than a proper class). This problem is inherent to set
1317 theory, whether or not the Knaster-Tarski Theorem is employed. We must
1318 exhibit a bounding set (called a domain above). For inductive definitions,
1319 this is often trivial. For datatype definitions, I have had to formalize
1320 much set theory. To justify infinitely branching datatype definitions, I
1321 have had to develop a theory of cardinal arithmetic, such as the theorem
1322 that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for
1323 all $\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
1324 The need for such efforts is not a drawback of the fixedpoint
1325 approach, for the alternative is to take such definitions on faith.
1327 The approach is not restricted to set theory. It should be suitable for
1328 any logic that has some notion of set and the Knaster-Tarski Theorem. I
1329 have ported the (co)inductive definition package from Isabelle/ZF to
1330 Isabelle/HOL (higher-order logic). I hope to port the (co)datatype package
1331 later. HOL represents sets by unary predicates; defining the corresponding
1332 types may cause complications.
1335 \bibliographystyle{springer}
1336 \bibliography{string-abbrv,atp,theory,funprog,isabelle}
1339 \ifCADE\typeout{****Omitting appendices from CADE version!}
1343 \section{Inductive and coinductive definitions: users guide}
1344 A theory file may contain any number of inductive and coinductive
1345 definitions. They may be intermixed with other declarations; in
1346 particular, the (co)inductive sets {\bf must} be declared separately as
1347 constants, and may have mixfix syntax or be subject to syntax translations.
1349 Each (co)inductive definition adds definitions to the theory and also
1350 proves some theorems. Each definition creates an ML structure, which is a
1351 substructure of the main theory structure.
1353 \subsection{The result structure}
1354 Many of the result structure's components have been discussed
1355 in~\S\ref{basic-sec}; others are self-explanatory.
1357 \item[\tt thy] is the new theory containing the recursive sets.
1359 \item[\tt defs] is the list of definitions of the recursive sets.
1361 \item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
1363 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
1364 the recursive sets, in the case of mutual recursion).
1366 \item[\tt dom\_subset] is a theorem stating inclusion in the domain.
1368 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1369 the recursive sets. The rules are also available individually, using the
1370 names given them in the theory file.
1372 \item[\tt elim] is the elimination rule.
1374 \item[\tt mk\_cases] is a function to create simplified instances of {\tt
1375 elim}, using freeness reasoning on some underlying datatype.
1378 For an inductive definition, the result structure contains two induction rules,
1379 {\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
1380 contains the rule \verb|coinduct|.
1382 Figure~\ref{def-result-fig} summarizes the two result signatures,
1383 specifying the types of all these components.
1392 val dom_subset : thm
1393 val intrs : thm list
1395 val mk_cases : thm list -> string -> thm
1396 {\it(Inductive definitions only)}
1398 val mutual_induct: thm
1399 {\it(Coinductive definitions only)}
1404 \caption{The result of a (co)inductive definition} \label{def-result-fig}
1407 \subsection{The syntax of a (co)inductive definition}
1408 An inductive definition has the form
1411 domains {\it domain declarations}
1412 intrs {\it introduction rules}
1413 monos {\it monotonicity theorems}
1414 con_defs {\it constructor definitions}
1415 type_intrs {\it introduction rules for type-checking}
1416 type_elims {\it elimination rules for type-checking}
1418 A coinductive definition is identical save that it starts with the keyword
1421 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
1422 sections are optional. If present, each is specified as a string, which
1423 must be a valid ML expression of type {\tt thm list}. It is simply
1424 inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger
1425 ML error messages. You can then inspect the file on your directory.
1428 \item[\it domain declarations] consist of one or more items of the form
1429 {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
1432 \item[\it introduction rules] specify one or more introduction rules in
1433 the form {\it ident\/}~{\it string}, where the identifier gives the name of
1434 the rule in the result structure.
1436 \item[\it monotonicity theorems] are required for each operator applied to
1437 a recursive set in the introduction rules. There {\bf must} be a theorem
1438 of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$
1439 in an introduction rule!
1441 \item[\it constructor definitions] contain definitions of constants
1442 appearing in the introduction rules. The (co)datatype package supplies
1443 the constructors' definitions here. Most (co)inductive definitions omit
1444 this section; one exception is the primitive recursive functions example
1445 (\S\ref{primrec-sec}).
1447 \item[\it type\_intrs] consists of introduction rules for type-checking the
1448 definition, as discussed in~\S\ref{basic-sec}. They are applied using
1449 depth-first search; you can trace the proof by setting
1451 \verb|trace_DEPTH_FIRST := true|.
1453 \item[\it type\_elims] consists of elimination rules for type-checking the
1454 definition. They are presumed to be `safe' and are applied as much as
1455 possible, prior to the {\tt type\_intrs} search.
1458 The package has a few notable restrictions:
1460 \item The theory must separately declare the recursive sets as
1463 \item The names of the recursive sets must be identifiers, not infix
1466 \item Side-conditions must not be conjunctions. However, an introduction rule
1467 may contain any number of side-conditions.
1469 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
1470 occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
1474 \section{Datatype and codatatype definitions: users guide}
1475 This section explains how to include (co)datatype declarations in a theory
1479 \subsection{The result structure}
1480 The result structure extends that of (co)inductive definitions
1481 (Figure~\ref{def-result-fig}) with several additional items:
1483 val con_defs : thm list
1484 val case_eqns : thm list
1485 val free_iffs : thm list
1486 val free_SEs : thm list
1487 val mk_free : string -> thm
1489 Most of these have been discussed in~\S\ref{data-sec}. Here is a summary:
1491 \item[\tt con\_defs] is a list of definitions: the case operator followed by
1492 the constructors. This theorem list can be supplied to \verb|mk_cases|, for
1495 \item[\tt case\_eqns] is a list of equations, stating that the case operator
1496 inverts each constructor.
1498 \item[\tt free\_iffs] is a list of logical equivalences to perform freeness
1499 reasoning by rewriting. A typical application has the form
1501 by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
1504 \item[\tt free\_SEs] is a list of `safe' elimination rules to perform freeness
1505 reasoning. It can be supplied to \verb|eresolve_tac| or to the classical
1508 by (fast_tac (ZF_cs addSEs free_SEs) 1);
1511 \item[\tt mk\_free] is a function to prove freeness properties, specified as
1512 strings. The theorems can be expressed in various forms, such as logical
1513 equivalences or elimination rules.
1516 The result structure also inherits everything from the underlying
1517 (co)inductive definition, such as the introduction rules, elimination rule,
1518 and (co)induction rule.
1521 \subsection{The syntax of a (co)datatype definition}
1522 A datatype definition has the form
1524 datatype <={\it domain}
1525 {\it datatype declaration} and {\it datatype declaration} and \ldots
1526 monos {\it monotonicity theorems}
1527 type_intrs {\it introduction rules for type-checking}
1528 type_elims {\it elimination rules for type-checking}
1530 A codatatype definition is identical save that it starts with the keyword
1531 {\tt codatatype}. The syntax is rather complicated; please consult the
1532 examples above (\S\ref{lists-sec}) and the theory files on the ZF source
1535 The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are
1536 optional. They are treated like their counterparts in a (co)inductive
1537 definition, as described above. The package supplements your type-checking
1538 rules (if any) with additional ones that should cope with any
1539 finitely-branching (co)datatype definition.
1542 \item[\it domain] specifies a single domain to use for all the mutually
1543 recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are
1544 omitted, the package supplies a domain automatically. Suppose the
1545 definition involves the set parameters $A_1$, \ldots, $A_k$. Then
1546 $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and
1547 $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
1549 These choices should work for all finitely-branching (co)datatype
1550 definitions. For examples of infinitely-branching datatype
1551 definitions, see the file {\tt ZF/ex/Brouwer.thy}.
1553 \item[\it datatype declaration] has the form
1555 {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}
1558 The {\it string\/} is the datatype, say {\tt"list(A)"}. Each
1559 {\it constructor\/} has the form
1561 {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}
1564 The {\it name\/} specifies a new constructor while the {\it premises\/} its
1565 typing conditions. The optional {\it mixfix\/} phrase may give
1566 the constructor infix, for example.
1568 Mutually recursive {\it datatype declarations\/} are separated by the
1573 In the definitions of the constructors, the right-hand sides may overlap.
1574 For instance, the datatype of combinators has constructors defined by
1576 {\tt K} & \equiv & \Inl(\emptyset) \\
1577 {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\
1578 p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q}))
1580 Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the
1581 longest right-hand sides are folded first.