author  wenzelm 
Mon, 15 Jan 1996 15:49:21 +0100  
changeset 1440  de6f18da81bb 
parent 1421  1471e85624a7 
child 1533  771474fd33be 
permissions  rwrr 
1197  1 
\documentstyle[a4,proof209,iman,extra,12pt]{llncs} 
103  2 
\newif\ifCADE 
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset

3 
\CADEfalse 
103  4 

355  5 
\title{A Fixedpoint Approach to Implementing\\ 
6 
(Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed 

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

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

9 
`Types'.}} 

103  10 

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

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

15 

16 
\newcommand\sbs{\subseteq} 

17 
\let\To=\Rightarrow 

18 

19 

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

22 
\newcommand\RepFun{\hbox{\tt RepFun}} 

23 
\newcommand\cons{\hbox{\tt cons}} 

24 
\def\succ{\hbox{\tt succ}} 

25 
\newcommand\split{\hbox{\tt split}} 

26 
\newcommand\fst{\hbox{\tt fst}} 

27 
\newcommand\snd{\hbox{\tt snd}} 

28 
\newcommand\converse{\hbox{\tt converse}} 

29 
\newcommand\domain{\hbox{\tt domain}} 

30 
\newcommand\range{\hbox{\tt range}} 

31 
\newcommand\field{\hbox{\tt field}} 

32 
\newcommand\lfp{\hbox{\tt lfp}} 

33 
\newcommand\gfp{\hbox{\tt gfp}} 

34 
\newcommand\id{\hbox{\tt id}} 

35 
\newcommand\trans{\hbox{\tt trans}} 

36 
\newcommand\wf{\hbox{\tt wf}} 

37 
\newcommand\nat{\hbox{\tt nat}} 

38 
\newcommand\rank{\hbox{\tt rank}} 

39 
\newcommand\univ{\hbox{\tt univ}} 

40 
\newcommand\Vrec{\hbox{\tt Vrec}} 

41 
\newcommand\Inl{\hbox{\tt Inl}} 

42 
\newcommand\Inr{\hbox{\tt Inr}} 

43 
\newcommand\case{\hbox{\tt case}} 

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

45 
\newcommand\Nil{\hbox{\tt Nil}} 

46 
\newcommand\Cons{\hbox{\tt Cons}} 

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

355  49 
\newcommand\length{\hbox{\tt length}} 
50 
\newcommand\listn{\hbox{\tt listn}} 

51 
\newcommand\acc{\hbox{\tt acc}} 

52 
\newcommand\primrec{\hbox{\tt primrec}} 

53 
\newcommand\SC{\hbox{\tt SC}} 

54 
\newcommand\CONST{\hbox{\tt CONST}} 

55 
\newcommand\PROJ{\hbox{\tt PROJ}} 

56 
\newcommand\COMP{\hbox{\tt COMP}} 

57 
\newcommand\PREC{\hbox{\tt PREC}} 

103  58 

355  59 
\newcommand\quniv{\hbox{\tt quniv}} 
60 
\newcommand\llist{\hbox{\tt llist}} 

61 
\newcommand\LNil{\hbox{\tt LNil}} 

62 
\newcommand\LCons{\hbox{\tt LCons}} 

63 
\newcommand\lconst{\hbox{\tt lconst}} 

64 
\newcommand\lleq{\hbox{\tt lleq}} 

65 
\newcommand\map{\hbox{\tt map}} 

66 
\newcommand\term{\hbox{\tt term}} 

67 
\newcommand\Apply{\hbox{\tt Apply}} 

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

69 
\newcommand\rev{\hbox{\tt rev}} 

70 
\newcommand\reflect{\hbox{\tt reflect}} 

71 
\newcommand\tree{\hbox{\tt tree}} 

72 
\newcommand\forest{\hbox{\tt forest}} 

73 
\newcommand\Part{\hbox{\tt Part}} 

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

75 
\newcommand\Tcons{\hbox{\tt Tcons}} 

76 
\newcommand\Fcons{\hbox{\tt Fcons}} 

77 
\newcommand\Fnil{\hbox{\tt Fnil}} 

103  78 
\newcommand\TFcase{\hbox{\tt TF\_case}} 
355  79 
\newcommand\Fin{\hbox{\tt Fin}} 
80 
\newcommand\QInl{\hbox{\tt QInl}} 

81 
\newcommand\QInr{\hbox{\tt QInr}} 

82 
\newcommand\qsplit{\hbox{\tt qsplit}} 

83 
\newcommand\qcase{\hbox{\tt qcase}} 

84 
\newcommand\Con{\hbox{\tt Con}} 

85 
\newcommand\data{\hbox{\tt data}} 

103  86 

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

88 

89 
\begin{document} 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

90 
\pagestyle{empty} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

91 
\begin{titlepage} 
103  92 
\maketitle 
93 
\begin{abstract} 

355  94 
This paper presents a fixedpoint approach to inductive definitions. 
95 
Instead of using a syntactic test such as `strictly positive,' the 

96 
approach lets definitions involve any operators that have been proved 

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

98 
implementation of mutual recursion and other conveniences. It also 

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

100 
greatest fixedpoint. This represents the first automated support for 

101 
coinductive definitions. 

130  102 

597  103 
The method has been implemented in two of Isabelle's logics, ZF set theory 
104 
and higherorder logic. It should be applicable to any logic in which 

105 
the KnasterTarski Theorem can be proved. Examples include lists of $n$ 

106 
elements, the accessible part of a relation and the set of primitive 

107 
recursive functions. One example of a coinductive definition is 

108 
bisimulations for lazy lists. \ifCADE\else Recursive datatypes are 

109 
examined in detail, as well as one example of a {\bf codatatype}: lazy 

110 
lists. The appendices are simple user's manuals for this Isabelle 

111 
package.\fi 

103  112 
\end{abstract} 
113 
% 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

114 
\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

115 
\thispagestyle{empty} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

116 
\end{titlepage} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

117 
\tableofcontents\cleardoublepage\pagestyle{plain} 
103  118 

119 
\section{Introduction} 

120 
Several theorem provers provide commands for formalizing recursive data 

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

597  122 
principle~\cite{bm79} and Melham's recursive type package for the Cambridge HOL 
103  123 
system~\cite{melham89}. Such data structures are called {\bf datatypes} 
124 
below, by analogy with {\tt datatype} definitions in Standard~ML\@. 

125 

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

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

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

131 
provide commands for formalizing inductive definitions; these include 

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

133 

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

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

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

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

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

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

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

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

146 
to prove it. 

103  147 

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

149 
fixedpoints yield inductive definitions; greatest fixedpoints yield 

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

154 
iterated definitions. 

597  155 
\item It accepts a wide class of datatype definitions, including those with 
156 
infinite branching. 

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

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

597  163 
The package has been implemented in Isabelle~\cite{isabelleintro} using ZF 
164 
set theory \cite{paulsonsetI,paulsonsetII}; part of it has since been 

165 
ported to Isabelle's higherorder logic. However, the fixedpoint approach is 

166 
independent of Isabelle. The recursion equations are specified as 

167 
introduction rules for the mutually recursive sets. The package transforms 

168 
these rules into a mapping over sets, and attempts to prove that the 

169 
mapping is monotonic and welltyped. If successful, the package makes 

170 
fixedpoint definitions and proves the introduction, elimination and 

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

103  175 

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

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

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

180 
logical tools~\cite{paulsonsetII}. 

103  181 

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

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

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

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

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

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

597  189 
user's manuals for this Isabelle package.\fi 
103  190 

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

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

193 

194 
\section{Fixedpoint operators} 

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

196 
follows: 

197 
\begin{eqnarray*} 

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

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

200 
\end{eqnarray*} 

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

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

205 
\begin{eqnarray*} 

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

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

208 
\end{eqnarray*} 

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

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

213 

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

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

103  221 

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

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

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

103  226 

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

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

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

232 
under an injection. Reasons for this are discussed 

130  233 
elsewhere~\cite[\S4.5]{paulsonsetII}. 
103  234 

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

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

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

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

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

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

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

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

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

246 

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

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

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

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

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

252 
sideconditions. 

253 

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

255 
sets, satisfying the rule 

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

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

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

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

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

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

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

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

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

103  267 

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

269 
premises consisting of arbitrary formulae not mentioning the recursive 

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

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

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

273 

274 
\subsection{The fixedpoint definitions} 

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

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

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

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

281 
\] 

282 

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

286 
\begin{eqnarray*} 

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

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

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

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

291 
\end{array} 

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

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

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

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

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

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

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

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

103  305 
only if $\forall x.P(x)\imp Q(x)$.} 
306 

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

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

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

310 
It also contains some theorems; {\tt dom\_subset} is an inclusion such as 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

311 
$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

312 
definition is monotonic. 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

313 

1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

314 
Internally the package uses the theorem {\tt unfold}, a fixedpoint equation 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

315 
such as 
103  316 
\begin{eqnarray*} 
317 
\Fin(A) & = & 

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

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

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

321 
\end{array} 

322 
\end{eqnarray*} 

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

323 
In order to save space, this theorem is not exported. 
103  324 

325 

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

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

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

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

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

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

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

336 
\begin{eqnarray*} 

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

338 
\end{eqnarray*} 

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

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

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

342 
\begin{eqnarray*} 

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

346 

347 

348 
\subsection{Proving the introduction rules} 

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

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

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

356 
attempting to prove the result. 

357 

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

359 
in the rules, the package must prove 

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

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

362 
\] 

597  363 
Such proofs can be regarded as typechecking the definition.\footnote{The 
364 
Isabelle/HOL version does not require these proofs, as HOL has implicit 

365 
typechecking.} The user supplies the package with typechecking rules to 

366 
apply. Usually these are general purpose rules from the ZF theory. They 

367 
could however be rules specifically proved for a particular inductive 

368 
definition; sometimes this is the easiest way to get the definition 

369 
through! 

103  370 

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

103  373 

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

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

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

380 
\] 

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

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

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

386 

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

389 
definitions involving datatypes, such as an inductively defined relation 

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

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

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

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

394 

103  395 

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

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

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

130  401 
coinductive definition, the package returns a basic coinduction rule. 
103  402 

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

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

407 

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

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

410 
introduction rule: 

411 
\begin{itemize} 

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

413 
is~$P(t)$. 

414 

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

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

103  418 

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

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

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

422 
then the minor premise discharges the single assumption 

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

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

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

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

427 
\end{itemize} 

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

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

432 
\] 

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

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

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

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

438 
and inductive relations. 

103  439 

440 
\subsection{Mutual induction} 

441 
The mutual induction rule is called {\tt 

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

443 
\begin{itemize} 

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

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

446 

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

448 
refers to all the recursive sets: 

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

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

451 
\] 

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

103  454 

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

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

456 
$A_1\times\cdots\times A_m$ (associated to the right), then the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

457 
corresponding predicate $P_i$ takes $m$ arguments and the corresponding 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

458 
conjunct of the conclusion is 
103  459 
\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) 
460 
\] 

461 
\end{itemize} 

462 
The last point above simplifies reasoning about inductively defined 

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

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

465 

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

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

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

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

474 
\] 

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

130  478 
(see~\S\ref{univsec}). Coinductive definitions use these variant sums and 
103  479 
products. 
480 

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

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

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

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

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

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

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

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

130  497 

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

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

502 

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

507 

455  508 
\subsection{The finite powerset operator} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

509 
This operator has been discussed extensively above. Here is the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

510 
corresponding invocation in an Isabelle theory file. Note that 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

511 
$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF. 
103  512 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

513 
Finite = Arith + 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

514 
consts Fin :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

515 
inductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

516 
domains "Fin(A)" <= "Pow(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

517 
intrs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

518 
emptyI "0 : Fin(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

519 
consI "[ a: A; b: Fin(A) ] ==> cons(a,b) : Fin(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

520 
type_intrs "[empty_subsetI, cons_subsetI, PowI]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

521 
type_elims "[make_elim PowD]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

522 
end 
103  523 
\end{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

524 
Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

525 
unary function symbol~$\Fin$, which is defined inductively. Its domain is 
355  526 
specified as $\pow(A)$, where $A$ is the parameter appearing in the 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

527 
introduction rules. For typechecking, we supply two introduction 
355  528 
rules: 
103  529 
\[ \emptyset\sbs A \qquad 
530 
\infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} 

531 
\] 

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

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

355  534 
involves mostly introduction rules. 
535 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

536 
Like all Isabelle theory files, this one yields a structure containing the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

537 
new theory as an \ML{} value. Structure {\tt Finite} also has a 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

538 
substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

539 
can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

540 
or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

541 
rule is {\tt Fin.induct}. 
355  542 

103  543 

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

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

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

548 
But her introduction rules 

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

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

553 
are not acceptable to the inductive definition package: 

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

555 

597  556 
The Isabelle version of this example suggests a general treatment of 
355  557 
varying parameters. Here, we use the existing datatype definition of 
558 
$\lst(A)$, with constructors $\Nil$ and~$\Cons$. Then incorporate the 

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

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

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

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

563 
rules are 

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

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

567 
\] 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

568 
The Isabelle theory file takes, as parent, the theory~{\tt List} of lists. 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

569 
We declare the constant~$\listn$ and supply an inductive definition, 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

570 
specifying the domain as $\nat\times\lst(A)$: 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

571 
\begin{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

572 
ListN = List + 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

573 
consts listn :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

574 
inductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

575 
domains "listn(A)" <= "nat*list(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

576 
intrs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

577 
NilI "<0,Nil> : listn(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

578 
ConsI "[ a: A; <n,l> : listn(A) ] ==> <succ(n), Cons(a,l)> : listn(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

579 
type_intrs "nat_typechecks @ list.intrs" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

580 
end 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

581 
\end{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

582 
The typechecking rules include those for 0, $\succ$, $\Nil$ and $\Cons$. 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

583 
Because $\listn(A)$ is a set of pairs, typechecking requires the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

584 
equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$; the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

585 
package always includes the necessary rules. 
103  586 

587 
The package returns introduction, elimination and induction rules for 

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

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

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

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

592 
\] 

593 
This rule requires the induction formula to be a 

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

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

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

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

600 
\] 

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

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

607 

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

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

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

103  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 $+$ here denotes addition on the natural numbers and @ denotes append. 

616 

355  617 
\subsection{A demonstration of rule inversion}\label{mkcases} 
103  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 
\] 

179  628 
The 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} 

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

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

636 
\end{ttbox} 

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

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

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

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

643 
\] 

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

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

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

647 

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

650 
prove the rule 

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

653 
\] 

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

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

657 
of the diamond property for parallel contraction on combinators. 

103  658 

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

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

662 
and 

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

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

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

667 

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

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

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

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

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

103  676 

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

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

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

103  681 
\] 
682 

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

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

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

103  689 
\] 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

690 
To make this coinductive definition, the theory file includes (after the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

691 
declaration of $\llist(A)$) the following lines: 
103  692 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

693 
consts lleq :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

694 
coinductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

695 
domains "lleq(A)" <= "llist(A) * llist(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

696 
intrs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

697 
LNil "<LNil, LNil> : lleq(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

698 
LCons "[ a:A; <l,l'>: lleq(A) ] ==> <LCons(a,l), LCons(a,l')>: lleq(A)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

130  702 
The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The typechecking 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

703 
rules include the introduction rules for $\llist(A)$, whose 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

704 
declaration is discussed below (\S\ref{listssec}). 
103  705 

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

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

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

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

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

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

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

717 
% \end{array} 

718 
}{[z\in X]_z} 

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

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

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

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

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

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

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

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

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

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

733 
introduction rule of the form 

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

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

597  736 
difficulties for other systems. Its premise is not acceptable to the 
737 
inductive definition package of the Cambridge HOL 

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

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

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

103  741 

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

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

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

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

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

747 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

748 
The theory file below follows this approach. Here $r$ is~$\prec$ and 
130  749 
$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

750 
relation is the union of its domain and range.) Finally $r^{}``\{a\}$ 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

751 
denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

752 
Pow\_mono}, which asserts that $\pow$ is monotonic. 
103  753 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

754 
Acc = WF + 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

755 
consts acc :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

756 
inductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

757 
domains "acc(r)" <= "field(r)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

758 
intrs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

759 
vimage "[ r``\{a\}: Pow(acc(r)); a: field(r) ] ==> a: acc(r)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

760 
monos "[Pow_mono]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

761 
end 
103  762 
\end{ttbox} 
763 
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For 

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

765 
$\acc(\prec)$. 

766 

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

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

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

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

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

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

773 
\] 

774 
The strange induction hypothesis is equivalent to 

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

776 
Therefore the rule expresses wellfounded induction on the accessible part 

777 
of~$\prec$. 

778 

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

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

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

782 
equivalently as 

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

786 
where $M=\lst$. 

787 

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

789 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

793 
the notion of composition, is less easily circumvented. 

794 

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

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

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

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

799 
\begin{itemize} 

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

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

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

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

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

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

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

807 
such that 

808 
\begin{eqnarray*} 

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

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

811 
\end{eqnarray*} 

812 

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

814 
recursive, such that 

815 
\begin{eqnarray*} 

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

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

818 
\end{eqnarray*} 

819 
\end{itemize} 

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

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

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

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

824 
tuplevalued functions. This modified the inductive definition such that 

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

826 

827 
\begin{figure} 

355  828 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

829 
Primrec = List + 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

830 
consts 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

831 
primrec :: i 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

832 
SC :: i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

833 
\(\vdots\) 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

834 
defs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

835 
SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

836 
\(\vdots\) 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

837 
inductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

838 
domains "primrec" <= "list(nat)>nat" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

839 
intrs 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

840 
SC "SC : primrec" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

841 
CONST "k: nat ==> CONST(k) : primrec" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

842 
PROJ "i: nat ==> PROJ(i) : primrec" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

843 
COMP "[ g: primrec; fs: list(primrec) ] ==> COMP(g,fs): primrec" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

844 
PREC "[ f: primrec; g: primrec ] ==> PREC(f,g): primrec" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

845 
monos "[list_mono]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

846 
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

847 
type_intrs "nat_typechecks @ list.intrs @ \ttback 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

848 
\ttback [lam_type, list_case_type, drop_type, map_type, \ttback 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

849 
\ttback apply_type, rec_type]" 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

850 
end 
355  851 
\end{ttbox} 
103  852 
\hrule 
853 
\caption{Inductive definition of the primitive recursive functions} 

854 
\label{primrecfig} 

855 
\end{figure} 

856 
\def\fs{{\it fs}} 

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

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

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

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

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

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

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

866 
an unusual induction hypothesis: 

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

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

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

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

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

874 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

875 
Figure~\ref{primrecfig} presents the theory file. Theory {\tt Primrec} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

876 
defines the constants $\SC$, $\CONST$, etc. These are not constructors of 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

877 
a new datatype, but functions over lists of numbers. Their definitions, 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

878 
most of which are omitted, consist of routine list programming. In 
355  879 
Isabelle/ZF, the primitive recursive functions are defined as a subset of 
880 
the function set $\lst(\nat)\to\nat$. 

103  881 

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

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

103  885 

886 

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

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

103  891 
involving any pair of constructors. 
892 

893 

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

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

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

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

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

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

103  902 

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

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

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

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

909 

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

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

916 

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

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

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

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

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

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

923 

924 
The standard pairs and injections can only yield wellfounded 

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

130  926 
over datatypes. But they are unsuitable for codatatypes, which typically 
103  927 
contain nonwellfounded objects. 
928 

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

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

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

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

103  939 

940 
\subsection{The case analysis operator} 

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

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

945 
for products and sums. 

103  946 

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

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

949 
\begin{eqnarray*} 

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

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

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

953 
\end{eqnarray*} 

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

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

956 
constructor: 

957 
\begin{eqnarray*} 

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 
\end{eqnarray*} 

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

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

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

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

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

103  967 
operators. Here are two examples: 
968 
\begin{itemize} 

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

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

971 
\begin{eqnarray*} 

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

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

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

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

976 
\end{eqnarray*} 

977 

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

979 
verify one of the three equations: 

980 
\begin{eqnarray*} 

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

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

983 
& = & g(b) 

984 
\end{eqnarray*} 

985 
\end{itemize} 

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

989 

355  990 
\medskip 
103  991 

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

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

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

996 
CADE version!} \else 

103  997 

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

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

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

1001 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1002 

5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1003 
\subsection{Example: lists and lazy lists}\label{listssec} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1004 
Here is a theory file that declares the datatype of lists: 
103  1005 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1006 
List = Datatype + 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1007 
consts list :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1008 
datatype "list(A)" = Nil  Cons ("a:A", "l: list(A)") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1009 
end 
103  1010 
\end{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1011 
And here is the theory file that declares the codatatype of lazy lists: 
103  1012 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1013 
LList = Datatype + 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1014 
consts llist :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1015 
codatatype "llist(A)" = LNil  LCons ("a: A", "l: llist(A)") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1016 
end 
103  1017 
\end{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1018 
They highlight the (many) similarities and (few) differences between 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1019 
datatype and codatatype definitions.\footnote{The real theory files contain 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1020 
many more declarations, mainly of functions over lists; the declaration 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1021 
of lazy lists is followed by the coinductive definition of lazy list 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1022 
equality.} 
103  1023 

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

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

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1026 
lists over a given set~$A$. Each specifies {\tt Datatype} as the parent 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1027 
theory; this implicitly specifies {\tt Univ} and {\tt QUniv} as ancestors, 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1028 
making available the definitions of $\univ$ and $\quniv$. Each is 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1029 
automatically given the appropriate domain: 
103  1030 
\begin{itemize} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1031 
\item $\lst(A)$ uses the domain $\univ(A)$ (the default choice can be 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1032 
overridden). 
103  1033 

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1034 
\item $\llist(A)$ uses the domain $\quniv(A)$. 
103  1035 
\end{itemize} 
1036 

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

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

1041 
\] 

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

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

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

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

1046 
is 

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

1048 

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

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

1053 
example, the definition 

1054 
\begin{eqnarray*} 

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

1056 
\end{eqnarray*} 

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

1058 

1059 
\medskip 

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

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

1062 
The list constructors are defined as follows: 

1063 
\begin{eqnarray*} 

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

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

1066 
\end{eqnarray*} 

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

1068 
\begin{eqnarray*} 

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

1070 
\end{eqnarray*} 

1071 
Let us verify the two equations: 

1072 
\begin{eqnarray*} 

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

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

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

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

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

130  1080 
& = & h(x,y) 
103  1081 
\end{eqnarray*} 
1082 

1083 

1084 
\subsection{Example: mutual recursion} 

130  1085 
In mutually recursive trees and forests~\cite[\S4.5]{paulsonsetII}, trees 
103  1086 
have the one constructor $\Tcons$, while forests have the two constructors 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1087 
$\Fnil$ and~$\Fcons$: 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1088 
\begin{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1089 
TF = List + 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1090 
consts tree, forest, tree_forest :: i=>i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1091 
datatype "tree(A)" = Tcons ("a: A", "f: forest(A)") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1092 
and "forest(A)" = Fnil  Fcons ("t: tree(A)", "f: forest(A)") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1093 
end 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1094 
\end{ttbox} 
103  1095 
The three introduction rules define the mutual recursion. The 
1096 
distinguishing feature of this example is its two induction rules. 

1097 

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

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

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

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

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

1103 
\end{array} 

1104 
\right]_{a,f}} 

1105 
& P(\Fnil) 

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

1109 
\end{array} 

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

1111 
\] 

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

1113 
recursive sets. 

1114 

1115 
Although such reasoning is sometimes useful 

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

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

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

1119 
induction hypotheses: 

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

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

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

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

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

1125 
\end{array} 

1126 
\right]_{a,f}} 

1127 
& Q(\Fnil) 

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

1131 
\end{array} 

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

1133 
\] 

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

1135 
operator. I have described elsewhere how this is done 

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

1137 

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

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

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

1141 
\begin{eqnarray*} 

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

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

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

1145 
\end{eqnarray*} 

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

1147 
forests: 

1148 
\begin{eqnarray*} 

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

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

1151 
\end{eqnarray*} 

1152 

1153 

1154 
\subsection{A fourconstructor datatype} 

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

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1156 
constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities. 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1157 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1158 
Data = Datatype + 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1159 
consts data :: [i,i] => i 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1160 
datatype "data(A,B)" = Con0 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1161 
 Con1 ("a: A") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1162 
 Con2 ("a: A", "b: B") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1163 
 Con3 ("a: A", "b: B", "d: data(A,B)") 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1164 
end 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1165 
\end{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1166 
Because this datatype has two set parameters, $A$ and~$B$, the package 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1167 
automatically supplies $\univ(A\un B)$ as its domain. The structural 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1168 
induction rule has four minor premises, one per constructor: 
103  1169 
\[ \infer{P(x)}{x\in\data(A,B) & 
1170 
P(\Con_0) & 

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

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

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

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

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

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

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

1178 
\end{array} 

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

1180 
\] 

1181 

1182 
The constructor definitions are 

1183 
\begin{eqnarray*} 

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

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

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

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

1188 
\end{eqnarray*} 

1189 
The case operator is 

1190 
\begin{eqnarray*} 

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

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

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

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

1195 
\end{array} 

1196 
\end{eqnarray*} 

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

1198 

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

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

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

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

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

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

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

1206 
numeral systems. 

1207 

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

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

1212 
\end{eqnarray*} 

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

1214 

1215 
\subsection{Proving freeness theorems} 

1216 
There are two kinds of freeness theorems: 

1217 
\begin{itemize} 

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

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

1220 

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

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

1223 
\end{itemize} 

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

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

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

1227 
simplification or classical reasoning. 

1228 

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

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

1231 
equations. The theorem list contains logical equivalences such as 

1232 
\begin{eqnarray*} 

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

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

1235 
& \vdots & \\ 

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

130  1237 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ 
103  1238 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 
1239 
\end{eqnarray*} 

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

1241 

1242 
The theorem list \verbfree_SEs enables the classical 

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

355  1244 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the 
103  1245 
assumptions. 
1246 

1247 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1251 
restores the defined constants. 

1252 
\fi %CADE 

1253 

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

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

1257 

1258 
Most automated logics can only express inductive definitions by asserting 

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

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

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

1262 
wellordering types) express datatype definitions, but the version 

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

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

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

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

1267 
researchers tried hard to circumvent these problems before finally 

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

1269 

1270 
Higherorder logic can express inductive definitions through quantification 

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

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

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

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

597  1275 
little used in the Cambridge HOL system. Melham~\cite{melham89} clearly 
1276 
describes the development. The natural numbers are defined as shown above, 

1277 
but lists are defined as functions over the natural numbers. Unlabelled 

355  1278 
trees are defined using G\"odel numbering; a labelled tree consists of an 
1279 
unlabelled tree paired with a list of labels. Melham's datatype package 

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

597  1281 
highly successful, but a fixedpoint approach might have yielded greater 
355  1282 
functionality with less effort. 
1283 

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

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

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

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

1288 
many monotone inductive definitions. 

1289 

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

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

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

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

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

597  1295 
asserts axioms.} 
355  1296 
LCF is a firstorder logic of domain theory; the relevant fixedpoint 
1297 
theorem is not KnasterTarski but concerns fixedpoints of continuous 

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

597  1299 
Thus it would appear that the Isabelle package is the first to be based 
355  1300 
on the KnasterTarski Theorem. 
1301 

1302 

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

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

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

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

1309 
could introduce unsoundness. 

1310 

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

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

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

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

1316 
version took under a week to code. 

1317 

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

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

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

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

597  1323 
much set theory. To justify infinitely branching datatype definitions, I 
1324 
have had to develop a theory of cardinal arithmetic, such as the theorem 

1325 
that if $\kappa$ is an infinite cardinal and $X(\alpha) \le \kappa$ for 

1326 
all $\alpha<\kappa$ then $\union\sb{\alpha<\kappa} X(\alpha) \le \kappa$. 

1327 
The need for such efforts is not a drawback of the fixedpoint 

355  1328 
approach, for the alternative is to take such definitions on faith. 
103  1329 

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1330 
Inductive and datatype definitions can take up considerable storage. The 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1331 
introduction rules are replicated in slightly different forms as fixedpoint 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1332 
definitions, elimination rules and induction rules. Here are two examples. 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1333 
Three datatypes and three inductive definitions specify the operational 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1334 
semantics of a simple imperative language; they occupy over 600K in total. 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1335 
One datatype definition, an enumeration type with 60 constructors, requires 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1336 
nearly 560K\@. 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1337 

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

597  1340 
have ported the (co)inductive definition package from Isabelle/ZF to 
1341 
Isabelle/HOL (higherorder logic). I hope to port the (co)datatype package 

1342 
later. HOL represents sets by unary predicates; defining the corresponding 

1343 
types may cause complications. 

103  1344 

1345 

355  1346 
\bibliographystyle{springer} 
1197  1347 
\bibliography{stringabbrv,atp,theory,funprog,isabelle,crossref} 
103  1348 
%%%%%\doendnotes 
1349 

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

1351 
\else 

1352 
\newpage 

1353 
\appendix 

130  1354 
\section{Inductive and coinductive definitions: users guide} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1355 
A theory file may contain any number of inductive and coinductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1356 
definitions. They may be intermixed with other declarations; in 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1357 
particular, the (co)inductive sets {\bf must} be declared separately as 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1358 
constants, and may have mixfix syntax or be subject to syntax translations. 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1359 

5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1360 
Each (co)inductive definition adds definitions to the theory and also 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1361 
proves some theorems. Each definition creates an ML structure, which is a 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1362 
substructure of the main theory structure. 
103  1363 

1364 
\subsection{The result structure} 

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

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

1367 
\begin{description} 

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

1369 

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

1371 

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

1373 

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

1375 

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

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1377 
the recursive sets. The rules are also available individually, using the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1378 
names given them in the theory file. 
103  1379 

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

1381 

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

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

1384 
\end{description} 

1385 

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

1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1387 
{\tt induct} and \verbmutual_induct. (To save storage, the latter rule is 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1388 
replaced by {\tt True} if it is not significantly different from 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1389 
{\tt induct}.) For a coinductive definition, it 
130  1390 
contains the rule \verbcoinduct. 
1391 

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

1393 
specifying the types of all these components. 

103  1394 

1395 
\begin{figure} 

1396 
\begin{ttbox} 

1397 
sig 

1398 
val thy : theory 

1399 
val defs : thm list 

1400 
val bnd_mono : thm 

1401 
val dom_subset : thm 

1402 
val intrs : thm list 

1403 
val elim : thm 

1404 
val mk_cases : thm list > string > thm 

1405 
{\it(Inductive definitions only)} 

1406 
val induct : thm 

1407 
val mutual_induct: thm 

130  1408 
{\it(Coinductive definitions only)} 
1409 
val coinduct : thm 

103  1410 
end 
1411 
\end{ttbox} 

1412 
\hrule 

130  1413 
\caption{The result of a (co)inductive definition} \label{defresultfig} 
103  1414 
\end{figure} 
1415 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1416 
\subsection{The syntax of a (co)inductive definition} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1417 
An inductive definition has the form 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1418 
\begin{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1419 
inductive 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1420 
domains {\it domain declarations} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1421 
intrs {\it introduction rules} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1422 
monos {\it monotonicity theorems} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1423 
con_defs {\it constructor definitions} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1424 
type_intrs {\it introduction rules for typechecking} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1425 
type_elims {\it elimination rules for typechecking} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1426 
\end{ttbox} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1427 
A coinductive definition is identical save that it starts with the keyword 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1428 
{\tt coinductive}. 
103  1429 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1430 
The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1431 
sections are optional. If present, each is specified as a string, which 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1432 
must be a valid ML expression of type {\tt thm list}. It is simply 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1433 
inserted into the {\tt .thy.ML} file; if it is illformed, it will trigger 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1434 
ML error messages. You can then inspect the file on your directory. 
103  1435 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1436 
\begin{description} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1437 
\item[\it domain declarations] consist of one or more items of the form 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1438 
{\it string\/}~{\tt <=}~{\it string}, associating each recursive set with 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1439 
its domain. 
103  1440 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1441 
\item[\it introduction rules] specify one or more introduction rules in 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1442 
the form {\it ident\/}~{\it string}, where the identifier gives the name of 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1443 
the rule in the result structure. 
103  1444 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1445 
\item[\it monotonicity theorems] are required for each operator applied to 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1446 
a recursive set in the introduction rules. There {\bf must} be a theorem 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1447 
of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$ 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1448 
in an introduction rule! 
103  1449 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1450 
\item[\it constructor definitions] contain definitions of constants 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1451 
appearing in the introduction rules. The (co)datatype package supplies 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1452 
the constructors' definitions here. Most (co)inductive definitions omit 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1453 
this section; one exception is the primitive recursive functions example 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1454 
(\S\ref{primrecsec}). 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1455 

5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1456 
\item[\it type\_intrs] consists of introduction rules for typechecking the 
103  1457 
definition, as discussed in~\S\ref{basicsec}. They are applied using 
1458 
depthfirst search; you can trace the proof by setting 

584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1459 

103  1460 
\verbtrace_DEPTH_FIRST := true. 
1461 