summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/ind-defs.tex

author | oheimb |

Sat Feb 15 16:10:00 1997 +0100 (1997-02-15) | |

changeset 2628 | 1fe7c9f599c2 |

parent 2219 | 5687d7dec139 |

child 2974 | bb55cab416af |

permissions | -rw-r--r-- |

description of del(eq)congs, safe and unsafe solver

1 \documentstyle[a4,alltt,iman,extra,proof209,12pt]{article}

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

3 \shortfalse%%%%%\shorttrue

5 \title{A Fixedpoint Approach to\\

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

7 \thanks{J. Grundy and S. Thompson made detailed

8 comments; the referees were also helpful. Research funded by

9 SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453

10 ``Types''.}}

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

13 Computer Laboratory, University of Cambridge, England}

14 \date{\today}

15 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

17 \newcommand\sbs{\subseteq}

18 \let\To=\Rightarrow

20 \newcommand\emph[1]{{\em#1\/}}

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

22 \newcommand\textsc[1]{{\sc#1}}

23 \newcommand\texttt[1]{{\tt#1}}

25 \newcommand\pow{{\cal P}}

26 %%%\let\pow=\wp

27 \newcommand\RepFun{\hbox{\tt RepFun}}

28 \newcommand\cons{\hbox{\tt cons}}

29 \def\succ{\hbox{\tt succ}}

30 \newcommand\split{\hbox{\tt split}}

31 \newcommand\fst{\hbox{\tt fst}}

32 \newcommand\snd{\hbox{\tt snd}}

33 \newcommand\converse{\hbox{\tt converse}}

34 \newcommand\domain{\hbox{\tt domain}}

35 \newcommand\range{\hbox{\tt range}}

36 \newcommand\field{\hbox{\tt field}}

37 \newcommand\lfp{\hbox{\tt lfp}}

38 \newcommand\gfp{\hbox{\tt gfp}}

39 \newcommand\id{\hbox{\tt id}}

40 \newcommand\trans{\hbox{\tt trans}}

41 \newcommand\wf{\hbox{\tt wf}}

42 \newcommand\nat{\hbox{\tt nat}}

43 \newcommand\rank{\hbox{\tt rank}}

44 \newcommand\univ{\hbox{\tt univ}}

45 \newcommand\Vrec{\hbox{\tt Vrec}}

46 \newcommand\Inl{\hbox{\tt Inl}}

47 \newcommand\Inr{\hbox{\tt Inr}}

48 \newcommand\case{\hbox{\tt case}}

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

50 \newcommand\Nil{\hbox{\tt Nil}}

51 \newcommand\Cons{\hbox{\tt Cons}}

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

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

54 \newcommand\length{\hbox{\tt length}}

55 \newcommand\listn{\hbox{\tt listn}}

56 \newcommand\acc{\hbox{\tt acc}}

57 \newcommand\primrec{\hbox{\tt primrec}}

58 \newcommand\SC{\hbox{\tt SC}}

59 \newcommand\CONST{\hbox{\tt CONST}}

60 \newcommand\PROJ{\hbox{\tt PROJ}}

61 \newcommand\COMP{\hbox{\tt COMP}}

62 \newcommand\PREC{\hbox{\tt PREC}}

64 \newcommand\quniv{\hbox{\tt quniv}}

65 \newcommand\llist{\hbox{\tt llist}}

66 \newcommand\LNil{\hbox{\tt LNil}}

67 \newcommand\LCons{\hbox{\tt LCons}}

68 \newcommand\lconst{\hbox{\tt lconst}}

69 \newcommand\lleq{\hbox{\tt lleq}}

70 \newcommand\map{\hbox{\tt map}}

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

72 \newcommand\Apply{\hbox{\tt Apply}}

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

74 \newcommand\rev{\hbox{\tt rev}}

75 \newcommand\reflect{\hbox{\tt reflect}}

76 \newcommand\tree{\hbox{\tt tree}}

77 \newcommand\forest{\hbox{\tt forest}}

78 \newcommand\Part{\hbox{\tt Part}}

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

80 \newcommand\Tcons{\hbox{\tt Tcons}}

81 \newcommand\Fcons{\hbox{\tt Fcons}}

82 \newcommand\Fnil{\hbox{\tt Fnil}}

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

84 \newcommand\Fin{\hbox{\tt Fin}}

85 \newcommand\QInl{\hbox{\tt QInl}}

86 \newcommand\QInr{\hbox{\tt QInr}}

87 \newcommand\qsplit{\hbox{\tt qsplit}}

88 \newcommand\qcase{\hbox{\tt qcase}}

89 \newcommand\Con{\hbox{\tt Con}}

90 \newcommand\data{\hbox{\tt data}}

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

94 \begin{document}

95 \pagestyle{empty}

96 \begin{titlepage}

97 \maketitle

98 \begin{abstract}

99 This paper presents a fixedpoint approach to inductive definitions.

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

101 approach lets definitions involve any operators that have been proved

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

103 implementation of mutual recursion and iterated definitions. It also

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

105 greatest fixedpoint.

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

108 theory and higher-order logic. It should be applicable to any logic in

109 which the Knaster-Tarski theorem can be proved. Examples include lists of

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

111 recursive functions. One example of a coinductive definition is

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

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

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

116 including two proofs of the Church-Rosser theorem and a coinductive proof of

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

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

119 \end{abstract}

120 %

121 \bigskip

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

123 \thispagestyle{empty}

124 \end{titlepage}

125 \tableofcontents\cleardoublepage\pagestyle{plain}

127 \setcounter{page}{1}

129 \section{Introduction}

130 Several theorem provers provide commands for formalizing recursive data

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

132 of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}. Given a description

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

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

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

136 Such data structures are called \defn{datatypes}

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

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

139 principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.

141 A datatype is but one example of an \defn{inductive definition}. This

142 specifies the least set closed under given rules~\cite{aczel77}. The

143 collection of theorems in a logic is inductively defined. A structural

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

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

146 provide commands for formalizing inductive definitions; these include

147 Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}.

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

150 the greatest set closed under given rules. Important examples include

151 using bisimulation relations to formalize equivalence of

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

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

154 are called \defn{codatatypes} below.

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

157 definitions are a large, well-behaved class. Monotonicity can be enforced

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

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

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

161 to prove it.

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

164 fixedpoints yield inductive definitions; greatest fixedpoints yield

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

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

168 The package supports mutual recursion and infinitely-branching datatypes and

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

170 thus accepting all provably monotone inductive definitions, including

171 iterated definitions.

173 The package has been implemented in

174 Isabelle~\cite{paulson-markt,paulson-isa-book} using

175 \textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has

176 since been ported to Isabelle/\textsc{hol} (higher-order logic). The

177 recursion equations are specified as introduction rules for the mutually

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

179 and attempts to prove that the mapping is monotonic and well-typed. If

180 successful, the package makes fixedpoint definitions and proves the

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

182 by making simple declarations in Isabelle theory files.

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

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

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

187 theory provides well-founded recursion~\cite{paulson-set-II}, which is harder

188 to use than structural recursion but considerably more general.

189 Slind~\cite{slind-tfl} has written a package to automate the definition of

190 well-founded recursive functions in Isabelle/\textsc{hol}.

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

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

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

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

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

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

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

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

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

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

204 \section{Fixedpoint operators}

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

206 follows:

207 \begin{eqnarray*}

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

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

210 \end{eqnarray*}

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

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

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

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

215 \begin{eqnarray*}

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

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

218 \end{eqnarray*}

219 These equations are instances of the Knaster-Tarski theorem, which states

220 that every monotonic function over a complete lattice has a

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

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

224 This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to

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

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

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

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

229 infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}. Bounding

230 sets are also called \defn{domains}.

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

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

234 there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates

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

237 \section{Elements of an inductive or coinductive definition}\label{basic-sec}

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

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

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

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

242 under an injection. Reasons for this are discussed

243 elsewhere~\cite[\S4.5]{paulson-set-II}.

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

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

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

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

249 Coq~\cite{paulin-tlca}. For instance, we cannot define the lists of

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

251 varies. Section~\ref{listn-sec} describes how to express this set using the

252 inductive definition package.

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

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

257 \subsection{The form of the introduction rules}\label{intro-sec}

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

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

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

261 $t\in M(R_i)$ or express arbitrary side-conditions.

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

264 sets, satisfying the rule

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

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

268 The ability to introduce new monotone operators makes the approach

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

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

271 expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The \emph{list of}

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

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

274 recursion; see \S\ref{primrec-sec} and also my earlier

275 paper~\cite[\S4.4]{paulson-set-II}.

277 Introduction rules may also contain \defn{side-conditions}. These are

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

279 sets. Side-conditions typically involve type-checking. One example is the

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

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

283 \subsection{The fixedpoint definitions}

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

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

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

287 defined as the least set closed under the rules

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

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

290 \]

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

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

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

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

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

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

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

299 \end{array}

300 \]

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

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

303 of~$\lfp$.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

320 definition is monotonic.

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

323 such as

324 \[

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

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

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

328 \end{array}

329 \]

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

333 \subsection{Mutual recursion} \label{mutual-sec}

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

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

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

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

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

340 As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the

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

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

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

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

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

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

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

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

351 \subsection{Proving the introduction rules}

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

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

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

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

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

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

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

359 attempting to prove the result.

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

362 in the rules, the package must prove

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

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

365 \]

366 Such proofs can be regarded as type-checking the definition.\footnote{The

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

368 has implicit type-checking.} The user supplies the package with

369 type-checking rules to apply. Usually these are general purpose rules from

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

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

372 definition through!

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

375 intrs}.

377 \subsection{The case analysis rule}

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

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

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

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

382 is written

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

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

385 \]

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

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

390 \section{Induction and coinduction rules}

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

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

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

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

395 basic coinduction rule.

397 \subsection{The basic induction rule}\label{basic-ind-sec}

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

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

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

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

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

404 product; inductively defined relations are treated slightly differently.

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

407 introduction rule:

408 \begin{itemize}

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

410 is~$P(t)$.

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

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

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

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

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

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

419 then the minor premise discharges the single assumption

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

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

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

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

424 \end{itemize}

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

426 but includes an induction hypothesis:

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

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

429 \]

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

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

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

433 Isabelle/\textsc{zf} theory also supports well-founded induction and recursion

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

435 set~\cite[\S3.4]{paulson-set-II}.

438 \subsection{Modified induction rules}

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

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

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

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

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

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

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

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

448 split} appears in the rule.

450 The mutual induction rule is called {\tt

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

452 \begin{itemize}

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

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

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

457 refers to all the recursive sets:

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

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

460 \]

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

462 \ldots,~$n$.

463 \end{itemize}

464 %

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

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

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

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

470 \subsection{Coinduction}\label{coind-sec}

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

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

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

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

475 greatest fixedpoint satisfying the rules

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

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

478 \]

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

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

481 forms of sum and product that are used to represent non-well-founded data

482 structures (see~\S\ref{univ-sec}).

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

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

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

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

488 \infer*{

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

490 z=\LNil\disj

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

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

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

494 \]

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

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

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

498 is the set of natural numbers.)

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

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

502 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.

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

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

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

509 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}

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

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

512 well-founded part of a relation, and the primitive recursive functions.

514 \subsection{The finite powerset operator}

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

516 corresponding invocation in an Isabelle theory file. Note that

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

518 \begin{ttbox}

519 Finite = Arith +

520 consts Fin :: i=>i

521 inductive

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

523 intrs

524 emptyI "0 : Fin(A)"

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

526 type_intrs "[empty_subsetI, cons_subsetI, PowI]"

527 type_elims "[make_elim PowD]"

528 end

529 \end{ttbox}

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

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

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

533 introduction rules. For type-checking, we supply two introduction

534 rules:

535 \[ \emptyset\sbs A \qquad

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

537 \]

538 A further introduction rule and an elimination rule express both

539 directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking

540 involves mostly introduction rules.

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

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

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

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

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

547 rule is {\tt Fin.induct}.

550 \subsection{Lists of $n$ elements}\label{listn-sec}

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

552 Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype

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

554 But her introduction rules

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

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

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

558 \]

559 are not acceptable to the inductive definition package:

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

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

563 varying parameters. It uses the existing datatype definition of

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

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

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

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

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

569 rules are

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

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

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

573 \]

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

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

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

577 \begin{ttbox}

578 ListN = List +

579 consts listn :: i=>i

580 inductive

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

582 intrs

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

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

585 type_intrs "nat_typechecks @ list.intrs"

586 end

587 \end{ttbox}

588 The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.

589 Because $\listn(A)$ is a set of pairs, type-checking requires the

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

591 package always includes the rules for ordered pairs.

593 The package returns introduction, elimination and induction rules for

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

595 \[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & 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 This rule lets the induction formula to be a

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

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

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

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

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

605 --- asserts that the inductive definition agrees with the obvious notion of

606 $n$-element list.

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

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

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

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

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

613 \]

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

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

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

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

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

620 \infer*{Q}

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

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

623 a\in A \\

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

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

626 \]

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

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

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

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

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

632 Here is a sample session:

633 \begin{ttbox}

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

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

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

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

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

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

640 \end{ttbox}

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

642 second rule is

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

644 \infer*{Q}

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

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

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

648 \]

649 The package also has built-in rules for freeness reasoning about $0$

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

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

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

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

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

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

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

658 \]

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

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

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

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

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

664 residuals~\cite{rasmussen95}.

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

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

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

670 and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.

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

672 pairing and injection operators, it contains non-well-founded elements such as

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

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

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

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

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

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

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

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

682 coinduction principle for equalities.

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

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

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

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

688 \]

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

690 bisimulation. Equivalence can be coinductively defined as the greatest

691 fixedpoint for the introduction rules

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

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

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

695 \]

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

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

698 \begin{ttbox}

699 consts lleq :: i=>i

700 coinductive

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

702 intrs

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

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

705 type_intrs "llist.intrs"

706 \end{ttbox}

707 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking

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

709 declaration is discussed below (\S\ref{lists-sec}).

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

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

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

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

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

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

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

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

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

720 \end{array}

721 }{[z\in X]_z}

722 \]

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

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

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

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

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

729 \subsection{The accessible part of a relation}\label{acc-sec}

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

731 The \defn{accessible} or \defn{well-founded} part of~$\prec$, written

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

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

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

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

736 introduction rule of the form

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

738 Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes

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

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

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

742 (recall \S\ref{intro-sec}), but fortunately can be transformed into the

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

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

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

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

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

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

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

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

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

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

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

756 \begin{ttbox}

757 consts acc :: i=>i

758 inductive

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

760 intrs

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

762 monos "[Pow_mono]"

763 \end{ttbox}

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

765 instance, $\prec$ is well-founded if and only if its field is contained in

766 $\acc(\prec)$.

768 As mentioned in~\S\ref{basic-ind-sec}, 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)}{\left[

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

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

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

776 \end{array}

777 \right]_a}}

778 \]

779 The strange induction hypothesis is equivalent to

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

781 Therefore the rule expresses well-founded induction on the accessible part

782 of~$\prec$.

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

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

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

787 equivalently as

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

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

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

791 where $M=\lst$.

793 \subsection{The primitive recursive functions}\label{primrec-sec}

794 The primitive recursive functions are traditionally defined inductively, as

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

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

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

798 the notion of composition, is less easily circumvented.

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

801 $x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,

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

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

804 \begin{itemize}

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

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

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

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

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

810 \item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$,

811 where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,

812 such that

813 \[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] =

814 g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \]

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

817 recursive, such that

818 \begin{eqnarray*}

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

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

821 \end{eqnarray*}

822 \end{itemize}

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

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

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

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

827 tuple-valued functions. This modified the inductive definition such that

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

830 \begin{figure}

831 \begin{ttbox}

832 Primrec = List +

833 consts

834 primrec :: i

835 SC :: i

836 \(\vdots\)

837 defs

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

839 \(\vdots\)

840 inductive

841 domains "primrec" <= "list(nat)->nat"

842 intrs

843 SC "SC : primrec"

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

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

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

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

848 monos "[list_mono]"

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

850 type_intrs "nat_typechecks @ list.intrs @

851 [lam_type, list_case_type, drop_type, map_type,

852 apply_type, rec_type]"

853 end

854 \end{ttbox}

855 \hrule

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

857 \label{primrec-fig}

858 \end{figure}

859 \def\fs{{\it fs}}

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

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

863 since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and

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

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

866 $\COMP$:

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

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

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

870 an unusual induction hypothesis:

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

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

873 \]

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

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

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

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

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

880 Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec}

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

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

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

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

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

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

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

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

892 \section{Datatypes and codatatypes}\label{data-sec}

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

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

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

896 involving any pair of constructors.

899 \subsection{Constructors and their domain}\label{univ-sec}

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

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

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

903 as domains for (co)inductive definitions.

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

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

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

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

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

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

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

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

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

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

916 in~\S\ref{mutual-sec}. Further nested injections ensure that the

917 constructors for~$R_i$ are pairwise distinct.

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

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

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

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

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

924 datatypes~\cite[\S4.2]{paulson-set-II}.

926 The standard pairs and injections can only yield well-founded

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

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

929 contain non-well-founded objects.

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

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

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

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

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

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

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

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

939 elsewhere~\cite{paulson-final}.

941 \subsection{The case analysis operator}

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

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

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

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

946 for products and sums.

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

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

950 \begin{eqnarray*}

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

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

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

954 \end{eqnarray*}

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

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

957 constructor:

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

959 \qquad i = 1, \ldots, k

960 \]

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

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

963 theorem prover for higher-order logic. If $f$ and~$g$ have meta-type $i\To i$

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

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

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

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

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

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

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

971 $\qsplit$ and~$\qcase$.

973 \medskip

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

976 examine some examples. Further details are available

977 elsewhere~\cite{paulson-set-II}.

980 \subsection{Example: lists and lazy lists}\label{lists-sec}

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

982 file:

983 \begin{ttbox}

984 consts list :: i=>i

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

986 \end{ttbox}

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

988 \begin{ttbox}

989 consts llist :: i=>i

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

991 \end{ttbox}

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

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

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

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

997 can be overridden.

999 \ifshort

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

1001 \else

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

1003 list.induct}:

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

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

1006 \]

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

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

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

1010 consequence, which justifies structural recursion on lists

1011 \cite[\S4.3]{paulson-set-II}, is

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

1013 \par

1014 \fi

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

1016 the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and

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

1018 components, fixedpoint operators can create cyclic constructions. For

1019 example, the definition

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

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

1023 \ifshort

1024 \typeout{****SHORT VERSION}

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

1026 \else

1027 \medskip

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

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

1030 The list constructors are defined as follows:

1031 \begin{eqnarray*}

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

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

1034 \end{eqnarray*}

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

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

1037 Let us verify the two equations:

1038 \begin{eqnarray*}

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

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

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

1042 & = & c\\[1ex]

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

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

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

1046 & = & h(x,y)

1047 \end{eqnarray*}

1048 \fi

1051 \ifshort

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

1053 \else

1054 \subsection{Example: mutual recursion}

1055 In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees

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

1057 $\Fnil$ and~$\Fcons$:

1058 \begin{ttbox}

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

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

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

1062 \end{ttbox}

1063 The three introduction rules define the mutual recursion. The

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

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

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

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

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

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

1071 \end{array}

1072 \right]_{a,f}}

1073 & P(\Fnil)

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

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

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

1077 \end{array}

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

1079 \]

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

1081 recursive sets. Although such reasoning is sometimes useful

1082 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish

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

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

1085 the induction hypotheses:

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

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

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

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

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

1091 \end{array}

1092 \right]_{a,f}}

1093 & Q(\Fnil)

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

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

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

1097 \end{array}

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

1099 \]

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

1101 forests \cite[\S4.5]{paulson-set-II}.

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

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

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

1106 \begin{eqnarray*}

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

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

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

1110 \end{eqnarray*}

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

1112 forests:

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

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

1115 \]

1116 \fi

1119 \subsection{Example: a four-constructor datatype}

1120 A bigger datatype will illustrate some efficiency

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

1122 corresponding arities.

1123 \begin{ttbox}

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

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

1126 | Con1 ("a: A")

1127 | Con2 ("a: A", "b: B")

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

1129 \end{ttbox}

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

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

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

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

1135 The constructors are defined by the equations

1136 \begin{eqnarray*}

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

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

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

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

1141 \end{eqnarray*}

1142 The case analysis operator is

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

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

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

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

1147 \end{array}

1148 \]

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

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

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

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

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

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

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

1157 advantage of binary notation over unary.

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

1160 the theorem list \verb|con_defs|. It contains the case equations, such as

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

1162 as the theorem list \verb|case_eqns|. There is one equation per constructor.

1164 \subsection{Proving freeness theorems}

1165 There are two kinds of freeness theorems:

1166 \begin{itemize}

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

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

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

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

1172 \end{itemize}

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

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

1175 proving desired theorems --- either manually or during

1176 simplification or classical reasoning.

1178 The theorem list \verb|free_iffs| enables the simplifier to perform freeness

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

1180 equations. The theorem list contains logical equivalences such as

1181 \begin{eqnarray*}

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

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

1184 & \vdots & \\

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

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

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

1188 \end{eqnarray*}

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

1191 The theorem list \verb|free_SEs| enables the classical

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

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

1194 assumptions.

1196 Such incremental unfolding combines freeness reasoning with other proof

1197 steps. It has the unfortunate side-effect of unfolding definitions of

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

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

1200 restores the defined constants.

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

1204 The use of least fixedpoints to express inductive definitions seems

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

1207 Most automated logics can only express inductive definitions by asserting

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

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

1210 complex; earlier versions of Martin-L\"of's type theory could (using

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

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

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

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

1215 definitions~\cite{paulin-tlca}. It seems that researchers tried hard to

1216 circumvent these problems before finally extending the Calculus with rule

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

1218 the Calculus of Constructions with inductive and coinductive

1219 types~\cite{gimenez-codifying}, with mechanized support in Coq.

1221 Higher-order logic can express inductive definitions through quantification

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

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

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

1225 This technique can be used to prove the Knaster-Tarski theorem, which (in its

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

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

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

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

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

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

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

1233 greater power with less effort.

1235 Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the

1236 Cambridge \textsc{hol} system with mutual recursion and infinitely-branching

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

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

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

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

1242 syntactic form that excludes many monotone inductive definitions.

1244 \textsc{pvs}~\cite{pvs-language} is another proof assistant based on

1245 higher-order logic. It supports both inductive definitions and datatypes,

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

1247 may use recursion over the built-in $\lst$ type.

1249 The earliest use of least fixedpoints is probably Robin Milner's. Brian

1250 Monahan extended this package considerably~\cite{monahan84}, as did I in

1251 unpublished work.\footnote{The datatype package described in my \textsc{lcf}

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

1253 axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant

1254 fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of

1255 continuous functions over domains. \textsc{lcf} is too weak to express

1256 recursive predicates. The Isabelle package might be the first to be based on

1257 the Knaster-Tarski theorem.

1260 \section{Conclusions and future work}

1261 Higher-order logic and set theory are both powerful enough to express

1262 inductive definitions. A growing number of theorem provers implement one

1263 of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive

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

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

1266 could introduce unsoundness.

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

1269 (co)in\-duc\-tive definitions that does not assert axioms. It is efficient:

1270 it processes most definitions in seconds and even a 60-constructor datatype

1271 requires only a few minutes. It is also simple: The first working version took

1272 under a week to code, consisting of under 1100 lines (35K bytes) of Standard

1273 \textsc{ml}.

1275 In set theory, care is needed to ensure that the inductive definition yields

1276 a set (rather than a proper class). This problem is inherent to set theory,

1277 whether or not the Knaster-Tarski theorem is employed. We must exhibit a

1278 bounding set (called a domain above). For inductive definitions, this is

1279 often trivial. For datatype definitions, I have had to formalize much set

1280 theory. To justify infinitely-branching datatype definitions, I have had to

1281 develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem

1282 that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all

1283 $\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.

1284 The need for such efforts is not a drawback of the fixedpoint approach, for

1285 the alternative is to take such definitions on faith.

1287 Care is also needed to ensure that the greatest fixedpoint really yields a

1288 coinductive definition. In set theory, standard pairs admit only well-founded

1289 constructions. Aczel's anti-foundation axiom~\cite{aczel88} could be used to

1290 get non-well-founded objects, but it does not seem easy to mechanize.

1291 Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which

1292 can be generalized to a variant notion of function. Elsewhere I have

1293 proved that this simple approach works (yielding final coalgebras) for a broad

1294 class of definitions~\cite{paulson-final}.

1296 Several large studies make heavy use of inductive definitions. L\"otzbeyer

1297 and Sandner have formalized two chapters of a semantics book~\cite{winskel93},

1298 proving the equivalence between the operational and denotational semantics of

1299 a simple imperative language. A single theory file contains three datatype

1300 definitions (of arithmetic expressions, boolean expressions and commands) and

1301 three inductive definitions (the corresponding operational rules). Using

1302 different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}

1303 have both proved the Church-Rosser theorem; inductive definitions specify

1304 several reduction relations on $\lambda$-terms. Recently, I have applied

1305 inductive definitions to the analysis of cryptographic

1306 protocols~\cite{paulson-markt}.

1308 To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the

1309 consistency of the dynamic and static semantics for a small functional

1310 language. The example is due to Milner and Tofte~\cite{milner-coind}. It

1311 concerns an extended correspondence relation, which is defined coinductively.

1312 A codatatype definition specifies values and value environments in mutual

1313 recursion. Non-well-founded values represent recursive functions. Value

1314 environments are variant functions from variables into values. This one key

1315 definition uses most of the package's novel features.

1317 The approach is not restricted to set theory. It should be suitable for any

1318 logic that has some notion of set and the Knaster-Tarski theorem. I have

1319 ported the (co)inductive definition package from Isabelle/\textsc{zf} to

1320 Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95}

1321 is investigating how to port the (co)datatype package. \textsc{hol}

1322 represents sets by unary predicates; defining the corresponding types may

1323 cause complications.

1326 \begin{footnotesize}

1327 \bibliographystyle{springer}

1328 \bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}

1329 \end{footnotesize}

1330 %%%%%\doendnotes

1332 \ifshort\typeout{****Omitting appendices}

1333 \else

1334 \newpage

1335 \appendix

1336 \section{Inductive and coinductive definitions: users guide}

1337 A theory file may contain any number of inductive and coinductive

1338 definitions. They may be intermixed with other declarations; in

1339 particular, the (co)inductive sets \defn{must} be declared separately as

1340 constants, and may have mixfix syntax or be subject to syntax translations.

1342 The syntax is rather complicated. Please consult the examples above and the

1343 theory files on the \textsc{zf} source directory.

1345 Each (co)inductive definition adds definitions to the theory and also proves

1346 some theorems. Each definition creates an \textsc{ml} structure, which is a

1347 substructure of the main theory structure.

1349 Inductive and datatype definitions can take up considerable storage. The

1350 introduction rules are replicated in slightly different forms as fixedpoint

1351 definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's

1352 six definitions occupy over 600K in total. Defining the 60-constructor

1353 datatype requires nearly 560K\@.

1355 \subsection{The result structure}

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

1357 in~\S\ref{basic-sec}; others are self-explanatory.

1358 \begin{description}

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

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

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

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

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

1368 the recursive sets. The rules are also available individually, using the

1369 names given them in the theory file.

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

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

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

1375 \end{description}

1377 For an inductive definition, the result structure contains two induction

1378 rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter

1379 rule is just {\tt True} unless more than one set is being defined.) For a

1380 coinductive definition, it contains the rule \verb|coinduct|.

1382 Figure~\ref{def-result-fig} summarizes the two result signatures,

1383 specifying the types of all these components.

1385 \begin{figure}

1386 \begin{ttbox}

1387 sig

1388 val thy : theory

1389 val defs : thm list

1390 val bnd_mono : thm

1391 val dom_subset : thm

1392 val intrs : thm list

1393 val elim : thm

1394 val mk_cases : thm list -> string -> thm

1395 {\it(Inductive definitions only)}

1396 val induct : thm

1397 val mutual_induct: thm

1398 {\it(Coinductive definitions only)}

1399 val coinduct : thm

1400 end

1401 \end{ttbox}

1402 \hrule

1403 \caption{The result of a (co)inductive definition} \label{def-result-fig}

1404 \end{figure}

1406 \subsection{The syntax of a (co)inductive definition}

1407 An inductive definition has the form

1408 \begin{ttbox}

1409 inductive

1410 domains {\it domain declarations}

1411 intrs {\it introduction rules}

1412 monos {\it monotonicity theorems}

1413 con_defs {\it constructor definitions}

1414 type_intrs {\it introduction rules for type-checking}

1415 type_elims {\it elimination rules for type-checking}

1416 \end{ttbox}

1417 A coinductive definition is identical, but starts with the keyword

1418 {\tt coinductive}.

1420 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}

1421 sections are optional. If present, each is specified as a string, which

1422 must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply

1423 inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger

1424 \textsc{ml} error messages. You can then inspect the file on your directory.

1426 \begin{description}

1427 \item[\it domain declarations] consist of one or more items of the form

1428 {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with

1429 its domain.

1431 \item[\it introduction rules] specify one or more introduction rules in

1432 the form {\it ident\/}~{\it string}, where the identifier gives the name of

1433 the rule in the result structure.

1435 \item[\it monotonicity theorems] are required for each operator applied to

1436 a recursive set in the introduction rules. There \defn{must} be a theorem

1437 of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$

1438 in an introduction rule!

1440 \item[\it constructor definitions] contain definitions of constants

1441 appearing in the introduction rules. The (co)datatype package supplies

1442 the constructors' definitions here. Most (co)inductive definitions omit

1443 this section; one exception is the primitive recursive functions example

1444 (\S\ref{primrec-sec}).

1446 \item[\it type\_intrs] consists of introduction rules for type-checking the

1447 definition, as discussed in~\S\ref{basic-sec}. They are applied using

1448 depth-first search; you can trace the proof by setting

1450 \verb|trace_DEPTH_FIRST := true|.

1452 \item[\it type\_elims] consists of elimination rules for type-checking the

1453 definition. They are presumed to be safe and are applied as much as

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

1455 \end{description}

1457 The package has a few notable restrictions:

1458 \begin{itemize}

1459 \item The theory must separately declare the recursive sets as

1460 constants.

1462 \item The names of the recursive sets must be identifiers, not infix

1463 operators.

1465 \item Side-conditions must not be conjunctions. However, an introduction rule

1466 may contain any number of side-conditions.

1468 \item Side-conditions of the form $x=t$, where the variable~$x$ does not

1469 occur in~$t$, will be substituted through the rule \verb|mutual_induct|.

1470 \end{itemize}

1472 Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,

1473 thanks to type-checking. There are no \texttt{domains}, \texttt{type\_intrs}

1474 or \texttt{type\_elims} parts.

1477 \section{Datatype and codatatype definitions: users guide}

1478 This section explains how to include (co)datatype declarations in a theory

1479 file. Please include {\tt Datatype} as a parent theory; this makes available

1480 the definitions of $\univ$ and $\quniv$.

1483 \subsection{The result structure}

1484 The result structure extends that of (co)inductive definitions

1485 (Figure~\ref{def-result-fig}) with several additional items:

1486 \begin{ttbox}

1487 val con_defs : thm list

1488 val case_eqns : thm list

1489 val free_iffs : thm list

1490 val free_SEs : thm list

1491 val mk_free : string -> thm

1492 \end{ttbox}

1493 Most of these have been discussed in~\S\ref{data-sec}. Here is a summary:

1494 \begin{description}

1495 \item[\tt con\_defs] is a list of definitions: the case operator followed by

1496 the constructors. This theorem list can be supplied to \verb|mk_cases|, for

1497 example.

1499 \item[\tt case\_eqns] is a list of equations, stating that the case operator

1500 inverts each constructor.

1502 \item[\tt free\_iffs] is a list of logical equivalences to perform freeness

1503 reasoning by rewriting. A typical application has the form

1504 \begin{ttbox}

1505 by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);

1506 \end{ttbox}

1508 \item[\tt free\_SEs] is a list of safe elimination rules to perform freeness

1509 reasoning. It can be supplied to \verb|eresolve_tac| or to the classical

1510 reasoner:

1511 \begin{ttbox}

1512 by (fast_tac (ZF_cs addSEs free_SEs) 1);

1513 \end{ttbox}

1515 \item[\tt mk\_free] is a function to prove freeness properties, specified as

1516 strings. The theorems can be expressed in various forms, such as logical

1517 equivalences or elimination rules.

1518 \end{description}

1520 The result structure also inherits everything from the underlying

1521 (co)inductive definition, such as the introduction rules, elimination rule,

1522 and (co)induction rule.

1525 \subsection{The syntax of a (co)datatype definition}

1526 A datatype definition has the form

1527 \begin{ttbox}

1528 datatype <={\it domain}

1529 {\it datatype declaration} and {\it datatype declaration} and \ldots

1530 monos {\it monotonicity theorems}

1531 type_intrs {\it introduction rules for type-checking}

1532 type_elims {\it elimination rules for type-checking}

1533 \end{ttbox}

1534 A codatatype definition is identical save that it starts with the keyword {\tt

1535 codatatype}.

1537 The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are

1538 optional. They are treated like their counterparts in a (co)inductive

1539 definition, as described above. The package supplements your type-checking

1540 rules (if any) with additional ones that should cope with any

1541 finitely-branching (co)datatype definition.

1543 \begin{description}

1544 \item[\it domain] specifies a single domain to use for all the mutually

1545 recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are

1546 omitted, the package supplies a domain automatically. Suppose the

1547 definition involves the set parameters $A_1$, \ldots, $A_k$. Then

1548 $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and

1549 $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.

1551 These choices should work for all finitely-branching (co)datatype

1552 definitions. For examples of infinitely-branching datatypes,

1553 see file {\tt ZF/ex/Brouwer.thy}.

1555 \item[\it datatype declaration] has the form

1556 \begin{quote}

1557 {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}

1558 \ldots

1559 \end{quote}

1560 The {\it string\/} is the datatype, say {\tt"list(A)"}. Each

1561 {\it constructor\/} has the form

1562 \begin{quote}

1563 {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}

1564 {\it mixfix\/}

1565 \end{quote}

1566 The {\it name\/} specifies a new constructor while the {\it premises\/} its

1567 typing conditions. The optional {\it mixfix\/} phrase may give

1568 the constructor infix, for example.

1570 Mutually recursive {\it datatype declarations\/} are separated by the

1571 keyword~{\tt and}.

1572 \end{description}

1574 Isabelle/\textsc{hol}'s datatype definition package is (as of this writing)

1575 entirely different from Isabelle/\textsc{zf}'s. The syntax is different, and

1576 instead of making an inductive definition it asserts axioms.

1578 \paragraph*{Note.}

1579 In the definitions of the constructors, the right-hand sides may overlap.

1580 For instance, the datatype of combinators has constructors defined by

1581 \begin{eqnarray*}

1582 {\tt K} & \equiv & \Inl(\emptyset) \\

1583 {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\

1584 p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q}))

1585 \end{eqnarray*}

1586 Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the

1587 longest right-hand sides are folded first.

1589 \fi

1590 \end{document}