3162

1 
\documentclass[12pt]{article}


2 
\usepackage{a4,latexsym,proof}


3 


4 
\makeatletter


5 
\input{../rail.sty}


6 
\input{../iman.sty}


7 
\input{../extra.sty}


8 
\makeatother


9 


10 
\newif\ifshort%''Short'' means a published version, not the documentation


11 
\shortfalse%%%%%\shorttrue


12 


13 
\title{A Fixedpoint Approach to\\


14 
(Co)Inductive and (Co)Datatype Definitions%


15 
\thanks{J. Grundy and S. Thompson made detailed comments. Mads Tofte and


16 
the referees were also helpful. The research was funded by the SERC


17 
grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}


18 


19 
\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\


20 
Computer Laboratory, University of Cambridge, England}


21 
\date{\today}


22 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}


23 


24 
\newcommand\sbs{\subseteq}


25 
\let\To=\Rightarrow


26 


27 
%\newcommand\emph[1]{{\em#1\/}}


28 
\newcommand\defn[1]{{\bf#1}}


29 
%\newcommand\textsc[1]{{\sc#1}}


30 
%\newcommand\texttt[1]{{\tt#1}}


31 


32 
\newcommand\pow{{\cal P}}


33 
%%%\let\pow=\wp


34 
\newcommand\RepFun{\hbox{\tt RepFun}}


35 
\newcommand\cons{\hbox{\tt cons}}


36 
\def\succ{\hbox{\tt succ}}


37 
\newcommand\split{\hbox{\tt split}}


38 
\newcommand\fst{\hbox{\tt fst}}


39 
\newcommand\snd{\hbox{\tt snd}}


40 
\newcommand\converse{\hbox{\tt converse}}


41 
\newcommand\domain{\hbox{\tt domain}}


42 
\newcommand\range{\hbox{\tt range}}


43 
\newcommand\field{\hbox{\tt field}}


44 
\newcommand\lfp{\hbox{\tt lfp}}


45 
\newcommand\gfp{\hbox{\tt gfp}}


46 
\newcommand\id{\hbox{\tt id}}


47 
\newcommand\trans{\hbox{\tt trans}}


48 
\newcommand\wf{\hbox{\tt wf}}


49 
\newcommand\nat{\hbox{\tt nat}}


50 
\newcommand\rank{\hbox{\tt rank}}


51 
\newcommand\univ{\hbox{\tt univ}}


52 
\newcommand\Vrec{\hbox{\tt Vrec}}


53 
\newcommand\Inl{\hbox{\tt Inl}}


54 
\newcommand\Inr{\hbox{\tt Inr}}


55 
\newcommand\case{\hbox{\tt case}}


56 
\newcommand\lst{\hbox{\tt list}}


57 
\newcommand\Nil{\hbox{\tt Nil}}


58 
\newcommand\Cons{\hbox{\tt Cons}}


59 
\newcommand\lstcase{\hbox{\tt list\_case}}


60 
\newcommand\lstrec{\hbox{\tt list\_rec}}


61 
\newcommand\length{\hbox{\tt length}}


62 
\newcommand\listn{\hbox{\tt listn}}


63 
\newcommand\acc{\hbox{\tt acc}}


64 
\newcommand\primrec{\hbox{\tt primrec}}


65 
\newcommand\SC{\hbox{\tt SC}}


66 
\newcommand\CONST{\hbox{\tt CONST}}


67 
\newcommand\PROJ{\hbox{\tt PROJ}}


68 
\newcommand\COMP{\hbox{\tt COMP}}


69 
\newcommand\PREC{\hbox{\tt PREC}}


70 


71 
\newcommand\quniv{\hbox{\tt quniv}}


72 
\newcommand\llist{\hbox{\tt llist}}


73 
\newcommand\LNil{\hbox{\tt LNil}}


74 
\newcommand\LCons{\hbox{\tt LCons}}


75 
\newcommand\lconst{\hbox{\tt lconst}}


76 
\newcommand\lleq{\hbox{\tt lleq}}


77 
\newcommand\map{\hbox{\tt map}}


78 
\newcommand\term{\hbox{\tt term}}


79 
\newcommand\Apply{\hbox{\tt Apply}}


80 
\newcommand\termcase{\hbox{\tt term\_case}}


81 
\newcommand\rev{\hbox{\tt rev}}


82 
\newcommand\reflect{\hbox{\tt reflect}}


83 
\newcommand\tree{\hbox{\tt tree}}


84 
\newcommand\forest{\hbox{\tt forest}}


85 
\newcommand\Part{\hbox{\tt Part}}


86 
\newcommand\TF{\hbox{\tt tree\_forest}}


87 
\newcommand\Tcons{\hbox{\tt Tcons}}


88 
\newcommand\Fcons{\hbox{\tt Fcons}}


89 
\newcommand\Fnil{\hbox{\tt Fnil}}


90 
\newcommand\TFcase{\hbox{\tt TF\_case}}


91 
\newcommand\Fin{\hbox{\tt Fin}}


92 
\newcommand\QInl{\hbox{\tt QInl}}


93 
\newcommand\QInr{\hbox{\tt QInr}}


94 
\newcommand\qsplit{\hbox{\tt qsplit}}


95 
\newcommand\qcase{\hbox{\tt qcase}}


96 
\newcommand\Con{\hbox{\tt Con}}


97 
\newcommand\data{\hbox{\tt data}}


98 


99 
\binperiod %%%treat . like a binary operator


100 


101 
\begin{document}


102 
\pagestyle{empty}


103 
\begin{titlepage}


104 
\maketitle


105 
\begin{abstract}


106 
This paper presents a fixedpoint approach to inductive definitions.


107 
Instead of using a syntactic test such as ``strictly positive,'' the


108 
approach lets definitions involve any operators that have been proved


109 
monotone. It is conceptually simple, which has allowed the easy


110 
implementation of mutual recursion and iterated definitions. It also


111 
handles coinductive definitions: simply replace the least fixedpoint by a


112 
greatest fixedpoint.


113 


114 
The method has been implemented in two of Isabelle's logics, \textsc{zf} set


115 
theory and higherorder logic. It should be applicable to any logic in


116 
which the KnasterTarski theorem can be proved. Examples include lists of


117 
$n$ elements, the accessible part of a relation and the set of primitive


118 
recursive functions. One example of a coinductive definition is


119 
bisimulations for lazy lists. Recursive datatypes are examined in detail,


120 
as well as one example of a \defn{codatatype}: lazy lists.


121 


122 
The Isabelle package has been applied in several large case studies,


123 
including two proofs of the ChurchRosser theorem and a coinductive proof of


124 
semantic consistency. The package can be trusted because it proves theorems


125 
from definitions, instead of asserting desired properties as axioms.


126 
\end{abstract}


127 
%


128 
\bigskip


129 
\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}


130 
\thispagestyle{empty}


131 
\end{titlepage}


132 
\tableofcontents\cleardoublepage\pagestyle{plain}


133 


134 
\setcounter{page}{1}


135 


136 
\section{Introduction}


137 
Several theorem provers provide commands for formalizing recursive data


138 
structures, like lists and trees. Robin Milner implemented one of the first


139 
of these, for Edinburgh \textsc{lcf}~\cite{milnerind}. Given a description


140 
of the desired data structure, Milner's package formulated appropriate


141 
definitions and proved the characteristic theorems. Similar is Melham's


142 
recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}.


143 
Such data structures are called \defn{datatypes}


144 
below, by analogy with datatype declarations in Standard~\textsc{ml}\@.


145 
Some logics take datatypes as primitive; consider Boyer and Moore's shell


146 
principle~\cite{bm79} and the Coq type theory~\cite{paulintlca}.


147 


148 
A datatype is but one example of an \defn{inductive definition}. Such a


149 
definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}


150 
given rules: applying a rule to elements of~$R$ yields a result within~$R$.


151 
Inductive definitions have many applications. The collection of theorems in a


152 
logic is inductively defined. A structural operational


153 
semantics~\cite{hennessy90} is an inductive definition of a reduction or


154 
evaluation relation on programs. A few theorem provers provide commands for


155 
formalizing inductive definitions; these include Coq~\cite{paulintlca} and


156 
again the \textsc{hol} system~\cite{camilleri92}.


157 


158 
The dual notion is that of a \defn{coinductive definition}. Such a definition


159 
specifies the greatest set~$R$ \defn{consistent with} given rules: every


160 
element of~$R$ can be seen as arising by applying a rule to elements of~$R$.


161 
Important examples include using bisimulation relations to formalize


162 
equivalence of processes~\cite{milner89} or lazy functional


163 
programs~\cite{abramsky90}. Other examples include lazy lists and other


164 
infinite data structures; these are called \defn{codatatypes} below.


165 


166 
Not all inductive definitions are meaningful. \defn{Monotone} inductive


167 
definitions are a large, wellbehaved class. Monotonicity can be enforced


168 
by syntactic conditions such as ``strictly positive,'' but this could lead to


169 
monotone definitions being rejected on the grounds of their syntactic form.


170 
More flexible is to formalize monotonicity within the logic and allow users


171 
to prove it.


172 


173 
This paper describes a package based on a fixedpoint approach. Least


174 
fixedpoints yield inductive definitions; greatest fixedpoints yield


175 
coinductive definitions. Most of the discussion below applies equally to


176 
inductive and coinductive definitions, and most of the code is shared.


177 


178 
The package supports mutual recursion and infinitelybranching datatypes and


179 
codatatypes. It allows use of any operators that have been proved monotone,


180 
thus accepting all provably monotone inductive definitions, including


181 
iterated definitions.


182 


183 
The package has been implemented in


184 
Isabelle~\cite{paulsonmarkt,paulsonisabook} using


185 
\textsc{zf} set theory \cite{paulsonsetI,paulsonsetII}; part of it has


186 
since been ported to Isabelle/\textsc{hol} (higherorder logic). The


187 
recursion equations are specified as introduction rules for the mutually


188 
recursive sets. The package transforms these rules into a mapping over sets,


189 
and attempts to prove that the mapping is monotonic and welltyped. If


190 
successful, the package makes fixedpoint definitions and proves the


191 
introduction, elimination and (co)induction rules. Users invoke the package


192 
by making simple declarations in Isabelle theory files.


193 


194 
Most datatype packages equip the new datatype with some means of expressing


195 
recursive functions. This is the main omission from my package. Its


196 
fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf}


197 
theory provides wellfounded recursion~\cite{paulsonsetII}, which is harder


198 
to use than structural recursion but considerably more general.


199 
Slind~\cite{slindtfl} has written a package to automate the definition of


200 
wellfounded recursive functions in Isabelle/\textsc{hol}.


201 


202 
\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint


203 
operators. Section~3 discusses the form of introduction rules, mutual


204 
recursion and other points common to inductive and coinductive definitions.


205 
Section~4 discusses induction and coinduction rules separately. Section~5


206 
presents several examples, including a coinductive definition. Section~6


207 
describes datatype definitions. Section~7 presents related work.


208 
Section~8 draws brief conclusions. \ifshort\else The appendices are simple


209 
user's manuals for this Isabelle package.\fi


210 


211 
Most of the definitions and theorems shown below have been generated by the


212 
package. I have renamed some variables to improve readability.


213 


214 
\section{Fixedpoint operators}


215 
In set theory, the least and greatest fixedpoint operators are defined as


216 
follows:


217 
\begin{eqnarray*}


218 
\lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\


219 
\gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\}


220 
\end{eqnarray*}


221 
Let $D$ be a set. Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and


222 
\defn{monotone below~$D$} if


223 
$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is


224 
bounded by~$D$ and monotone then both operators yield fixedpoints:


225 
\begin{eqnarray*}


226 
\lfp(D,h) & = & h(\lfp(D,h)) \\


227 
\gfp(D,h) & = & h(\gfp(D,h))


228 
\end{eqnarray*}


229 
These equations are instances of the KnasterTarski theorem, which states


230 
that every monotonic function over a complete lattice has a


231 
fixedpoint~\cite{davey&priestley}. It is obvious from their definitions


232 
that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.


233 


234 
This fixedpoint theory is simple. The KnasterTarski theorem is easy to


235 
prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must


236 
also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when


237 
a set of theorems is (co)inductively defined over some previously existing set


238 
of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for


239 
infinitelybranching (co)datatype definitions; see~\S\ref{univsec}. Bounding


240 
sets are also called \defn{domains}.


241 


242 
The powerset operator is monotone, but by Cantor's theorem there is no


243 
set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because


244 
there is no suitable domain~$D$. But \S\ref{accsec} demonstrates


245 
that~$\pow$ is still useful in inductive definitions.


246 


247 
\section{Elements of an inductive or coinductive definition}\label{basicsec}


248 
Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in


249 
mutual recursion. They will be constructed from domains $D_1$,


250 
\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but


251 
$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$


252 
under an injection. Reasons for this are discussed


253 
elsewhere~\cite[\S4.5]{paulsonsetII}.


254 


255 
The definition may involve arbitrary parameters $\vec{p}=p_1$,


256 
\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The


257 
parameters must be identical every time they occur within a definition. This


258 
would appear to be a serious restriction compared with other systems such as


259 
Coq~\cite{paulintlca}. For instance, we cannot define the lists of


260 
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$


261 
varies. Section~\ref{listnsec} describes how to express this set using the


262 
inductive definition package.


263 


264 
To avoid clutter below, the recursive sets are shown as simply $R_i$


265 
instead of~$R_i(\vec{p})$.


266 


267 
\subsection{The form of the introduction rules}\label{introsec}


268 
The body of the definition consists of the desired introduction rules. The


269 
conclusion of each rule must have the form $t\in R_i$, where $t$ is any term.


270 
Premises typically have the same form, but they can have the more general form


271 
$t\in M(R_i)$ or express arbitrary sideconditions.


272 


273 
The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on


274 
sets, satisfying the rule


275 
\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]


276 
The user must supply the package with monotonicity rules for all such premises.


277 


278 
The ability to introduce new monotone operators makes the approach


279 
flexible. A suitable choice of~$M$ and~$t$ can express a lot. The


280 
powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$


281 
expresses $t\sbs R$; see \S\ref{accsec} for an example. The \emph{list of}


282 
operator is monotone, as is easily proved by induction. The premise


283 
$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual


284 
recursion; see \S\ref{primrecsec} and also my earlier


285 
paper~\cite[\S4.4]{paulsonsetII}.


286 


287 
Introduction rules may also contain \defn{sideconditions}. These are


288 
premises consisting of arbitrary formul{\ae} not mentioning the recursive


289 
sets. Sideconditions typically involve typechecking. One example is the


290 
premise $a\in A$ in the following rule from the definition of lists:


291 
\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]


292 


293 
\subsection{The fixedpoint definitions}


294 
The package translates the list of desired introduction rules into a fixedpoint


295 
definition. Consider, as a running example, the finite powerset operator


296 
$\Fin(A)$: the set of all finite subsets of~$A$. It can be


297 
defined as the least set closed under the rules


298 
\[ \emptyset\in\Fin(A) \qquad


299 
\infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)}


300 
\]


301 


302 
The domain in a (co)inductive definition must be some existing set closed


303 
under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all


304 
subsets of~$A$. The package generates the definition


305 
\[ \Fin(A) \equiv \lfp(\pow(A), \,


306 
\begin{array}[t]{r@{\,}l}


307 
\lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\


308 
&(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})


309 
\end{array}


310 
\]


311 
The contribution of each rule to the definition of $\Fin(A)$ should be


312 
obvious. A coinductive definition is similar but uses $\gfp$ instead


313 
of~$\lfp$.


314 


315 
The package must prove that the fixedpoint operator is applied to a


316 
monotonic function. If the introduction rules have the form described


317 
above, and if the package is supplied a monotonicity theorem for every


318 
$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the


319 
presence of logical connectives in the fixedpoint's body, the


320 
monotonicity proof requires some unusual rules. These state that the


321 
connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect


322 
to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and


323 
only if $\forall x.P(x)\imp Q(x)$.}


324 


325 
The package returns its result as an \textsc{ml} structure, which consists of named


326 
components; we may regard it as a record. The result structure contains


327 
the definitions of the recursive sets as a theorem list called {\tt defs}.


328 
It also contains some theorems; {\tt dom\_subset} is an inclusion such as


329 
$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint


330 
definition is monotonic.


331 


332 
Internally the package uses the theorem {\tt unfold}, a fixedpoint equation


333 
such as


334 
\[


335 
\begin{array}[t]{r@{\,}l}


336 
\Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\


337 
&(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}


338 
\end{array}


339 
\]


340 
In order to save space, this theorem is not exported.


341 


342 


343 
\subsection{Mutual recursion} \label{mutualsec}


344 
In a mutually recursive definition, the domain of the fixedpoint construction


345 
is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,


346 
\ldots,~$n$. The package uses the injections of the


347 
binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections


348 
$h_{1n}$, \ldots, $h_{nn}$ for the $n$ary disjoint sum $D_1+\cdots+D_n$.


349 


350 
As discussed elsewhere \cite[\S4.5]{paulsonsetII}, Isabelle/\textsc{zf} defines the


351 
operator $\Part$ to support mutual recursion. The set $\Part(A,h)$


352 
contains those elements of~$A$ having the form~$h(z)$:


353 
\[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \]


354 
For mutually recursive sets $R_1$, \ldots,~$R_n$ with


355 
$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using


356 
a fixedpoint operator. The remaining $n$ definitions have the form


357 
\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \]


358 
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.


359 


360 


361 
\subsection{Proving the introduction rules}


362 
The user supplies the package with the desired form of the introduction


363 
rules. Once it has derived the theorem {\tt unfold}, it attempts


364 
to prove those rules. From the user's point of view, this is the


365 
trickiest stage; the proofs often fail. The task is to show that the domain


366 
$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is


367 
closed under all the introduction rules. This essentially involves replacing


368 
each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and


369 
attempting to prove the result.


370 


371 
Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$


372 
in the rules, the package must prove


373 
\[ \emptyset\in\pow(A) \qquad


374 
\infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)}


375 
\]


376 
Such proofs can be regarded as typechecking the definition.\footnote{The


377 
Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}


378 
has implicit typechecking.} The user supplies the package with


379 
typechecking rules to apply. Usually these are general purpose rules from


380 
the \textsc{zf} theory. They could however be rules specifically proved for a


381 
particular inductive definition; sometimes this is the easiest way to get the


382 
definition through!


383 


384 
The result structure contains the introduction rules as the theorem list {\tt


385 
intrs}.


386 


387 
\subsection{The case analysis rule}


388 
The elimination rule, called {\tt elim}, performs case analysis. It is a


389 
simple consequence of {\tt unfold}. There is one case for each introduction


390 
rule. If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for


391 
some $a\in A$ and $b\in\Fin(A)$. Formally, the elimination rule for $\Fin(A)$


392 
is written


393 
\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}


394 
& \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }


395 
\]


396 
The subscripted variables $a$ and~$b$ above the third premise are


397 
eigenvariables, subject to the usual ``not free in \ldots'' proviso.


398 


399 


400 
\section{Induction and coinduction rules}


401 
Here we must consider inductive and coinductive definitions separately. For


402 
an inductive definition, the package returns an induction rule derived


403 
directly from the properties of least fixedpoints, as well as a modified rule


404 
for mutual recursion. For a coinductive definition, the package returns a


405 
basic coinduction rule.


406 


407 
\subsection{The basic induction rule}\label{basicindsec}


408 
The basic rule, called {\tt induct}, is appropriate in most situations.


409 
For inductive definitions, it is strong rule induction~\cite{camilleri92}; for


410 
datatype definitions (see below), it is just structural induction.


411 


412 
The induction rule for an inductively defined set~$R$ has the form described


413 
below. For the time being, assume that $R$'s domain is not a Cartesian


414 
product; inductively defined relations are treated slightly differently.


415 


416 
The major premise is $x\in R$. There is a minor premise for each


417 
introduction rule:


418 
\begin{itemize}


419 
\item If the introduction rule concludes $t\in R_i$, then the minor premise


420 
is~$P(t)$.


421 


422 
\item The minor premise's eigenvariables are precisely the introduction


423 
rule's free variables that are not parameters of~$R$. For instance, the


424 
eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.


425 


426 
\item If the introduction rule has a premise $t\in R_i$, then the minor


427 
premise discharges the assumption $t\in R_i$ and the induction


428 
hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$


429 
then the minor premise discharges the single assumption


430 
\[ t\in M(\{z\in R_i. P(z)\}). \]


431 
Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The


432 
occurrence of $P$ gives the effect of an induction hypothesis, which may be


433 
exploited by appealing to properties of~$M$.


434 
\end{itemize}


435 
The induction rule for $\Fin(A)$ resembles the elimination rule shown above,


436 
but includes an induction hypothesis:


437 
\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)


438 
& \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }


439 
\]


440 
Stronger induction rules often suggest themselves. We can derive a rule for


441 
$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.


442 
The package provides rules for mutual induction and inductive relations. The


443 
Isabelle/\textsc{zf} theory also supports wellfounded induction and recursion


444 
over datatypes, by reasoning about the \defn{rank} of a


445 
set~\cite[\S3.4]{paulsonsetII}.


446 


447 


448 
\subsection{Modified induction rules}


449 


450 
If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$


451 
(however nested), then the corresponding predicate $P_i$ takes $m$ arguments.


452 
The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$;


453 
the conclusion becomes $P(z_1,\ldots,z_m)$. This simplifies reasoning about


454 
inductively defined relations, eliminating the need to express properties of


455 
$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.


456 
Occasionally it may require you to split up the induction variable


457 
using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt


458 
split} appears in the rule.


459 


460 
The mutual induction rule is called {\tt


461 
mutual\_induct}. It differs from the basic rule in two respects:


462 
\begin{itemize}


463 
\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,


464 
\ldots,~$P_n$: one for each recursive set.


465 


466 
\item There is no major premise such as $x\in R_i$. Instead, the conclusion


467 
refers to all the recursive sets:


468 
\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj


469 
(\forall z.z\in R_n\imp P_n(z))


470 
\]


471 
Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,


472 
\ldots,~$n$.


473 
\end{itemize}


474 
%


475 
If the domain of some $R_i$ is a Cartesian product, then the mutual induction


476 
rule is modified accordingly. The predicates are made to take $m$ separate


477 
arguments instead of a tuple, and the quantification in the conclusion is over


478 
the separate variables $z_1$, \ldots, $z_m$.


479 


480 
\subsection{Coinduction}\label{coindsec}


481 
A coinductive definition yields a primitive coinduction rule, with no


482 
refinements such as those for the induction rules. (Experience may suggest


483 
refinements later.) Consider the codatatype of lazy lists as an example. For


484 
suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the


485 
greatest set consistent with the rules


486 
\[ \LNil\in\llist(A) \qquad


487 
\infer[()]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}


488 
\]


489 
The $()$ tag stresses that this is a coinductive definition. A suitable


490 
domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant


491 
forms of sum and product that are used to represent nonwellfounded data


492 
structures (see~\S\ref{univsec}).


493 


494 
The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$.


495 
Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$


496 
is the greatest solution to this equation contained in $\quniv(A)$:


497 
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &


498 
\infer*{


499 
\begin{array}[b]{r@{}l}


500 
z=\LNil\disj


501 
\bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\


502 
& l\in X\un\llist(A) \bigr)


503 
\end{array} }{[z\in X]_z}}


504 
\]


505 
This rule complements the introduction rules; it provides a means of showing


506 
$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then


507 
applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$


508 
is the set of natural numbers.)


509 


510 
Having $X\un\llist(A)$ instead of simply $X$ in the third premise above


511 
represents a slight strengthening of the greatest fixedpoint property. I


512 
discuss several forms of coinduction rules elsewhere~\cite{paulsoncoind}.


513 


514 
The clumsy form of the third premise makes the rule hard to use, especially in


515 
large definitions. Probably a constant should be declared to abbreviate the


516 
large disjunction, and rules derived to allow proving the separate disjuncts.


517 


518 


519 
\section{Examples of inductive and coinductive definitions}\label{indegsec}


520 
This section presents several examples from the literature: the finite


521 
powerset operator, lists of $n$ elements, bisimulations on lazy lists, the


522 
wellfounded part of a relation, and the primitive recursive functions.


523 


524 
\subsection{The finite powerset operator}


525 
This operator has been discussed extensively above. Here is the


526 
corresponding invocation in an Isabelle theory file. Note that


527 
$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.


528 
\begin{ttbox}


529 
Finite = Arith +


530 
consts Fin :: i=>i


531 
inductive


532 
domains "Fin(A)" <= "Pow(A)"


533 
intrs


534 
emptyI "0 : Fin(A)"


535 
consI "[ a: A; b: Fin(A) ] ==> cons(a,b) : Fin(A)"


536 
type_intrs "[empty_subsetI, cons_subsetI, PowI]"


537 
type_elims "[make_elim PowD]"


538 
end


539 
\end{ttbox}


540 
Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the


541 
unary function symbol~$\Fin$, which is defined inductively. Its domain is


542 
specified as $\pow(A)$, where $A$ is the parameter appearing in the


543 
introduction rules. For typechecking, we supply two introduction


544 
rules:


545 
\[ \emptyset\sbs A \qquad


546 
\infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}


547 
\]


548 
A further introduction rule and an elimination rule express both


549 
directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Typechecking


550 
involves mostly introduction rules.


551 


552 
Like all Isabelle theory files, this one yields a structure containing the


553 
new theory as an \textsc{ml} value. Structure {\tt Finite} also has a


554 
substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we


555 
can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}


556 
or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction


557 
rule is {\tt Fin.induct}.


558 


559 


560 
\subsection{Lists of $n$ elements}\label{listnsec}


561 
This has become a standard example of an inductive definition. Following


562 
PaulinMohring~\cite{paulintlca}, we could attempt to define a new datatype


563 
$\listn(A,n)$, for lists of length~$n$, as an $n$indexed family of sets.


564 
But her introduction rules


565 
\[ \hbox{\tt Niln}\in\listn(A,0) \qquad


566 
\infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}


567 
{n\in\nat & a\in A & l\in\listn(A,n)}


568 
\]


569 
are not acceptable to the inductive definition package:


570 
$\listn$ occurs with three different parameter lists in the definition.


571 


572 
The Isabelle version of this example suggests a general treatment of


573 
varying parameters. It uses the existing datatype definition of


574 
$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the


575 
parameter~$n$ into the inductive set itself. It defines $\listn(A)$ as a


576 
relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$


577 
and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the


578 
converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction


579 
rules are


580 
\[ \pair{0,\Nil}\in\listn(A) \qquad


581 
\infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}


582 
{a\in A & \pair{n,l}\in\listn(A)}


583 
\]


584 
The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.


585 
We declare the constant~$\listn$ and supply an inductive definition,


586 
specifying the domain as $\nat\times\lst(A)$:


587 
\begin{ttbox}


588 
ListN = List +


589 
consts listn :: i=>i


590 
inductive


591 
domains "listn(A)" <= "nat*list(A)"


592 
intrs


593 
NilI "<0,Nil>: listn(A)"


594 
ConsI "[ a: A; <n,l>: listn(A) ] ==> <succ(n), Cons(a,l)>: listn(A)"


595 
type_intrs "nat_typechecks @ list.intrs"


596 
end


597 
\end{ttbox}


598 
The typechecking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.


599 
Because $\listn(A)$ is a set of pairs, typechecking requires the


600 
equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The


601 
package always includes the rules for ordered pairs.


602 


603 
The package returns introduction, elimination and induction rules for


604 
$\listn$. The basic induction rule, {\tt listn.induct}, is


605 
\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) &


606 
\infer*{P(\succ(n),\Cons(a,l))}


607 
{[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}


608 
\]


609 
This rule lets the induction formula to be a


610 
binary property of pairs, $P(n,l)$.


611 
It is now a simple matter to prove theorems about $\listn(A)$, such as


612 
\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]


613 
\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]


614 
This latter result  here $r``X$ denotes the image of $X$ under $r$


615 
 asserts that the inductive definition agrees with the obvious notion of


616 
$n$element list.


617 


618 
A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.


619 
It is subject to list operators such as append (concatenation). For example,


620 
a trivial induction on $\pair{m,l}\in\listn(A)$ yields


621 
\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}


622 
{\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)}


623 
\]


624 
where $+$ denotes addition on the natural numbers and @ denotes append.


625 


626 
\subsection{Rule inversion: the function {\tt mk\_cases}}


627 
The elimination rule, {\tt listn.elim}, is cumbersome:


628 
\[ \infer{Q}{x\in\listn(A) &


629 
\infer*{Q}{[x = \pair{0,\Nil}]} &


630 
\infer*{Q}


631 
{\left[\begin{array}{l}


632 
x = \pair{\succ(n),\Cons(a,l)} \\


633 
a\in A \\


634 
\pair{n,l}\in\listn(A)


635 
\end{array} \right]_{a,l,n}}}


636 
\]


637 
The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of


638 
this rule. It works by freeness reasoning on the list constructors:


639 
$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If


640 
$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases}


641 
deduces the corresponding form of~$i$; this is called rule inversion.


642 
Here is a sample session:


643 
\begin{ttbox}


644 
listn.mk_cases list.con_defs "<i,Nil> : listn(A)";


645 
{\out "[ <?i, []> : listn(?A); ?i = 0 ==> ?Q ] ==> ?Q" : thm}


646 
listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";


647 
{\out "[ <?i, Cons(?a, ?l)> : listn(?A);}


648 
{\out !!n. [ ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) ] ==> ?Q }


649 
{\out ] ==> ?Q" : thm}


650 
\end{ttbox}


651 
Each of these rules has only two premises. In conventional notation, the


652 
second rule is


653 
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) &


654 
\infer*{Q}


655 
{\left[\begin{array}{l}


656 
a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)


657 
\end{array} \right]_{n}}}


658 
\]


659 
The package also has builtin rules for freeness reasoning about $0$


660 
and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt


661 
listn.mk\_cases} can deduce the corresponding form of~$l$.


662 


663 
The function {\tt mk\_cases} is also useful with datatype definitions. The


664 
instance from the definition of lists, namely {\tt list.mk\_cases}, can


665 
prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$:


666 
\[ \infer{Q}{\Cons(a,l)\in\lst(A) &


667 
& \infer*{Q}{[a\in A &l\in\lst(A)]} }


668 
\]


669 
A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation


670 
relations. Then rule inversion yields case analysis on possible evaluations.


671 
For example, Isabelle/\textsc{zf} includes a short proof of the


672 
diamond property for parallel contraction on combinators. Ole Rasmussen used


673 
{\tt mk\_cases} extensively in his development of the theory of


674 
residuals~\cite{rasmussen95}.


675 


676 


677 
\subsection{A coinductive definition: bisimulations on lazy lists}


678 
This example anticipates the definition of the codatatype $\llist(A)$, which


679 
consists of finite and infinite lists over~$A$. Its constructors are $\LNil$


680 
and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coindsec}.


681 
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant


682 
pairing and injection operators, it contains nonwellfounded elements such as


683 
solutions to $\LCons(a,l)=l$.


684 


685 
The next step in the development of lazy lists is to define a coinduction


686 
principle for proving equalities. This is done by showing that the equality


687 
relation on lazy lists is the greatest fixedpoint of some monotonic


688 
operation. The usual approach~\cite{pitts94} is to define some notion of


689 
bisimulation for lazy lists, define equivalence to be the greatest


690 
bisimulation, and finally to prove that two lazy lists are equivalent if and


691 
only if they are equal. The coinduction rule for equivalence then yields a


692 
coinduction principle for equalities.


693 


694 
A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs


695 
R^+$, where $R^+$ is the relation


696 
\[ \{\pair{\LNil,\LNil}\} \un


697 
\{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.


698 
\]


699 
A pair of lazy lists are \defn{equivalent} if they belong to some


700 
bisimulation. Equivalence can be coinductively defined as the greatest


701 
fixedpoint for the introduction rules


702 
\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad


703 
\infer[()]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}


704 
{a\in A & \pair{l,l'}\in \lleq(A)}


705 
\]


706 
To make this coinductive definition, the theory file includes (after the


707 
declaration of $\llist(A)$) the following lines:


708 
\begin{ttbox}


709 
consts lleq :: i=>i


710 
coinductive


711 
domains "lleq(A)" <= "llist(A) * llist(A)"


712 
intrs


713 
LNil "<LNil,LNil> : lleq(A)"


714 
LCons "[ a:A; <l,l'>: lleq(A) ] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"


715 
type_intrs "llist.intrs"


716 
\end{ttbox}


717 
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The typechecking


718 
rules include the introduction rules for $\llist(A)$, whose


719 
declaration is discussed below (\S\ref{listssec}).


720 


721 
The package returns the introduction rules and the elimination rule, as


722 
usual. But instead of induction rules, it returns a coinduction rule.


723 
The rule is too big to display in the usual notation; its conclusion is


724 
$x\in\lleq(A)$ and its premises are $x\in X$,


725 
${X\sbs\llist(A)\times\llist(A)}$ and


726 
\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,


727 
\begin{array}[t]{@{}l}


728 
z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\


729 
\pair{l,l'}\in X\un\lleq(A) \bigr)


730 
\end{array}


731 
}{[z\in X]_z}


732 
\]


733 
Thus if $x\in X$, where $X$ is a bisimulation contained in the


734 
domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that


735 
$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And


736 
$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that


737 
$\lleq(A)$ coincides with the equality relation takes some work.


738 


739 
\subsection{The accessible part of a relation}\label{accsec}


740 
Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.


741 
The \defn{accessible} or \defn{wellfounded} part of~$\prec$, written


742 
$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits


743 
no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is


744 
inductively defined to be the least set that contains $a$ if it contains


745 
all $\prec$predecessors of~$a$, for $a\in D$. Thus we need an


746 
introduction rule of the form


747 
\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]


748 
PaulinMohring treats this example in Coq~\cite{paulintlca}, but it causes


749 
difficulties for other systems. Its premise is not acceptable to the


750 
inductive definition package of the Cambridge \textsc{hol}


751 
system~\cite{camilleri92}. It is also unacceptable to the Isabelle package


752 
(recall \S\ref{introsec}), but fortunately can be transformed into the


753 
acceptable form $t\in M(R)$.


754 


755 
The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to


756 
$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To


757 
express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a


758 
term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is


759 
the inverse image of~$\{a\}$ under~$\prec$.


760 


761 
The definition below follows this approach. Here $r$ is~$\prec$ and


762 
$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a


763 
relation is the union of its domain and range.) Finally $r^{}``\{a\}$


764 
denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt


765 
Pow\_mono}, which asserts that $\pow$ is monotonic.


766 
\begin{ttbox}


767 
consts acc :: i=>i


768 
inductive


769 
domains "acc(r)" <= "field(r)"


770 
intrs


771 
vimage "[ r``\{a\}: Pow(acc(r)); a: field(r) ] ==> a: acc(r)"


772 
monos "[Pow_mono]"


773 
\end{ttbox}


774 
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For


775 
instance, $\prec$ is wellfounded if and only if its field is contained in


776 
$\acc(\prec)$.


777 


778 
As mentioned in~\S\ref{basicindsec}, a premise of the form $t\in M(R)$


779 
gives rise to an unusual induction hypothesis. Let us examine the


780 
induction rule, {\tt acc.induct}:


781 
\[ \infer{P(x)}{x\in\acc(r) &


782 
\infer*{P(a)}{\left[


783 
\begin{array}{r@{}l}


784 
r^{}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\


785 
a &\, \in\field(r)


786 
\end{array}


787 
\right]_a}}


788 
\]


789 
The strange induction hypothesis is equivalent to


790 
$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.


791 
Therefore the rule expresses wellfounded induction on the accessible part


792 
of~$\prec$.


793 


794 
The use of inverse image is not essential. The Isabelle package can accept


795 
introduction rules with arbitrary premises of the form $\forall


796 
\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed


797 
equivalently as


798 
\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \]


799 
provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The


800 
following section demonstrates another use of the premise $t\in M(R)$,


801 
where $M=\lst$.


802 


803 
\subsection{The primitive recursive functions}\label{primrecsec}


804 
The primitive recursive functions are traditionally defined inductively, as


805 
a subset of the functions over the natural numbers. One difficulty is that


806 
functions of all arities are taken together, but this is easily


807 
circumvented by regarding them as functions on lists. Another difficulty,


808 
the notion of composition, is less easily circumvented.


809 


810 
Here is a more precise definition. Letting $\vec{x}$ abbreviate


811 
$x_0,\ldots,x_{n1}$, we can write lists such as $[\vec{x}]$,


812 
$[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it


813 
belongs to the least set of functions in $\lst(\nat)\to\nat$ containing


814 
\begin{itemize}


815 
\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.


816 
\item All \defn{constant} functions $\CONST(k)$, such that


817 
$\CONST(k)[\vec{x}]=k$.


818 
\item All \defn{projection} functions $\PROJ(i)$, such that


819 
$\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$.


820 
\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m1}])$,


821 
where $g$ and $f_0$, \ldots, $f_{m1}$ are primitive recursive,


822 
such that


823 
\[ \COMP(g,[f_0,\ldots,f_{m1}])[\vec{x}] =


824 
g[f_0[\vec{x}],\ldots,f_{m1}[\vec{x}]]. \]


825 


826 
\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive


827 
recursive, such that


828 
\begin{eqnarray*}


829 
\PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\


830 
\PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].


831 
\end{eqnarray*}


832 
\end{itemize}


833 
Composition is awkward because it combines not two functions, as is usual,


834 
but $m+1$ functions. In her proof that Ackermann's function is not


835 
primitive recursive, Nora Szasz was unable to formalize this definition


836 
directly~\cite{szasz93}. So she generalized primitive recursion to


837 
tuplevalued functions. This modified the inductive definition such that


838 
each operation on primitive recursive functions combined just two functions.


839 


840 
\begin{figure}


841 
\begin{ttbox}


842 
Primrec = List +


843 
consts


844 
primrec :: i


845 
SC :: i


846 
\(\vdots\)


847 
defs


848 
SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"


849 
\(\vdots\)


850 
inductive


851 
domains "primrec" <= "list(nat)>nat"


852 
intrs


853 
SC "SC : primrec"


854 
CONST "k: nat ==> CONST(k) : primrec"


855 
PROJ "i: nat ==> PROJ(i) : primrec"


856 
COMP "[ g: primrec; fs: list(primrec) ] ==> COMP(g,fs): primrec"


857 
PREC "[ f: primrec; g: primrec ] ==> PREC(f,g): primrec"


858 
monos "[list_mono]"


859 
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"


860 
type_intrs "nat_typechecks @ list.intrs @


861 
[lam_type, list_case_type, drop_type, map_type,


862 
apply_type, rec_type]"


863 
end


864 
\end{ttbox}


865 
\hrule


866 
\caption{Inductive definition of the primitive recursive functions}


867 
\label{primrecfig}


868 
\end{figure}


869 
\def\fs{{\it fs}}


870 


871 
Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have


872 
problems accepting this definition. Isabelle's package accepts it easily


873 
since $[f_0,\ldots,f_{m1}]$ is a list of primitive recursive functions and


874 
$\lst$ is monotonic. There are five introduction rules, one for each of the


875 
five forms of primitive recursive function. Let us examine the one for


876 
$\COMP$:


877 
\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]


878 
The induction rule for $\primrec$ has one case for each introduction rule.


879 
Due to the use of $\lst$ as a monotone operator, the composition case has


880 
an unusual induction hypothesis:


881 
\[ \infer*{P(\COMP(g,\fs))}


882 
{[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}}


883 
\]


884 
The hypothesis states that $\fs$ is a list of primitive recursive functions,


885 
each satisfying the induction formula. Proving the $\COMP$ case typically


886 
requires structural induction on lists, yielding two subcases: either


887 
$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and


888 
$\fs'$ is another list of primitive recursive functions satisfying~$P$.


889 


890 
Figure~\ref{primrecfig} presents the theory file. Theory {\tt Primrec}


891 
defines the constants $\SC$, $\CONST$, etc. These are not constructors of


892 
a new datatype, but functions over lists of numbers. Their definitions,


893 
most of which are omitted, consist of routine list programming. In


894 
Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of


895 
the function set $\lst(\nat)\to\nat$.


896 


897 
The Isabelle theory goes on to formalize Ackermann's function and prove


898 
that it is not primitive recursive, using the induction rule {\tt


899 
primrec.induct}. The proof follows Szasz's excellent account.


900 


901 


902 
\section{Datatypes and codatatypes}\label{datasec}


903 
A (co)datatype definition is a (co)inductive definition with automatically


904 
defined constructors and a case analysis operator. The package proves that


905 
the case operator inverts the constructors and can prove freeness theorems


906 
involving any pair of constructors.


907 


908 


909 
\subsection{Constructors and their domain}\label{univsec}


910 
A (co)inductive definition selects a subset of an existing set; a (co)datatype


911 
definition creates a new set. The package reduces the latter to the former.


912 
Isabelle/\textsc{zf} supplies sets having strong closure properties to serve


913 
as domains for (co)inductive definitions.


914 


915 
Isabelle/\textsc{zf} defines the Cartesian product $A\times


916 
B$, containing ordered pairs $\pair{a,b}$; it also defines the


917 
disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and


918 
$\Inr(b)\equiv\pair{1,b}$. For use below, define the $m$tuple


919 
$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$


920 
if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.


921 


922 
A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be


923 
$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.


924 
In a mutually recursive definition, all constructors for the set~$R_i$ have


925 
the outer form~$h_{in}$, where $h_{in}$ is the injection described


926 
in~\S\ref{mutualsec}. Further nested injections ensure that the


927 
constructors for~$R_i$ are pairwise distinct.


928 


929 
Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and


930 
furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,


931 
$b\in\univ(A)$. In a typical datatype definition with set parameters


932 
$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is


933 
$\univ(A_1\un\cdots\un A_k)$. This solves the problem for


934 
datatypes~\cite[\S4.2]{paulsonsetII}.


935 


936 
The standard pairs and injections can only yield wellfounded


937 
constructions. This eases the (manual!) definition of recursive functions


938 
over datatypes. But they are unsuitable for codatatypes, which typically


939 
contain nonwellfounded objects.


940 


941 
To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of


942 
ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant


943 
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$


944 
and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the


945 
set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$,


946 
$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype


947 
definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is


948 
$\quniv(A_1\un\cdots\un A_k)$. Details are published


949 
elsewhere~\cite{paulsonfinal}.


950 


951 
\subsection{The case analysis operator}


952 
The (co)datatype package automatically defines a case analysis operator,


953 
called {\tt$R$\_case}. A mutually recursive definition still has only one


954 
operator, whose name combines those of the recursive sets: it is called


955 
{\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those


956 
for products and sums.


957 


958 
Datatype definitions employ standard products and sums, whose operators are


959 
$\split$ and $\case$ and satisfy the equations


960 
\begin{eqnarray*}


961 
\split(f,\pair{x,y}) & = & f(x,y) \\


962 
\case(f,g,\Inl(x)) & = & f(x) \\


963 
\case(f,g,\Inr(y)) & = & g(y)


964 
\end{eqnarray*}


965 
Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then


966 
its case operator takes $k+1$ arguments and satisfies an equation for each


967 
constructor:


968 
\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),


969 
\qquad i = 1, \ldots, k


970 
\]


971 
The case operator's definition takes advantage of Isabelle's representation of


972 
syntax in the typed $\lambda$calculus; it could readily be adapted to a


973 
theorem prover for higherorder logic. If $f$ and~$g$ have metatype $i\To i$


974 
then so do $\split(f)$ and $\case(f,g)$. This works because $\split$ and


975 
$\case$ operate on their last argument. They are easily combined to make


976 
complex case analysis operators. For example, $\case(f,\case(g,h))$ performs


977 
case analysis for $A+(B+C)$; let us verify one of the three equations:


978 
\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \]


979 
Codatatype definitions are treated in precisely the same way. They express


980 
case operators using those for the variant products and sums, namely


981 
$\qsplit$ and~$\qcase$.


982 


983 
\medskip


984 


985 
To see how constructors and the case analysis operator are defined, let us


986 
examine some examples. Further details are available


987 
elsewhere~\cite{paulsonsetII}.


988 


989 


990 
\subsection{Example: lists and lazy lists}\label{listssec}


991 
Here is a declaration of the datatype of lists, as it might appear in a theory


992 
file:


993 
\begin{ttbox}


994 
consts list :: i=>i


995 
datatype "list(A)" = Nil  Cons ("a:A", "l: list(A)")


996 
\end{ttbox}


997 
And here is a declaration of the codatatype of lazy lists:


998 
\begin{ttbox}


999 
consts llist :: i=>i


1000 
codatatype "llist(A)" = LNil  LCons ("a: A", "l: llist(A)")


1001 
\end{ttbox}


1002 


1003 
Each form of list has two constructors, one for the empty list and one for


1004 
adding an element to a list. Each takes a parameter, defining the set of


1005 
lists over a given set~$A$. Each is automatically given the appropriate


1006 
domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$. The default


1007 
can be overridden.


1008 


1009 
\ifshort


1010 
Now $\lst(A)$ is a datatype and enjoys the usual induction rule.


1011 
\else


1012 
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt


1013 
list.induct}:


1014 
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)


1015 
& \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }


1016 
\]


1017 
Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this,


1018 
Isabelle/\textsc{zf} defines the rank of a set and proves that the standard


1019 
pairs and injections have greater rank than their components. An immediate


1020 
consequence, which justifies structural recursion on lists


1021 
\cite[\S4.3]{paulsonsetII}, is


1022 
\[ \rank(l) < \rank(\Cons(a,l)). \]


1023 
\par


1024 
\fi


1025 
But $\llist(A)$ is a codatatype and has no induction rule. Instead it has


1026 
the coinduction rule shown in \S\ref{coindsec}. Since variant pairs and


1027 
injections are monotonic and need not have greater rank than their


1028 
components, fixedpoint operators can create cyclic constructions. For


1029 
example, the definition


1030 
\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]


1031 
yields $\lconst(a) = \LCons(a,\lconst(a))$.


1032 


1033 
\ifshort


1034 
\typeout{****SHORT VERSION}


1035 
\typeout{****Omitting discussion of constructors!}


1036 
\else


1037 
\medskip


1038 
It may be instructive to examine the definitions of the constructors and


1039 
case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar.


1040 
The list constructors are defined as follows:


1041 
\begin{eqnarray*}


1042 
\Nil & \equiv & \Inl(\emptyset) \\


1043 
\Cons(a,l) & \equiv & \Inr(\pair{a,l})


1044 
\end{eqnarray*}


1045 
The operator $\lstcase$ performs case analysis on these two alternatives:


1046 
\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]


1047 
Let us verify the two equations:


1048 
\begin{eqnarray*}


1049 
\lstcase(c, h, \Nil) & = &


1050 
\case(\lambda u.c, \split(h), \Inl(\emptyset)) \\


1051 
& = & (\lambda u.c)(\emptyset) \\


1052 
& = & c\\[1ex]


1053 
\lstcase(c, h, \Cons(x,y)) & = &


1054 
\case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\


1055 
& = & \split(h, \pair{x,y}) \\


1056 
& = & h(x,y)


1057 
\end{eqnarray*}


1058 
\fi


1059 


1060 


1061 
\ifshort


1062 
\typeout{****Omitting mutual recursion example!}


1063 
\else


1064 
\subsection{Example: mutual recursion}


1065 
In mutually recursive trees and forests~\cite[\S4.5]{paulsonsetII}, trees


1066 
have the one constructor $\Tcons$, while forests have the two constructors


1067 
$\Fnil$ and~$\Fcons$:


1068 
\begin{ttbox}


1069 
consts tree, forest, tree_forest :: i=>i


1070 
datatype "tree(A)" = Tcons ("a: A", "f: forest(A)")


1071 
and "forest(A)" = Fnil  Fcons ("t: tree(A)", "f: forest(A)")


1072 
\end{ttbox}


1073 
The three introduction rules define the mutual recursion. The


1074 
distinguishing feature of this example is its two induction rules.


1075 


1076 
The basic induction rule is called {\tt tree\_forest.induct}:


1077 
\[ \infer{P(x)}{x\in\TF(A) &


1078 
\infer*{P(\Tcons(a,f))}


1079 
{\left[\begin{array}{l} a\in A \\


1080 
f\in\forest(A) \\ P(f)


1081 
\end{array}


1082 
\right]_{a,f}}


1083 
& P(\Fnil)


1084 
& \infer*{P(\Fcons(t,f))}


1085 
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\


1086 
f\in\forest(A) \\ P(f)


1087 
\end{array}


1088 
\right]_{t,f}} }


1089 
\]


1090 
This rule establishes a single predicate for $\TF(A)$, the union of the


1091 
recursive sets. Although such reasoning is sometimes useful


1092 
\cite[\S4.5]{paulsonsetII}, a proper mutual induction rule should establish


1093 
separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this


1094 
rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in


1095 
the induction hypotheses:


1096 
\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj


1097 
(\forall z. z\in\forest(A)\imp Q(z))}


1098 
{\infer*{P(\Tcons(a,f))}


1099 
{\left[\begin{array}{l} a\in A \\


1100 
f\in\forest(A) \\ Q(f)


1101 
\end{array}


1102 
\right]_{a,f}}


1103 
& Q(\Fnil)


1104 
& \infer*{Q(\Fcons(t,f))}


1105 
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\


1106 
f\in\forest(A) \\ Q(f)


1107 
\end{array}


1108 
\right]_{t,f}} }


1109 
\]


1110 
Elsewhere I describe how to define mutually recursive functions over trees and


1111 
forests \cite[\S4.5]{paulsonsetII}.


1112 


1113 
Both forest constructors have the form $\Inr(\cdots)$,


1114 
while the tree constructor has the form $\Inl(\cdots)$. This pattern would


1115 
hold regardless of how many tree or forest constructors there were.


1116 
\begin{eqnarray*}


1117 
\Tcons(a,l) & \equiv & \Inl(\pair{a,l}) \\


1118 
\Fnil & \equiv & \Inr(\Inl(\emptyset)) \\


1119 
\Fcons(a,l) & \equiv & \Inr(\Inr(\pair{a,l}))


1120 
\end{eqnarray*}


1121 
There is only one case operator; it works on the union of the trees and


1122 
forests:


1123 
\[ {\tt tree\_forest\_case}(f,c,g) \equiv


1124 
\case(\split(f),\, \case(\lambda u.c, \split(g)))


1125 
\]


1126 
\fi


1127 


1128 


1129 
\subsection{Example: a fourconstructor datatype}


1130 
A bigger datatype will illustrate some efficiency


1131 
refinements. It has four constructors $\Con_0$, \ldots, $\Con_3$, with the


1132 
corresponding arities.


1133 
\begin{ttbox}


1134 
consts data :: [i,i] => i


1135 
datatype "data(A,B)" = Con0


1136 
 Con1 ("a: A")


1137 
 Con2 ("a: A", "b: B")


1138 
 Con3 ("a: A", "b: B", "d: data(A,B)")


1139 
\end{ttbox}


1140 
Because this datatype has two set parameters, $A$ and~$B$, the package


1141 
automatically supplies $\univ(A\un B)$ as its domain. The structural


1142 
induction rule has four minor premises, one per constructor, and only the last


1143 
has an induction hypothesis. (Details are left to the reader.)


1144 


1145 
The constructors are defined by the equations


1146 
\begin{eqnarray*}


1147 
\Con_0 & \equiv & \Inl(\Inl(\emptyset)) \\


1148 
\Con_1(a) & \equiv & \Inl(\Inr(a)) \\


1149 
\Con_2(a,b) & \equiv & \Inr(\Inl(\pair{a,b})) \\


1150 
\Con_3(a,b,c) & \equiv & \Inr(\Inr(\pair{a,b,c})).


1151 
\end{eqnarray*}


1152 
The case analysis operator is


1153 
\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv


1154 
\case(\begin{array}[t]{@{}l}


1155 
\case(\lambda u.f_0,\; f_1),\, \\


1156 
\case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )


1157 
\end{array}


1158 
\]


1159 
This may look cryptic, but the case equations are trivial to verify.


1160 


1161 
In the constructor definitions, the injections are balanced. A more naive


1162 
approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;


1163 
instead, each constructor has two injections. The difference here is small.


1164 
But the \textsc{zf} examples include a 60element enumeration type, where each


1165 
constructor has 5 or~6 injections. The naive approach would require 1 to~59


1166 
injections; the definitions would be quadratic in size. It is like the


1167 
advantage of binary notation over unary.


1168 


1169 
The result structure contains the case operator and constructor definitions as


1170 
the theorem list \verbcon_defs. It contains the case equations, such as


1171 
\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]


1172 
as the theorem list \verbcase_eqns. There is one equation per constructor.


1173 


1174 
\subsection{Proving freeness theorems}


1175 
There are two kinds of freeness theorems:


1176 
\begin{itemize}


1177 
\item \defn{injectiveness} theorems, such as


1178 
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]


1179 


1180 
\item \defn{distinctness} theorems, such as


1181 
\[ \Con_1(a) \not= \Con_2(a',b') \]


1182 
\end{itemize}


1183 
Since the number of such theorems is quadratic in the number of constructors,


1184 
the package does not attempt to prove them all. Instead it returns tools for


1185 
proving desired theorems  either manually or during


1186 
simplification or classical reasoning.


1187 


1188 
The theorem list \verbfree_iffs enables the simplifier to perform freeness


1189 
reasoning. This works by incremental unfolding of constructors that appear in


1190 
equations. The theorem list contains logical equivalences such as


1191 
\begin{eqnarray*}


1192 
\Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\


1193 
\Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\


1194 
& \vdots & \\


1195 
\Inl(a)=\Inl(b) & \bimp & a=b \\


1196 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\


1197 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'


1198 
\end{eqnarray*}


1199 
For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.


1200 


1201 
The theorem list \verbfree_SEs enables the classical


1202 
reasoner to perform similar replacements. It consists of elimination rules


1203 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the


1204 
assumptions.


1205 


1206 
Such incremental unfolding combines freeness reasoning with other proof


1207 
steps. It has the unfortunate sideeffect of unfolding definitions of


1208 
constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should


1209 
be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs}


1210 
restores the defined constants.


1211 


1212 


1213 
\section{Related work}\label{related}


1214 
The use of least fixedpoints to express inductive definitions seems


1215 
obvious. Why, then, has this technique so seldom been implemented?


1216 


1217 
Most automated logics can only express inductive definitions by asserting


1218 
axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if their


1219 
shell principle were removed. With \textsc{alf} the situation is more


1220 
complex; earlier versions of MartinL\"of's type theory could (using


1221 
wellordering types) express datatype definitions, but the version underlying


1222 
\textsc{alf} requires new rules for each definition~\cite{dybjer91}. With Coq


1223 
the situation is subtler still; its underlying Calculus of Constructions can


1224 
express inductive definitions~\cite{huet88}, but cannot quite handle datatype


1225 
definitions~\cite{paulintlca}. It seems that researchers tried hard to


1226 
circumvent these problems before finally extending the Calculus with rule


1227 
schemes for strictly positive operators. Recently Gim{\'e}nez has extended


1228 
the Calculus of Constructions with inductive and coinductive


1229 
types~\cite{gimenezcodifying}, with mechanized support in Coq.


1230 


1231 
Higherorder logic can express inductive definitions through quantification


1232 
over unary predicates. The following formula expresses that~$i$ belongs to the


1233 
least set containing~0 and closed under~$\succ$:


1234 
\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \]


1235 
This technique can be used to prove the KnasterTarski theorem, which (in its


1236 
general form) is little used in the Cambridge \textsc{hol} system.


1237 
Melham~\cite{melham89} describes the development. The natural numbers are


1238 
defined as shown above, but lists are defined as functions over the natural


1239 
numbers. Unlabelled trees are defined using G\"odel numbering; a labelled


1240 
tree consists of an unlabelled tree paired with a list of labels. Melham's


1241 
datatype package expresses the user's datatypes in terms of labelled trees.


1242 
It has been highly successful, but a fixedpoint approach might have yielded


1243 
greater power with less effort.


1244 


1245 
Elsa Gunter~\cite{guntertrees} reports an ongoing project to generalize the


1246 
Cambridge \textsc{hol} system with mutual recursion and infinitelybranching


1247 
trees. She retains many features of Melham's approach.


1248 


1249 
Melham's inductive definition package~\cite{camilleri92} also uses


1250 
quantification over predicates. But instead of formalizing the notion of


1251 
monotone function, it requires definitions to consist of finitary rules, a


1252 
syntactic form that excludes many monotone inductive definitions.


1253 


1254 
\textsc{pvs}~\cite{pvslanguage} is another proof assistant based on


1255 
higherorder logic. It supports both inductive definitions and datatypes,


1256 
apparently by asserting axioms. Datatypes may not be iterated in general, but


1257 
may use recursion over the builtin $\lst$ type.


1258 


1259 
The earliest use of least fixedpoints is probably Robin Milner's. Brian


1260 
Monahan extended this package considerably~\cite{monahan84}, as did I in


1261 
unpublished work.\footnote{The datatype package described in my \textsc{lcf}


1262 
book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts


1263 
axioms.} \textsc{lcf} is a firstorder logic of domain theory; the relevant


1264 
fixedpoint theorem is not KnasterTarski but concerns fixedpoints of


1265 
continuous functions over domains. \textsc{lcf} is too weak to express


1266 
recursive predicates. The Isabelle package might be the first to be based on


1267 
the KnasterTarski theorem.


1268 


1269 


1270 
\section{Conclusions and future work}


1271 
Higherorder logic and set theory are both powerful enough to express


1272 
inductive definitions. A growing number of theorem provers implement one


1273 
of these~\cite{IMPS,saaltinkfme}. The easiest sort of inductive


1274 
definition package to write is one that asserts new axioms, not one that


1275 
makes definitions and proves theorems about them. But asserting axioms


1276 
could introduce unsoundness.


1277 


1278 
The fixedpoint approach makes it fairly easy to implement a package for


1279 
(co)in\duc\tive definitions that does not assert axioms. It is efficient:


1280 
it processes most definitions in seconds and even a 60constructor datatype


1281 
requires only a few minutes. It is also simple: The first working version took


1282 
under a week to code, consisting of under 1100 lines (35K bytes) of Standard


1283 
\textsc{ml}.


1284 


1285 
In set theory, care is needed to ensure that the inductive definition yields


1286 
a set (rather than a proper class). This problem is inherent to set theory,


1287 
whether or not the KnasterTarski theorem is employed. We must exhibit a


1288 
bounding set (called a domain above). For inductive definitions, this is


1289 
often trivial. For datatype definitions, I have had to formalize much set


1290 
theory. To justify infinitelybranching datatype definitions, I have had to


1291 
develop a theory of cardinal arithmetic~\cite{paulsongr}, such as the theorem


1292 
that if $\kappa$ is an infinite cardinal and $X(\alpha) \le \kappa$ for all


1293 
$\alpha<\kappa$ then $\union\sb{\alpha<\kappa} X(\alpha) \le \kappa$.


1294 
The need for such efforts is not a drawback of the fixedpoint approach, for


1295 
the alternative is to take such definitions on faith.


1296 


1297 
Care is also needed to ensure that the greatest fixedpoint really yields a


1298 
coinductive definition. In set theory, standard pairs admit only wellfounded


1299 
constructions. Aczel's antifoundation axiom~\cite{aczel88} could be used to


1300 
get nonwellfounded objects, but it does not seem easy to mechanize.


1301 
Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which


1302 
can be generalized to a variant notion of function. Elsewhere I have


1303 
proved that this simple approach works (yielding final coalgebras) for a broad


1304 
class of definitions~\cite{paulsonfinal}.


1305 


1306 
Several large studies make heavy use of inductive definitions. L\"otzbeyer


1307 
and Sandner have formalized two chapters of a semantics book~\cite{winskel93},


1308 
proving the equivalence between the operational and denotational semantics of


1309 
a simple imperative language. A single theory file contains three datatype


1310 
definitions (of arithmetic expressions, boolean expressions and commands) and


1311 
three inductive definitions (the corresponding operational rules). Using


1312 
different techniques, Nipkow~\cite{nipkowCR} and Rasmussen~\cite{rasmussen95}


1313 
have both proved the ChurchRosser theorem; inductive definitions specify


1314 
several reduction relations on $\lambda$terms. Recently, I have applied


1315 
inductive definitions to the analysis of cryptographic


1316 
protocols~\cite{paulsonmarkt}.


1317 


1318 
To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the


1319 
consistency of the dynamic and static semantics for a small functional


1320 
language. The example is due to Milner and Tofte~\cite{milnercoind}. It


1321 
concerns an extended correspondence relation, which is defined coinductively.


1322 
A codatatype definition specifies values and value environments in mutual


1323 
recursion. Nonwellfounded values represent recursive functions. Value


1324 
environments are variant functions from variables into values. This one key


1325 
definition uses most of the package's novel features.


1326 


1327 
The approach is not restricted to set theory. It should be suitable for any


1328 
logic that has some notion of set and the KnasterTarski theorem. I have


1329 
ported the (co)inductive definition package from Isabelle/\textsc{zf} to


1330 
Isabelle/\textsc{hol} (higherorder logic). V\"olker~\cite{voelker95}


1331 
is investigating how to port the (co)datatype package. \textsc{hol}


1332 
represents sets by unary predicates; defining the corresponding types may


1333 
cause complications.


1334 


1335 


1336 
\begin{footnotesize}


1337 
\bibliographystyle{springer}


1338 
\bibliography{stringabbrv,atp,theory,funprog,isabelle,crossref}


1339 
\end{footnotesize}


1340 
%%%%%\doendnotes


1341 


1342 
\ifshort\typeout{****Omitting appendices}


1343 
\else


1344 
\newpage


1345 
\appendix


1346 
\section{Inductive and coinductive definitions: users guide}


1347 
A theory file may contain any number of inductive and coinductive


1348 
definitions. They may be intermixed with other declarations; in


1349 
particular, the (co)inductive sets \defn{must} be declared separately as


1350 
constants, and may have mixfix syntax or be subject to syntax translations.


1351 


1352 
The syntax is rather complicated. Please consult the examples above and the


1353 
theory files on the \textsc{zf} source directory.


1354 


1355 
Each (co)inductive definition adds definitions to the theory and also proves


1356 
some theorems. Each definition creates an \textsc{ml} structure, which is a


1357 
substructure of the main theory structure.


1358 


1359 
Inductive and datatype definitions can take up considerable storage. The


1360 
introduction rules are replicated in slightly different forms as fixedpoint


1361 
definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's


1362 
six definitions occupy over 600K in total. Defining the 60constructor


1363 
datatype requires nearly 560K\@.


1364 


1365 
\subsection{The result structure}


1366 
Many of the result structure's components have been discussed


1367 
in~\S\ref{basicsec}; others are selfexplanatory.


1368 
\begin{description}


1369 
\item[\tt thy] is the new theory containing the recursive sets.


1370 


1371 
\item[\tt defs] is the list of definitions of the recursive sets.


1372 


1373 
\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.


1374 


1375 
\item[\tt dom\_subset] is a theorem stating inclusion in the domain.


1376 


1377 
\item[\tt intrs] is the list of introduction rules, now proved as theorems, for


1378 
the recursive sets. The rules are also available individually, using the


1379 
names given them in the theory file.


1380 


1381 
\item[\tt elim] is the elimination rule.


1382 


1383 
\item[\tt mk\_cases] is a function to create simplified instances of {\tt


1384 
elim}, using freeness reasoning on some underlying datatype.


1385 
\end{description}


1386 


1387 
For an inductive definition, the result structure contains two induction


1388 
rules, {\tt induct} and \verbmutual_induct. (To save storage, the latter


1389 
rule is just {\tt True} unless more than one set is being defined.) For a


1390 
coinductive definition, it contains the rule \verbcoinduct.


1391 


1392 
Figure~\ref{defresultfig} summarizes the two result signatures,


1393 
specifying the types of all these components.


1394 


1395 
\begin{figure}


1396 
\begin{ttbox}


1397 
sig


1398 
val thy : theory


1399 
val defs : thm list


1400 
val bnd_mono : thm


1401 
val dom_subset : thm


1402 
val intrs : thm list


1403 
val elim : thm


1404 
val mk_cases : thm list > string > thm


1405 
{\it(Inductive definitions only)}


1406 
val induct : thm


1407 
val mutual_induct: thm


1408 
{\it(Coinductive definitions only)}


1409 
val coinduct : thm


1410 
end


1411 
\end{ttbox}


1412 
\hrule


1413 
\caption{The result of a (co)inductive definition} \label{defresultfig}


1414 
\end{figure}


1415 


1416 
\subsection{The syntax of a (co)inductive definition}


1417 
An inductive definition has the form


1418 
\begin{ttbox}


1419 
inductive


1420 
domains {\it domain declarations}


1421 
intrs {\it introduction rules}


1422 
monos {\it monotonicity theorems}


1423 
con_defs {\it constructor definitions}


1424 
type_intrs {\it introduction rules for typechecking}


1425 
type_elims {\it elimination rules for typechecking}


1426 
\end{ttbox}


1427 
A coinductive definition is identical, but starts with the keyword


1428 
{\tt coinductive}.


1429 


1430 
The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}


1431 
sections are optional. If present, each is specified as a string, which


1432 
must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply


1433 
inserted into the {\tt .thy.ML} file; if it is illformed, it will trigger


1434 
\textsc{ml} error messages. You can then inspect the file on your directory.


1435 


1436 
\begin{description}


1437 
\item[\it domain declarations] consist of one or more items of the form


1438 
{\it string\/}~{\tt <=}~{\it string}, associating each recursive set with


1439 
its domain.


1440 


1441 
\item[\it introduction rules] specify one or more introduction rules in


1442 
the form {\it ident\/}~{\it string}, where the identifier gives the name of


1443 
the rule in the result structure.


1444 


1445 
\item[\it monotonicity theorems] are required for each operator applied to


1446 
a recursive set in the introduction rules. There \defn{must} be a theorem


1447 
of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$


1448 
in an introduction rule!


1449 


1450 
\item[\it constructor definitions] contain definitions of constants


1451 
appearing in the introduction rules. The (co)datatype package supplies


1452 
the constructors' definitions here. Most (co)inductive definitions omit


1453 
this section; one exception is the primitive recursive functions example


1454 
(\S\ref{primrecsec}).


1455 


1456 
\item[\it type\_intrs] consists of introduction rules for typechecking the


1457 
definition, as discussed in~\S\ref{basicsec}. They are applied using


1458 
depthfirst search; you can trace the proof by setting


1459 


1460 
\verbtrace_DEPTH_FIRST := true.


1461 


1462 
\item[\it type\_elims] consists of elimination rules for typechecking the


1463 
definition. They are presumed to be safe and are applied as much as


1464 
possible, prior to the {\tt type\_intrs} search.


1465 
\end{description}


1466 


1467 
The package has a few notable restrictions:


1468 
\begin{itemize}


1469 
\item The theory must separately declare the recursive sets as


1470 
constants.


1471 


1472 
\item The names of the recursive sets must be identifiers, not infix


1473 
operators.


1474 


1475 
\item Sideconditions must not be conjunctions. However, an introduction rule


1476 
may contain any number of sideconditions.


1477 


1478 
\item Sideconditions of the form $x=t$, where the variable~$x$ does not


1479 
occur in~$t$, will be substituted through the rule \verbmutual_induct.


1480 
\end{itemize}


1481 


1482 
Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,


1483 
thanks to typechecking. There are no \texttt{domains}, \texttt{type\_intrs}


1484 
or \texttt{type\_elims} parts.


1485 


1486 


1487 
\section{Datatype and codatatype definitions: users guide}


1488 
This section explains how to include (co)datatype declarations in a theory


1489 
file. Please include {\tt Datatype} as a parent theory; this makes available


1490 
the definitions of $\univ$ and $\quniv$.


1491 


1492 


1493 
\subsection{The result structure}


1494 
The result structure extends that of (co)inductive definitions


1495 
(Figure~\ref{defresultfig}) with several additional items:


1496 
\begin{ttbox}


1497 
val con_defs : thm list


1498 
val case_eqns : thm list


1499 
val free_iffs : thm list


1500 
val free_SEs : thm list


1501 
val mk_free : string > thm


1502 
\end{ttbox}


1503 
Most of these have been discussed in~\S\ref{datasec}. Here is a summary:


1504 
