author  paulson 
Thu, 21 Mar 1996 13:02:26 +0100  
changeset 1601  0ef6ea27ab15 
parent 1533  771474fd33be 
child 1742  328fb06a1648 
permissions  rwrr 
1533  1 
\documentstyle[a4,alltt,iman,extra,proof209,12pt]{article} 
2 
\newif\ifshort 

3 
\shortfalse 

103  4 

1533  5 
\title{A Fixedpoint Approach to\\ 
6 
(Co)Inductive and (Co)Datatype Definitions% 

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

355  8 
comments; the referees were also helpful. Research funded by 
9 
SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 

1533  10 
``Types''.}} 
103  11 

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

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

16 

17 
\newcommand\sbs{\subseteq} 

18 
\let\To=\Rightarrow 

19 

1533  20 
\newcommand\emph[1]{{\em#1\/}} 
21 
\newcommand\defn[1]{{\bf#1}} 

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

103  23 

355  24 
\newcommand\pow{{\cal P}} 
25 
%%%\let\pow=\wp 

26 
\newcommand\RepFun{\hbox{\tt RepFun}} 

27 
\newcommand\cons{\hbox{\tt cons}} 

28 
\def\succ{\hbox{\tt succ}} 

29 
\newcommand\split{\hbox{\tt split}} 

30 
\newcommand\fst{\hbox{\tt fst}} 

31 
\newcommand\snd{\hbox{\tt snd}} 

32 
\newcommand\converse{\hbox{\tt converse}} 

33 
\newcommand\domain{\hbox{\tt domain}} 

34 
\newcommand\range{\hbox{\tt range}} 

35 
\newcommand\field{\hbox{\tt field}} 

36 
\newcommand\lfp{\hbox{\tt lfp}} 

37 
\newcommand\gfp{\hbox{\tt gfp}} 

38 
\newcommand\id{\hbox{\tt id}} 

39 
\newcommand\trans{\hbox{\tt trans}} 

40 
\newcommand\wf{\hbox{\tt wf}} 

41 
\newcommand\nat{\hbox{\tt nat}} 

42 
\newcommand\rank{\hbox{\tt rank}} 

43 
\newcommand\univ{\hbox{\tt univ}} 

44 
\newcommand\Vrec{\hbox{\tt Vrec}} 

45 
\newcommand\Inl{\hbox{\tt Inl}} 

46 
\newcommand\Inr{\hbox{\tt Inr}} 

47 
\newcommand\case{\hbox{\tt case}} 

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

49 
\newcommand\Nil{\hbox{\tt Nil}} 

50 
\newcommand\Cons{\hbox{\tt Cons}} 

103  51 
\newcommand\lstcase{\hbox{\tt list\_case}} 
52 
\newcommand\lstrec{\hbox{\tt list\_rec}} 

355  53 
\newcommand\length{\hbox{\tt length}} 
54 
\newcommand\listn{\hbox{\tt listn}} 

55 
\newcommand\acc{\hbox{\tt acc}} 

56 
\newcommand\primrec{\hbox{\tt primrec}} 

57 
\newcommand\SC{\hbox{\tt SC}} 

58 
\newcommand\CONST{\hbox{\tt CONST}} 

59 
\newcommand\PROJ{\hbox{\tt PROJ}} 

60 
\newcommand\COMP{\hbox{\tt COMP}} 

61 
\newcommand\PREC{\hbox{\tt PREC}} 

103  62 

355  63 
\newcommand\quniv{\hbox{\tt quniv}} 
64 
\newcommand\llist{\hbox{\tt llist}} 

65 
\newcommand\LNil{\hbox{\tt LNil}} 

66 
\newcommand\LCons{\hbox{\tt LCons}} 

67 
\newcommand\lconst{\hbox{\tt lconst}} 

68 
\newcommand\lleq{\hbox{\tt lleq}} 

69 
\newcommand\map{\hbox{\tt map}} 

70 
\newcommand\term{\hbox{\tt term}} 

71 
\newcommand\Apply{\hbox{\tt Apply}} 

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

73 
\newcommand\rev{\hbox{\tt rev}} 

74 
\newcommand\reflect{\hbox{\tt reflect}} 

75 
\newcommand\tree{\hbox{\tt tree}} 

76 
\newcommand\forest{\hbox{\tt forest}} 

77 
\newcommand\Part{\hbox{\tt Part}} 

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

79 
\newcommand\Tcons{\hbox{\tt Tcons}} 

80 
\newcommand\Fcons{\hbox{\tt Fcons}} 

81 
\newcommand\Fnil{\hbox{\tt Fnil}} 

103  82 
\newcommand\TFcase{\hbox{\tt TF\_case}} 
355  83 
\newcommand\Fin{\hbox{\tt Fin}} 
84 
\newcommand\QInl{\hbox{\tt QInl}} 

85 
\newcommand\QInr{\hbox{\tt QInr}} 

86 
\newcommand\qsplit{\hbox{\tt qsplit}} 

87 
\newcommand\qcase{\hbox{\tt qcase}} 

88 
\newcommand\Con{\hbox{\tt Con}} 

89 
\newcommand\data{\hbox{\tt data}} 

103  90 

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

92 

93 
\begin{document} 

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

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

95 
\begin{titlepage} 
103  96 
\maketitle 
97 
\begin{abstract} 

355  98 
This paper presents a fixedpoint approach to inductive definitions. 
1533  99 
Instead of using a syntactic test such as ``strictly positive,'' the 
355  100 
approach lets definitions involve any operators that have been proved 
101 
monotone. It is conceptually simple, which has allowed the easy 

102 
implementation of mutual recursion and other conveniences. It also 

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

104 
greatest fixedpoint. This represents the first automated support for 

105 
coinductive definitions. 

130  106 

1533  107 
The method has been implemented in two of Isabelle's logics, \textsc{zf} set 
108 
theory and higherorder logic. It should be applicable to any logic in 

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

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

597  111 
recursive functions. One example of a coinductive definition is 
1533  112 
bisimulations for lazy lists. Recursive datatypes are examined in detail, 
113 
as well as one example of a \defn{codatatype}: lazy lists. 

114 

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

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

117 
semantic consistency. 

103  118 
\end{abstract} 
119 
% 

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

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

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

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

124 
\tableofcontents\cleardoublepage\pagestyle{plain} 
103  125 

1533  126 
\setcounter{page}{1} 
127 

103  128 
\section{Introduction} 
129 
Several theorem provers provide commands for formalizing recursive data 

1533  130 
structures, like lists and trees. Robin Milner implemented one of the first 
131 
of these, for Edinburgh \textsc{lcf}~\cite{milnerind}. Given a description 

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

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

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

135 
Such data structures are called \defn{datatypes} 

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

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

138 
principle~\cite{bm79} and the Coq type theory~\cite{paulin92}. 

103  139 

1533  140 
A datatype is but one example of an \defn{inductive definition}. This 
103  141 
specifies the least set closed under given rules~\cite{aczel77}. The 
142 
collection of theorems in a logic is inductively defined. A structural 

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

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

145 
provide commands for formalizing inductive definitions; these include 

1533  146 
Coq~\cite{paulin92} and again the \textsc{hol} system~\cite{camilleri92}. 
103  147 

1533  148 
The dual notion is that of a \defn{coinductive definition}. This specifies 
103  149 
the greatest set closed under given rules. Important examples include 
150 
using bisimulation relations to formalize equivalence of 

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

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

1533  153 
are called \defn{codatatypes} below. 
103  154 

1533  155 
Not all inductive definitions are meaningful. \defn{Monotone} inductive 
355  156 
definitions are a large, wellbehaved class. Monotonicity can be enforced 
1533  157 
by syntactic conditions such as ``strictly positive,'' but this could lead to 
355  158 
monotone definitions being rejected on the grounds of their syntactic form. 
159 
More flexible is to formalize monotonicity within the logic and allow users 

160 
to prove it. 

103  161 

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

163 
fixedpoints yield inductive definitions; greatest fixedpoints yield 

1533  164 
coinductive definitions. Most of the discussion below applies equally to 
165 
inductive and coinductive definitions, and most of the code is shared. To my 

166 
knowledge, this is the only package supporting coinductive definitions. 

167 

168 
The package supports mutual recursion and infinitelybranching datatypes and 

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

170 
thus accepting all provably monotone inductive definitions, including 

171 
iterated definitions. 

172 

173 
The package has been implemented in Isabelle~\cite{isabelleintro} using 

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

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

176 
recursion equations are specified as introduction rules for the mutually 

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

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

179 
successful, the package makes fixedpoint definitions and proves the 

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

181 
by making simple declarations in Isabelle theory files. 

103  182 

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

355  184 
recursive functions. This is the main omission from my package. Its 
1533  185 
fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf} 
186 
theory provides wellfounded recursion~\cite{paulsonsetII}, which is harder 

187 
to use than structural recursion but considerably more general. 

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

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

103  190 

1533  191 
\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint 
355  192 
operators. Section~3 discusses the form of introduction rules, mutual 
193 
recursion and other points common to inductive and coinductive definitions. 

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

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

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

1533  197 
Section~8 draws brief conclusions. \ifshort\else The appendices are simple 
597  198 
user's manuals for this Isabelle package.\fi 
103  199 

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

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

202 

203 
\section{Fixedpoint operators} 

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

205 
follows: 

206 
\begin{eqnarray*} 

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

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

209 
\end{eqnarray*} 

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

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

214 
\begin{eqnarray*} 

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

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

217 
\end{eqnarray*} 

1533  218 
These equations are instances of the KnasterTarski theorem, which states 
103  219 
that every monotonic function over a complete lattice has a 
220 
fixedpoint~\cite{davey&priestley}. It is obvious from their definitions 

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

222 

1533  223 
This fixedpoint theory is simple. The KnasterTarski theorem is easy to 
103  224 
prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must 
1533  225 
also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when 
226 
a set of theorems is (co)inductively defined over some previously existing set 

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

228 
branching (co)datatype definitions; see~\S\ref{univsec}. Bounding sets are 

229 
also called \defn{domains}. 

103  230 

1533  231 
The powerset operator is monotone, but by Cantor's theorem there is no 
355  232 
set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because 
233 
there is no suitable domain~$D$. But \S\ref{accsec} demonstrates 

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

103  235 

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

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

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

241 
under an injection. Reasons for this are discussed 

130  242 
elsewhere~\cite[\S4.5]{paulsonsetII}. 
103  243 

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

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

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

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

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

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

355  250 
varies. Section~\ref{listnsec} describes how to express this set using the 
130  251 
inductive definition package. 
103  252 

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

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

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

1533  257 
The body of the definition consists of the desired introduction rules. The 
258 
conclusion of each rule must have the form $t\in R_i$, where $t$ is any term. 

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

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

103  261 

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

263 
sets, satisfying the rule 

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

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

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

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

1533  270 
expresses $t\sbs R$; see \S\ref{accsec} for an example. The \emph{list of} 
355  271 
operator is monotone, as is easily proved by induction. The premise 
272 
$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual 

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

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

103  275 

1533  276 
Introduction rules may also contain \defn{sideconditions}. These are 
277 
premises consisting of arbitrary formul{\ae} not mentioning the recursive 

103  278 
sets. Sideconditions typically involve typechecking. One example is the 
279 
premise $a\in A$ in the following rule from the definition of lists: 

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

281 

282 
\subsection{The fixedpoint definitions} 

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

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

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

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

289 
\] 

290 

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

1533  294 
\[ \Fin(A) \equiv \lfp(\pow(A), \, 
103  295 
\begin{array}[t]{r@{\,}l} 
296 
\lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\ 

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

298 
\end{array} 

1533  299 
\] 
103  300 
The contribution of each rule to the definition of $\Fin(A)$ should be 
130  301 
obvious. A coinductive definition is similar but uses $\gfp$ instead 
103  302 
of~$\lfp$. 
303 

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

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

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

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

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

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

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

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

1533  314 
The package returns its result as an \textsc{ml} structure, which consists of named 
355  315 
components; we may regard it as a record. The result structure contains 
316 
the definitions of the recursive sets as a theorem list called {\tt defs}. 

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

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

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

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

320 

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

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

322 
such as 
1533  323 
\[ 
103  324 
\begin{array}[t]{r@{\,}l} 
1533  325 
\Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\ 
103  326 
&(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\} 
327 
\end{array} 

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

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

331 

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

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

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

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

1533  339 
As discussed elsewhere \cite[\S4.5]{paulsonsetII}, Isabelle/\textsc{zf} defines the 
103  340 
operator $\Part$ to support mutual recursion. The set $\Part(A,h)$ 
341 
contains those elements of~$A$ having the form~$h(z)$: 

1533  342 
\[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \] 
103  343 
For mutually recursive sets $R_1$, \ldots,~$R_n$ with 
344 
$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using 

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

1533  346 
\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \] 
103  347 
It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint. 
348 

349 

350 
\subsection{Proving the introduction rules} 

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

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

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

358 
attempting to prove the result. 

359 

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

361 
in the rules, the package must prove 

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

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

364 
\] 

597  365 
Such proofs can be regarded as typechecking the definition.\footnote{The 
1533  366 
Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol} 
367 
has implicit typechecking.} The user supplies the package with 

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

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

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

371 
definition through! 

103  372 

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

103  375 

355  376 
\subsection{The case analysis rule} 
1533  377 
The elimination rule, called {\tt elim}, performs case analysis. It is a 
378 
simple consequence of {\tt unfold}. There is one case for each introduction 

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

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

381 
is written 

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

384 
\] 

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

103  388 

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

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

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

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

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

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

400 

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

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

403 
introduction rule: 

404 
\begin{itemize} 

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

406 
is~$P(t)$. 

407 

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

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

103  411 

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

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

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

415 
then the minor premise discharges the single assumption 

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

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

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

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

420 
\end{itemize} 

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

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

425 
\] 

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

1533  428 
b$. The Isabelle/\textsc{zf} theory defines the \defn{rank} of a 
355  429 
set~\cite[\S3.4]{paulsonsetII}, which supports wellfounded induction and 
430 
recursion over datatypes. The package proves a rule for mutual induction 

431 
and inductive relations. 

103  432 

433 
\subsection{Mutual induction} 

434 
The mutual induction rule is called {\tt 

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

436 
\begin{itemize} 

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

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

439 

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

441 
refers to all the recursive sets: 

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

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

444 
\] 

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

103  447 

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

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

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

450 
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

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

454 
\end{itemize} 

455 
The last point above simplifies reasoning about inductively defined 

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

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

458 

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

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

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

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

467 
\] 

130  468 
The $()$ tag stresses that this is a coinductive definition. A suitable 
1533  469 
domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant 
470 
forms of sum and product that are used to represent nonwellfounded data 

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

103  472 

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

355  474 
Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$ 
103  475 
is the greatest solution to this equation contained in $\quniv(A)$: 
130  476 
\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) & 
1533  477 
\infer*{ 
478 
\begin{array}[b]{r@{}l} 

479 
z=\LNil\disj 

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

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

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

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

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

130  488 

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

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

1533  493 
The clumsy form of the third premise makes the rule hard to use, especially in 
494 
large definitions. Probably a constant should be declared to abbreviate the 

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

496 

103  497 

130  498 
\section{Examples of inductive and coinductive definitions}\label{indegsec} 
1533  499 
This section presents several examples from the literature: the finite 
500 
powerset operator, lists of $n$ elements, bisimulations on lazy lists, the 

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

103  502 

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

504 
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

505 
corresponding invocation in an Isabelle theory file. Note that 
1533  506 
$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}. 
103  507 
\begin{ttbox} 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

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

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

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

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

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

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

514 
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

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

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

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

519 
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

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

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

526 
\] 

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

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

355  529 
involves mostly introduction rules. 
530 

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

531 
Like all Isabelle theory files, this one yields a structure containing the 
1533  532 
new theory as an \textsc{ml} value. Structure {\tt Finite} also has a 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

533 
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

534 
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

535 
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

536 
rule is {\tt Fin.induct}. 
355  537 

103  538 

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

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

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

543 
But her introduction rules 

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

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

548 
are not acceptable to the inductive definition package: 

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

550 

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

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

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

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

1533  557 
converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction 
355  558 
rules are 
103  559 
\[ \pair{0,\Nil}\in\listn(A) \qquad 
560 
\infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} 

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

562 
\] 

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

563 
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

564 
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

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

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

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

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

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

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

571 
intrs 
1533  572 
NilI "<0,Nil>: listn(A)" 
573 
ConsI "[ a: A; <n,l>: listn(A) ] ==> <succ(n), Cons(a,l)>: listn(A)" 

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

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

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

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

577 
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

578 
Because $\listn(A)$ is a set of pairs, typechecking requires the 
1533  579 
equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The 
580 
package always includes the rules for ordered pairs. 

103  581 

582 
The package returns introduction, elimination and induction rules for 

1533  583 
$\listn$. The basic induction rule, {\tt listn.induct}, is 
103  584 
\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & 
585 
\infer*{P(\pair{\succ(n),\Cons(a,l)})} 

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

587 
\] 

588 
This rule requires the induction formula to be a 

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

1533  590 
listn.mutual\_induct}, uses a binary property instead: 
130  591 
\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} 
103  592 
{P(0,\Nil) & 
593 
\infer*{P(\succ(n),\Cons(a,l))} 

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

595 
\] 

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

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

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

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

602 

1533  603 
Unlike in Coq, the definition does not declare a new datatype. A ``list of 
604 
$n$ elements'' really is a list and is subject to list operators such 

130  605 
as append (concatenation). For example, a trivial induction on 
606 
$\pair{m,l}\in\listn(A)$ yields 

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

609 
\] 

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

611 

1533  612 
\subsection{Rule inversion: the function {\tt mk\_cases}} 
613 
The elimination rule, {\tt listn.elim}, is cumbersome: 

103  614 
\[ \infer{Q}{x\in\listn(A) & 
615 
\infer*{Q}{[x = \pair{0,\Nil}]} & 

616 
\infer*{Q} 

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

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

619 
a\in A \\ 

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

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

622 
\] 

1533  623 
The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of 
179  624 
this rule. It works by freeness reasoning on the list constructors: 
625 
$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If 

1533  626 
$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases} 
627 
deduces the corresponding form of~$i$; this is called rule inversion. 

628 
Here is a sample session: 

103  629 
\begin{ttbox} 
1533  630 
listn.mk_cases list.con_defs "<i,Nil> : listn(A)"; 
631 
{\out "[ <?i, []> : listn(?A); ?i = 0 ==> ?Q ] ==> ?Q" : thm} 

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

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

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

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

103  636 
\end{ttbox} 
1533  637 
Each of these rules has only two premises. In conventional notation, the 
638 
second rule is 

103  639 
\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
640 
\infer*{Q} 

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

1533  642 
a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n) 
103  643 
\end{array} \right]_{n}}} 
644 
\] 

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

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

1533  647 
listn.mk\_cases} can deduce the corresponding form of~$l$. 
103  648 

355  649 
The function {\tt mk\_cases} is also useful with datatype definitions. The 
1533  650 
instance from the definition of lists, namely {\tt list.mk\_cases}, can 
651 
prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$: 

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

654 
\] 

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

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

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

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

660 
residuals~\cite{rasmussen95}. 

661 

103  662 

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

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

1533  666 
and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coindsec}. 
103  667 
Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant 
668 
pairing and injection operators, it contains nonwellfounded elements such as 

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

670 

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

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

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

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

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

103  679 

1533  680 
A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs 
103  681 
R^+$, where $R^+$ is the relation 
130  682 
\[ \{\pair{\LNil,\LNil}\} \un 
683 
\{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}. 

103  684 
\] 
685 

1533  686 
A pair of lazy lists are \defn{equivalent} if they belong to some bisimulation. 
130  687 
Equivalence can be coinductively defined as the greatest fixedpoint for the 
103  688 
introduction rules 
130  689 
\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad 
690 
\infer[()]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} 

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

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

693 
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

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

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

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

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

699 
intrs 
1533  700 
LNil "<LNil,LNil> : lleq(A)" 
701 
LCons "[ a:A; <l,l'>: lleq(A) ] ==> <LCons(a,l),LCons(a,l')>: lleq(A)" 

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

702 
type_intrs "llist.intrs" 
103  703 
\end{ttbox} 
130  704 
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

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

706 
declaration is discussed below (\S\ref{listssec}). 
103  707 

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

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

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

1533  714 
\begin{array}[t]{@{}l} 
715 
z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\ 

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

717 
\end{array} 

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

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

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

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

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

1533  728 
The \defn{accessible} or \defn{wellfounded} part of~$\prec$, written 
103  729 
$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits 
730 
no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is 

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

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

733 
introduction rule of the form 

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

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

597  736 
difficulties for other systems. Its premise is not acceptable to the 
1533  737 
inductive definition package of the Cambridge \textsc{hol} 
597  738 
system~\cite{camilleri92}. It is also unacceptable to Isabelle package 
739 
(recall \S\ref{introsec}), but fortunately can be transformed into the 

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

103  741 

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

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

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

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

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

747 

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

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

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

752 
Pow\_mono}, which asserts that $\pow$ is monotonic. 
103  753 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

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

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

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

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

758 
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

759 
monos "[Pow_mono]" 
103  760 
\end{ttbox} 
761 
The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For 

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

763 
$\acc(\prec)$. 

764 

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

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

1533  767 
induction rule, {\tt acc.induct}: 
103  768 
\[ \infer{P(x)}{x\in\acc(r) & 
1533  769 
\infer*{P(a)}{\left[ 
770 
\begin{array}{r@{}l} 

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

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

773 
\end{array} 

774 
\right]_a}} 

103  775 
\] 
776 
The strange induction hypothesis is equivalent to 

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

778 
Therefore the rule expresses wellfounded induction on the accessible part 

779 
of~$\prec$. 

780 

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

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

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

784 
equivalently as 

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

788 
where $M=\lst$. 

789 

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

791 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

795 
the notion of composition, is less easily circumvented. 

796 

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

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

1533  799 
$[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it 
103  800 
belongs to the least set of functions in $\lst(\nat)\to\nat$ containing 
801 
\begin{itemize} 

1533  802 
\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$. 
803 
\item All \defn{constant} functions $\CONST(k)$, such that 

103  804 
$\CONST(k)[\vec{x}]=k$. 
1533  805 
\item All \defn{projection} functions $\PROJ(i)$, such that 
103  806 
$\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 
1533  807 
\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m1}])$, 
103  808 
where $g$ and $f_0$, \ldots, $f_{m1}$ are primitive recursive, 
809 
such that 

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

103  812 

1533  813 
\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive 
103  814 
recursive, such that 
815 
\begin{eqnarray*} 

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

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

818 
\end{eqnarray*} 

819 
\end{itemize} 

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

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

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

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

824 
tuplevalued functions. This modified the inductive definition such that 

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

826 

827 
\begin{figure} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

846 
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" 
1533  847 
type_intrs "nat_typechecks @ list.intrs @ 
848 
[lam_type, list_case_type, drop_type, map_type, 

849 
apply_type, rec_type]" 

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

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

854 
\label{primrecfig} 

855 
\end{figure} 

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

1533  857 

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

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

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

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

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

863 
$\COMP$: 

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

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

867 
an unusual induction hypothesis: 

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

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

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

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

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

875 

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

876 
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

877 
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

878 
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

879 
most of which are omitted, consist of routine list programming. In 
1533  880 
Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of 
355  881 
the function set $\lst(\nat)\to\nat$. 
103  882 

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

1533  885 
primrec.induct}. The proof follows Szasz's excellent account. 
103  886 

887 

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

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

103  892 
involving any pair of constructors. 
893 

894 

130  895 
\subsection{Constructors and their domain}\label{univsec} 
1533  896 
A (co)inductive definition selects a subset of an existing set; a (co)datatype 
897 
definition creates a new set. The package reduces the latter to the 

898 
former. Isabelle/\textsc{zf} supplies sets having strong closure properties to serve 

899 
as domains for (co)inductive definitions. 

103  900 

1533  901 
Isabelle/\textsc{zf} defines the Cartesian product $A\times 
902 
B$, containing ordered pairs $\pair{a,b}$; it also defines the 

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

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

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

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

907 

103  908 

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

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

915 

1533  916 
Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and 
103  917 
furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$, 
918 
$b\in\univ(A)$. In a typical datatype definition with set parameters 

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

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

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

922 

923 
The standard pairs and injections can only yield wellfounded 

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

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

1533  928 
To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of 
929 
ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant 

103  930 
notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$ 
1533  931 
and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the 
932 
set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$, 

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

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

935 
$\quniv(A_1\un\cdots\un A_k)$. 

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: 

1533  954 
\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}), 
103  955 
\qquad i = 1, \ldots, k 
1533  956 
\] 
957 
The case operator's definition takes advantage of Isabelle's representation of 

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

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

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

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

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

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

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

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

968 

355  969 
\medskip 
103  970 

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

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

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

974 

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

975 

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

976 
\subsection{Example: lists and lazy lists}\label{listssec} 
1533  977 
Here is a declaration of the datatype of lists, as it might appear in a theory 
978 
file: 

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

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

981 
datatype "list(A)" = Nil  Cons ("a:A", "l: list(A)") 
103  982 
\end{ttbox} 
1533  983 
And here is a declaration of the codatatype of lazy lists: 
103  984 
\begin{ttbox} 
1421
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

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

986 
codatatype "llist(A)" = LNil  LCons ("a: A", "l: llist(A)") 
103  987 
\end{ttbox} 
988 

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

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

1533  991 
lists over a given set~$A$. Each requires {\tt Datatype} as a parent theory; 
992 
this makes available the definitions of $\univ$ and $\quniv$. Each is 

993 
automatically given the appropriate domain: $\univ(A)$ for $\lst(A)$ and 

994 
$\quniv(A)$ for $\llist(A)$. The default can be overridden. 

103  995 

130  996 
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt 
1533  997 
list.induct}: 
103  998 
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) 
999 
& \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } 

1000 
\] 

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

1533  1002 
Isabelle/\textsc{zf} defines the rank of a set and proves that the standard pairs and 
103  1003 
injections have greater rank than their components. An immediate consequence, 
1004 
which justifies structural recursion on lists \cite[\S4.3]{paulsonsetII}, 

1005 
is 

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

1007 

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

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

1012 
example, the definition 

1533  1013 
\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \] 
103  1014 
yields $\lconst(a) = \LCons(a,\lconst(a))$. 
1015 

1016 
\medskip 

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

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

1019 
The list constructors are defined as follows: 

1020 
\begin{eqnarray*} 

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

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

1023 
\end{eqnarray*} 

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

1533  1025 
\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \] 
103  1026 
Let us verify the two equations: 
1027 
\begin{eqnarray*} 

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

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

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

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

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

130  1035 
& = & h(x,y) 
103  1036 
\end{eqnarray*} 
1037 

1038 

1039 
\subsection{Example: mutual recursion} 

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

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

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

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

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

1046 
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

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

1050 

1533  1051 
The basic induction rule is called {\tt tree\_forest.induct}: 
103  1052 
\[ \infer{P(x)}{x\in\TF(A) & 
1053 
\infer*{P(\Tcons(a,f))} 

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

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

1056 
\end{array} 

1057 
\right]_{a,f}} 

1058 
& P(\Fnil) 

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

1062 
\end{array} 

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

1064 
\] 

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

1533  1066 
recursive sets. Although such reasoning is sometimes useful 
103  1067 
\cite[\S4.5]{paulsonsetII}, a proper mutual induction rule should establish 
1533  1068 
separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this 
1069 
rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in 

1070 
the induction hypotheses: 

103  1071 
\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj 
1072 
(\forall z. z\in\forest(A)\imp Q(z))} 

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

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

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

1076 
\end{array} 

1077 
\right]_{a,f}} 

1078 
& Q(\Fnil) 

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

1082 
\end{array} 

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

1084 
\] 

1533  1085 
Elsewhere I describe how to define mutually recursive functions over trees and 
1086 
forests \cite[\S4.5]{paulsonsetII}. 

103  1087 

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

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

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

1091 
\begin{eqnarray*} 

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

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

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

1095 
\end{eqnarray*} 

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

1097 
forests: 

1533  1098 
\[ {\tt tree\_forest\_case}(f,c,g) \equiv 
1099 
\case(\split(f),\, \case(\lambda u.c, \split(g))) \] 

103  1100 

1101 

1102 
\subsection{A fourconstructor datatype} 

1103 
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

1104 
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

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

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

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

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

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

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

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

1112 
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

1113 
automatically supplies $\univ(A\un B)$ as its domain. The structural 
1533  1114 
induction rule has four minor premises, one per constructor, and only the last 
1115 
has an induction hypothesis. (Details are left to the reader.) 

103  1116 

1117 
The constructor definitions are 

1118 
\begin{eqnarray*} 

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

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

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

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

1123 
\end{eqnarray*} 

1124 
The case operator is 

1533  1125 
\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv 
103  1126 
\case(\begin{array}[t]{@{}l} 
1127 
\case(\lambda u.f_0,\; f_1),\, \\ 

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

1129 
\end{array} 

1533  1130 
\] 
103  1131 
This may look cryptic, but the case equations are trivial to verify. 
1132 

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

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

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

1533  1136 
injections. The difference here is small. But the \textsc{zf} examples include a 
103  1137 
60element enumeration type, where each constructor has 5 or~6 injections. 
1138 
The naive approach would require 1 to~59 injections; the definitions would be 

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

1140 
numeral systems. 

1141 

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

1533  1144 
\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \] 
103  1145 
as the theorem list \verbcase_eqns. There is one equation per constructor. 
1146 

1147 
\subsection{Proving freeness theorems} 

1148 
There are two kinds of freeness theorems: 

1149 
\begin{itemize} 

1533  1150 
\item \defn{injectiveness} theorems, such as 
103  1151 
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] 
1152 

1533  1153 
\item \defn{distinctness} theorems, such as 
103  1154 
\[ \Con_1(a) \not= \Con_2(a',b') \] 
1155 
\end{itemize} 

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

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

1533  1158 
proving desired theorems  either manually or during 
103  1159 
simplification or classical reasoning. 
1160 

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

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

1163 
equations. The theorem list contains logical equivalences such as 

1164 
\begin{eqnarray*} 

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

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

1167 
& \vdots & \\ 

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

130  1169 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ 
103  1170 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 
1171 
\end{eqnarray*} 

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

1173 

1174 
The theorem list \verbfree_SEs enables the classical 

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

355  1176 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the 
103  1177 
assumptions. 
1178 

1179 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1183 
restores the defined constants. 

1533  1184 

103  1185 

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

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

1189 

1190 
Most automated logics can only express inductive definitions by asserting 

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

1533  1192 
their shell principle were removed. With \textsc{alf} the situation is more 
355  1193 
complex; earlier versions of MartinL\"of's type theory could (using 
1194 
wellordering types) express datatype definitions, but the version 

1533  1195 
underlying \textsc{alf} requires new rules for each definition~\cite{dybjer91}. 
355  1196 
With Coq the situation is subtler still; its underlying Calculus of 
1197 
Constructions can express inductive definitions~\cite{huet88}, but cannot 

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

1199 
researchers tried hard to circumvent these problems before finally 

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

1201 

1202 
Higherorder logic can express inductive definitions through quantification 

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

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

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

1533  1206 
This technique can be used to prove the KnasterTarski theorem, which (in its 
1207 
general form) is little used in the Cambridge \textsc{hol} system. 

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

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

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

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

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

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

1214 
greater power with less effort. 

355  1215 

1533  1216 
Melham's inductive definition package~\cite{camilleri92} also uses 
1217 
quantification over predicates. But instead of formalizing the notion of 

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

1219 
syntactic form that excludes many monotone inductive definitions. 

355  1220 

1533  1221 
The earliest use of least fixedpoints is probably Robin Milner's. Brian 
1222 
Monahan extended this package considerably~\cite{monahan84}, as did I in 

1223 
unpublished work.\footnote{The datatype package described in my \textsc{lcf} 

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

1225 
axioms.} \textsc{lcf} is a firstorder logic of domain theory; the relevant 

1226 
fixedpoint theorem is not KnasterTarski but concerns fixedpoints of 

1227 
continuous functions over domains. \textsc{lcf} is too weak to express 

1228 
recursive predicates. The Isabelle package might be the first to be based on 

1229 
the KnasterTarski theorem. 

355  1230 

1231 

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

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

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

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

1238 
could introduce unsoundness. 

1239 

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

1533  1241 
(co)in\duc\tive definitions that does not assert axioms. It is efficient: 
1242 
it processes most definitions in seconds and even a 60constructor datatype 

1243 
requires only a few minutes. It is also simple: The first working version took 

1244 
under a week to code, consisting of under 1100 lines (35K bytes) of Standard 

1245 
\textsc{ml}. 

1246 

1247 
In set theory, care is needed to ensure that the inductive definition yields 

1248 
a set (rather than a proper class). This problem is inherent to set theory, 

1249 
whether or not the KnasterTarski theorem is employed. We must exhibit a 

1250 
bounding set (called a domain above). For inductive definitions, this is 

1251 
often trivial. For datatype definitions, I have had to formalize much set 

1252 
theory. To justify infinitely branching datatype definitions, I have had to 

1253 
develop a theory of cardinal arithmetic~\cite{paulsongr}, such as the theorem 

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

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

1256 
The need for such efforts is not a drawback of the fixedpoint approach, for 

1257 
the alternative is to take such definitions on faith. 

1258 

1259 
Care is also needed to ensure that the greatest fixedpoint really yields a 

1260 
coinductive definition. In set theory, standard pairs admit only wellfounded 

1261 
constructions. Aczel's antifoundation axiom~\cite{aczel88} could be used to 

1262 
get nonwellfounded objects, but it does not seem easy to mechanize. 

1263 
Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which 

1264 
can be generalized to a variant notion of function. Elsewhere I have 

1265 
proved that this simple approach works (yielding final coalgebras) for a broad 

1266 
class of definitions~\cite{paulsonfinal}. 

103  1267 

1533  1268 
Several large studies make heavy use of inductive definitions. L\"otzbeyer 
1269 
and Sandner have formalized two chapters of a semantics book~\cite{winskel93}, 

1270 
proving the equivalence between the operational and denotational semantics of 

1271 
a simple imperative language. A single theory file contains three datatype 

1272 
definitions (of arithmetic expressions, boolean expressions and commands) and 

1273 
three inductive definitions (the corresponding operational rules). Using 

1274 
different techniques, Nipkow~\cite{nipkowCR} and Rasmussen~\cite{rasmussen95} 

1275 
have both proved the ChurchRosser theorem. A datatype specifies the set of 

1276 
$\lambda$terms, while inductive definitions specify several reduction 

1277 
relations. 

103  1278 

1533  1279 
To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the 
1280 
consistency of the dynamic and static semantics for a small functional 

1281 
language. The example is due to Milner and Tofte~\cite{milnercoind}. It 

1282 
concerns an extended correspondence relation, which is defined coinductively. 

1283 
A codatatype definition specifies values and value environments in mutual 

1284 
recursion. Nonwellfounded values represent recursive functions. Value 

1285 
environments are variant functions from variables into values. This one key 

1286 
definition uses most of the package's novel features. 

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

1287 

1533  1288 
The approach is not restricted to set theory. It should be suitable for any 
1289 
logic that has some notion of set and the KnasterTarski theorem. I have 

1290 
ported the (co)inductive definition package from Isabelle/\textsc{zf} to 

1291 
Isabelle/\textsc{hol} (higherorder logic). V\"olker~\cite{voelker95} 

1292 
is investigating how to port the (co)datatype package. \textsc{hol} 

1293 
represents sets by unary predicates; defining the corresponding types may 

1294 
cause complications. 

103  1295 

1296 

1533  1297 
\begin{footnotesize} 
355  1298 
\bibliographystyle{springer} 
1197  1299 
\bibliography{stringabbrv,atp,theory,funprog,isabelle,crossref} 
1533  1300 
\end{footnotesize} 
103  1301 
%%%%%\doendnotes 
1302 

1533  1303 
\ifshort\typeout{****Omitting appendices from short version!} 
103  1304 
\else 
1305 
\newpage 

1306 
\appendix 

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

1308 
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

1309 
definitions. They may be intermixed with other declarations; in 
1533  1310 
particular, the (co)inductive sets \defn{must} be declared separately as 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1311 
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

1312 

1533  1313 
Each (co)inductive definition adds definitions to the theory and also proves 
1314 
some theorems. Each definition creates an \textsc{ml} structure, which is a 

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

1315 
substructure of the main theory structure. 
103  1316 

1533  1317 
Inductive and datatype definitions can take up considerable storage. The 
1318 
introduction rules are replicated in slightly different forms as fixedpoint 

1319 
definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's 

1320 
six definitions occupy over 600K in total. Defining the 60constructor 

1321 
datatype requires nearly 560K\@. 

1322 

103  1323 
\subsection{The result structure} 
1324 
Many of the result structure's components have been discussed 

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

1326 
\begin{description} 

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

1328 

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

1330 

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

1332 

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

1334 

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

1336 
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

1337 
names given them in the theory file. 
103  1338 

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

1340 

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

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

1343 
\end{description} 

1344 

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

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

1346 
{\tt induct} and \verbmutual_induct. (To save storage, the latter rule is 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1347 
replaced by {\tt True} if it is not significantly different from 
1471e85624a7
Note that unfold is not exported, that mutual_induct can
paulson
parents:
1197
diff
changeset

1348 
{\tt induct}.) For a coinductive definition, it 
130  1349 
contains the rule \verbcoinduct. 
1350 

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

1352 
specifying the types of all these components. 

103  1353 

1354 
\begin{figure} 

1355 
\begin{ttbox} 

1356 
sig 

1357 
val thy : theory 

1358 
val defs : thm list 

1359 
val bnd_mono : thm 

1360 
val dom_subset : thm 

1361 
val intrs : thm list 

1362 
val elim : thm 

1363 
val mk_cases : thm list > string > thm 

1364 
{\it(Inductive definitions only)} 

1365 
val induct : thm 

1366 
val mutual_induct: thm 

130  1367 
{\it(Coinductive definitions only)} 
1368 
val coinduct : thm 

103  1369 
end 
1370 
\end{ttbox} 

1371 
\hrule 

130  1372 
\caption{The result of a (co)inductive definition} \label{defresultfig} 
103  1373 
\end{figure} 
1374 

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

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

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

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

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

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

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

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

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

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

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

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

1386 
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

1387 
{\tt coinductive}. 
103  1388 

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

1389 
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

1390 
sections are optional. If present, each is specified as a string, which 
1533  1391 
must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1392 
inserted into the {\tt .thy.ML} file; if it is illformed, it will trigger 
1533  1393 
\textsc{ml} error messages. You can then inspect the file on your directory. 
103  1394 

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

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

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

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

1398 
its domain. 
103  1399 

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

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

1401 
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

1402 
the rule in the result structure. 
103  1403 

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

1404 
\item[\it monotonicity theorems] are required for each operator applied to 
1533  1405 
a recursive set in the introduction rules. There \defn{must} be a theorem 
584
5b1a0e50c79a
documentation of theory sections (co)inductive and (co)datatype
lcp
parents:
497
diff
changeset

1406 
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

1407 
in an introduction rule! 
103  1408 

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

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

1410 
appearing in the introduction rules. The (co)datatype package supplies 