author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 9695  ec7d7f877712 
child 42637  381fdcab0f36 
permissions  rwrr 
4265  1 
%% $Id$ 
7829  2 
\documentclass[12pt,a4paper]{article} 
9695  3 
\usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup} 
3162  4 

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

6 
\shortfalse%%%%%\shorttrue 

7 

8 
\title{A Fixedpoint Approach to\\ 

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

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

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

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

13 

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

15 
Computer Laboratory, University of Cambridge, England} 

16 
\date{\today} 

17 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 

18 

19 
\newcommand\sbs{\subseteq} 

20 
\let\To=\Rightarrow 

21 

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

23 

24 
\newcommand\pow{{\cal P}} 

25 
\newcommand\RepFun{\hbox{\tt RepFun}} 

26 
\newcommand\cons{\hbox{\tt cons}} 

27 
\def\succ{\hbox{\tt succ}} 

28 
\newcommand\split{\hbox{\tt split}} 

29 
\newcommand\fst{\hbox{\tt fst}} 

30 
\newcommand\snd{\hbox{\tt snd}} 

31 
\newcommand\converse{\hbox{\tt converse}} 

32 
\newcommand\domain{\hbox{\tt domain}} 

33 
\newcommand\range{\hbox{\tt range}} 

34 
\newcommand\field{\hbox{\tt field}} 

35 
\newcommand\lfp{\hbox{\tt lfp}} 

36 
\newcommand\gfp{\hbox{\tt gfp}} 

37 
\newcommand\id{\hbox{\tt id}} 

38 
\newcommand\trans{\hbox{\tt trans}} 

39 
\newcommand\wf{\hbox{\tt wf}} 

40 
\newcommand\nat{\hbox{\tt nat}} 

41 
\newcommand\rank{\hbox{\tt rank}} 

42 
\newcommand\univ{\hbox{\tt univ}} 

43 
\newcommand\Vrec{\hbox{\tt Vrec}} 

44 
\newcommand\Inl{\hbox{\tt Inl}} 

45 
\newcommand\Inr{\hbox{\tt Inr}} 

46 
\newcommand\case{\hbox{\tt case}} 

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

48 
\newcommand\Nil{\hbox{\tt Nil}} 

49 
\newcommand\Cons{\hbox{\tt Cons}} 

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

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

52 
\newcommand\length{\hbox{\tt length}} 

53 
\newcommand\listn{\hbox{\tt listn}} 

54 
\newcommand\acc{\hbox{\tt acc}} 

55 
\newcommand\primrec{\hbox{\tt primrec}} 

56 
\newcommand\SC{\hbox{\tt SC}} 

57 
\newcommand\CONST{\hbox{\tt CONST}} 

58 
\newcommand\PROJ{\hbox{\tt PROJ}} 

59 
\newcommand\COMP{\hbox{\tt COMP}} 

60 
\newcommand\PREC{\hbox{\tt PREC}} 

61 

62 
\newcommand\quniv{\hbox{\tt quniv}} 

63 
\newcommand\llist{\hbox{\tt llist}} 

64 
\newcommand\LNil{\hbox{\tt LNil}} 

65 
\newcommand\LCons{\hbox{\tt LCons}} 

66 
\newcommand\lconst{\hbox{\tt lconst}} 

67 
\newcommand\lleq{\hbox{\tt lleq}} 

68 
\newcommand\map{\hbox{\tt map}} 

69 
\newcommand\term{\hbox{\tt term}} 

70 
\newcommand\Apply{\hbox{\tt Apply}} 

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

72 
\newcommand\rev{\hbox{\tt rev}} 

73 
\newcommand\reflect{\hbox{\tt reflect}} 

74 
\newcommand\tree{\hbox{\tt tree}} 

75 
\newcommand\forest{\hbox{\tt forest}} 

76 
\newcommand\Part{\hbox{\tt Part}} 

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

78 
\newcommand\Tcons{\hbox{\tt Tcons}} 

79 
\newcommand\Fcons{\hbox{\tt Fcons}} 

80 
\newcommand\Fnil{\hbox{\tt Fnil}} 

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

82 
\newcommand\Fin{\hbox{\tt Fin}} 

83 
\newcommand\QInl{\hbox{\tt QInl}} 

84 
\newcommand\QInr{\hbox{\tt QInr}} 

85 
\newcommand\qsplit{\hbox{\tt qsplit}} 

86 
\newcommand\qcase{\hbox{\tt qcase}} 

87 
\newcommand\Con{\hbox{\tt Con}} 

88 
\newcommand\data{\hbox{\tt data}} 

89 

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

91 

92 
\begin{document} 

93 
\pagestyle{empty} 

94 
\begin{titlepage} 

95 
\maketitle 

96 
\begin{abstract} 

97 
This paper presents a fixedpoint approach to inductive definitions. 

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

99 
approach lets definitions involve any operators that have been proved 

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

101 
implementation of mutual recursion and iterated definitions. It also 

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

103 
greatest fixedpoint. 

104 

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

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

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

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

109 
recursive functions. One example of a coinductive definition is 

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

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

112 

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

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

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

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

117 
\end{abstract} 

118 
% 

119 
\bigskip 

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

121 
\thispagestyle{empty} 

122 
\end{titlepage} 

123 
\tableofcontents\cleardoublepage\pagestyle{plain} 

124 

125 
\setcounter{page}{1} 

126 

127 
\section{Introduction} 

128 
Several theorem provers provide commands for formalizing recursive data 

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

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

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

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

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

134 
Such data structures are called \defn{datatypes} 

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

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

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

138 

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

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

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

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

143 
logic is inductively defined. A structural operational 

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

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

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

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

148 

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

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

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

152 
Important examples include using bisimulation relations to formalize 

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

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

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

156 

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

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

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

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

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

162 
to prove it. 

163 

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

165 
fixedpoints yield inductive definitions; greatest fixedpoints yield 

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

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

168 

169 
The package supports mutual recursion and infinitelybranching datatypes and 

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

171 
thus accepting all provably monotone inductive definitions, including 

172 
iterated definitions. 

173 

174 
The package has been implemented in 

175 
Isabelle~\cite{paulsonmarkt,paulsonisabook} using 

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

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

178 
recursion equations are specified as introduction rules for the mutually 

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

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

181 
successful, the package makes fixedpoint definitions and proves the 

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

183 
by making simple declarations in Isabelle theory files. 

184 

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

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

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

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

189 
to use than structural recursion but considerably more general. 

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

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

192 

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

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

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

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

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

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

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

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

201 

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

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

204 

205 
\section{Fixedpoint operators} 

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

207 
follows: 

208 
\begin{eqnarray*} 

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

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

211 
\end{eqnarray*} 

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

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

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

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

216 
\begin{eqnarray*} 

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

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

219 
\end{eqnarray*} 

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

221 
that every monotonic function over a complete lattice has a 

6745  222 
fixedpoint~\cite{daveypriestley}. It is obvious from their definitions 
3162  223 
that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest. 
224 

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

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

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

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

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

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

231 
sets are also called \defn{domains}. 

232 

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

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

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

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

237 

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

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

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

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

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

243 
under an injection. Reasons for this are discussed 

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

245 

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

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

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

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

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

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

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

253 
inductive definition package. 

254 

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

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

257 

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

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

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

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

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

263 

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

265 
sets, satisfying the rule 

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

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

268 

269 
The ability to introduce new monotone operators makes the approach 

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

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

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

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

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

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

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

277 

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

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

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

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

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

283 

284 
\subsection{The fixedpoint definitions} 

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

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

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

288 
defined as the least set closed under the rules 

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

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

291 
\] 

292 

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

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

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

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

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

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

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

300 
\end{array} 

301 
\] 

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

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

304 
of~$\lfp$. 

305 

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

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

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

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

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

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

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

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

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

315 

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

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

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

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

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

321 
definition is monotonic. 

322 

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

324 
such as 

325 
\[ 

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

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

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

329 
\end{array} 

330 
\] 

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

332 

333 

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

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

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

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

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

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

340 

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

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

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

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

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

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

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

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

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

350 

351 

352 
\subsection{Proving the introduction rules} 

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

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

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

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

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

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

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

360 
attempting to prove the result. 

361 

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

363 
in the rules, the package must prove 

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

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

366 
\] 

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

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

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

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

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

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

373 
definition through! 

374 

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

376 
intrs}. 

377 

378 
\subsection{The case analysis rule} 

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

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

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

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

383 
is written 

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

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

386 
\] 

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

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

389 

390 

391 
\section{Induction and coinduction rules} 

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

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

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

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

396 
basic coinduction rule. 

397 

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

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

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

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

402 

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

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

405 
product; inductively defined relations are treated slightly differently. 

406 

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

408 
introduction rule: 

409 
\begin{itemize} 

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

411 
is~$P(t)$. 

412 

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

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

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

416 

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

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

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

420 
then the minor premise discharges the single assumption 

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

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

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

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

425 
\end{itemize} 

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

427 
but includes an induction hypothesis: 

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

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

430 
\] 

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

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

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

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

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

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

437 

438 

439 
\subsection{Modified induction rules} 

440 

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

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

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

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

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

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

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

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

449 
split} appears in the rule. 

450 

451 
The mutual induction rule is called {\tt 

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

453 
\begin{itemize} 

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

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

456 

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

458 
refers to all the recursive sets: 

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

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

461 
\] 

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

463 
\ldots,~$n$. 

464 
\end{itemize} 

465 
% 

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

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

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

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

470 

471 
\subsection{Coinduction}\label{coindsec} 

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

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

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

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

476 
greatest set consistent with the rules 

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

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

479 
\] 

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

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

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

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

484 

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

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

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

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

489 
\infer*{ 

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

491 
z=\LNil\disj 

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

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

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

495 
\] 

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

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

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

499 
is the set of natural numbers.) 

500 

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

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

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

504 

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

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

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

508 

509 

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

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

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

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

514 

515 
\subsection{The finite powerset operator} 

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

517 
corresponding invocation in an Isabelle theory file. Note that 

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

519 
\begin{ttbox} 

520 
Finite = Arith + 

521 
consts Fin :: i=>i 

522 
inductive 

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

524 
intrs 

525 
emptyI "0 : Fin(A)" 

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

6124
3aa7926f039a
deleted the appendices because documentation exists in the HOL and ZF manuals
paulson
parents:
4265
diff
changeset

527 
type_intrs empty_subsetI, cons_subsetI, PowI 
3162  528 
type_elims "[make_elim PowD]" 
529 
end 

530 
\end{ttbox} 

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

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

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

534 
introduction rules. For typechecking, we supply two introduction 

535 
rules: 

536 
\[ \emptyset\sbs A \qquad 

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

538 
\] 

539 
A further introduction rule and an elimination rule express both 

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

541 
involves mostly introduction rules. 

542 

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

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

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

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

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

548 
rule is {\tt Fin.induct}. 

549 

550 

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

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

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

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

555 
But her introduction rules 

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

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

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

559 
\] 

560 
are not acceptable to the inductive definition package: 

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

562 

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

564 
varying parameters. It uses the existing datatype definition of 

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

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

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

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

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

570 
rules are 

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

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

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

574 
\] 

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

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

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

578 
\begin{ttbox} 

579 
ListN = List + 

580 
consts listn :: i=>i 

581 
inductive 

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

583 
intrs 

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

6631  585 
ConsI "[ a:A; <n,l>:listn(A) ] ==> <succ(n), Cons(a,l)>: listn(A)" 
3162  586 
type_intrs "nat_typechecks @ list.intrs" 
587 
end 

588 
\end{ttbox} 

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

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

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

592 
package always includes the rules for ordered pairs. 

593 

594 
The package returns introduction, elimination and induction rules for 

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

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

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

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

599 
\] 

600 
This rule lets the induction formula to be a 

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

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

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

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

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

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

607 
$n$element list. 

608 

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

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

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

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

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

614 
\] 

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

616 

6637  617 
\subsection{Rule inversion: the function \texttt{mk\_cases}} 
3162  618 
The elimination rule, {\tt listn.elim}, is cumbersome: 
619 
\[ \infer{Q}{x\in\listn(A) & 

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

621 
\infer*{Q} 

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

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

624 
a\in A \\ 

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

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

627 
\] 

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

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

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

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

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

633 
Here is a sample session: 

634 
\begin{ttbox} 

6141  635 
listn.mk_cases "<i,Nil> : listn(A)"; 
3162  636 
{\out "[ <?i, []> : listn(?A); ?i = 0 ==> ?Q ] ==> ?Q" : thm} 
6141  637 
listn.mk_cases "<i,Cons(a,l)> : listn(A)"; 
3162  638 
{\out "[ <?i, Cons(?a, ?l)> : listn(?A);} 
639 
{\out !!n. [ ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) ] ==> ?Q } 

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

641 
\end{ttbox} 

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

643 
second rule is 

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

645 
\infer*{Q} 

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

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

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

649 
\] 

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

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

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

653 

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

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

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

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

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

659 
\] 

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

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

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

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

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

665 
residuals~\cite{rasmussen95}. 

666 

667 

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

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

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

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

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

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

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

675 

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

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

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

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

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

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

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

683 
coinduction principle for equalities. 

684 

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

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

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

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

689 
\] 

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

691 
bisimulation. Equivalence can be coinductively defined as the greatest 

692 
fixedpoint for the introduction rules 

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

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

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

696 
\] 

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

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

6631  699 
\bgroup\leftmargini=\parindent 
3162  700 
\begin{ttbox} 
701 
consts lleq :: i=>i 

702 
coinductive 

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

704 
intrs 

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

6631  706 
LCons "[ a:A; <l,l'>:lleq(A) ] ==> <LCons(a,l),LCons(a,l')>: lleq(A)" 
3162  707 
type_intrs "llist.intrs" 
708 
\end{ttbox} 

6631  709 
\egroup 
3162  710 
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The typechecking 
711 
rules include the introduction rules for $\llist(A)$, whose 

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

713 

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

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

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

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

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

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

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

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

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

723 
\end{array} 

724 
}{[z\in X]_z} 

725 
\] 

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

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

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

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

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

731 

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

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

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

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

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

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

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

739 
introduction rule of the form 

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

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

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

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

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

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

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

747 

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

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

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

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

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

753 

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

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

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

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

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

759 
\begin{ttbox} 

760 
consts acc :: i=>i 

761 
inductive 

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

763 
intrs 

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

6124
3aa7926f039a
deleted the appendices because documentation exists in the HOL and ZF manuals
paulson
parents:
4265
diff
changeset

765 
monos Pow_mono 
3162  766 
\end{ttbox} 
767 
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For 

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

769 
$\acc(\prec)$. 

770 

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

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

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

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

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

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

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

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

779 
\end{array} 

780 
\right]_a}} 

781 
\] 

782 
The strange induction hypothesis is equivalent to 

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

784 
Therefore the rule expresses wellfounded induction on the accessible part 

785 
of~$\prec$. 

786 

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

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

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

790 
equivalently as 

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

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

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

794 
where $M=\lst$. 

795 

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

797 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

801 
the notion of composition, is less easily circumvented. 

802 

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

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

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

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

807 
\begin{itemize} 

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

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

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

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

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

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

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

815 
such that 

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

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

818 

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

820 
recursive, such that 

821 
\begin{eqnarray*} 

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

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

824 
\end{eqnarray*} 

825 
\end{itemize} 

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

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

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

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

830 
tuplevalued functions. This modified the inductive definition such that 

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

832 

833 
\begin{figure} 

834 
\begin{ttbox} 

6631  835 
Primrec_defs = Main + 
836 
consts SC :: i 

837 
\(\vdots\) 

3162  838 
defs 
6631  839 
SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)" 
840 
\(\vdots\) 

841 
end 

842 

843 
Primrec = Primrec_defs + 

844 
consts prim_rec :: i 

3162  845 
inductive 
6631  846 
domains "primrec" <= "list(nat)>nat" 
847 
intrs 

848 
SC "SC : primrec" 

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

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

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

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

853 
monos list_mono 

854 
con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def 

855 
type_intrs "nat_typechecks @ list.intrs @ 

856 
[lam_type, list_case_type, drop_type, map_type, 

857 
apply_type, rec_type]" 

3162  858 
end 
859 
\end{ttbox} 

860 
\hrule 

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

862 
\label{primrecfig} 

863 
\end{figure} 

864 
\def\fs{{\it fs}} 

865 

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

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

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

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

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

871 
$\COMP$: 

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

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

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

875 
an unusual induction hypothesis: 

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

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

878 
\] 

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

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

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

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

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

884 

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

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

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

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

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

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

891 

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

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

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

895 

896 

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

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

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

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

901 
involving any pair of constructors. 

902 

903 

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

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

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

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

908 
as domains for (co)inductive definitions. 

909 

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

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

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

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

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

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

916 

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

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

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

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

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

922 
constructors for~$R_i$ are pairwise distinct. 

923 

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

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

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

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

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

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

930 

931 
The standard pairs and injections can only yield wellfounded 

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

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

934 
contain nonwellfounded objects. 

935 

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

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

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

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

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

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

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

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

6631  944 
elsewhere~\cite{paulsonmscs}. 
3162  945 

946 
\subsection{The case analysis operator} 

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

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

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

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

951 
for products and sums. 

952 

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

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

955 
\begin{eqnarray*} 

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

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

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

959 
\end{eqnarray*} 

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

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

962 
constructor: 

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

964 
\qquad i = 1, \ldots, k 

965 
\] 

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

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

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

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

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

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

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

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

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

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

976 
$\qsplit$ and~$\qcase$. 

977 

978 
\medskip 

979 

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

981 
examine some examples. Further details are available 

982 
elsewhere~\cite{paulsonsetII}. 

983 

984 

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

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

987 
file: 

988 
\begin{ttbox} 

989 
consts list :: i=>i 

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

991 
\end{ttbox} 

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

993 
\begin{ttbox} 

994 
consts llist :: i=>i 

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

996 
\end{ttbox} 

997 

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

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

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

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

1002 
can be overridden. 

1003 

1004 
\ifshort 

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

1006 
\else 

6631  1007 
Since $\lst(A)$ is a datatype, it has a structural induction rule, {\tt 
3162  1008 
list.induct}: 
1009 
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) 

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

1011 
\] 

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

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

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

1015 
consequence, which justifies structural recursion on lists 

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

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

1018 
\par 

1019 
\fi 

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

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

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

1023 
components, fixedpoint operators can create cyclic constructions. For 

1024 
example, the definition 

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

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

1027 

1028 
\ifshort 

1029 
\typeout{****SHORT VERSION} 

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

1031 
\else 

1032 
\medskip 

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

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

1035 
The list constructors are defined as follows: 

1036 
\begin{eqnarray*} 

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

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

1039 
\end{eqnarray*} 

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

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

1042 
Let us verify the two equations: 

1043 
\begin{eqnarray*} 

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

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

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

1047 
& = & c\\[1ex] 

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

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

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

1051 
& = & h(x,y) 

1052 
\end{eqnarray*} 

1053 
\fi 

1054 

1055 

1056 
\ifshort 

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

1058 
\else 

1059 
\subsection{Example: mutual recursion} 

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

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

1062 
$\Fnil$ and~$\Fcons$: 

1063 
\begin{ttbox} 

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

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

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

1067 
\end{ttbox} 

1068 
The three introduction rules define the mutual recursion. The 

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

1070 

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

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

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

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

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

1076 
\end{array} 

1077 
\right]_{a,f}} 

1078 
& P(\Fnil) 

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

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

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

1082 
\end{array} 

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

1084 
\] 

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

6631  1086 
recursive sets. Although such reasoning can be useful 
3162  1087 
\cite[\S4.5]{paulsonsetII}, a proper mutual induction rule should establish 
1088 
separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this 

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

1090 
the induction hypotheses: 

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

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

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

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

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

1096 
\end{array} 

1097 
\right]_{a,f}} 

1098 
& Q(\Fnil) 

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

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

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

1102 
\end{array} 

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

1104 
\] 

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

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

1107 

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

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

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

1111 
\begin{eqnarray*} 

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

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

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

1115 
\end{eqnarray*} 

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

1117 
forests: 

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

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

1120 
\] 

1121 
\fi 

1122 

1123 

1124 
\subsection{Example: a fourconstructor datatype} 

1125 
A bigger datatype will illustrate some efficiency 

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

1127 
corresponding arities. 

1128 
\begin{ttbox} 

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

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

1131 
 Con1 ("a: A") 

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

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

1134 
\end{ttbox} 

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

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

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

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

1139 

1140 
The constructors are defined by the equations 

1141 
\begin{eqnarray*} 

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

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

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

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

1146 
\end{eqnarray*} 

1147 
The case analysis operator is 

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

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

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

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

1152 
\end{array} 

1153 
\] 

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

1155 

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

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

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

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

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

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

1162 
advantage of binary notation over unary. 

1163 

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

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

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

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

1168 

1169 
\subsection{Proving freeness theorems} 

1170 
There are two kinds of freeness theorems: 

1171 
\begin{itemize} 

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

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

1174 

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

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

1177 
\end{itemize} 

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

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

1180 
proving desired theorems  either manually or during 

1181 
simplification or classical reasoning. 

1182 

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

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

1185 
equations. The theorem list contains logical equivalences such as 

1186 
\begin{eqnarray*} 

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

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

1189 
& \vdots & \\ 

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

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

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

1193 
\end{eqnarray*} 

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

1195 

1196 
The theorem list \verbfree_SEs enables the classical 

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

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

1199 
assumptions. 

1200 

1201 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1205 
restores the defined constants. 

1206 

1207 

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

1209 
The use of least fixedpoints to express inductive definitions seems 

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

1211 

1212 
Most automated logics can only express inductive definitions by asserting 

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

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

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

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

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

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

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

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

1221 
circumvent these problems before finally extending the Calculus with rule 

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

1223 
the Calculus of Constructions with inductive and coinductive 

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

1225 

1226 
Higherorder logic can express inductive definitions through quantification 

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

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

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

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

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

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

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

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

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

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

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

1238 
greater power with less effort. 

1239 

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

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

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

1243 

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

1245 
quantification over predicates. But instead of formalizing the notion of 

1246 
monotone function, it requires definitions to consist of finitary rules, a 

1247 
syntactic form that excludes many monotone inductive definitions. 

1248 

1249 
\textsc{pvs}~\cite{pvslanguage} is another proof assistant based on 

1250 
higherorder logic. It supports both inductive definitions and datatypes, 

1251 
apparently by asserting axioms. Datatypes may not be iterated in general, but 

1252 
may use recursion over the builtin $\lst$ type. 

1253 

1254 
The earliest use of least fixedpoints is probably Robin Milner's. Brian 

1255 
Monahan extended this package considerably~\cite{monahan84}, as did I in 

1256 
unpublished work.\footnote{The datatype package described in my \textsc{lcf} 

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

1258 
axioms.} \textsc{lcf} is a firstorder logic of domain theory; the relevant 

1259 
fixedpoint theorem is not KnasterTarski but concerns fixedpoints of 

1260 
continuous functions over domains. \textsc{lcf} is too weak to express 

1261 
recursive predicates. The Isabelle package might be the first to be based on 

1262 
the KnasterTarski theorem. 

1263 

1264 

1265 
\section{Conclusions and future work} 

1266 
Higherorder logic and set theory are both powerful enough to express 

1267 
inductive definitions. A growing number of theorem provers implement one 

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

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

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

1271 
could introduce unsoundness. 

1272 

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

1274 
(co)in\duc\tive definitions that does not assert axioms. It is efficient: 

1275 
it processes most definitions in seconds and even a 60constructor datatype 

1276 
requires only a few minutes. It is also simple: The first working version took 

1277 
under a week to code, consisting of under 1100 lines (35K bytes) of Standard 

1278 
\textsc{ml}. 

1279 

1280 
In set theory, care is needed to ensure that the inductive definition yields 

1281 
a set (rather than a proper class). This problem is inherent to set theory, 

1282 
whether or not the KnasterTarski theorem is employed. We must exhibit a 

1283 
bounding set (called a domain above). For inductive definitions, this is 

1284 
often trivial. For datatype definitions, I have had to formalize much set 

1285 
theory. To justify infinitelybranching datatype definitions, I have had to 

1286 
develop a theory of cardinal arithmetic~\cite{paulsongr}, such as the theorem 

1287 
that if $\kappa$ is an infinite cardinal and $X(\alpha) \le \kappa$ for all 

1288 
$\alpha<\kappa$ then $\union\sb{\alpha<\kappa} X(\alpha) \le \kappa$. 

1289 
The need for such efforts is not a drawback of the fixedpoint approach, for 

1290 
the alternative is to take such definitions on faith. 

1291 

1292 
Care is also needed to ensure that the greatest fixedpoint really yields a 

1293 
coinductive definition. In set theory, standard pairs admit only wellfounded 

1294 
constructions. Aczel's antifoundation axiom~\cite{aczel88} could be used to 

1295 
get nonwellfounded objects, but it does not seem easy to mechanize. 

1296 
Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which 

1297 
can be generalized to a variant notion of function. Elsewhere I have 

1298 
proved that this simple approach works (yielding final coalgebras) for a broad 

6631  1299 
class of definitions~\cite{paulsonmscs}. 
3162  1300 

1301 
Several large studies make heavy use of inductive definitions. L\"otzbeyer 

1302 
and Sandner have formalized two chapters of a semantics book~\cite{winskel93}, 

1303 
proving the equivalence between the operational and denotational semantics of 

1304 
a simple imperative language. A single theory file contains three datatype 

1305 
definitions (of arithmetic expressions, boolean expressions and commands) and 

1306 
three inductive definitions (the corresponding operational rules). Using 

1307 
different techniques, Nipkow~\cite{nipkowCR} and Rasmussen~\cite{rasmussen95} 

1308 
have both proved the ChurchRosser theorem; inductive definitions specify 

1309 
several reduction relations on $\lambda$terms. Recently, I have applied 

1310 
inductive definitions to the analysis of cryptographic 

1311 
protocols~\cite{paulsonmarkt}. 

1312 

1313 
To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the 

1314 
consistency of the dynamic and static semantics for a small functional 

1315 
language. The example is due to Milner and Tofte~\cite{milnercoind}. It 

1316 
concerns an extended correspondence relation, which is defined coinductively. 

1317 
A codatatype definition specifies values and value environments in mutual 

1318 
recursion. Nonwellfounded values represent recursive functions. Value 

1319 
environments are variant functions from variables into values. This one key 

1320 
definition uses most of the package's novel features. 

1321 

1322 
The approach is not restricted to set theory. It should be suitable for any 

1323 
logic that has some notion of set and the KnasterTarski theorem. I have 

1324 
ported the (co)inductive definition package from Isabelle/\textsc{zf} to 

6631  1325 
Isabelle/\textsc{hol} (higherorder logic). 
3162  1326 

1327 

1328 
\begin{footnotesize} 

6637  1329 
\bibliographystyle{plain} 
6631  1330 
\bibliography{../manual} 
3162  1331 
\end{footnotesize} 
1332 
%%%%%\doendnotes 

1333 

1334 
\end{document} 