author  lcp 
Tue, 12 Jul 1994 18:05:03 +0200  
changeset 467  92868dab2939 
parent 455  466dd59b3645 
child 497  990d2573efa6 
permissions  rwrr 
355  1 
\documentstyle[a4,proof,iman,extra,times]{llncs} 
103  2 
\newif\ifCADE 
355  3 
\CADEtrue 
103  4 

355  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 

9 
`Types'.}} 

103  10 

355  11 
\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}} 
12 
\institute{Computer Laboratory, University of Cambridge, England} 

103  13 
\date{\today} 
14 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 

15 

16 
\newcommand\sbs{\subseteq} 

17 
\let\To=\Rightarrow 

18 

19 

355  20 
\newcommand\pow{{\cal P}} 
21 
%%%\let\pow=\wp 

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}} 

103  47 
\newcommand\lstcase{\hbox{\tt list\_case}} 
48 
\newcommand\lstrec{\hbox{\tt list\_rec}} 

355  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}} 

103  58 

355  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}} 

103  78 
\newcommand\TFcase{\hbox{\tt TF\_case}} 
355  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}} 

103  86 

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

88 

89 
\begin{document} 

355  90 
%CADE%\pagestyle{empty} 
91 
%CADE%\begin{titlepage} 

103  92 
\maketitle 
93 
\begin{abstract} 

355  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. 

130  102 

103 
The method has been implemented in Isabelle's formalization of ZF set 

179  104 
theory. It should be applicable to any logic in which the KnasterTarski 
355  105 
Theorem can be proved. Examples include lists of $n$ elements, the 
106 
accessible part of a relation and the set of primitive recursive 

107 
functions. One example of a coinductive definition is bisimulations for 

108 
lazy lists. \ifCADE\else Recursive datatypes are examined in detail, as 

109 
well as one example of a {\bf codatatype}: lazy lists. The appendices 

110 
are simple user's manuals for this Isabelle/ZF package.\fi 

103  111 
\end{abstract} 
112 
% 

355  113 
%CADE%\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} 
114 
%CADE%\thispagestyle{empty} 

115 
%CADE%\end{titlepage} 

116 
%CADE%\tableofcontents\cleardoublepage\pagestyle{headings} 

103  117 

118 
\section{Introduction} 

119 
Several theorem provers provide commands for formalizing recursive data 

120 
structures, like lists and trees. Examples include Boyer and Moore's shell 

121 
principle~\cite{bm79} and Melham's recursive type package for the HOL 

122 
system~\cite{melham89}. Such data structures are called {\bf datatypes} 

123 
below, by analogy with {\tt datatype} definitions in Standard~ML\@. 

124 

130  125 
A datatype is but one example of an {\bf inductive definition}. This 
103  126 
specifies the least set closed under given rules~\cite{aczel77}. The 
127 
collection of theorems in a logic is inductively defined. A structural 

128 
operational semantics~\cite{hennessy90} is an inductive definition of a 

129 
reduction or evaluation relation on programs. A few theorem provers 

130 
provide commands for formalizing inductive definitions; these include 

131 
Coq~\cite{paulin92} and again the HOL system~\cite{camilleri92}. 

132 

130  133 
The dual notion is that of a {\bf coinductive definition}. This specifies 
103  134 
the greatest set closed under given rules. Important examples include 
135 
using bisimulation relations to formalize equivalence of 

136 
processes~\cite{milner89} or lazy functional programs~\cite{abramsky90}. 

137 
Other examples include lazy lists and other infinite data structures; these 

130  138 
are called {\bf codatatypes} below. 
103  139 

355  140 
Not all inductive definitions are meaningful. {\bf Monotone} inductive 
141 
definitions are a large, wellbehaved class. Monotonicity can be enforced 

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

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

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

145 
to prove it. 

103  146 

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

148 
fixedpoints yield inductive definitions; greatest fixedpoints yield 

355  149 
coinductive definitions. The package has several advantages: 
103  150 
\begin{itemize} 
355  151 
\item It allows reference to any operators that have been proved monotone. 
152 
Thus it accepts all provably monotone inductive definitions, including 

153 
iterated definitions. 

154 
\item It accepts a wide class of datatype definitions, though at present 

155 
restricted to finite branching. 

130  156 
\item It handles coinductive and codatatype definitions. Most of 
157 
the discussion below applies equally to inductive and coinductive 

103  158 
definitions, and most of the code is shared. To my knowledge, this is 
130  159 
the only package supporting coinductive definitions. 
103  160 
\item Definitions may be mutually recursive. 
161 
\end{itemize} 

162 
The package is implemented in Isabelle~\cite{isabelleintro}, using ZF set 

163 
theory \cite{paulsonsetI,paulsonsetII}. However, the fixedpoint 

164 
approach is independent of Isabelle. The recursion equations are specified 

165 
as introduction rules for the mutually recursive sets. The package 

166 
transforms these rules into a mapping over sets, and attempts to prove that 

167 
the mapping is monotonic and welltyped. If successful, the package 

168 
makes fixedpoint definitions and proves the introduction, elimination and 

130  169 
(co)induction rules. The package consists of several Standard ML 
103  170 
functors~\cite{paulson91}; it accepts its argument and returns its result 
355  171 
as ML structures.\footnote{This use of ML modules is not essential; the 
172 
package could also be implemented as a function on records.} 

103  173 

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

355  175 
recursive functions. This is the main omission from my package. Its 
176 
fixedpoint operators define only recursive sets. To define recursive 

177 
functions, the Isabelle/ZF theory provides wellfounded recursion and other 

178 
logical tools~\cite{paulsonsetII}. 

103  179 

355  180 
{\bf Outline.} Section~2 introduces the least and greatest fixedpoint 
181 
operators. Section~3 discusses the form of introduction rules, mutual 

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

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

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

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

186 
Section~8 draws brief conclusions. \ifCADE\else The appendices are simple 

187 
user's manuals for this Isabelle/ZF package.\fi 

103  188 

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

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

191 

192 
\section{Fixedpoint operators} 

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

194 
follows: 

195 
\begin{eqnarray*} 

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

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

198 
\end{eqnarray*} 

130  199 
Let $D$ be a set. Say that $h$ is {\bf bounded by}~$D$ if $h(D)\sbs D$, and 
200 
{\bf monotone below~$D$} if 

103  201 
$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is 
202 
bounded by~$D$ and monotone then both operators yield fixedpoints: 

203 
\begin{eqnarray*} 

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

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

206 
\end{eqnarray*} 

355  207 
These equations are instances of the KnasterTarski Theorem, which states 
103  208 
that every monotonic function over a complete lattice has a 
209 
fixedpoint~\cite{davey&priestley}. It is obvious from their definitions 

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

211 

355  212 
This fixedpoint theory is simple. The KnasterTarski Theorem is easy to 
103  213 
prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must 
355  214 
also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as 
179  215 
when a set of `theorems' is (co)inductively defined over some previously 
355  216 
existing set of `formulae.' Isabelle/ZF provides a suitable bounding set 
217 
for finitely branching (co)datatype definitions; see~\S\ref{univsec} 

218 
below. Bounding sets are also called {\bf domains}. 

103  219 

355  220 
The powerset operator is monotone, but by Cantor's Theorem there is no 
221 
set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because 

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

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

103  224 

130  225 
\section{Elements of an inductive or coinductive definition}\label{basicsec} 
226 
Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in 

355  227 
mutual recursion. They will be constructed from domains $D_1$, 
228 
\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but 

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

230 
under an injection. Reasons for this are discussed 

130  231 
elsewhere~\cite[\S4.5]{paulsonsetII}. 
103  232 

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

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

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

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

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

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

355  239 
varies. Section~\ref{listnsec} describes how to express this set using the 
130  240 
inductive definition package. 
103  241 

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

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

244 

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

246 
The body of the definition consists of the desired introduction rules, 

247 
specified as strings. The conclusion of each rule must have the form $t\in 

248 
R_i$, where $t$ is any term. Premises typically have the same form, but 

249 
they can have the more general form $t\in M(R_i)$ or express arbitrary 

250 
sideconditions. 

251 

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

253 
sets, satisfying the rule 

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

130  255 
The user must supply the package with monotonicity rules for all such premises. 
103  256 

355  257 
The ability to introduce new monotone operators makes the approach 
258 
flexible. A suitable choice of~$M$ and~$t$ can express a lot. The 

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

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

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

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

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

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

103  265 

266 
Introduction rules may also contain {\bf sideconditions}. These are 

267 
premises consisting of arbitrary formulae not mentioning the recursive 

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

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

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

271 

272 
\subsection{The fixedpoint definitions} 

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

455  274 
definition. Consider, as a running example, the finite powerset operator 
103  275 
$\Fin(A)$: the set of all finite subsets of~$A$. It can be 
276 
defined as the least set closed under the rules 

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

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

279 
\] 

280 

130  281 
The domain in a (co)inductive definition must be some existing set closed 
103  282 
under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all 
283 
subsets of~$A$. The package generates the definition 

284 
\begin{eqnarray*} 

285 
\Fin(A) & \equiv & \lfp(\pow(A), \; 

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

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

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

289 
\end{array} 

130  290 
\end{eqnarray*} 
103  291 
The contribution of each rule to the definition of $\Fin(A)$ should be 
130  292 
obvious. A coinductive definition is similar but uses $\gfp$ instead 
103  293 
of~$\lfp$. 
294 

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

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

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

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

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

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

130  301 
connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect 
302 
to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and 

103  303 
only if $\forall x.P(x)\imp Q(x)$.} 
304 

355  305 
The package returns its result as an ML structure, which consists of named 
306 
components; we may regard it as a record. The result structure contains 

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

308 
It also contains, as the theorem {\tt unfold}, a fixedpoint equation such 

309 
as 

103  310 
\begin{eqnarray*} 
311 
\Fin(A) & = & 

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

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

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

315 
\end{array} 

316 
\end{eqnarray*} 

130  317 
It also contains, as the theorem {\tt dom\_subset}, an inclusion such as 
103  318 
$\Fin(A)\sbs\pow(A)$. 
319 

320 

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

130  322 
In a mutually recursive definition, the domain of the fixedpoint construction 
103  323 
is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$, 
324 
\ldots,~$n$. The package uses the injections of the 

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

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

328 
As discussed elsewhere \cite[\S4.5]{paulsonsetII}, Isabelle/ZF defines the 

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

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

331 
\begin{eqnarray*} 

332 
\Part(A,h) & \equiv & \{x\in A. \exists z. x=h(z)\}. 

333 
\end{eqnarray*} 

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

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

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

337 
\begin{eqnarray*} 

130  338 
R_i & \equiv & \Part(R,h_{in}), \qquad i=1,\ldots, n. 
103  339 
\end{eqnarray*} 
340 
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. 

341 

342 

343 
\subsection{Proving the introduction rules} 

130  344 
The user supplies the package with the desired form of the introduction 
103  345 
rules. Once it has derived the theorem {\tt unfold}, it attempts 
130  346 
to prove those rules. From the user's point of view, this is the 
103  347 
trickiest stage; the proofs often fail. The task is to show that the domain 
348 
$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is 

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

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

351 
attempting to prove the result. 

352 

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

354 
in the rules, the package must prove 

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

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

357 
\] 

358 
Such proofs can be regarded as typechecking the definition. The user 

359 
supplies the package with typechecking rules to apply. Usually these are 

360 
general purpose rules from the ZF theory. They could however be rules 

361 
specifically proved for a particular inductive definition; sometimes this is 

362 
the easiest way to get the definition through! 

363 

130  364 
The result structure contains the introduction rules as the theorem list {\tt 
365 
intrs}. 

103  366 

355  367 
\subsection{The case analysis rule} 
368 
The elimination rule, called {\tt elim}, performs case analysis. There is one 

130  369 
case for each introduction rule. The elimination rule 
370 
for $\Fin(A)$ is 

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

373 
\] 

355  374 
The subscripted variables $a$ and~$b$ above the third premise are 
375 
eigenvariables, subject to the usual `not free in \ldots' proviso. 

376 
The rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else 

130  377 
$x=\{a\}\un b$ for some $a\in A$ and $b\in\Fin(A)$; it is a simple consequence 
378 
of {\tt unfold}. 

379 

355  380 
The package also returns a function for generating simplified instances of 
381 
the case analysis rule. It works for datatypes and for inductive 

382 
definitions involving datatypes, such as an inductively defined relation 

383 
between lists. It instantiates {\tt elim} with a usersupplied term then 

384 
simplifies the cases using freeness of the underlying datatype. The 

385 
simplified rules perform `rule inversion' on the inductive definition. 

386 
Section~\S\ref{mkcases} presents an example. 

387 

103  388 

130  389 
\section{Induction and coinduction rules} 
390 
Here we must consider inductive and coinductive definitions separately. 

103  391 
For an inductive definition, the package returns an induction rule derived 
392 
directly from the properties of least fixedpoints, as well as a modified 

393 
rule for mutual recursion and inductively defined relations. For a 

130  394 
coinductive definition, the package returns a basic coinduction rule. 
103  395 

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

130  397 
The basic rule, called {\tt induct}, is appropriate in most situations. 
103  398 
For inductive definitions, it is strong rule induction~\cite{camilleri92}; for 
399 
datatype definitions (see below), it is just structural induction. 

400 

401 
The induction rule for an inductively defined set~$R$ has the following form. 

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

403 
introduction rule: 

404 
\begin{itemize} 

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

406 
is~$P(t)$. 

407 

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

130  409 
rule's free variables that are not parameters of~$R$. For instance, the 
410 
eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$. 

103  411 

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

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

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

415 
then the minor premise discharges the single assumption 

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

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

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

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

420 
\end{itemize} 

130  421 
The induction rule for $\Fin(A)$ resembles the elimination rule shown above, 
422 
but includes an induction hypothesis: 

103  423 
\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset) 
424 
& \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} } 

425 
\] 

355  426 
Stronger induction rules often suggest themselves. We can derive a rule 
427 
for $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in 

428 
b$. The Isabelle/ZF theory defines the {\bf rank} of a 

429 
set~\cite[\S3.4]{paulsonsetII}, which supports wellfounded induction and 

430 
recursion over datatypes. The package proves a rule for mutual induction 

431 
and inductive relations. 

103  432 

433 
\subsection{Mutual induction} 

434 
The mutual induction rule is called {\tt 

435 
mutual\_induct}. It differs from the basic rule in several respects: 

436 
\begin{itemize} 

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

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

439 

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

441 
refers to all the recursive sets: 

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

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

444 
\] 

355  445 
Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$, 
446 
\ldots,~$n$. 

103  447 

448 
\item If the domain of some $R_i$ is the Cartesian product 

449 
$A_1\times\cdots\times A_m$, then the corresponding predicate $P_i$ takes $m$ 

450 
arguments and the corresponding conjunct of the conclusion is 

451 
\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) 

452 
\] 

453 
\end{itemize} 

454 
The last point above simplifies reasoning about inductively defined 

455 
relations. It eliminates the need to express properties of $z_1$, 

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

457 

130  458 
\subsection{Coinduction}\label{coindsec} 
459 
A coinductive definition yields a primitive coinduction rule, with no 

103  460 
refinements such as those for the induction rules. (Experience may suggest 
130  461 
refinements later.) Consider the codatatype of lazy lists as an example. For 
103  462 
suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the 
463 
greatest fixedpoint satisfying the rules 

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

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

466 
\] 

130  467 
The $()$ tag stresses that this is a coinductive definition. A suitable 
103  468 
domain for $\llist(A)$ is $\quniv(A)$, a set closed under variant forms of 
469 
sum and product for representing infinite data structures 

130  470 
(see~\S\ref{univsec}). Coinductive definitions use these variant sums and 
103  471 
products. 
472 

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

355  474 
Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ 
103  475 
is the greatest solution to this equation contained in $\quniv(A)$: 
130  476 
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & 
103  477 
\infer*{z=\LNil\disj \bigl(\exists a\,l.\, 
355  478 
z=\LCons(a,l) \conj a\in A \conj l\in X\un\llist(A) \bigr)} 
479 
{[z\in X]_z}} 

480 
% \begin{array}[t]{@{}l} 

481 
% z=\LCons(a,l) \conj a\in A \conj{}\\ 

482 
% l\in X\un\llist(A) \bigr) 

483 
% \end{array} }{[z\in X]_z}} 

103  484 
\] 
130  485 
This rule complements the introduction rules; it provides a means of showing 
486 
$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then 

355  487 
applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$ 
488 
is the set of natural numbers.) 

130  489 

103  490 
Having $X\un\llist(A)$ instead of simply $X$ in the third premise above 
491 
represents a slight strengthening of the greatest fixedpoint property. I 

130  492 
discuss several forms of coinduction rules elsewhere~\cite{paulsoncoind}. 
103  493 

494 

130  495 
\section{Examples of inductive and coinductive definitions}\label{indegsec} 
455  496 
This section presents several examples: the finite powerset operator, 
103  497 
lists of $n$ elements, bisimulations on lazy lists, the wellfounded part 
498 
of a relation, and the primitive recursive functions. 

499 

455  500 
\subsection{The finite powerset operator} 
501 
This operator has been discussed extensively above. Here 

103  502 
is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates 
503 
$\{a\}\un b$ in Isabelle/ZF): 

504 
\begin{ttbox} 

505 
structure Fin = Inductive_Fun 

355  506 
(val thy = Arith.thy addconsts [(["Fin"],"i=>i")] 
507 
val rec_doms = [("Fin","Pow(A)")] 

508 
val sintrs = ["0 : Fin(A)", 

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

510 
val monos = [] 

511 
val con_defs = [] 

512 
val type_intrs = [empty_subsetI, cons_subsetI, PowI] 

103  513 
val type_elims = [make_elim PowD]); 
514 
\end{ttbox} 

355  515 
We apply the functor {\tt Inductive\_Fun} to a structure describing the 
516 
desired inductive definition. The parent theory~{\tt thy} is obtained from 

517 
{\tt Arith.thy} by adding the unary function symbol~$\Fin$. Its domain is 

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

519 
introduction rules. For typechecking, the structure supplies introduction 

520 
rules: 

103  521 
\[ \emptyset\sbs A \qquad 
522 
\infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} 

523 
\] 

524 
A further introduction rule and an elimination rule express the two 

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

355  526 
involves mostly introduction rules. 
527 

528 
ML is Isabelle's top level, so such functor invocations can take place at 

529 
any time. The result structure is declared with the name~{\tt Fin}; we can 

530 
refer to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction 

531 
rule as {\tt Fin.induct} and so forth. There are plans to integrate the 

532 
package better into Isabelle so that users can place inductive definitions 

533 
in Isabelle theory files instead of applying functors. 

534 

103  535 

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

179  537 
This has become a standard example of an inductive definition. Following 
538 
PaulinMohring~\cite{paulin92}, we could attempt to define a new datatype 

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

540 
But her introduction rules 

355  541 
\[ \hbox{\tt Niln}\in\listn(A,0) \qquad 
542 
\infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} 

103  543 
{n\in\nat & a\in A & l\in\listn(A,n)} 
544 
\] 

545 
are not acceptable to the inductive definition package: 

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

547 

548 
\begin{figure} 

355  549 
\begin{ttbox} 
103  550 
structure ListN = Inductive_Fun 
355  551 
(val thy = ListFn.thy addconsts [(["listn"],"i=>i")] 
552 
val rec_doms = [("listn", "nat*list(A)")] 

553 
val sintrs = 

554 
["<0,Nil>: listn(A)", 

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

556 
val monos = [] 

557 
val con_defs = [] 

558 
val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] 

103  559 
val type_elims = [SigmaE2]); 
355  560 
\end{ttbox} 
103  561 
\hrule 
562 
\caption{Defining lists of $n$ elements} \label{listnfig} 

563 
\end{figure} 

564 

355  565 
The Isabelle/ZF version of this example suggests a general treatment of 
566 
varying parameters. Here, we use the existing datatype definition of 

567 
$\lst(A)$, with constructors $\Nil$ and~$\Cons$. Then incorporate the 

568 
parameter~$n$ into the inductive set itself, defining $\listn(A)$ as a 

569 
relation. It consists of pairs $\pair{n,l}$ such that $n\in\nat$ 

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

571 
converse of the length function on~$\lst(A)$. The Isabelle/ZF introduction 

572 
rules are 

103  573 
\[ \pair{0,\Nil}\in\listn(A) \qquad 
574 
\infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} 

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

576 
\] 

577 
Figure~\ref{listnfig} presents the ML invocation. A theory of lists, 

578 
extended with a declaration of $\listn$, is the parent theory. The domain 

579 
is specified as $\nat\times\lst(A)$. The typechecking rules include those 

580 
for 0, $\succ$, $\Nil$ and $\Cons$. Because $\listn(A)$ is a set of pairs, 

581 
typechecking also requires introduction and elimination rules to express 

582 
both directions of the equivalence $\pair{a,b}\in A\times B \bimp a\in A 

583 
\conj b\in B$. 

584 

585 
The package returns introduction, elimination and induction rules for 

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

587 
\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & 

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

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

590 
\] 

591 
This rule requires the induction formula to be a 

592 
unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt 

593 
ListN.mutual\_induct}, uses a binary property instead: 

130  594 
\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} 
103  595 
{P(0,\Nil) & 
596 
\infer*{P(\succ(n),\Cons(a,l))} 

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

598 
\] 

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

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

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

130  602 
This latter result  here $r``X$ denotes the image of $X$ under $r$ 
103  603 
 asserts that the inductive definition agrees with the obvious notion of 
604 
$n$element list. 

605 

606 
Unlike in Coq, the definition does not declare a new datatype. A `list of 

130  607 
$n$ elements' really is a list and is subject to list operators such 
608 
as append (concatenation). For example, a trivial induction on 

609 
$\pair{m,l}\in\listn(A)$ yields 

103  610 
\[ \infer{\pair{m\mathbin{+} m,\, l@l'}\in\listn(A)} 
611 
{\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 

612 
\] 

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

614 

355  615 
\subsection{A demonstration of rule inversion}\label{mkcases} 
103  616 
The elimination rule, {\tt ListN.elim}, is cumbersome: 
617 
\[ \infer{Q}{x\in\listn(A) & 

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

619 
\infer*{Q} 

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

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

622 
a\in A \\ 

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

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

625 
\] 

179  626 
The ML function {\tt ListN.mk\_cases} generates simplified instances of 
627 
this rule. It works by freeness reasoning on the list constructors: 

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

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

355  630 
deduces the corresponding form of~$i$; this is called rule inversion. For 
631 
example, 

103  632 
\begin{ttbox} 
633 
ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)" 

634 
\end{ttbox} 

130  635 
yields a rule with only two premises: 
103  636 
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
637 
\infer*{Q} 

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

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

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

641 
\] 

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

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

644 
ListN.mk\_cases} can similarly deduce the corresponding form of~$l$. 

645 

355  646 
The function {\tt mk\_cases} is also useful with datatype definitions. The 
647 
instance from the definition of lists, namely {\tt List.mk\_cases}, can 

648 
prove the rule 

103  649 
\[ \infer{Q}{\Cons(a,l)\in\lst(A) & 
650 
& \infer*{Q}{[a\in A &l\in\lst(A)]} } 

651 
\] 

355  652 
A typical use of {\tt mk\_cases} concerns inductive definitions of 
653 
evaluation relations. Then rule inversion yields case analysis on possible 

654 
evaluations. For example, the Isabelle/ZF theory includes a short proof 

655 
of the diamond property for parallel contraction on combinators. 

103  656 

130  657 
\subsection{A coinductive definition: bisimulations on lazy lists} 
658 
This example anticipates the definition of the codatatype $\llist(A)$, which 

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

660 
and 

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

103  662 
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant 
663 
pairing and injection operators, it contains nonwellfounded elements such as 

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

665 

130  666 
The next step in the development of lazy lists is to define a coinduction 
103  667 
principle for proving equalities. This is done by showing that the equality 
668 
relation on lazy lists is the greatest fixedpoint of some monotonic 

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

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

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

130  672 
only if they are equal. The coinduction rule for equivalence then yields a 
673 
coinduction principle for equalities. 

103  674 

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

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

130  677 
\[ \{\pair{\LNil,\LNil}\} \un 
678 
\{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}. 

103  679 
\] 
680 

681 
A pair of lazy lists are {\bf equivalent} if they belong to some bisimulation. 

130  682 
Equivalence can be coinductively defined as the greatest fixedpoint for the 
103  683 
introduction rules 
130  684 
\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad 
685 
\infer[()]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} 

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

103  687 
\] 
130  688 
To make this coinductive definition, we invoke \verbCoInductive_Fun: 
103  689 
\begin{ttbox} 
130  690 
structure LList_Eq = CoInductive_Fun 
355  691 
(val thy = LList.thy addconsts [(["lleq"],"i=>i")] 
692 
val rec_doms = [("lleq", "llist(A) * llist(A)")] 

693 
val sintrs = 

694 
["<LNil, LNil> : lleq(A)", 

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

696 
val monos = [] 

697 
val con_defs = [] 

698 
val type_intrs = LList.intrs @ [SigmaI] 

699 
val type_elims = [SigmaE2]); 

103  700 
\end{ttbox} 
701 
Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. 

130  702 
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The typechecking 
703 
rules include the introduction rules for lazy lists as well as rules 

704 
for both directions of the equivalence 

705 
$\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. 

103  706 

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

130  708 
usual. But instead of induction rules, it returns a coinduction rule. 
103  709 
The rule is too big to display in the usual notation; its conclusion is 
130  710 
$x\in\lleq(A)$ and its premises are $x\in X$, 
711 
${X\sbs\llist(A)\times\llist(A)}$ and 

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

355  713 
z=\pair{\LCons(a,l),\LCons(a,l')} \conj 
714 
a\in A \conj\pair{l,l'}\in X\un\lleq(A) \bigr) 

715 
% \begin{array}[t]{@{}l} 

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

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

718 
% \end{array} 

719 
}{[z\in X]_z} 

103  720 
\] 
130  721 
Thus if $x\in X$, where $X$ is a bisimulation contained in the 
722 
domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that 

103  723 
$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And 
724 
$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that 

130  725 
$\lleq(A)$ coincides with the equality relation takes some work. 
103  726 

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

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

729 
The {\bf accessible} or {\bf wellfounded} part of~$\prec$, written 

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

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

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

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

734 
introduction rule of the form 

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

736 
PaulinMohring treats this example in Coq~\cite{paulin92}, but it causes 

737 
difficulties for other systems. Its premise does not conform to 

738 
the structure of introduction rules for HOL's inductive definition 

739 
package~\cite{camilleri92}. It is also unacceptable to Isabelle package 

130  740 
(\S\ref{introsec}), but fortunately can be transformed into the acceptable 
103  741 
form $t\in M(R)$. 
742 

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

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

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

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

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

748 

749 
The ML invocation below follows this approach. Here $r$ is~$\prec$ and 

130  750 
$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a 
751 
relation is the union of its domain and range.) Finally 

752 
$r^{}``\{a\}$ denotes the inverse image of~$\{a\}$ under~$r$. The package is 

753 
supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic. 

103  754 
\begin{ttbox} 
755 
structure Acc = Inductive_Fun 

355  756 
(val thy = WF.thy addconsts [(["acc"],"i=>i")] 
757 
val rec_doms = [("acc", "field(r)")] 

758 
val sintrs = ["[ r``\{a\}:\,Pow(acc(r)); a:\,field(r) ] ==> a:\,acc(r)"] 

759 
val monos = [Pow_mono] 

760 
val con_defs = [] 

761 
val type_intrs = [] 

103  762 
val type_elims = []); 
763 
\end{ttbox} 

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

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

766 
$\acc(\prec)$. 

767 

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

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

770 
induction rule, {\tt Acc.induct}: 

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

772 
\infer*{P(a)}{[r^{}``\{a\}\in\pow(\{z\in\acc(r).P(z)\}) & 

773 
a\in\field(r)]_a}} 

774 
\] 

775 
The strange induction hypothesis is equivalent to 

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

777 
Therefore the rule expresses wellfounded induction on the accessible part 

778 
of~$\prec$. 

779 

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

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

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

783 
equivalently as 

130  784 
\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
103  785 
provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The 
786 
following section demonstrates another use of the premise $t\in M(R)$, 

787 
where $M=\lst$. 

788 

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

790 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

794 
the notion of composition, is less easily circumvented. 

795 

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

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

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

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

800 
\begin{itemize} 

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

802 
\item All {\bf constant} functions $\CONST(k)$, such that 

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

804 
\item All {\bf projection} functions $\PROJ(i)$, such that 

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

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

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

808 
such that 

809 
\begin{eqnarray*} 

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

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

812 
\end{eqnarray*} 

813 

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

815 
recursive, such that 

816 
\begin{eqnarray*} 

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

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

819 
\end{eqnarray*} 

820 
\end{itemize} 

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

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

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

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

825 
tuplevalued functions. This modified the inductive definition such that 

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

827 

828 
\begin{figure} 

355  829 
\begin{ttbox} 
103  830 
structure Primrec = Inductive_Fun 
355  831 
(val thy = Primrec0.thy 
832 
val rec_doms = [("primrec", "list(nat)>nat")] 

833 
val sintrs = 

834 
["SC : primrec", 

835 
"k: nat ==> CONST(k) : primrec", 

836 
"i: nat ==> PROJ(i) : primrec", 

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

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

839 
val monos = [list_mono] 

840 
val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def] 

841 
val type_intrs = pr0_typechecks 

103  842 
val type_elims = []); 
355  843 
\end{ttbox} 
103  844 
\hrule 
845 
\caption{Inductive definition of the primitive recursive functions} 

846 
\label{primrecfig} 

847 
\end{figure} 

848 
\def\fs{{\it fs}} 

849 
Szasz was using ALF, but Coq and HOL would also have problems accepting 

850 
this definition. Isabelle's package accepts it easily since 

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

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

355  853 
the five forms of primitive recursive function. Let us examine the one for 
854 
$\COMP$: 

103  855 
\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \] 
856 
The induction rule for $\primrec$ has one case for each introduction rule. 

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

858 
an unusual induction hypothesis: 

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

130  860 
{[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} \] 
103  861 
The hypothesis states that $\fs$ is a list of primitive recursive functions 
862 
satisfying the induction formula. Proving the $\COMP$ case typically requires 

863 
structural induction on lists, yielding two subcases: either $\fs=\Nil$ or 

864 
else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and $\fs'$ is 

865 
another list of primitive recursive functions satisfying~$P$. 

866 

867 
Figure~\ref{primrecfig} presents the ML invocation. Theory {\tt 

355  868 
Primrec0.thy} defines the constants $\SC$, $\CONST$, etc. These are not 
869 
constructors of a new datatype, but functions over lists of numbers. Their 

870 
definitions, which are omitted, consist of routine list programming. In 

871 
Isabelle/ZF, the primitive recursive functions are defined as a subset of 

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

103  873 

355  874 
The Isabelle theory goes on to formalize Ackermann's function and prove 
875 
that it is not primitive recursive, using the induction rule {\tt 

876 
Primrec.induct}. The proof follows Szasz's excellent account. 

103  877 

878 

130  879 
\section{Datatypes and codatatypes}\label{datasec} 
880 
A (co)datatype definition is a (co)inductive definition with automatically 

355  881 
defined constructors and a case analysis operator. The package proves that 
882 
the case operator inverts the constructors and can prove freeness theorems 

103  883 
involving any pair of constructors. 
884 

885 

130  886 
\subsection{Constructors and their domain}\label{univsec} 
355  887 
Conceptually, our two forms of definition are distinct. A (co)inductive 
888 
definition selects a subset of an existing set; a (co)datatype definition 

889 
creates a new set. But the package reduces the latter to the former. A 

890 
set having strong closure properties must serve as the domain of the 

891 
(co)inductive definition. Constructing this set requires some theoretical 

892 
effort, which must be done anyway to show that (co)datatypes exist. It is 

893 
not obvious that standard set theory is suitable for defining codatatypes. 

103  894 

895 
Isabelle/ZF defines the standard notion of Cartesian product $A\times B$, 

896 
containing ordered pairs $\pair{a,b}$. Now the $m$tuple 

355  897 
$\pair{x_1,\ldots,x_m}$ is the empty set~$\emptyset$ if $m=0$, simply 
898 
$x_1$ if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. 

103  899 
Isabelle/ZF also defines the disjoint sum $A+B$, containing injections 
900 
$\Inl(a)\equiv\pair{0,a}$ and $\Inr(b)\equiv\pair{1,b}$. 

901 

355  902 
A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be 
903 
$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. 

103  904 
In a mutually recursive definition, all constructors for the set~$R_i$ have 
130  905 
the outer form~$h_{in}$, where $h_{in}$ is the injection described 
103  906 
in~\S\ref{mutualsec}. Further nested injections ensure that the 
907 
constructors for~$R_i$ are pairwise distinct. 

908 

909 
Isabelle/ZF defines the set $\univ(A)$, which contains~$A$ and 

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

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

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

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

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

915 

916 
The standard pairs and injections can only yield wellfounded 

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

130  918 
over datatypes. But they are unsuitable for codatatypes, which typically 
103  919 
contain nonwellfounded objects. 
920 

130  921 
To support codatatypes, Isabelle/ZF defines a variant notion of ordered 
103  922 
pair, written~$\pair{a;b}$. It also defines the corresponding variant 
923 
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ 

355  924 
and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines 
103  925 
the set $\quniv(A)$, which contains~$A$ and furthermore contains 
926 
$\pair{a;b}$, $\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a 

130  927 
typical codatatype definition with set parameters $A_1$, \ldots, $A_k$, a 
928 
suitable domain is $\quniv(A_1\un\cdots\un A_k)$. This approach using 

355  929 
standard ZF set theory~\cite{paulsonfinal} is an alternative to adopting 
930 
Aczel's AntiFoundation Axiom~\cite{aczel88}. 

103  931 

932 
\subsection{The case analysis operator} 

130  933 
The (co)datatype package automatically defines a case analysis operator, 
179  934 
called {\tt$R$\_case}. A mutually recursive definition still has only one 
935 
operator, whose name combines those of the recursive sets: it is called 

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

937 
for products and sums. 

103  938 

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

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

941 
\begin{eqnarray*} 

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

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

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

945 
\end{eqnarray*} 

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

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

948 
constructor: 

949 
\begin{eqnarray*} 

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

951 
\qquad i = 1, \ldots, k 

952 
\end{eqnarray*} 

130  953 
The case operator's definition takes advantage of Isabelle's representation 
954 
of syntax in the typed $\lambda$calculus; it could readily be adapted to a 

955 
theorem prover for higherorder logic. If $f$ and~$g$ have metatype 

956 
$i\To i$ then so do $\split(f)$ and 

957 
$\case(f,g)$. This works because $\split$ and $\case$ operate on their last 

958 
argument. They are easily combined to make complex case analysis 

103  959 
operators. Here are two examples: 
960 
\begin{itemize} 

961 
\item $\split(\lambda x.\split(f(x)))$ performs case analysis for 

962 
$A\times (B\times C)$, as is easily verified: 

963 
\begin{eqnarray*} 

964 
\split(\lambda x.\split(f(x)), \pair{a,b,c}) 

965 
& = & (\lambda x.\split(f(x))(a,\pair{b,c}) \\ 

966 
& = & \split(f(a), \pair{b,c}) \\ 

967 
& = & f(a,b,c) 

968 
\end{eqnarray*} 

969 

970 
\item $\case(f,\case(g,h))$ performs case analysis for $A+(B+C)$; let us 

971 
verify one of the three equations: 

972 
\begin{eqnarray*} 

973 
\case(f,\case(g,h), \Inr(\Inl(b))) 

974 
& = & \case(g,h,\Inl(b)) \\ 

975 
& = & g(b) 

976 
\end{eqnarray*} 

977 
\end{itemize} 

130  978 
Codatatype definitions are treated in precisely the same way. They express 
103  979 
case operators using those for the variant products and sums, namely 
980 
$\qsplit$ and~$\qcase$. 

981 

355  982 
\medskip 
103  983 

355  984 
\ifCADE The package has processed all the datatypes discussed in 
985 
my earlier paper~\cite{paulsonsetII} and the codatatype of lazy lists. 

986 
Space limitations preclude discussing these examples here, but they are 

987 
distributed with Isabelle. \typeout{****Omitting datatype examples from 

988 
CADE version!} \else 

103  989 

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

991 
examine some examples. These include lists and trees/forests, which I have 

992 
discussed extensively in another paper~\cite{paulsonsetII}. 

993 

994 
\begin{figure} 

995 
\begin{ttbox} 

996 
structure List = Datatype_Fun 

355  997 
(val thy = Univ.thy 
998 
val rec_specs = [("list", "univ(A)", 

999 
[(["Nil"], "i"), 

1000 
(["Cons"], "[i,i]=>i")])] 

1001 
val rec_styp = "i=>i" 

1002 
val ext = None 

1003 
val sintrs = ["Nil : list(A)", 

1004 
"[ a: A; l: list(A) ] ==> Cons(a,l) : list(A)"] 

1005 
val monos = [] 

1006 
val type_intrs = datatype_intrs 

103  1007 
val type_elims = datatype_elims); 
1008 
\end{ttbox} 

1009 
\hrule 

1010 
\caption{Defining the datatype of lists} \label{listfig} 

1011 

1012 
\medskip 

1013 
\begin{ttbox} 

130  1014 
structure LList = CoDatatype_Fun 
355  1015 
(val thy = QUniv.thy 
1016 
val rec_specs = [("llist", "quniv(A)", 

1017 
[(["LNil"], "i"), 

1018 
(["LCons"], "[i,i]=>i")])] 

1019 
val rec_styp = "i=>i" 

1020 
val ext = None 

1021 
val sintrs = ["LNil : llist(A)", 

1022 
"[ a: A; l: llist(A) ] ==> LCons(a,l) : llist(A)"] 

1023 
val monos = [] 

1024 
val type_intrs = codatatype_intrs 

130  1025 
val type_elims = codatatype_elims); 
103  1026 
\end{ttbox} 
1027 
\hrule 

130  1028 
\caption{Defining the codatatype of lazy lists} \label{llistfig} 
103  1029 
\end{figure} 
1030 

1031 
\subsection{Example: lists and lazy lists} 

1032 
Figures \ref{listfig} and~\ref{llistfig} present the ML definitions of 

1033 
lists and lazy lists, respectively. They highlight the (many) similarities 

130  1034 
and (few) differences between datatype and codatatype definitions. 
103  1035 

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

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

1038 
lists over a given set~$A$. Each uses the appropriate domain from a 

1039 
Isabelle/ZF theory: 

1040 
\begin{itemize} 

1041 
\item $\lst(A)$ specifies domain $\univ(A)$ and parent theory {\tt Univ.thy}. 

1042 

1043 
\item $\llist(A)$ specifies domain $\quniv(A)$ and parent theory {\tt 

1044 
QUniv.thy}. 

1045 
\end{itemize} 

1046 

130  1047 
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt 
1048 
List.induct}: 

103  1049 
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) 
1050 
& \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } 

1051 
\] 

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

1053 
Isabelle/ZF defines the rank of a set and proves that the standard pairs and 

1054 
injections have greater rank than their components. An immediate consequence, 

1055 
which justifies structural recursion on lists \cite[\S4.3]{paulsonsetII}, 

1056 
is 

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

1058 

130  1059 
Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has 
1060 
the coinduction rule shown in \S\ref{coindsec}. Since variant pairs and 

103  1061 
injections are monotonic and need not have greater rank than their 
1062 
components, fixedpoint operators can create cyclic constructions. For 

1063 
example, the definition 

1064 
\begin{eqnarray*} 

1065 
\lconst(a) & \equiv & \lfp(\univ(a), \lambda l. \LCons(a,l)) 

1066 
\end{eqnarray*} 

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

1068 

1069 
\medskip 

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

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

1072 
The list constructors are defined as follows: 

1073 
\begin{eqnarray*} 

1074 
\Nil & = & \Inl(\emptyset) \\ 

1075 
\Cons(a,l) & = & \Inr(\pair{a,l}) 

1076 
\end{eqnarray*} 

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

1078 
\begin{eqnarray*} 

1079 
\lstcase(c,h) & \equiv & \case(\lambda u.c, \split(h)) 

1080 
\end{eqnarray*} 

1081 
Let us verify the two equations: 

1082 
\begin{eqnarray*} 

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

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

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

130  1086 
& = & c\\[1ex] 
103  1087 
\lstcase(c, h, \Cons(x,y)) & = & 
1088 
\case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\ 

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

130  1090 
& = & h(x,y) 
103  1091 
\end{eqnarray*} 
1092 

1093 
\begin{figure} 

355  1094 
\begin{ttbox} 
103  1095 
structure TF = Datatype_Fun 
355  1096 
(val thy = Univ.thy 
1097 
val rec_specs = [("tree", "univ(A)", 

1098 
[(["Tcons"], "[i,i]=>i")]), 

1099 
("forest", "univ(A)", 

1100 
[(["Fnil"], "i"), 

1101 
(["Fcons"], "[i,i]=>i")])] 

1102 
val rec_styp = "i=>i" 

1103 
val ext = None 

1104 
val sintrs = 

1105 
["[ a:A; f: forest(A) ] ==> Tcons(a,f) : tree(A)", 

1106 
"Fnil : forest(A)", 

1107 
"[ t: tree(A); f: forest(A) ] ==> Fcons(t,f) : forest(A)"] 

1108 
val monos = [] 

1109 
val type_intrs = datatype_intrs 

103  1110 
val type_elims = datatype_elims); 
355  1111 
\end{ttbox} 
103  1112 
\hrule 
1113 
\caption{Defining the datatype of trees and forests} \label{tffig} 

1114 
\end{figure} 

1115 

1116 

1117 
\subsection{Example: mutual recursion} 

130  1118 
In mutually recursive trees and forests~\cite[\S4.5]{paulsonsetII}, trees 
103  1119 
have the one constructor $\Tcons$, while forests have the two constructors 
1120 
$\Fnil$ and~$\Fcons$. Figure~\ref{tffig} presents the ML 

1121 
definition. It has much in common with that of $\lst(A)$, including its 

1122 
use of $\univ(A)$ for the domain and {\tt Univ.thy} for the parent theory. 

1123 
The three introduction rules define the mutual recursion. The 

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

1125 

1126 
The basic induction rule is called {\tt TF.induct}: 

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

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

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

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

1131 
\end{array} 

1132 
\right]_{a,f}} 

1133 
& P(\Fnil) 

130  1134 
& \infer*{P(\Fcons(t,f))} 
103  1135 
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ 
1136 
f\in\forest(A) \\ P(f) 

1137 
\end{array} 

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

1139 
\] 

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

1141 
recursive sets. 

1142 

1143 
Although such reasoning is sometimes useful 

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

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

1146 
rule {\tt TF.mutual\_induct}. Observe the usage of $P$ and $Q$ in the 

1147 
induction hypotheses: 

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

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

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

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

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

1153 
\end{array} 

1154 
\right]_{a,f}} 

1155 
& Q(\Fnil) 

130  1156 
& \infer*{Q(\Fcons(t,f))} 
103  1157 
{\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\ 
1158 
f\in\forest(A) \\ Q(f) 

1159 
\end{array} 

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

1161 
\] 

1162 
As mentioned above, the package does not define a structural recursion 

1163 
operator. I have described elsewhere how this is done 

1164 
\cite[\S4.5]{paulsonsetII}. 

1165 

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

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

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

1169 
\begin{eqnarray*} 

1170 
\Tcons(a,l) & = & \Inl(\pair{a,l}) \\ 

1171 
\Fnil & = & \Inr(\Inl(\emptyset)) \\ 

1172 
\Fcons(a,l) & = & \Inr(\Inr(\pair{a,l})) 

1173 
\end{eqnarray*} 

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

1175 
forests: 

1176 
\begin{eqnarray*} 

1177 
{\tt tree\_forest\_case}(f,c,g) & \equiv & 

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

1179 
\end{eqnarray*} 

1180 

1181 
\begin{figure} 

355  1182 
\begin{ttbox} 
103  1183 
structure Data = Datatype_Fun 
355  1184 
(val thy = Univ.thy 
1185 
val rec_specs = [("data", "univ(A Un B)", 

1186 
[(["Con0"], "i"), 

1187 
(["Con1"], "i=>i"), 

1188 
(["Con2"], "[i,i]=>i"), 

1189 
(["Con3"], "[i,i,i]=>i")])] 

1190 
val rec_styp = "[i,i]=>i" 

1191 
val ext = None 

1192 
val sintrs = 

1193 
["Con0 : data(A,B)", 

1194 
"[ a: A ] ==> Con1(a) : data(A,B)", 

1195 
"[ a: A; b: B ] ==> Con2(a,b) : data(A,B)", 

1196 
"[ a: A; b: B; d: data(A,B) ] ==> Con3(a,b,d) : data(A,B)"] 

1197 
val monos = [] 

1198 
val type_intrs = datatype_intrs 

103  1199 
val type_elims = datatype_elims); 
355  1200 
\end{ttbox} 
103  1201 
\hrule 
1202 
\caption{Defining the fourconstructor sample datatype} \label{datafig} 

1203 
\end{figure} 

1204 

1205 
\subsection{A fourconstructor datatype} 

1206 
Finally let us consider a fairly general datatype. It has four 

130  1207 
constructors $\Con_0$, \ldots, $\Con_3$, with the 
103  1208 
corresponding arities. Figure~\ref{datafig} presents the ML definition. 
1209 
Because this datatype has two set parameters, $A$ and~$B$, it specifies 

1210 
$\univ(A\un B)$ as its domain. The structural induction rule has four 

1211 
minor premises, one per constructor: 

1212 
\[ \infer{P(x)}{x\in\data(A,B) & 

1213 
P(\Con_0) & 

1214 
\infer*{P(\Con_1(a))}{[a\in A]_a} & 

1215 
\infer*{P(\Con_2(a,b))} 

1216 
{\left[\begin{array}{l} a\in A \\ b\in B \end{array} 

1217 
\right]_{a,b}} & 

1218 
\infer*{P(\Con_3(a,b,d))} 

1219 
{\left[\begin{array}{l} a\in A \\ b\in B \\ 

1220 
d\in\data(A,B) \\ P(d) 

1221 
\end{array} 

1222 
\right]_{a,b,d}} } 

1223 
\] 

1224 

1225 
The constructor definitions are 

1226 
\begin{eqnarray*} 

1227 
\Con_0 & = & \Inl(\Inl(\emptyset)) \\ 

1228 
\Con_1(a) & = & \Inl(\Inr(a)) \\ 

1229 
\Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\ 

1230 
\Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})). 

1231 
\end{eqnarray*} 

1232 
The case operator is 

1233 
\begin{eqnarray*} 

1234 
{\tt data\_case}(f_0,f_1,f_2,f_3) & \equiv & 

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

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

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

1238 
\end{array} 

1239 
\end{eqnarray*} 

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

1241 

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

1243 
approach is to define $\Con_3(a,b,c)$ as 

1244 
$\Inr(\Inr(\Inr(\pair{a,b,c})))$; instead, each constructor has two 

1245 
injections. The difference here is small. But the ZF examples include a 

1246 
60element enumeration type, where each constructor has 5 or~6 injections. 

1247 
The naive approach would require 1 to~59 injections; the definitions would be 

1248 
quadratic in size. It is like the difference between the binary and unary 

1249 
numeral systems. 

1250 

130  1251 
The result structure contains the case operator and constructor definitions as 
1252 
the theorem list \verbcon_defs. It contains the case equations, such as 

103  1253 
\begin{eqnarray*} 
1254 
{\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) & = & f_3(a,b,c), 

1255 
\end{eqnarray*} 

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

1257 

1258 
\subsection{Proving freeness theorems} 

1259 
There are two kinds of freeness theorems: 

1260 
\begin{itemize} 

1261 
\item {\bf injectiveness} theorems, such as 

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

1263 

1264 
\item {\bf distinctness} theorems, such as 

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

1266 
\end{itemize} 

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

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

1269 
proving desired theorems  either explicitly or `on the fly' during 

1270 
simplification or classical reasoning. 

1271 

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

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

1274 
equations. The theorem list contains logical equivalences such as 

1275 
\begin{eqnarray*} 

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

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

1278 
& \vdots & \\ 

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

130  1280 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ 
103  1281 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 
1282 
\end{eqnarray*} 

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

1284 

1285 
The theorem list \verbfree_SEs enables the classical 

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

355  1287 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the 
103  1288 
assumptions. 
1289 

1290 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1294 
restores the defined constants. 

1295 
\fi %CADE 

1296 

355  1297 
\section{Related work}\label{related} 
1298 
The use of least fixedpoints to express inductive definitions seems 

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

1300 

1301 
Most automated logics can only express inductive definitions by asserting 

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

1303 
their shell principle were removed. With ALF the situation is more 

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

1305 
wellordering types) express datatype definitions, but the version 

1306 
underlying ALF requires new rules for each definition~\cite{dybjer91}. 

1307 
With Coq the situation is subtler still; its underlying Calculus of 

1308 
Constructions can express inductive definitions~\cite{huet88}, but cannot 

1309 
quite handle datatype definitions~\cite{paulin92}. It seems that 

1310 
researchers tried hard to circumvent these problems before finally 

1311 
extending the Calculus with rule schemes for strictly positive operators. 

1312 

1313 
Higherorder logic can express inductive definitions through quantification 

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

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

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

1317 
This technique can be used to prove the KnasterTarski Theorem, but it is 

1318 
little used in the HOL system. Melham~\cite{melham89} clearly describes 

1319 
the development. The natural numbers are defined as shown above, but lists 

1320 
are defined as functions over the natural numbers. Unlabelled 

1321 
trees are defined using G\"odel numbering; a labelled tree consists of an 

1322 
unlabelled tree paired with a list of labels. Melham's datatype package 

1323 
expresses the user's datatypes in terms of labelled trees. It has been 

1324 
highly successful, but a fixedpoint approach would have yielded greater 

1325 
functionality with less effort. 

1326 

1327 
Melham's inductive definition package~\cite{camilleri92} uses 

1328 
quantification over predicates, which is implicitly a fixedpoint approach. 

1329 
Instead of formalizing the notion of monotone function, it requires 

1330 
definitions to consist of finitary rules, a syntactic form that excludes 

1331 
many monotone inductive definitions. 

1332 

1333 
The earliest use of least fixedpoints is probably Robin Milner's datatype 

1334 
package for Edinburgh LCF~\cite{milnerind}. Brian Monahan extended this 

1335 
package considerably~\cite{monahan84}, as did I in unpublished 

1336 
work.\footnote{The datatype package described in my LCF 

1337 
book~\cite{paulson87} does {\it not\/} make definitions, but merely 

1338 
asserts axioms. I justified this shortcut on grounds of efficiency: 

1339 
existing packages took tens of minutes to run. Such an explanation would 

1340 
not do today.} 

1341 
LCF is a firstorder logic of domain theory; the relevant fixedpoint 

1342 
theorem is not KnasterTarski but concerns fixedpoints of continuous 

1343 
functions over domains. LCF is too weak to express recursive predicates. 

1344 
Thus it would appear that the Isabelle/ZF package is the first to be based 

1345 
on the KnasterTarski Theorem. 

1346 

1347 

103  1348 
\section{Conclusions and future work} 
355  1349 
Higherorder logic and set theory are both powerful enough to express 
1350 
inductive definitions. A growing number of theorem provers implement one 

1351 
of these~\cite{IMPS,saaltinkfme}. The easiest sort of inductive 

1352 
definition package to write is one that asserts new axioms, not one that 

1353 
makes definitions and proves theorems about them. But asserting axioms 

1354 
could introduce unsoundness. 

1355 

1356 
The fixedpoint approach makes it fairly easy to implement a package for 

1357 
(co)inductive definitions that does not assert axioms. It is efficient: it 

103  1358 
processes most definitions in seconds and even a 60constructor datatype 
1359 
requires only two minutes. It is also simple: the package consists of 

1360 
under 1100 lines (35K bytes) of Standard ML code. The first working 

1361 
version took under a week to code. 

1362 

355  1363 
In set theory, care is required to ensure that the inductive definition 
1364 
yields a set (rather than a proper class). This problem is inherent to set 

1365 
theory, whether or not the KnasterTarski Theorem is employed. We must 

1366 
exhibit a bounding set (called a domain above). For inductive definitions, 

1367 
this is often trivial. For datatype definitions, I have had to formalize 

1368 
much set theory. I intend to formalize cardinal arithmetic and the 

1369 
$\aleph$sequence to handle datatype definitions that have infinite 

1370 
branching. The need for such efforts is not a drawback of the fixedpoint 

1371 
approach, for the alternative is to take such definitions on faith. 

103  1372 

355  1373 
The approach is not restricted to set theory. It should be suitable for 
1374 
any logic that has some notion of set and the KnasterTarski Theorem. I 

1375 
intend to use the Isabelle/ZF package as the basis for a higherorder logic 

1376 
one, using Isabelle/HOL\@. The necessary theory is already 

130  1377 
mechanized~\cite{paulsoncoind}. HOL represents sets by unary predicates; 
355  1378 
defining the corresponding types may cause complications. 
103  1379 

1380 

355  1381 
\bibliographystyle{springer} 
1382 
\bibliography{stringabbrv,atp,theory,funprog,isabelle} 

103  1383 
%%%%%\doendnotes 
1384 

1385 
\ifCADE\typeout{****Omitting appendices from CADE version!} 

1386 
\else 

1387 
\newpage 

1388 
\appendix 

130  1389 
\section{Inductive and coinductive definitions: users guide} 
1390 
The ML functors \verbInductive_Fun and \verbCoInductive_Fun build 

1391 
inductive and coinductive definitions, respectively. This section describes 

103  1392 
how to invoke them. 
1393 

1394 
\subsection{The result structure} 

1395 
Many of the result structure's components have been discussed 

1396 
in~\S\ref{basicsec}; others are selfexplanatory. 

1397 
\begin{description} 

1398 
\item[\tt thy] is the new theory containing the recursive sets. 

1399 

1400 
\item[\tt defs] is the list of definitions of the recursive sets. 

1401 

1402 
\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator. 

1403 

1404 
\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of 

1405 
the recursive sets, in the case of mutual recursion). 

1406 

1407 
\item[\tt dom\_subset] is a theorem stating inclusion in the domain. 

1408 

1409 
\item[\tt intrs] is the list of introduction rules, now proved as theorems, for 

1410 
the recursive sets. 

1411 

1412 
\item[\tt elim] is the elimination rule. 

1413 

1414 
\item[\tt mk\_cases] is a function to create simplified instances of {\tt 

1415 
elim}, using freeness reasoning on some underlying datatype. 

1416 
\end{description} 

1417 

1418 
For an inductive definition, the result structure contains two induction rules, 

130  1419 
{\tt induct} and \verbmutual_induct. For a coinductive definition, it 
1420 
contains the rule \verbcoinduct. 

1421 

1422 
Figure~\ref{defresultfig} summarizes the two result signatures, 

1423 
specifying the types of all these components. 

103  1424 

1425 
\begin{figure} 

1426 
\begin{ttbox} 

1427 
sig 

1428 
val thy : theory 

1429 
val defs : thm list 

1430 
val bnd_mono : thm 

1431 
val unfold : thm 

1432 
val dom_subset : thm 

1433 
val intrs : thm list 

1434 
val elim : thm 

1435 
val mk_cases : thm list > string > thm 

1436 
{\it(Inductive definitions only)} 

1437 
val induct : thm 

1438 
val mutual_induct: thm 

130  1439 
{\it(Coinductive definitions only)} 
1440 
val coinduct : thm 

103  1441 
end 
1442 
\end{ttbox} 

1443 
\hrule 

130  1444 
\caption{The result of a (co)inductive definition} \label{defresultfig} 
103  1445 

130  1446 
\medskip 
103  1447 
\begin{ttbox} 
1448 
sig 

1449 
val thy : theory 

1450 
val rec_doms : (string*string) list 

1451 
val sintrs : string list 

1452 
val monos : thm list 

1453 
val con_defs : thm list 

1454 
val type_intrs : thm list 

1455 
val type_elims : thm list 

1456 
end 

1457 
\end{ttbox} 

1458 
\hrule 

130  1459 
\caption{The argument of a (co)inductive definition} \label{defargfig} 
103  1460 
\end{figure} 
1461 

1462 
\subsection{The argument structure} 

130  1463 
Both \verbInductive_Fun and \verbCoInductive_Fun take the same argument 
103  1464 
structure (Figure~\ref{defargfig}). Its components are as follows: 
1465 
\begin{description} 

1466 
\item[\tt thy] is the definition's parent theory, which {\it must\/} 

1467 
declare constants for the recursive sets. 

1468 

1469 
\item[\tt rec\_doms] is a list of pairs, associating the name of each recursive 

1470 
set with its domain. 

1471 

1472 
\item[\tt sintrs] specifies the desired introduction rules as strings. 

1473 

1474 
\item[\tt monos] consists of monotonicity theorems for each operator applied 

1475 
to a recursive set in the introduction rules. 

1476 

1477 
\item[\tt con\_defs] contains definitions of constants appearing in the 

130  1478 
introduction rules. The (co)datatype package supplies the constructors' 
103  1479 
definitions here. Most direct calls of \verbInductive_Fun or 
130  1480 
\verbCoInductive_Fun pass the empty list; one exception is the primitive 
103  1481 
recursive functions example (\S\ref{primrecsec}). 
1482 

1483 
\item[\tt type\_intrs] consists of introduction rules for typechecking the 

1484 
definition, as discussed in~\S\ref{basicsec}. They are applied using 

1485 
depthfirst search; you can trace the proof by setting 

1486 
\verbtrace_DEPTH_FIRST := true. 

1487 

1488 
\item[\tt type\_elims] consists of elimination rules for typechecking the 

1489 
definition. They are presumed to be `safe' and are applied as much as 

1490 
possible, prior to the {\tt type\_intrs} search. 

1491 
\end{description} 

1492 
The package has a few notable restrictions: 

1493 
\begin{itemize} 

1494 
\item The parent theory, {\tt thy}, must declare the recursive sets as 

30bd42401ab2
Initial revision
lcp
