author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2219  5687d7dec139 
child 2974  bb55cab416af 
permissions  rwrr 
1533  1 
\documentstyle[a4,alltt,iman,extra,proof209,12pt]{article} 
2137  2 
\newif\ifshort%''Short'' means a published version, not the documentation 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

3 
\shortfalse%%%%%\shorttrue 
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}} 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

103  63 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

103  91 

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

93 

94 
\begin{document} 

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

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

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

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

103 
implementation of mutual recursion and iterated definitions. It also 
355  104 
handles coinductive definitions: simply replace the least fixedpoint by a 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

105 
greatest fixedpoint. 
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 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

117 
semantic consistency. The package can be trusted because it proves theorems 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

118 
from definitions, instead of asserting desired properties as axioms. 
103  119 
\end{abstract} 
120 
% 

1533  121 
\bigskip 
122 
\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

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

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

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

1533  127 
\setcounter{page}{1} 
128 

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

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

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

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

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

136 
Such data structures are called \defn{datatypes} 

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

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

2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

139 
principle~\cite{bm79} and the Coq type theory~\cite{paulintlca}. 
103  140 

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

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

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

146 
provide commands for formalizing inductive definitions; these include 

2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

147 
Coq~\cite{paulintlca} and again the \textsc{hol} system~\cite{camilleri92}. 
103  148 

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

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

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

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

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

161 
to prove it. 

103  162 

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

164 
fixedpoints yield inductive definitions; greatest fixedpoints yield 

1533  165 
coinductive definitions. Most of the discussion below applies equally to 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

166 
inductive and coinductive definitions, and most of the code is shared. 
1533  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 

2137  173 
The package has been implemented in 
174 
Isabelle~\cite{paulsonmarkt,paulsonisabook} using 

1533  175 
\textsc{zf} set theory \cite{paulsonsetI,paulsonsetII}; part of it has 
176 
since been ported to Isabelle/\textsc{hol} (higherorder logic). The 

177 
recursion equations are specified as introduction rules for the mutually 

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

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

180 
successful, the package makes fixedpoint definitions and proves the 

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

182 
by making simple declarations in Isabelle theory files. 

103  183 

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

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

188 
to use than structural recursion but considerably more general. 

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

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

103  191 

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

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

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

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

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

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

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

203 

204 
\section{Fixedpoint operators} 

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

206 
follows: 

207 
\begin{eqnarray*} 

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

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

210 
\end{eqnarray*} 

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

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

215 
\begin{eqnarray*} 

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

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

218 
\end{eqnarray*} 

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

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

223 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

228 
of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

229 
infinitelybranching (co)datatype definitions; see~\S\ref{univsec}. Bounding 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

230 
sets are also called \defn{domains}. 
103  231 

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

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

103  236 

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

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

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

242 
under an injection. Reasons for this are discussed 

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

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

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

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

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

2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

249 
Coq~\cite{paulintlca}. For instance, we cannot define the lists of 
103  250 
$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$ 
355  251 
varies. Section~\ref{listnsec} describes how to express this set using the 
130  252 
inductive definition package. 
103  253 

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

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

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

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

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

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

103  262 

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

264 
sets, satisfying the rule 

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

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

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

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

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

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

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

103  276 

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

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

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

282 

283 
\subsection{The fixedpoint definitions} 

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

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

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

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

290 
\] 

291 

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

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

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

299 
\end{array} 

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

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

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

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

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

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

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

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

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

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

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

318 
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

319 
$\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

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

321 

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

322 
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

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

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

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

332 

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

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

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

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

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

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

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

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

350 

351 
\subsection{Proving the introduction rules} 

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

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

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

359 
attempting to prove the result. 

360 

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

362 
in the rules, the package must prove 

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

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

365 
\] 

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

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

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

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

372 
definition through! 

103  373 

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

103  376 

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

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

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

382 
is written 

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

385 
\] 

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

103  389 

130  390 
\section{Induction and coinduction rules} 
1742  391 
Here we must consider inductive and coinductive definitions separately. For 
392 
an inductive definition, the package returns an induction rule derived 

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

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

395 
basic coinduction rule. 

103  396 

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

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

401 

1742  402 
The induction rule for an inductively defined set~$R$ has the form described 
403 
below. For the time being, assume that $R$'s domain is not a Cartesian 

404 
product; inductively defined relations are treated slightly differently. 

405 

103  406 
The major premise is $x\in R$. There is a minor premise for each 
407 
introduction rule: 

408 
\begin{itemize} 

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

410 
is~$P(t)$. 

411 

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

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

103  415 

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

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

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

419 
then the minor premise discharges the single assumption 

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

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

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

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

424 
\end{itemize} 

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

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

429 
\] 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

430 
Stronger induction rules often suggest themselves. We can derive a rule for 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

431 
$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

432 
The package provides rules for mutual induction and inductive relations. The 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

433 
Isabelle/\textsc{zf} theory also supports wellfounded induction and recursion 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

434 
over datatypes, by reasoning about the \defn{rank} of a 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

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

437 

438 
\subsection{Modified induction rules} 

103  439 

1742  440 
If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$ 
441 
(however nested), then the corresponding predicate $P_i$ takes $m$ arguments. 

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

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

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

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

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

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

448 
split} appears in the rule. 

449 

103  450 
The mutual induction rule is called {\tt 
1742  451 
mutual\_induct}. It differs from the basic rule in two respects: 
103  452 
\begin{itemize} 
453 
\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$, 

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

455 

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

457 
refers to all the recursive sets: 

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

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

460 
\] 

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

103  463 
\end{itemize} 
1742  464 
% 
465 
If the domain of some $R_i$ is a Cartesian product, then the mutual induction 

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

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

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

103  469 

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

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

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

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

478 
\] 

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

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

103  483 

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

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

490 
z=\LNil\disj 

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

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

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

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

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

130  499 

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

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

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

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

507 

103  508 

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

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

103  513 

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

515 
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

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

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

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

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

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

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

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

525 
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

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

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

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

530 
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

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

533 
introduction rules. For typechecking, we supply two introduction 
355  534 
rules: 
103  535 
\[ \emptyset\sbs A \qquad 
536 
\infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} 

537 
\] 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

538 
A further introduction rule and an elimination rule express both 
103  539 
directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Typechecking 
355  540 
involves mostly introduction rules. 
541 

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

542 
Like all Isabelle theory files, this one yields a structure containing the 
1533  543 
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

544 
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

545 
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

546 
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

547 
rule is {\tt Fin.induct}. 
355  548 

103  549 

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

179  551 
This has become a standard example of an inductive definition. Following 
2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

552 
PaulinMohring~\cite{paulintlca}, we could attempt to define a new datatype 
179  553 
$\listn(A,n)$, for lists of length~$n$, as an $n$indexed family of sets. 
554 
But her introduction rules 

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

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

559 
are not acceptable to the inductive definition package: 

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

561 

597  562 
The Isabelle version of this example suggests a general treatment of 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

563 
varying parameters. It uses the existing datatype definition of 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

564 
$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

565 
parameter~$n$ into the inductive set itself. It defines $\listn(A)$ as a 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

566 
relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$ 
355  567 
and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the 
1533  568 
converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction 
355  569 
rules are 
103  570 
\[ \pair{0,\Nil}\in\listn(A) \qquad 
571 
\infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} 

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

573 
\] 

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

574 
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

575 
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

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

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

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

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

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

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

582 
intrs 
1533  583 
NilI "<0,Nil>: listn(A)" 
584 
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

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

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

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

588 
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

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

103  592 

593 
The package returns introduction, elimination and induction rules for 

1533  594 
$\listn$. The basic induction rule, {\tt listn.induct}, is 
1742  595 
\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) & 
596 
\infer*{P(\succ(n),\Cons(a,l))} 

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

1742  599 
This rule lets the induction formula to be a 
600 
binary property of pairs, $P(n,l)$. 

103  601 
It is now a simple matter to prove theorems about $\listn(A)$, such as 
602 
\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \] 

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

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

607 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

608 
A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

609 
It is subject to list operators such as append (concatenation). For example, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

610 
a trivial induction on $\pair{m,l}\in\listn(A)$ yields 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

611 
\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)} 
103  612 
{\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
613 
\] 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

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

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

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

620 
\infer*{Q} 

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

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

623 
a\in A \\ 

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

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

626 
\] 

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

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

632 
Here is a sample session: 

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

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

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

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

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

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

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

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

1533  646 
a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n) 
103  647 
\end{array} \right]_{n}}} 
648 
\] 

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

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

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

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

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

658 
\] 

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

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

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

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

664 
residuals~\cite{rasmussen95}. 

665 

103  666 

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

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

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

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

674 

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

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

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

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

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

103  683 

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

103  688 
\] 
1742  689 
A pair of lazy lists are \defn{equivalent} if they belong to some 
690 
bisimulation. Equivalence can be coinductively defined as the greatest 

691 
fixedpoint for the introduction rules 

130  692 
\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad 
693 
\infer[()]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} 

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

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

696 
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

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

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

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

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

702 
intrs 
1533  703 
LNil "<LNil,LNil> : lleq(A)" 
704 
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

705 
type_intrs "llist.intrs" 
103  706 
\end{ttbox} 
130  707 
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

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

709 
declaration is discussed below (\S\ref{listssec}). 
103  710 

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

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

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

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

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

720 
\end{array} 

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

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

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

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

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

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

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

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

736 
introduction rule of the form 

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

2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

738 
PaulinMohring treats this example in Coq~\cite{paulintlca}, but it causes 
597  739 
difficulties for other systems. Its premise is not acceptable to the 
1533  740 
inductive definition package of the Cambridge \textsc{hol} 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

741 
system~\cite{camilleri92}. It is also unacceptable to the Isabelle package 
597  742 
(recall \S\ref{introsec}), but fortunately can be transformed into the 
743 
acceptable form $t\in M(R)$. 

103  744 

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

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

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

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

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

750 

1533  751 
The definition below follows this approach. Here $r$ is~$\prec$ and 
130  752 
$\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

753 
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

754 
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

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

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

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

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

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

761 
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

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

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

766 
$\acc(\prec)$. 

767 

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

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

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

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

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

776 
\end{array} 

777 
\right]_a}} 

103  778 
\] 
779 
The strange induction hypothesis is equivalent to 

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

781 
Therefore the rule expresses wellfounded induction on the accessible part 

782 
of~$\prec$. 

783 

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

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

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

787 
equivalently as 

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

791 
where $M=\lst$. 

792 

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

794 
The primitive recursive functions are traditionally defined inductively, as 

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

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

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

798 
the notion of composition, is less easily circumvented. 

799 

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

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

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

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

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

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

103  815 

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

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

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

821 
\end{eqnarray*} 

822 
\end{itemize} 

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

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

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

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

827 
tuplevalued functions. This modified the inductive definition such that 

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

829 

830 
\begin{figure} 

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

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

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

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

835 
SC :: i 
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 
defs 
1533  838 
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

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

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

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

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

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

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

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

846 
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

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

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

849 
con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" 
1533  850 
type_intrs "nat_typechecks @ list.intrs @ 
851 
[lam_type, list_case_type, drop_type, map_type, 

852 
apply_type, rec_type]" 

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

853 
end 
355  854 
\end{ttbox} 
103  855 
\hrule 
856 
\caption{Inductive definition of the primitive recursive functions} 

857 
\label{primrecfig} 

858 
\end{figure} 

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

1533  860 

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

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

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

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

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

866 
$\COMP$: 

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

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

870 
an unusual induction hypothesis: 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

872 
{[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

873 
\] 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

874 
The hypothesis states that $\fs$ is a list of primitive recursive functions, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

875 
each satisfying the induction formula. Proving the $\COMP$ case typically 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

876 
requires structural induction on lists, yielding two subcases: either 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

877 
$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

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

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

880 
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

881 
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

882 
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

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

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

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

891 

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

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

103  896 
involving any pair of constructors. 
897 

898 

130  899 
\subsection{Constructors and their domain}\label{univsec} 
1533  900 
A (co)inductive definition selects a subset of an existing set; a (co)datatype 
1742  901 
definition creates a new set. The package reduces the latter to the former. 
902 
Isabelle/\textsc{zf} supplies sets having strong closure properties to serve 

1533  903 
as domains for (co)inductive definitions. 
103  904 

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

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

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

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

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

911 

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

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

918 

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

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

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

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

925 

926 
The standard pairs and injections can only yield wellfounded 

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

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

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

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

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

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

938 
$\quniv(A_1\un\cdots\un A_k)$. Details are published 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

939 
elsewhere~\cite{paulsonfinal}. 
103  940 

941 
\subsection{The case analysis operator} 

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

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

946 
for products and sums. 

103  947 

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

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

950 
\begin{eqnarray*} 

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

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

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

954 
\end{eqnarray*} 

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

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

957 
constructor: 

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

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

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

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

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

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

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

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

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

972 

355  973 
\medskip 
103  974 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

976 
examine some examples. Further details are available 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

977 
elsewhere~\cite{paulsonsetII}. 
103  978 

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

979 

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

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

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

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

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

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

990 
codatatype "llist(A)" = LNil  LCons ("a: A", "l: llist(A)") 
103  991 
\end{ttbox} 
992 

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

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

995 
lists over a given set~$A$. Each is automatically given the appropriate 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

996 
domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$. The default 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

997 
can be overridden. 
103  998 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

999 
\ifshort 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1000 
Now $\lst(A)$ is a datatype and enjoys the usual induction rule. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1001 
\else 
130  1002 
Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt 
1533  1003 
list.induct}: 
103  1004 
\[ \infer{P(x)}{x\in\lst(A) & P(\Nil) 
1005 
& \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} } 

1006 
\] 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1008 
Isabelle/\textsc{zf} defines the rank of a set and proves that the standard 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1009 
pairs and injections have greater rank than their components. An immediate 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1010 
consequence, which justifies structural recursion on lists 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1011 
\cite[\S4.3]{paulsonsetII}, is 
103  1012 
\[ \rank(l) < \rank(\Cons(a,l)). \] 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1013 
\par 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1014 
\fi 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1015 
But $\llist(A)$ is a codatatype and has no induction rule. Instead it has 
130  1016 
the coinduction rule shown in \S\ref{coindsec}. Since variant pairs and 
103  1017 
injections are monotonic and need not have greater rank than their 
1018 
components, fixedpoint operators can create cyclic constructions. For 

1019 
example, the definition 

1533  1020 
\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \] 
103  1021 
yields $\lconst(a) = \LCons(a,\lconst(a))$. 
1022 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1023 
\ifshort 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1024 
\typeout{****SHORT VERSION} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1025 
\typeout{****Omitting discussion of constructors!} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1026 
\else 
103  1027 
\medskip 
1028 
It may be instructive to examine the definitions of the constructors and 

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

1030 
The list constructors are defined as follows: 

1031 
\begin{eqnarray*} 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1032 
\Nil & \equiv & \Inl(\emptyset) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1033 
\Cons(a,l) & \equiv & \Inr(\pair{a,l}) 
103  1034 
\end{eqnarray*} 
1035 
The operator $\lstcase$ performs case analysis on these two alternatives: 

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

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

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

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

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

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

130  1046 
& = & h(x,y) 
103  1047 
\end{eqnarray*} 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1048 
\fi 
103  1049 

1050 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1051 
\ifshort 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1052 
\typeout{****Omitting mutual recursion example!} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1053 
\else 
103  1054 
\subsection{Example: mutual recursion} 
130  1055 
In mutually recursive trees and forests~\cite[\S4.5]{paulsonsetII}, trees 
103  1056 
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

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

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

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

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

1061 
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

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

1065 

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

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

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

1071 
\end{array} 

1072 
\right]_{a,f}} 

1073 
& P(\Fnil) 

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

1077 
\end{array} 

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

1079 
\] 

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

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

1085 
the induction hypotheses: 

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

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

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

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

1091 
\end{array} 

1092 
\right]_{a,f}} 

1093 
& Q(\Fnil) 

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

1097 
\end{array} 

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

1099 
\] 

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

103  1102 

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

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

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

1106 
\begin{eqnarray*} 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1107 
\Tcons(a,l) & \equiv & \Inl(\pair{a,l}) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1108 
\Fnil & \equiv & \Inr(\Inl(\emptyset)) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1109 
\Fcons(a,l) & \equiv & \Inr(\Inr(\pair{a,l})) 
103  1110 
\end{eqnarray*} 
1111 
There is only one case operator; it works on the union of the trees and 

1112 
forests: 

1533  1113 
\[ {\tt tree\_forest\_case}(f,c,g) \equiv 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1114 
\case(\split(f),\, \case(\lambda u.c, \split(g))) 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1115 
\] 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1116 
\fi 
103  1117 

1118 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1119 
\subsection{Example: a fourconstructor datatype} 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1120 
A bigger datatype will illustrate some efficiency 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1121 
refinements. It has four constructors $\Con_0$, \ldots, $\Con_3$, with the 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

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

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

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

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

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

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

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

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

1130 
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

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

103  1134 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1135 
The constructors are defined by the equations 
103  1136 
\begin{eqnarray*} 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1137 
\Con_0 & \equiv & \Inl(\Inl(\emptyset)) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1138 
\Con_1(a) & \equiv & \Inl(\Inr(a)) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1139 
\Con_2(a,b) & \equiv & \Inr(\Inl(\pair{a,b})) \\ 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1140 
\Con_3(a,b,c) & \equiv & \Inr(\Inr(\pair{a,b,c})). 
103  1141 
\end{eqnarray*} 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1142 
The case analysis operator is 
1533  1143 
\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv 
103  1144 
\case(\begin{array}[t]{@{}l} 
1145 
\case(\lambda u.f_0,\; f_1),\, \\ 

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

1147 
\end{array} 

1533  1148 
\] 
103  1149 
This may look cryptic, but the case equations are trivial to verify. 
1150 

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1152 
approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$; 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1153 
instead, each constructor has two injections. The difference here is small. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1154 
But the \textsc{zf} examples include a 60element enumeration type, where each 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1155 
constructor has 5 or~6 injections. The naive approach would require 1 to~59 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1156 
injections; the definitions would be quadratic in size. It is like the 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1157 
advantage of binary notation over unary. 
103  1158 

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

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

1164 
\subsection{Proving freeness theorems} 

1165 
There are two kinds of freeness theorems: 

1166 
\begin{itemize} 

1533  1167 
\item \defn{injectiveness} theorems, such as 
103  1168 
\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \] 
1169 

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

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

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

1533  1175 
proving desired theorems  either manually or during 
103  1176 
simplification or classical reasoning. 
1177 

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

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

1180 
equations. The theorem list contains logical equivalences such as 

1181 
\begin{eqnarray*} 

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

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

1184 
& \vdots & \\ 

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

130  1186 
\Inl(a)=\Inr(b) & \bimp & {\tt False} \\ 
103  1187 
\pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b' 
1188 
\end{eqnarray*} 

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

1190 

1191 
The theorem list \verbfree_SEs enables the classical 

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

355  1193 
to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the 
103  1194 
assumptions. 
1195 

1196 
Such incremental unfolding combines freeness reasoning with other proof 

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

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

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

1200 
restores the defined constants. 

1533  1201 

103  1202 

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

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

1206 

1207 
Most automated logics can only express inductive definitions by asserting 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1208 
axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if their 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1209 
shell principle were removed. With \textsc{alf} the situation is more 
355  1210 
complex; earlier versions of MartinL\"of's type theory could (using 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1211 
wellordering types) express datatype definitions, but the version underlying 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1212 
\textsc{alf} requires new rules for each definition~\cite{dybjer91}. With Coq 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1213 
the situation is subtler still; its underlying Calculus of Constructions can 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1214 
express inductive definitions~\cite{huet88}, but cannot quite handle datatype 
2219
5687d7dec139
Minor textual improvements; updating of a reference
paulson
parents:
2137
diff
changeset

1215 
definitions~\cite{paulintlca}. It seems that researchers tried hard to 
1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1216 
circumvent these problems before finally extending the Calculus with rule 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1217 
schemes for strictly positive operators. Recently Gim{\'e}nez has extended 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1218 
the Calculus of Constructions with inductive and coinductive 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1219 
types~\cite{gimenezcodifying}, with mechanized support in Coq. 
355  1220 

1221 
Higherorder logic can express inductive definitions through quantification 

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

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

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

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

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

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

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

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

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

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

1233 
greater power with less effort. 

355  1234 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1235 
Elsa Gunter~\cite{guntertrees} reports an ongoing project to generalize the 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1236 
Cambridge \textsc{hol} system with mutual recursion and infinitelybranching 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1237 
trees. She retains many features of Melham's approach. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1238 

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

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

1242 
syntactic form that excludes many monotone inductive definitions. 

355  1243 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1244 
\textsc{pvs}~\cite{pvslanguage} is another proof assistant based on 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1245 
higherorder logic. It supports both inductive definitions and datatypes, 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1246 
apparently by asserting axioms. Datatypes may not be iterated in general, but 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1247 
may use recursion over the builtin $\lst$ type. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1248 

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

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

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

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

1254 
fixedpoint theorem is not KnasterTarski but concerns fixedpoints of 

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

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

1257 
the KnasterTarski theorem. 

355  1258 

1259 

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

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

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

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

1266 
could introduce unsoundness. 

1267 

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

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

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

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

1273 
\textsc{ml}. 

1274 

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

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

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

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

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

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1280 
theory. To justify infinitelybranching datatype definitions, I have had to 
1533  1281 
develop a theory of cardinal arithmetic~\cite{paulsongr}, such as the theorem 
1282 
that if $\kappa$ is an infinite cardinal and $X(\alpha) \le \kappa$ for all 

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

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

1285 
the alternative is to take such definitions on faith. 

1286 

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

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

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

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

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

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

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

1294 
class of definitions~\cite{paulsonfinal}. 

103  1295 

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

1298 
proving the equivalence between the operational and denotational semantics of 

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

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

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

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

2137  1303 
have both proved the ChurchRosser theorem; inductive definitions specify 
1304 
several reduction relations on $\lambda$terms. Recently, I have applied 

1305 
inductive definitions to the analysis of cryptographic 

1306 
protocols~\cite{paulsonmarkt}. 

103  1307 

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

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

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

1312 
A codatatype definition specifies values and value environments in mutual 

1313 
recursion. Nonwellfounded values represent recursive functions. Value 

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

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

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

1316 

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

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

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

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

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

1323 
cause complications. 

103  1324 

1325 

1533  1326 
\begin{footnotesize} 
355  1327 
\bibliographystyle{springer} 
1197  1328 
\bibliography{stringabbrv,atp,theory,funprog,isabelle,crossref} 
1533  1329 
\end{footnotesize} 
103  1330 
%%%%%\doendnotes 
1331 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1332 
\ifshort\typeout{****Omitting appendices} 
103  1333 
\else 
1334 
\newpage 

1335 
\appendix 

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

1337 
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

1338 
definitions. They may be intermixed with other declarations; in 
1533  1339 
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

1340 
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

1341 

1871
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1342 
The syntax is rather complicated. Please consult the examples above and the 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1343 
theory files on the \textsc{zf} source directory. 
82246f607d7f
Edited in response to referees comments; new references
paulson
parents:
1742
diff
changeset

1344 

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

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

1347 
substructure of the main theory structure. 
103  1348 

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

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

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

1353 
datatype requires nearly 560K\@. 

1354 

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

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

1358 
\begin{description} 

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

1360 

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

1362 

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

1364 

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

1366 

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

1368 
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

1369 
names given them in the theory file. 
103  1370 

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

1372 

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

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

1375 
\end{description} 

1376 

1742  1377 
For an inductive definition, the result structure contains two induction 
1378 
rules, {\tt induct} and \verbmutual_induct. (To save storage, the latter 

1379 
rule is just {\tt True} unless more than one set is being defined.) For a 

1380 
coinductive definition, it contains the rule \verbcoinduct. 

130  1381 

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

1383 
specifying the types of all these components. 

103  1384 

1385 
\begin{figure} 

1386 
\begin{ttbox} 

1387 
sig 

1388 
val thy : theory 

1389 
val defs : thm list 

1390 
val bnd_mono : thm 

1391 