author  clasohm 
Thu, 29 Jun 1995 12:28:27 +0200  
changeset 1163  c080ff36d24e 
parent 597  ebf373c17ee2 
child 1197  ae58cd15e802 
permissions  rwrr 
497
990d2573efa6
revised for new theory system: removal of ext, addition of thy_name
lcp
parents:
455
diff
changeset

1 
\documentstyle[a4,proof,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}. 

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

311 
as 

103  312 
\begin{eqnarray*} 
313 
\Fin(A) & = & 

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

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

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

317 
\end{array} 

318 
\end{eqnarray*} 

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

322 

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

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

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

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

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

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

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

333 
\begin{eqnarray*} 

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

335 
\end{eqnarray*} 

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

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

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

339 
\begin{eqnarray*} 

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

343 

344 

345 
\subsection{Proving the introduction rules} 

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

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

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

353 
attempting to prove the result. 

354 

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

356 
in the rules, the package must prove 

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

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

359 
\] 

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

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

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

364 
could however be rules specifically proved for a particular inductive 

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

366 
through! 

103  367 

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

103  370 

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

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

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

377 
\] 

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

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

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

383 

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

386 
definitions involving datatypes, such as an inductively defined relation 

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

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

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

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

391 

103  392 

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

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

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

130  398 
coinductive definition, the package returns a basic coinduction rule. 
103  399 

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

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

404 

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

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

407 
introduction rule: 

408 
\begin{itemize} 

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

410 
is~$P(t)$. 

411 

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

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

103  415 

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

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

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

419 
then the minor premise discharges the single assumption 

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

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

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

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

424 
\end{itemize} 

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

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

429 
\] 

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

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

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

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

435 
and inductive relations. 

103  436 

437 
\subsection{Mutual induction} 

438 
The mutual induction rule is called {\tt 

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

440 
\begin{itemize} 

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

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

443 

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

445 
refers to all the recursive sets: 

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

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

448 
\] 

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

103  451 

452 
\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

453 
$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

454 
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

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

458 
\end{itemize} 

459 
The last point above simplifies reasoning about inductively defined 

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

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

462 

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

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

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

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

471 
\] 

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

130  475 
(see~\S\ref{univsec}). Coinductive definitions use these variant sums and 
103  476 
products. 
477 

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

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

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

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

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

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

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

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

130  494 

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

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

499 

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

504 

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

506 
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

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

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

510 
Finite = Arith + 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

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

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

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

516 
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

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

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

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

521 
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

522 
unary function symbol~$\Fin$, which is defined inductively. Its domain is 
355  523 
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

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

528 
\] 

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

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

355  531 
involves mostly introduction rules. 
532 

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

533 
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

534 
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

535 
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

536 
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

537 
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

538 
rule is {\tt Fin.induct}. 
355  539 

103  540 

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

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

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

545 
But her introduction rules 

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

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

550 
are not acceptable to the inductive definition package: 

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

552 

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

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

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

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

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

560 
rules are 

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

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

564 
\] 

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

565 
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

566 
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

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

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

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

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

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

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

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

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

575 
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

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

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

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

579 
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

580 
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

581 
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

582 
package always includes the necessary rules. 
103  583 

584 
The package returns introduction, elimination and induction rules for 

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

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

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

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

589 
\] 

590 
This rule requires the induction formula to be a 

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

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

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

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

597 
\] 

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

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

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

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

604 

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

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

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

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

611 
\] 

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

613 

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

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

618 
\infer*{Q} 

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

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

621 
a\in A \\ 

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

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

624 
\] 

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

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

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

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

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

633 
\end{ttbox} 

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

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

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

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

640 
\] 

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

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

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

644 

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

647 
prove the rule 

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

650 
\] 

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

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

654 
of the diamond property for parallel contraction on combinators. 

103  655 

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

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

659 
and 

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

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

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

664 

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

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

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

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

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

103  673 

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

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

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

103  678 
\] 
679 

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

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

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

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

687 
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

688 
declaration of $\llist(A)$) the following lines: 
103  689 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

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

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

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

695 
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

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

130  699 
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

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

701 
declaration is discussed below (\S\ref{listssec}). 
103  702 

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

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

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

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

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

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

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

714 
% \end{array} 

715 
}{[z\in X]_z} 

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

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

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

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

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

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

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

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

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

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

730 
introduction rule of the form 

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

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

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

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

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

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

103  738 

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

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

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

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

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

744 

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

745 
The theory file below follows this approach. Here $r$ is~$\prec$ and 
130  746 
$\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

747 
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

748 
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

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

751 
Acc = WF + 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

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

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

756 
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

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

758 
end 
103  759 
\end{ttbox} 
760 
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For 

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

762 
$\acc(\prec)$. 

763 

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

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

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

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

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

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

770 
\] 

771 
The strange induction hypothesis is equivalent to 

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

773 
Therefore the rule expresses wellfounded induction on the accessible part 

774 
of~$\prec$. 

775 

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

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

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

779 
equivalently as 

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

783 
where $M=\lst$. 

784 

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

786 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

790 
the notion of composition, is less easily circumvented. 

791 

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

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

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

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

796 
\begin{itemize} 

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

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

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

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

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

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

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

804 
such that 

805 
\begin{eqnarray*} 

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

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

808 
\end{eqnarray*} 

809 

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

811 
recursive, such that 

812 
\begin{eqnarray*} 

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

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

815 
\end{eqnarray*} 

816 
\end{itemize} 

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

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

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

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

821 
tuplevalued functions. This modified the inductive definition such that 

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

823 

824 
\begin{figure} 

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

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

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

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

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

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

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

832 
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

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

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

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

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

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

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

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

840 
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

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

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

843 
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

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

845 
\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

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

847 
end 
355  848 
\end{ttbox} 
103  849 
\hrule 
850 
\caption{Inductive definition of the primitive recursive functions} 

851 
\label{primrecfig} 

852 
\end{figure} 

853 
\def\fs{{\it fs}} 

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

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

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

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

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

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

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

863 
an unusual induction hypothesis: 

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

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

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

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

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

871 

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

872 
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

873 
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

874 
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

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

103  878 

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

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

103  882 

883 

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

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

103  888 
involving any pair of constructors. 
889 

890 

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

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

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

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

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

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

103  899 

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

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

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

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

906 

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

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

913 

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

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

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

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

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

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

920 

921 
The standard pairs and injections can only yield wellfounded 

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

130  923 
over datatypes. But they are unsuitable for codatatypes, which typically 
103  924 
contain nonwellfounded objects. 
925 

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

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

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

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

103  936 

937 
\subsection{The case analysis operator} 

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

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

942 
for products and sums. 

103  943 

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

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

946 
\begin{eqnarray*} 

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

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

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

950 
\end{eqnarray*} 

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

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

953 
constructor: 

954 
\begin{eqnarray*} 

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

956 
\qquad i = 1, \ldots, k 

957 
\end{eqnarray*} 

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

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

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

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

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

103  964 
operators. Here are two examples: 
965 
\begin{itemize} 

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

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

968 
\begin{eqnarray*} 

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

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

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

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

973 
\end{eqnarray*} 

974 

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

976 
verify one of the three equations: 

977 
\begin{eqnarray*} 

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

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

980 
& = & g(b) 

981 
\end{eqnarray*} 

982 
\end{itemize} 

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

986 

355  987 
\medskip 
103  988 

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

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

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

993 
CADE version!} \else 

103  994 

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

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

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

998 

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

999 

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

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

1001 
Here is a theory file that declares the datatype of lists: 
103  1002 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

1005 
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

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

1008 
And here is the theory file that declares the codatatype of lazy lists: 
103  1009 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1010 
LList = QUniv + 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

1012 
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

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

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

1016 
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

1017 
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

1018 
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

1019 
equality.} 
103  1020 

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

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

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

1024 
Isabelle/ZF theory: 

1025 
\begin{itemize} 

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

1026 
\item $\lst(A)$ requires the parent theory {\tt Univ}. The package 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

1028 
overridden). 
103  1029 

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

1030 
\item $\llist(A)$ requires the parent theory {\tt QUniv}. The package 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1031 
automatically uses the domain $\quniv(A)$. 
103  1032 
\end{itemize} 
1033 

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

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

1038 
\] 

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

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

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

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

1043 
is 

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

1045 

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

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

1050 
example, the definition 

1051 
\begin{eqnarray*} 

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

1053 
\end{eqnarray*} 

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

1055 

1056 
\medskip 

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

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

1059 
The list constructors are defined as follows: 

1060 
\begin{eqnarray*} 

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

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

1063 
\end{eqnarray*} 

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

1065 
\begin{eqnarray*} 

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

1067 
\end{eqnarray*} 

1068 
Let us verify the two equations: 

1069 
\begin{eqnarray*} 

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

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

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

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

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

130  1077 
& = & h(x,y) 
103  1078 
\end{eqnarray*} 
1079 

1080 

1081 
\subsection{Example: mutual recursion} 

130  1082 
In mutually recursive trees and forests~\cite[\S4.5]{paulsonsetII}, trees 
103  1083 
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

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

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

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

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

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

1089 
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

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

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

1094 

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

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

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

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

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

1100 
\end{array} 

1101 
\right]_{a,f}} 

1102 
& P(\Fnil) 

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

1106 
\end{array} 

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

1108 
\] 

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

1110 
recursive sets. 

1111 

1112 
Although such reasoning is sometimes useful 

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

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

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

1116 
induction hypotheses: 

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

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

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

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

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

1122 
\end{array} 

1123 
\right]_{a,f}} 

1124 
& Q(\Fnil) 

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

1128 
\end{array} 

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

1130 
\] 

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

1132 
operator. I have described elsewhere how this is done 

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

1134 

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

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

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

1138 
\begin{eqnarray*} 

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

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

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

1142 
\end{eqnarray*} 

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

1144 
forests: 

1145 
\begin{eqnarray*} 

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

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

1148 
\end{eqnarray*} 

1149 

1150 

1151 
\subsection{A fourconstructor datatype} 

1152 
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

1153 
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

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

1155 
Data = Univ + 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

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

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

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

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

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

1163 
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

1164 
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

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

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

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

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

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

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

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

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

1175 
\end{array} 

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

1177 
\] 

1178 

1179 
The constructor definitions are 

1180 
\begin{eqnarray*} 

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

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

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

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

1185 
\end{eqnarray*} 

1186 
The case operator is 

1187 
\begin{eqnarray*} 

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

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

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

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

1192 
\end{array} 

1193 
\end{eqnarray*} 

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

1195 

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

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

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

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

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

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

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

1203 
numeral systems. 

1204 

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

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

1209 
\end{eqnarray*} 

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

1211 

1212 
\subsection{Proving freeness theorems} 

1213 
There are two kinds of freeness theorems: 

1214 
\begin{itemize} 

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

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

1217 

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

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

1220 
\end{itemize} 

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

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

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

1224 
simplification or classical reasoning. 

1225 

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

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

1228 
equations. The theorem list contains logical equivalences such as 

1229 
\begin{eqnarray*} 

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

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

1232 
& \vdots & \\ 

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

130  1234 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ 
103  1235 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 
1236 
\end{eqnarray*} 

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

1238 

1239 
The theorem list \verbfree_SEs enables the classical 

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

355  1241 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the 
103  1242 
assumptions. 
1243 

1244 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1248 
restores the defined constants. 

1249 
\fi %CADE 

1250 

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

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

1254 

1255 
Most automated logics can only express inductive definitions by asserting 

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

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

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

1259 
wellordering types) express datatype definitions, but the version 

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

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

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

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

1264 
researchers tried hard to circumvent these problems before finally 

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

1266 

1267 
Higherorder logic can express inductive definitions through quantification 

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

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

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

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

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

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

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

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

597  1278 
highly successful, but a fixedpoint approach might have yielded greater 
355  1279 
functionality with less effort. 
1280 

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

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

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

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

1285 
many monotone inductive definitions. 

1286 

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

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

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

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

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

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

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

597  1296 
Thus it would appear that the Isabelle package is the first to be based 
355  1297 
on the KnasterTarski Theorem. 
1298 

1299 

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

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

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

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

1306 
could introduce unsoundness. 

1307 

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

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

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

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

1313 
version took under a week to code. 

1314 

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

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

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

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

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

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

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

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

355  1325 
approach, for the alternative is to take such definitions on faith. 
103  1326 

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

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

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

1332 
types may cause complications. 

103  1333 

1334 

355  1335 
\bibliographystyle{springer} 
1336 
\bibliography{stringabbrv,atp,theory,funprog,isabelle} 

103  1337 
%%%%%\doendnotes 
1338 

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

1340 
\else 

1341 
\newpage 

1342 
\appendix 

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

1344 
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

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

1346 
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

1347 
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

1348 

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

1349 
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

1350 
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

1351 
substructure of the main theory structure. 
103  1352 

1353 
\subsection{The result structure} 

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

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

1356 
\begin{description} 

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

1358 

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

1360 

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

1362 

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

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

1365 

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

1367 

1368 
\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

1369 
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

1370 
names given them in the theory file. 
103  1371 

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

1373 

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

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

1376 
\end{description} 

1377 

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

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

1381 

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

1383 
specifying the types of all these components. 

103  1384 

1385 
\begin{figure} 

1386 
\begin{ttbox} 

1387 
sig 

1388 
val thy : theory 

1389 
val defs : thm list 

1390 
val bnd_mono : thm 

1391 
val unfold : thm 

1392 
val dom_subset : thm 

1393 
val intrs : thm list 

1394 
val elim : thm 

1395 
val mk_cases : thm list > string > thm 

1396 
{\it(Inductive definitions only)} 

1397 
val induct : thm 

1398 
val mutual_induct: thm 

130  1399 
{\it(Coinductive definitions only)} 
1400 
val coinduct : thm 

103  1401 
end 
1402 
\end{ttbox} 

1403 
\hrule 

130  1404 
\caption{The result of a (co)inductive definition} \label{defresultfig} 
103  1405 
\end{figure} 
1406 

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

1407 
\subsection{The syntax of a (co)inductive definition} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1408 
An inductive definition has the form 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

1411 
domains {\it domain declarations} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1412 
intrs {\it introduction rules} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1413 
monos {\it monotonicity theorems} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1414 
con_defs {\it constructor definitions} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1415 
type_intrs {\it introduction rules for typechecking} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1416 
type_elims {\it elimination rules for typechecking} 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

1418 
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

1419 
{\tt coinductive}. 
103  1420 

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

1421 
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

1422 
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

1423 
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

1424 
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

1425 
ML error messages. You can then inspect the file on your directory. 
103  1426 

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

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

1428 
\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

1429 
{\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

1430 
its domain. 
103  1431 

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

1432 
\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

1433 
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

1434 
the rule in the result structure. 
103  1435 

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

1436 
\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

1437 
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

1438 
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

1439 
in an introduction rule! 
103  1440 

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

1441 
\item[\it constructor definitions] contain definitions of constants 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1442 
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

1443 
the constructors' definitions here. Most (co)inductive definitions omit 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1444 
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

1445 
(\S\ref{primrecsec}). 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1446 

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

1447 
\item[\it type\_intrs] consists of introduction rules for typechecking the 
103  1448 
definition, as discussed in~\S\ref{basicsec}. They are applied using 
1449 
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

1450 

103  1451 
\verbtrace_DEPTH_FIRST := true. 
1452 

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

1453 
\item[\it type\_elims] consists of elimination rules for typechecking the 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1454 
definition. They are presumed to be `safe' and are applied as much as 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1455 
possible, prior to the {\tt type\_intrs} search. 
103  1456 
\end{description} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1457 

103  1458 
The package has a few notable restrictions: 
1459 
\begin{itemize} 

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

1460 
\item The theory must separately declare the recursive sets as 
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1461 
constants. 
103  1462 

1463 
\item The names of the recursive sets must be identifiers, not infix 

1464 
operators. 

1465 

1466 
\item Sideconditions must not be conjunctions. However, an introduction rule 

30bd42401ab2
Initial revision
