1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Inductive/ind-defs.tex Mon May 12 17:13:12 1997 +0200
1.3 @@ -0,0 +1,1600 @@
1.4 +\documentclass[12pt]{article}
1.5 +\usepackage{a4,latexsym,proof}
1.6 +
1.7 +\makeatletter
1.8 +\input{../rail.sty}
1.9 +\input{../iman.sty}
1.10 +\input{../extra.sty}
1.11 +\makeatother
1.12 +
1.13 +\newif\ifshort%''Short'' means a published version, not the documentation
1.14 +\shortfalse%%%%%\shorttrue
1.15 +
1.16 +\title{A Fixedpoint Approach to\\
1.17 + (Co)Inductive and (Co)Datatype Definitions%
1.18 + \thanks{J. Grundy and S. Thompson made detailed comments. Mads Tofte and
1.19 + the referees were also helpful. The research was funded by the SERC
1.20 + grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}
1.21 +
1.22 +\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
1.23 + Computer Laboratory, University of Cambridge, England}
1.24 +\date{\today}
1.25 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
1.26 +
1.27 +\newcommand\sbs{\subseteq}
1.28 +\let\To=\Rightarrow
1.29 +
1.30 +%\newcommand\emph[1]{{\em#1\/}}
1.31 +\newcommand\defn[1]{{\bf#1}}
1.32 +%\newcommand\textsc[1]{{\sc#1}}
1.33 +%\newcommand\texttt[1]{{\tt#1}}
1.34 +
1.35 +\newcommand\pow{{\cal P}}
1.36 +%%%\let\pow=\wp
1.37 +\newcommand\RepFun{\hbox{\tt RepFun}}
1.38 +\newcommand\cons{\hbox{\tt cons}}
1.39 +\def\succ{\hbox{\tt succ}}
1.40 +\newcommand\split{\hbox{\tt split}}
1.41 +\newcommand\fst{\hbox{\tt fst}}
1.42 +\newcommand\snd{\hbox{\tt snd}}
1.43 +\newcommand\converse{\hbox{\tt converse}}
1.44 +\newcommand\domain{\hbox{\tt domain}}
1.45 +\newcommand\range{\hbox{\tt range}}
1.46 +\newcommand\field{\hbox{\tt field}}
1.47 +\newcommand\lfp{\hbox{\tt lfp}}
1.48 +\newcommand\gfp{\hbox{\tt gfp}}
1.49 +\newcommand\id{\hbox{\tt id}}
1.50 +\newcommand\trans{\hbox{\tt trans}}
1.51 +\newcommand\wf{\hbox{\tt wf}}
1.52 +\newcommand\nat{\hbox{\tt nat}}
1.53 +\newcommand\rank{\hbox{\tt rank}}
1.54 +\newcommand\univ{\hbox{\tt univ}}
1.55 +\newcommand\Vrec{\hbox{\tt Vrec}}
1.56 +\newcommand\Inl{\hbox{\tt Inl}}
1.57 +\newcommand\Inr{\hbox{\tt Inr}}
1.58 +\newcommand\case{\hbox{\tt case}}
1.59 +\newcommand\lst{\hbox{\tt list}}
1.60 +\newcommand\Nil{\hbox{\tt Nil}}
1.61 +\newcommand\Cons{\hbox{\tt Cons}}
1.62 +\newcommand\lstcase{\hbox{\tt list\_case}}
1.63 +\newcommand\lstrec{\hbox{\tt list\_rec}}
1.64 +\newcommand\length{\hbox{\tt length}}
1.65 +\newcommand\listn{\hbox{\tt listn}}
1.66 +\newcommand\acc{\hbox{\tt acc}}
1.67 +\newcommand\primrec{\hbox{\tt primrec}}
1.68 +\newcommand\SC{\hbox{\tt SC}}
1.69 +\newcommand\CONST{\hbox{\tt CONST}}
1.70 +\newcommand\PROJ{\hbox{\tt PROJ}}
1.71 +\newcommand\COMP{\hbox{\tt COMP}}
1.72 +\newcommand\PREC{\hbox{\tt PREC}}
1.73 +
1.74 +\newcommand\quniv{\hbox{\tt quniv}}
1.75 +\newcommand\llist{\hbox{\tt llist}}
1.76 +\newcommand\LNil{\hbox{\tt LNil}}
1.77 +\newcommand\LCons{\hbox{\tt LCons}}
1.78 +\newcommand\lconst{\hbox{\tt lconst}}
1.79 +\newcommand\lleq{\hbox{\tt lleq}}
1.80 +\newcommand\map{\hbox{\tt map}}
1.81 +\newcommand\term{\hbox{\tt term}}
1.82 +\newcommand\Apply{\hbox{\tt Apply}}
1.83 +\newcommand\termcase{\hbox{\tt term\_case}}
1.84 +\newcommand\rev{\hbox{\tt rev}}
1.85 +\newcommand\reflect{\hbox{\tt reflect}}
1.86 +\newcommand\tree{\hbox{\tt tree}}
1.87 +\newcommand\forest{\hbox{\tt forest}}
1.88 +\newcommand\Part{\hbox{\tt Part}}
1.89 +\newcommand\TF{\hbox{\tt tree\_forest}}
1.90 +\newcommand\Tcons{\hbox{\tt Tcons}}
1.91 +\newcommand\Fcons{\hbox{\tt Fcons}}
1.92 +\newcommand\Fnil{\hbox{\tt Fnil}}
1.93 +\newcommand\TFcase{\hbox{\tt TF\_case}}
1.94 +\newcommand\Fin{\hbox{\tt Fin}}
1.95 +\newcommand\QInl{\hbox{\tt QInl}}
1.96 +\newcommand\QInr{\hbox{\tt QInr}}
1.97 +\newcommand\qsplit{\hbox{\tt qsplit}}
1.98 +\newcommand\qcase{\hbox{\tt qcase}}
1.99 +\newcommand\Con{\hbox{\tt Con}}
1.100 +\newcommand\data{\hbox{\tt data}}
1.101 +
1.102 +\binperiod %%%treat . like a binary operator
1.103 +
1.104 +\begin{document}
1.105 +\pagestyle{empty}
1.106 +\begin{titlepage}
1.107 +\maketitle
1.108 +\begin{abstract}
1.109 + This paper presents a fixedpoint approach to inductive definitions.
1.110 + Instead of using a syntactic test such as ``strictly positive,'' the
1.111 + approach lets definitions involve any operators that have been proved
1.112 + monotone. It is conceptually simple, which has allowed the easy
1.113 + implementation of mutual recursion and iterated definitions. It also
1.114 + handles coinductive definitions: simply replace the least fixedpoint by a
1.115 + greatest fixedpoint.
1.116 +
1.117 + The method has been implemented in two of Isabelle's logics, \textsc{zf} set
1.118 + theory and higher-order logic. It should be applicable to any logic in
1.119 + which the Knaster-Tarski theorem can be proved. Examples include lists of
1.120 + $n$ elements, the accessible part of a relation and the set of primitive
1.121 + recursive functions. One example of a coinductive definition is
1.122 + bisimulations for lazy lists. Recursive datatypes are examined in detail,
1.123 + as well as one example of a \defn{codatatype}: lazy lists.
1.124 +
1.125 + The Isabelle package has been applied in several large case studies,
1.126 + including two proofs of the Church-Rosser theorem and a coinductive proof of
1.127 + semantic consistency. The package can be trusted because it proves theorems
1.128 + from definitions, instead of asserting desired properties as axioms.
1.129 +\end{abstract}
1.130 +%
1.131 +\bigskip
1.132 +\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
1.133 +\thispagestyle{empty}
1.134 +\end{titlepage}
1.135 +\tableofcontents\cleardoublepage\pagestyle{plain}
1.136 +
1.137 +\setcounter{page}{1}
1.138 +
1.139 +\section{Introduction}
1.140 +Several theorem provers provide commands for formalizing recursive data
1.141 +structures, like lists and trees. Robin Milner implemented one of the first
1.142 +of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}. Given a description
1.143 +of the desired data structure, Milner's package formulated appropriate
1.144 +definitions and proved the characteristic theorems. Similar is Melham's
1.145 +recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}.
1.146 +Such data structures are called \defn{datatypes}
1.147 +below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
1.148 +Some logics take datatypes as primitive; consider Boyer and Moore's shell
1.149 +principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
1.150 +
1.151 +A datatype is but one example of an \defn{inductive definition}. Such a
1.152 +definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}
1.153 +given rules: applying a rule to elements of~$R$ yields a result within~$R$.
1.154 +Inductive definitions have many applications. The collection of theorems in a
1.155 +logic is inductively defined. A structural operational
1.156 +semantics~\cite{hennessy90} is an inductive definition of a reduction or
1.157 +evaluation relation on programs. A few theorem provers provide commands for
1.158 +formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and
1.159 +again the \textsc{hol} system~\cite{camilleri92}.
1.160 +
1.161 +The dual notion is that of a \defn{coinductive definition}. Such a definition
1.162 +specifies the greatest set~$R$ \defn{consistent with} given rules: every
1.163 +element of~$R$ can be seen as arising by applying a rule to elements of~$R$.
1.164 +Important examples include using bisimulation relations to formalize
1.165 +equivalence of processes~\cite{milner89} or lazy functional
1.166 +programs~\cite{abramsky90}. Other examples include lazy lists and other
1.167 +infinite data structures; these are called \defn{codatatypes} below.
1.168 +
1.169 +Not all inductive definitions are meaningful. \defn{Monotone} inductive
1.170 +definitions are a large, well-behaved class. Monotonicity can be enforced
1.171 +by syntactic conditions such as ``strictly positive,'' but this could lead to
1.172 +monotone definitions being rejected on the grounds of their syntactic form.
1.173 +More flexible is to formalize monotonicity within the logic and allow users
1.174 +to prove it.
1.175 +
1.176 +This paper describes a package based on a fixedpoint approach. Least
1.177 +fixedpoints yield inductive definitions; greatest fixedpoints yield
1.178 +coinductive definitions. Most of the discussion below applies equally to
1.179 +inductive and coinductive definitions, and most of the code is shared.
1.180 +
1.181 +The package supports mutual recursion and infinitely-branching datatypes and
1.182 +codatatypes. It allows use of any operators that have been proved monotone,
1.183 +thus accepting all provably monotone inductive definitions, including
1.184 +iterated definitions.
1.185 +
1.186 +The package has been implemented in
1.187 +Isabelle~\cite{paulson-markt,paulson-isa-book} using
1.188 +\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
1.189 +since been ported to Isabelle/\textsc{hol} (higher-order logic). The
1.190 +recursion equations are specified as introduction rules for the mutually
1.191 +recursive sets. The package transforms these rules into a mapping over sets,
1.192 +and attempts to prove that the mapping is monotonic and well-typed. If
1.193 +successful, the package makes fixedpoint definitions and proves the
1.194 +introduction, elimination and (co)induction rules. Users invoke the package
1.195 +by making simple declarations in Isabelle theory files.
1.196 +
1.197 +Most datatype packages equip the new datatype with some means of expressing
1.198 +recursive functions. This is the main omission from my package. Its
1.199 +fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf}
1.200 +theory provides well-founded recursion~\cite{paulson-set-II}, which is harder
1.201 +to use than structural recursion but considerably more general.
1.202 +Slind~\cite{slind-tfl} has written a package to automate the definition of
1.203 +well-founded recursive functions in Isabelle/\textsc{hol}.
1.204 +
1.205 +\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint
1.206 +operators. Section~3 discusses the form of introduction rules, mutual
1.207 +recursion and other points common to inductive and coinductive definitions.
1.208 +Section~4 discusses induction and coinduction rules separately. Section~5
1.209 +presents several examples, including a coinductive definition. Section~6
1.210 +describes datatype definitions. Section~7 presents related work.
1.211 +Section~8 draws brief conclusions. \ifshort\else The appendices are simple
1.212 +user's manuals for this Isabelle package.\fi
1.213 +
1.214 +Most of the definitions and theorems shown below have been generated by the
1.215 +package. I have renamed some variables to improve readability.
1.216 +
1.217 +\section{Fixedpoint operators}
1.218 +In set theory, the least and greatest fixedpoint operators are defined as
1.219 +follows:
1.220 +\begin{eqnarray*}
1.221 + \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
1.222 + \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\}
1.223 +\end{eqnarray*}
1.224 +Let $D$ be a set. Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and
1.225 +\defn{monotone below~$D$} if
1.226 +$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is
1.227 +bounded by~$D$ and monotone then both operators yield fixedpoints:
1.228 +\begin{eqnarray*}
1.229 + \lfp(D,h) & = & h(\lfp(D,h)) \\
1.230 + \gfp(D,h) & = & h(\gfp(D,h))
1.231 +\end{eqnarray*}
1.232 +These equations are instances of the Knaster-Tarski theorem, which states
1.233 +that every monotonic function over a complete lattice has a
1.234 +fixedpoint~\cite{davey&priestley}. It is obvious from their definitions
1.235 +that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
1.236 +
1.237 +This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to
1.238 +prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must
1.239 +also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when
1.240 +a set of theorems is (co)inductively defined over some previously existing set
1.241 +of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for
1.242 +infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}. Bounding
1.243 +sets are also called \defn{domains}.
1.244 +
1.245 +The powerset operator is monotone, but by Cantor's theorem there is no
1.246 +set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because
1.247 +there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates
1.248 +that~$\pow$ is still useful in inductive definitions.
1.249 +
1.250 +\section{Elements of an inductive or coinductive definition}\label{basic-sec}
1.251 +Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
1.252 +mutual recursion. They will be constructed from domains $D_1$,
1.253 +\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but
1.254 +$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$
1.255 +under an injection. Reasons for this are discussed
1.256 +elsewhere~\cite[\S4.5]{paulson-set-II}.
1.257 +
1.258 +The definition may involve arbitrary parameters $\vec{p}=p_1$,
1.259 +\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The
1.260 +parameters must be identical every time they occur within a definition. This
1.261 +would appear to be a serious restriction compared with other systems such as
1.262 +Coq~\cite{paulin-tlca}. For instance, we cannot define the lists of
1.263 +$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
1.264 +varies. Section~\ref{listn-sec} describes how to express this set using the
1.265 +inductive definition package.
1.266 +
1.267 +To avoid clutter below, the recursive sets are shown as simply $R_i$
1.268 +instead of~$R_i(\vec{p})$.
1.269 +
1.270 +\subsection{The form of the introduction rules}\label{intro-sec}
1.271 +The body of the definition consists of the desired introduction rules. The
1.272 +conclusion of each rule must have the form $t\in R_i$, where $t$ is any term.
1.273 +Premises typically have the same form, but they can have the more general form
1.274 +$t\in M(R_i)$ or express arbitrary side-conditions.
1.275 +
1.276 +The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
1.277 +sets, satisfying the rule
1.278 +\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
1.279 +The user must supply the package with monotonicity rules for all such premises.
1.280 +
1.281 +The ability to introduce new monotone operators makes the approach
1.282 +flexible. A suitable choice of~$M$ and~$t$ can express a lot. The
1.283 +powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$
1.284 +expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The \emph{list of}
1.285 +operator is monotone, as is easily proved by induction. The premise
1.286 +$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual
1.287 +recursion; see \S\ref{primrec-sec} and also my earlier
1.288 +paper~\cite[\S4.4]{paulson-set-II}.
1.289 +
1.290 +Introduction rules may also contain \defn{side-conditions}. These are
1.291 +premises consisting of arbitrary formul{\ae} not mentioning the recursive
1.292 +sets. Side-conditions typically involve type-checking. One example is the
1.293 +premise $a\in A$ in the following rule from the definition of lists:
1.294 +\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
1.295 +
1.296 +\subsection{The fixedpoint definitions}
1.297 +The package translates the list of desired introduction rules into a fixedpoint
1.298 +definition. Consider, as a running example, the finite powerset operator
1.299 +$\Fin(A)$: the set of all finite subsets of~$A$. It can be
1.300 +defined as the least set closed under the rules
1.301 +\[ \emptyset\in\Fin(A) \qquad
1.302 + \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)}
1.303 +\]
1.304 +
1.305 +The domain in a (co)inductive definition must be some existing set closed
1.306 +under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
1.307 +subsets of~$A$. The package generates the definition
1.308 +\[ \Fin(A) \equiv \lfp(\pow(A), \,
1.309 + \begin{array}[t]{r@{\,}l}
1.310 + \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
1.311 + &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
1.312 + \end{array}
1.313 +\]
1.314 +The contribution of each rule to the definition of $\Fin(A)$ should be
1.315 +obvious. A coinductive definition is similar but uses $\gfp$ instead
1.316 +of~$\lfp$.
1.317 +
1.318 +The package must prove that the fixedpoint operator is applied to a
1.319 +monotonic function. If the introduction rules have the form described
1.320 +above, and if the package is supplied a monotonicity theorem for every
1.321 +$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
1.322 + presence of logical connectives in the fixedpoint's body, the
1.323 + monotonicity proof requires some unusual rules. These state that the
1.324 + connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
1.325 + to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
1.326 + only if $\forall x.P(x)\imp Q(x)$.}
1.327 +
1.328 +The package returns its result as an \textsc{ml} structure, which consists of named
1.329 +components; we may regard it as a record. The result structure contains
1.330 +the definitions of the recursive sets as a theorem list called {\tt defs}.
1.331 +It also contains some theorems; {\tt dom\_subset} is an inclusion such as
1.332 +$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
1.333 +definition is monotonic.
1.334 +
1.335 +Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
1.336 +such as
1.337 +\[
1.338 + \begin{array}[t]{r@{\,}l}
1.339 + \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\
1.340 + &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
1.341 + \end{array}
1.342 +\]
1.343 +In order to save space, this theorem is not exported.
1.344 +
1.345 +
1.346 +\subsection{Mutual recursion} \label{mutual-sec}
1.347 +In a mutually recursive definition, the domain of the fixedpoint construction
1.348 +is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
1.349 +\ldots,~$n$. The package uses the injections of the
1.350 +binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
1.351 +$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
1.352 +
1.353 +As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the
1.354 +operator $\Part$ to support mutual recursion. The set $\Part(A,h)$
1.355 +contains those elements of~$A$ having the form~$h(z)$:
1.356 +\[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \]
1.357 +For mutually recursive sets $R_1$, \ldots,~$R_n$ with
1.358 +$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using
1.359 +a fixedpoint operator. The remaining $n$ definitions have the form
1.360 +\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \]
1.361 +It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
1.362 +
1.363 +
1.364 +\subsection{Proving the introduction rules}
1.365 +The user supplies the package with the desired form of the introduction
1.366 +rules. Once it has derived the theorem {\tt unfold}, it attempts
1.367 +to prove those rules. From the user's point of view, this is the
1.368 +trickiest stage; the proofs often fail. The task is to show that the domain
1.369 +$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
1.370 +closed under all the introduction rules. This essentially involves replacing
1.371 +each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
1.372 +attempting to prove the result.
1.373 +
1.374 +Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$
1.375 +in the rules, the package must prove
1.376 +\[ \emptyset\in\pow(A) \qquad
1.377 + \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)}
1.378 +\]
1.379 +Such proofs can be regarded as type-checking the definition.\footnote{The
1.380 + Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}
1.381 + has implicit type-checking.} The user supplies the package with
1.382 +type-checking rules to apply. Usually these are general purpose rules from
1.383 +the \textsc{zf} theory. They could however be rules specifically proved for a
1.384 +particular inductive definition; sometimes this is the easiest way to get the
1.385 +definition through!
1.386 +
1.387 +The result structure contains the introduction rules as the theorem list {\tt
1.388 +intrs}.
1.389 +
1.390 +\subsection{The case analysis rule}
1.391 +The elimination rule, called {\tt elim}, performs case analysis. It is a
1.392 +simple consequence of {\tt unfold}. There is one case for each introduction
1.393 +rule. If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for
1.394 +some $a\in A$ and $b\in\Fin(A)$. Formally, the elimination rule for $\Fin(A)$
1.395 +is written
1.396 +\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
1.397 + & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
1.398 +\]
1.399 +The subscripted variables $a$ and~$b$ above the third premise are
1.400 +eigenvariables, subject to the usual ``not free in \ldots'' proviso.
1.401 +
1.402 +
1.403 +\section{Induction and coinduction rules}
1.404 +Here we must consider inductive and coinductive definitions separately. For
1.405 +an inductive definition, the package returns an induction rule derived
1.406 +directly from the properties of least fixedpoints, as well as a modified rule
1.407 +for mutual recursion. For a coinductive definition, the package returns a
1.408 +basic coinduction rule.
1.409 +
1.410 +\subsection{The basic induction rule}\label{basic-ind-sec}
1.411 +The basic rule, called {\tt induct}, is appropriate in most situations.
1.412 +For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
1.413 +datatype definitions (see below), it is just structural induction.
1.414 +
1.415 +The induction rule for an inductively defined set~$R$ has the form described
1.416 +below. For the time being, assume that $R$'s domain is not a Cartesian
1.417 +product; inductively defined relations are treated slightly differently.
1.418 +
1.419 +The major premise is $x\in R$. There is a minor premise for each
1.420 +introduction rule:
1.421 +\begin{itemize}
1.422 +\item If the introduction rule concludes $t\in R_i$, then the minor premise
1.423 +is~$P(t)$.
1.424 +
1.425 +\item The minor premise's eigenvariables are precisely the introduction
1.426 +rule's free variables that are not parameters of~$R$. For instance, the
1.427 +eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
1.428 +
1.429 +\item If the introduction rule has a premise $t\in R_i$, then the minor
1.430 +premise discharges the assumption $t\in R_i$ and the induction
1.431 +hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$
1.432 +then the minor premise discharges the single assumption
1.433 +\[ t\in M(\{z\in R_i. P(z)\}). \]
1.434 +Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The
1.435 +occurrence of $P$ gives the effect of an induction hypothesis, which may be
1.436 +exploited by appealing to properties of~$M$.
1.437 +\end{itemize}
1.438 +The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
1.439 +but includes an induction hypothesis:
1.440 +\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
1.441 + & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
1.442 +\]
1.443 +Stronger induction rules often suggest themselves. We can derive a rule for
1.444 +$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.
1.445 +The package provides rules for mutual induction and inductive relations. The
1.446 +Isabelle/\textsc{zf} theory also supports well-founded induction and recursion
1.447 +over datatypes, by reasoning about the \defn{rank} of a
1.448 +set~\cite[\S3.4]{paulson-set-II}.
1.449 +
1.450 +
1.451 +\subsection{Modified induction rules}
1.452 +
1.453 +If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$
1.454 +(however nested), then the corresponding predicate $P_i$ takes $m$ arguments.
1.455 +The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$;
1.456 +the conclusion becomes $P(z_1,\ldots,z_m)$. This simplifies reasoning about
1.457 +inductively defined relations, eliminating the need to express properties of
1.458 +$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
1.459 +Occasionally it may require you to split up the induction variable
1.460 +using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt
1.461 + split} appears in the rule.
1.462 +
1.463 +The mutual induction rule is called {\tt
1.464 +mutual\_induct}. It differs from the basic rule in two respects:
1.465 +\begin{itemize}
1.466 +\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
1.467 +\ldots,~$P_n$: one for each recursive set.
1.468 +
1.469 +\item There is no major premise such as $x\in R_i$. Instead, the conclusion
1.470 +refers to all the recursive sets:
1.471 +\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
1.472 + (\forall z.z\in R_n\imp P_n(z))
1.473 +\]
1.474 +Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
1.475 +\ldots,~$n$.
1.476 +\end{itemize}
1.477 +%
1.478 +If the domain of some $R_i$ is a Cartesian product, then the mutual induction
1.479 +rule is modified accordingly. The predicates are made to take $m$ separate
1.480 +arguments instead of a tuple, and the quantification in the conclusion is over
1.481 +the separate variables $z_1$, \ldots, $z_m$.
1.482 +
1.483 +\subsection{Coinduction}\label{coind-sec}
1.484 +A coinductive definition yields a primitive coinduction rule, with no
1.485 +refinements such as those for the induction rules. (Experience may suggest
1.486 +refinements later.) Consider the codatatype of lazy lists as an example. For
1.487 +suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
1.488 +greatest set consistent with the rules
1.489 +\[ \LNil\in\llist(A) \qquad
1.490 + \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
1.491 +\]
1.492 +The $(-)$ tag stresses that this is a coinductive definition. A suitable
1.493 +domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant
1.494 +forms of sum and product that are used to represent non-well-founded data
1.495 +structures (see~\S\ref{univ-sec}).
1.496 +
1.497 +The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$.
1.498 +Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
1.499 +is the greatest solution to this equation contained in $\quniv(A)$:
1.500 +\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
1.501 + \infer*{
1.502 + \begin{array}[b]{r@{}l}
1.503 + z=\LNil\disj
1.504 + \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\
1.505 + & l\in X\un\llist(A) \bigr)
1.506 + \end{array} }{[z\in X]_z}}
1.507 +\]
1.508 +This rule complements the introduction rules; it provides a means of showing
1.509 +$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then
1.510 +applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$
1.511 +is the set of natural numbers.)
1.512 +
1.513 +Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
1.514 +represents a slight strengthening of the greatest fixedpoint property. I
1.515 +discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
1.516 +
1.517 +The clumsy form of the third premise makes the rule hard to use, especially in
1.518 +large definitions. Probably a constant should be declared to abbreviate the
1.519 +large disjunction, and rules derived to allow proving the separate disjuncts.
1.520 +
1.521 +
1.522 +\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
1.523 +This section presents several examples from the literature: the finite
1.524 +powerset operator, lists of $n$ elements, bisimulations on lazy lists, the
1.525 +well-founded part of a relation, and the primitive recursive functions.
1.526 +
1.527 +\subsection{The finite powerset operator}
1.528 +This operator has been discussed extensively above. Here is the
1.529 +corresponding invocation in an Isabelle theory file. Note that
1.530 +$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.
1.531 +\begin{ttbox}
1.532 +Finite = Arith +
1.533 +consts Fin :: i=>i
1.534 +inductive
1.535 + domains "Fin(A)" <= "Pow(A)"
1.536 + intrs
1.537 + emptyI "0 : Fin(A)"
1.538 + consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
1.539 + type_intrs "[empty_subsetI, cons_subsetI, PowI]"
1.540 + type_elims "[make_elim PowD]"
1.541 +end
1.542 +\end{ttbox}
1.543 +Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
1.544 +unary function symbol~$\Fin$, which is defined inductively. Its domain is
1.545 +specified as $\pow(A)$, where $A$ is the parameter appearing in the
1.546 +introduction rules. For type-checking, we supply two introduction
1.547 +rules:
1.548 +\[ \emptyset\sbs A \qquad
1.549 + \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
1.550 +\]
1.551 +A further introduction rule and an elimination rule express both
1.552 +directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking
1.553 +involves mostly introduction rules.
1.554 +
1.555 +Like all Isabelle theory files, this one yields a structure containing the
1.556 +new theory as an \textsc{ml} value. Structure {\tt Finite} also has a
1.557 +substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we
1.558 +can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
1.559 +or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
1.560 +rule is {\tt Fin.induct}.
1.561 +
1.562 +
1.563 +\subsection{Lists of $n$ elements}\label{listn-sec}
1.564 +This has become a standard example of an inductive definition. Following
1.565 +Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
1.566 +$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
1.567 +But her introduction rules
1.568 +\[ \hbox{\tt Niln}\in\listn(A,0) \qquad
1.569 + \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
1.570 + {n\in\nat & a\in A & l\in\listn(A,n)}
1.571 +\]
1.572 +are not acceptable to the inductive definition package:
1.573 +$\listn$ occurs with three different parameter lists in the definition.
1.574 +
1.575 +The Isabelle version of this example suggests a general treatment of
1.576 +varying parameters. It uses the existing datatype definition of
1.577 +$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the
1.578 +parameter~$n$ into the inductive set itself. It defines $\listn(A)$ as a
1.579 +relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$
1.580 +and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the
1.581 +converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction
1.582 +rules are
1.583 +\[ \pair{0,\Nil}\in\listn(A) \qquad
1.584 + \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
1.585 + {a\in A & \pair{n,l}\in\listn(A)}
1.586 +\]
1.587 +The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
1.588 +We declare the constant~$\listn$ and supply an inductive definition,
1.589 +specifying the domain as $\nat\times\lst(A)$:
1.590 +\begin{ttbox}
1.591 +ListN = List +
1.592 +consts listn :: i=>i
1.593 +inductive
1.594 + domains "listn(A)" <= "nat*list(A)"
1.595 + intrs
1.596 + NilI "<0,Nil>: listn(A)"
1.597 + ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
1.598 + type_intrs "nat_typechecks @ list.intrs"
1.599 +end
1.600 +\end{ttbox}
1.601 +The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
1.602 +Because $\listn(A)$ is a set of pairs, type-checking requires the
1.603 +equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The
1.604 +package always includes the rules for ordered pairs.
1.605 +
1.606 +The package returns introduction, elimination and induction rules for
1.607 +$\listn$. The basic induction rule, {\tt listn.induct}, is
1.608 +\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) &
1.609 + \infer*{P(\succ(n),\Cons(a,l))}
1.610 + {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
1.611 +\]
1.612 +This rule lets the induction formula to be a
1.613 +binary property of pairs, $P(n,l)$.
1.614 +It is now a simple matter to prove theorems about $\listn(A)$, such as
1.615 +\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
1.616 +\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
1.617 +This latter result --- here $r``X$ denotes the image of $X$ under $r$
1.618 +--- asserts that the inductive definition agrees with the obvious notion of
1.619 +$n$-element list.
1.620 +
1.621 +A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.
1.622 +It is subject to list operators such as append (concatenation). For example,
1.623 +a trivial induction on $\pair{m,l}\in\listn(A)$ yields
1.624 +\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
1.625 + {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)}
1.626 +\]
1.627 +where $+$ denotes addition on the natural numbers and @ denotes append.
1.628 +
1.629 +\subsection{Rule inversion: the function {\tt mk\_cases}}
1.630 +The elimination rule, {\tt listn.elim}, is cumbersome:
1.631 +\[ \infer{Q}{x\in\listn(A) &
1.632 + \infer*{Q}{[x = \pair{0,\Nil}]} &
1.633 + \infer*{Q}
1.634 + {\left[\begin{array}{l}
1.635 + x = \pair{\succ(n),\Cons(a,l)} \\
1.636 + a\in A \\
1.637 + \pair{n,l}\in\listn(A)
1.638 + \end{array} \right]_{a,l,n}}}
1.639 +\]
1.640 +The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of
1.641 +this rule. It works by freeness reasoning on the list constructors:
1.642 +$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If
1.643 +$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases}
1.644 +deduces the corresponding form of~$i$; this is called rule inversion.
1.645 +Here is a sample session:
1.646 +\begin{ttbox}
1.647 +listn.mk_cases list.con_defs "<i,Nil> : listn(A)";
1.648 +{\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
1.649 +listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";
1.650 +{\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
1.651 +{\out !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
1.652 +{\out |] ==> ?Q" : thm}
1.653 +\end{ttbox}
1.654 +Each of these rules has only two premises. In conventional notation, the
1.655 +second rule is
1.656 +\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) &
1.657 + \infer*{Q}
1.658 + {\left[\begin{array}{l}
1.659 + a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)
1.660 + \end{array} \right]_{n}}}
1.661 +\]
1.662 +The package also has built-in rules for freeness reasoning about $0$
1.663 +and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
1.664 +listn.mk\_cases} can deduce the corresponding form of~$l$.
1.665 +
1.666 +The function {\tt mk\_cases} is also useful with datatype definitions. The
1.667 +instance from the definition of lists, namely {\tt list.mk\_cases}, can
1.668 +prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$:
1.669 +\[ \infer{Q}{\Cons(a,l)\in\lst(A) &
1.670 + & \infer*{Q}{[a\in A &l\in\lst(A)]} }
1.671 +\]
1.672 +A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation
1.673 +relations. Then rule inversion yields case analysis on possible evaluations.
1.674 +For example, Isabelle/\textsc{zf} includes a short proof of the
1.675 +diamond property for parallel contraction on combinators. Ole Rasmussen used
1.676 +{\tt mk\_cases} extensively in his development of the theory of
1.677 +residuals~\cite{rasmussen95}.
1.678 +
1.679 +
1.680 +\subsection{A coinductive definition: bisimulations on lazy lists}
1.681 +This example anticipates the definition of the codatatype $\llist(A)$, which
1.682 +consists of finite and infinite lists over~$A$. Its constructors are $\LNil$
1.683 +and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.
1.684 +Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
1.685 +pairing and injection operators, it contains non-well-founded elements such as
1.686 +solutions to $\LCons(a,l)=l$.
1.687 +
1.688 +The next step in the development of lazy lists is to define a coinduction
1.689 +principle for proving equalities. This is done by showing that the equality
1.690 +relation on lazy lists is the greatest fixedpoint of some monotonic
1.691 +operation. The usual approach~\cite{pitts94} is to define some notion of
1.692 +bisimulation for lazy lists, define equivalence to be the greatest
1.693 +bisimulation, and finally to prove that two lazy lists are equivalent if and
1.694 +only if they are equal. The coinduction rule for equivalence then yields a
1.695 +coinduction principle for equalities.
1.696 +
1.697 +A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs
1.698 +R^+$, where $R^+$ is the relation
1.699 +\[ \{\pair{\LNil,\LNil}\} \un
1.700 + \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
1.701 +\]
1.702 +A pair of lazy lists are \defn{equivalent} if they belong to some
1.703 +bisimulation. Equivalence can be coinductively defined as the greatest
1.704 +fixedpoint for the introduction rules
1.705 +\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad
1.706 + \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
1.707 + {a\in A & \pair{l,l'}\in \lleq(A)}
1.708 +\]
1.709 +To make this coinductive definition, the theory file includes (after the
1.710 +declaration of $\llist(A)$) the following lines:
1.711 +\begin{ttbox}
1.712 +consts lleq :: i=>i
1.713 +coinductive
1.714 + domains "lleq(A)" <= "llist(A) * llist(A)"
1.715 + intrs
1.716 + LNil "<LNil,LNil> : lleq(A)"
1.717 + LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
1.718 + type_intrs "llist.intrs"
1.719 +\end{ttbox}
1.720 +The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking
1.721 +rules include the introduction rules for $\llist(A)$, whose
1.722 +declaration is discussed below (\S\ref{lists-sec}).
1.723 +
1.724 +The package returns the introduction rules and the elimination rule, as
1.725 +usual. But instead of induction rules, it returns a coinduction rule.
1.726 +The rule is too big to display in the usual notation; its conclusion is
1.727 +$x\in\lleq(A)$ and its premises are $x\in X$,
1.728 +${X\sbs\llist(A)\times\llist(A)}$ and
1.729 +\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
1.730 + \begin{array}[t]{@{}l}
1.731 + z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
1.732 + \pair{l,l'}\in X\un\lleq(A) \bigr)
1.733 + \end{array}
1.734 + }{[z\in X]_z}
1.735 +\]
1.736 +Thus if $x\in X$, where $X$ is a bisimulation contained in the
1.737 +domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that
1.738 +$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And
1.739 +$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that
1.740 +$\lleq(A)$ coincides with the equality relation takes some work.
1.741 +
1.742 +\subsection{The accessible part of a relation}\label{acc-sec}
1.743 +Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
1.744 +The \defn{accessible} or \defn{well-founded} part of~$\prec$, written
1.745 +$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
1.746 +no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is
1.747 +inductively defined to be the least set that contains $a$ if it contains
1.748 +all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an
1.749 +introduction rule of the form
1.750 +\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
1.751 +Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
1.752 +difficulties for other systems. Its premise is not acceptable to the
1.753 +inductive definition package of the Cambridge \textsc{hol}
1.754 +system~\cite{camilleri92}. It is also unacceptable to the Isabelle package
1.755 +(recall \S\ref{intro-sec}), but fortunately can be transformed into the
1.756 +acceptable form $t\in M(R)$.
1.757 +
1.758 +The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
1.759 +$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To
1.760 +express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
1.761 +term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is
1.762 +the inverse image of~$\{a\}$ under~$\prec$.
1.763 +
1.764 +The definition below follows this approach. Here $r$ is~$\prec$ and
1.765 +$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a
1.766 +relation is the union of its domain and range.) Finally $r^{-}``\{a\}$
1.767 +denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt
1.768 + Pow\_mono}, which asserts that $\pow$ is monotonic.
1.769 +\begin{ttbox}
1.770 +consts acc :: i=>i
1.771 +inductive
1.772 + domains "acc(r)" <= "field(r)"
1.773 + intrs
1.774 + vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
1.775 + monos "[Pow_mono]"
1.776 +\end{ttbox}
1.777 +The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For
1.778 +instance, $\prec$ is well-founded if and only if its field is contained in
1.779 +$\acc(\prec)$.
1.780 +
1.781 +As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
1.782 +gives rise to an unusual induction hypothesis. Let us examine the
1.783 +induction rule, {\tt acc.induct}:
1.784 +\[ \infer{P(x)}{x\in\acc(r) &
1.785 + \infer*{P(a)}{\left[
1.786 + \begin{array}{r@{}l}
1.787 + r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\
1.788 + a &\, \in\field(r)
1.789 + \end{array}
1.790 + \right]_a}}
1.791 +\]
1.792 +The strange induction hypothesis is equivalent to
1.793 +$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
1.794 +Therefore the rule expresses well-founded induction on the accessible part
1.795 +of~$\prec$.
1.796 +
1.797 +The use of inverse image is not essential. The Isabelle package can accept
1.798 +introduction rules with arbitrary premises of the form $\forall
1.799 +\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed
1.800 +equivalently as
1.801 +\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \]
1.802 +provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The
1.803 +following section demonstrates another use of the premise $t\in M(R)$,
1.804 +where $M=\lst$.
1.805 +
1.806 +\subsection{The primitive recursive functions}\label{primrec-sec}
1.807 +The primitive recursive functions are traditionally defined inductively, as
1.808 +a subset of the functions over the natural numbers. One difficulty is that
1.809 +functions of all arities are taken together, but this is easily
1.810 +circumvented by regarding them as functions on lists. Another difficulty,
1.811 +the notion of composition, is less easily circumvented.
1.812 +
1.813 +Here is a more precise definition. Letting $\vec{x}$ abbreviate
1.814 +$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
1.815 +$[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it
1.816 +belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
1.817 +\begin{itemize}
1.818 +\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
1.819 +\item All \defn{constant} functions $\CONST(k)$, such that
1.820 + $\CONST(k)[\vec{x}]=k$.
1.821 +\item All \defn{projection} functions $\PROJ(i)$, such that
1.822 + $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$.
1.823 +\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$,
1.824 +where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
1.825 +such that
1.826 +\[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] =
1.827 + g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \]
1.828 +
1.829 +\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
1.830 + recursive, such that
1.831 +\begin{eqnarray*}
1.832 + \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
1.833 + \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
1.834 +\end{eqnarray*}
1.835 +\end{itemize}
1.836 +Composition is awkward because it combines not two functions, as is usual,
1.837 +but $m+1$ functions. In her proof that Ackermann's function is not
1.838 +primitive recursive, Nora Szasz was unable to formalize this definition
1.839 +directly~\cite{szasz93}. So she generalized primitive recursion to
1.840 +tuple-valued functions. This modified the inductive definition such that
1.841 +each operation on primitive recursive functions combined just two functions.
1.842 +
1.843 +\begin{figure}
1.844 +\begin{ttbox}
1.845 +Primrec = List +
1.846 +consts
1.847 + primrec :: i
1.848 + SC :: i
1.849 + \(\vdots\)
1.850 +defs
1.851 + SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
1.852 + \(\vdots\)
1.853 +inductive
1.854 + domains "primrec" <= "list(nat)->nat"
1.855 + intrs
1.856 + SC "SC : primrec"
1.857 + CONST "k: nat ==> CONST(k) : primrec"
1.858 + PROJ "i: nat ==> PROJ(i) : primrec"
1.859 + COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
1.860 + PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
1.861 + monos "[list_mono]"
1.862 + con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
1.863 + type_intrs "nat_typechecks @ list.intrs @
1.864 + [lam_type, list_case_type, drop_type, map_type,
1.865 + apply_type, rec_type]"
1.866 +end
1.867 +\end{ttbox}
1.868 +\hrule
1.869 +\caption{Inductive definition of the primitive recursive functions}
1.870 +\label{primrec-fig}
1.871 +\end{figure}
1.872 +\def\fs{{\it fs}}
1.873 +
1.874 +Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have
1.875 +problems accepting this definition. Isabelle's package accepts it easily
1.876 +since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
1.877 +$\lst$ is monotonic. There are five introduction rules, one for each of the
1.878 +five forms of primitive recursive function. Let us examine the one for
1.879 +$\COMP$:
1.880 +\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
1.881 +The induction rule for $\primrec$ has one case for each introduction rule.
1.882 +Due to the use of $\lst$ as a monotone operator, the composition case has
1.883 +an unusual induction hypothesis:
1.884 + \[ \infer*{P(\COMP(g,\fs))}
1.885 + {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}}
1.886 +\]
1.887 +The hypothesis states that $\fs$ is a list of primitive recursive functions,
1.888 +each satisfying the induction formula. Proving the $\COMP$ case typically
1.889 +requires structural induction on lists, yielding two subcases: either
1.890 +$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and
1.891 +$\fs'$ is another list of primitive recursive functions satisfying~$P$.
1.892 +
1.893 +Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec}
1.894 +defines the constants $\SC$, $\CONST$, etc. These are not constructors of
1.895 +a new datatype, but functions over lists of numbers. Their definitions,
1.896 +most of which are omitted, consist of routine list programming. In
1.897 +Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of
1.898 +the function set $\lst(\nat)\to\nat$.
1.899 +
1.900 +The Isabelle theory goes on to formalize Ackermann's function and prove
1.901 +that it is not primitive recursive, using the induction rule {\tt
1.902 + primrec.induct}. The proof follows Szasz's excellent account.
1.903 +
1.904 +
1.905 +\section{Datatypes and codatatypes}\label{data-sec}
1.906 +A (co)datatype definition is a (co)inductive definition with automatically
1.907 +defined constructors and a case analysis operator. The package proves that
1.908 +the case operator inverts the constructors and can prove freeness theorems
1.909 +involving any pair of constructors.
1.910 +
1.911 +
1.912 +\subsection{Constructors and their domain}\label{univ-sec}
1.913 +A (co)inductive definition selects a subset of an existing set; a (co)datatype
1.914 +definition creates a new set. The package reduces the latter to the former.
1.915 +Isabelle/\textsc{zf} supplies sets having strong closure properties to serve
1.916 +as domains for (co)inductive definitions.
1.917 +
1.918 +Isabelle/\textsc{zf} defines the Cartesian product $A\times
1.919 +B$, containing ordered pairs $\pair{a,b}$; it also defines the
1.920 +disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and
1.921 +$\Inr(b)\equiv\pair{1,b}$. For use below, define the $m$-tuple
1.922 +$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$
1.923 +if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.
1.924 +
1.925 +A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be
1.926 +$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
1.927 +In a mutually recursive definition, all constructors for the set~$R_i$ have
1.928 +the outer form~$h_{in}$, where $h_{in}$ is the injection described
1.929 +in~\S\ref{mutual-sec}. Further nested injections ensure that the
1.930 +constructors for~$R_i$ are pairwise distinct.
1.931 +
1.932 +Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and
1.933 +furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
1.934 +$b\in\univ(A)$. In a typical datatype definition with set parameters
1.935 +$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
1.936 +$\univ(A_1\un\cdots\un A_k)$. This solves the problem for
1.937 +datatypes~\cite[\S4.2]{paulson-set-II}.
1.938 +
1.939 +The standard pairs and injections can only yield well-founded
1.940 +constructions. This eases the (manual!) definition of recursive functions
1.941 +over datatypes. But they are unsuitable for codatatypes, which typically
1.942 +contain non-well-founded objects.
1.943 +
1.944 +To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of
1.945 +ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant
1.946 +notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
1.947 +and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the
1.948 +set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$,
1.949 +$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype
1.950 +definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
1.951 +$\quniv(A_1\un\cdots\un A_k)$. Details are published
1.952 +elsewhere~\cite{paulson-final}.
1.953 +
1.954 +\subsection{The case analysis operator}
1.955 +The (co)datatype package automatically defines a case analysis operator,
1.956 +called {\tt$R$\_case}. A mutually recursive definition still has only one
1.957 +operator, whose name combines those of the recursive sets: it is called
1.958 +{\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those
1.959 +for products and sums.
1.960 +
1.961 +Datatype definitions employ standard products and sums, whose operators are
1.962 +$\split$ and $\case$ and satisfy the equations
1.963 +\begin{eqnarray*}
1.964 + \split(f,\pair{x,y}) & = & f(x,y) \\
1.965 + \case(f,g,\Inl(x)) & = & f(x) \\
1.966 + \case(f,g,\Inr(y)) & = & g(y)
1.967 +\end{eqnarray*}
1.968 +Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then
1.969 +its case operator takes $k+1$ arguments and satisfies an equation for each
1.970 +constructor:
1.971 +\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),
1.972 + \qquad i = 1, \ldots, k
1.973 +\]
1.974 +The case operator's definition takes advantage of Isabelle's representation of
1.975 +syntax in the typed $\lambda$-calculus; it could readily be adapted to a
1.976 +theorem prover for higher-order logic. If $f$ and~$g$ have meta-type $i\To i$
1.977 +then so do $\split(f)$ and $\case(f,g)$. This works because $\split$ and
1.978 +$\case$ operate on their last argument. They are easily combined to make
1.979 +complex case analysis operators. For example, $\case(f,\case(g,h))$ performs
1.980 +case analysis for $A+(B+C)$; let us verify one of the three equations:
1.981 +\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \]
1.982 +Codatatype definitions are treated in precisely the same way. They express
1.983 +case operators using those for the variant products and sums, namely
1.984 +$\qsplit$ and~$\qcase$.
1.985 +
1.986 +\medskip
1.987 +
1.988 +To see how constructors and the case analysis operator are defined, let us
1.989 +examine some examples. Further details are available
1.990 +elsewhere~\cite{paulson-set-II}.
1.991 +
1.992 +
1.993 +\subsection{Example: lists and lazy lists}\label{lists-sec}
1.994 +Here is a declaration of the datatype of lists, as it might appear in a theory
1.995 +file:
1.996 +\begin{ttbox}
1.997 +consts list :: i=>i
1.998 +datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
1.999 +\end{ttbox}
1.1000 +And here is a declaration of the codatatype of lazy lists:
1.1001 +\begin{ttbox}
1.1002 +consts llist :: i=>i
1.1003 +codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
1.1004 +\end{ttbox}
1.1005 +
1.1006 +Each form of list has two constructors, one for the empty list and one for
1.1007 +adding an element to a list. Each takes a parameter, defining the set of
1.1008 +lists over a given set~$A$. Each is automatically given the appropriate
1.1009 +domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$. The default
1.1010 +can be overridden.
1.1011 +
1.1012 +\ifshort
1.1013 +Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
1.1014 +\else
1.1015 +Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
1.1016 + list.induct}:
1.1017 +\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
1.1018 + & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
1.1019 +\]
1.1020 +Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this,
1.1021 +Isabelle/\textsc{zf} defines the rank of a set and proves that the standard
1.1022 +pairs and injections have greater rank than their components. An immediate
1.1023 +consequence, which justifies structural recursion on lists
1.1024 +\cite[\S4.3]{paulson-set-II}, is
1.1025 +\[ \rank(l) < \rank(\Cons(a,l)). \]
1.1026 +\par
1.1027 +\fi
1.1028 +But $\llist(A)$ is a codatatype and has no induction rule. Instead it has
1.1029 +the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and
1.1030 +injections are monotonic and need not have greater rank than their
1.1031 +components, fixedpoint operators can create cyclic constructions. For
1.1032 +example, the definition
1.1033 +\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]
1.1034 +yields $\lconst(a) = \LCons(a,\lconst(a))$.
1.1035 +
1.1036 +\ifshort
1.1037 +\typeout{****SHORT VERSION}
1.1038 +\typeout{****Omitting discussion of constructors!}
1.1039 +\else
1.1040 +\medskip
1.1041 +It may be instructive to examine the definitions of the constructors and
1.1042 +case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar.
1.1043 +The list constructors are defined as follows:
1.1044 +\begin{eqnarray*}
1.1045 + \Nil & \equiv & \Inl(\emptyset) \\
1.1046 + \Cons(a,l) & \equiv & \Inr(\pair{a,l})
1.1047 +\end{eqnarray*}
1.1048 +The operator $\lstcase$ performs case analysis on these two alternatives:
1.1049 +\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]
1.1050 +Let us verify the two equations:
1.1051 +\begin{eqnarray*}
1.1052 + \lstcase(c, h, \Nil) & = &
1.1053 + \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
1.1054 + & = & (\lambda u.c)(\emptyset) \\
1.1055 + & = & c\\[1ex]
1.1056 + \lstcase(c, h, \Cons(x,y)) & = &
1.1057 + \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
1.1058 + & = & \split(h, \pair{x,y}) \\
1.1059 + & = & h(x,y)
1.1060 +\end{eqnarray*}
1.1061 +\fi
1.1062 +
1.1063 +
1.1064 +\ifshort
1.1065 +\typeout{****Omitting mutual recursion example!}
1.1066 +\else
1.1067 +\subsection{Example: mutual recursion}
1.1068 +In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
1.1069 +have the one constructor $\Tcons$, while forests have the two constructors
1.1070 +$\Fnil$ and~$\Fcons$:
1.1071 +\begin{ttbox}
1.1072 +consts tree, forest, tree_forest :: i=>i
1.1073 +datatype "tree(A)" = Tcons ("a: A", "f: forest(A)")
1.1074 +and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
1.1075 +\end{ttbox}
1.1076 +The three introduction rules define the mutual recursion. The
1.1077 +distinguishing feature of this example is its two induction rules.
1.1078 +
1.1079 +The basic induction rule is called {\tt tree\_forest.induct}:
1.1080 +\[ \infer{P(x)}{x\in\TF(A) &
1.1081 + \infer*{P(\Tcons(a,f))}
1.1082 + {\left[\begin{array}{l} a\in A \\
1.1083 + f\in\forest(A) \\ P(f)
1.1084 + \end{array}
1.1085 + \right]_{a,f}}
1.1086 + & P(\Fnil)
1.1087 + & \infer*{P(\Fcons(t,f))}
1.1088 + {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
1.1089 + f\in\forest(A) \\ P(f)
1.1090 + \end{array}
1.1091 + \right]_{t,f}} }
1.1092 +\]
1.1093 +This rule establishes a single predicate for $\TF(A)$, the union of the
1.1094 +recursive sets. Although such reasoning is sometimes useful
1.1095 +\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
1.1096 +separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this
1.1097 +rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in
1.1098 +the induction hypotheses:
1.1099 +\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
1.1100 + (\forall z. z\in\forest(A)\imp Q(z))}
1.1101 + {\infer*{P(\Tcons(a,f))}
1.1102 + {\left[\begin{array}{l} a\in A \\
1.1103 + f\in\forest(A) \\ Q(f)
1.1104 + \end{array}
1.1105 + \right]_{a,f}}
1.1106 + & Q(\Fnil)
1.1107 + & \infer*{Q(\Fcons(t,f))}
1.1108 + {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
1.1109 + f\in\forest(A) \\ Q(f)
1.1110 + \end{array}
1.1111 + \right]_{t,f}} }
1.1112 +\]
1.1113 +Elsewhere I describe how to define mutually recursive functions over trees and
1.1114 +forests \cite[\S4.5]{paulson-set-II}.
1.1115 +
1.1116 +Both forest constructors have the form $\Inr(\cdots)$,
1.1117 +while the tree constructor has the form $\Inl(\cdots)$. This pattern would
1.1118 +hold regardless of how many tree or forest constructors there were.
1.1119 +\begin{eqnarray*}
1.1120 + \Tcons(a,l) & \equiv & \Inl(\pair{a,l}) \\
1.1121 + \Fnil & \equiv & \Inr(\Inl(\emptyset)) \\
1.1122 + \Fcons(a,l) & \equiv & \Inr(\Inr(\pair{a,l}))
1.1123 +\end{eqnarray*}
1.1124 +There is only one case operator; it works on the union of the trees and
1.1125 +forests:
1.1126 +\[ {\tt tree\_forest\_case}(f,c,g) \equiv
1.1127 + \case(\split(f),\, \case(\lambda u.c, \split(g)))
1.1128 +\]
1.1129 +\fi
1.1130 +
1.1131 +
1.1132 +\subsection{Example: a four-constructor datatype}
1.1133 +A bigger datatype will illustrate some efficiency
1.1134 +refinements. It has four constructors $\Con_0$, \ldots, $\Con_3$, with the
1.1135 +corresponding arities.
1.1136 +\begin{ttbox}
1.1137 +consts data :: [i,i] => i
1.1138 +datatype "data(A,B)" = Con0
1.1139 + | Con1 ("a: A")
1.1140 + | Con2 ("a: A", "b: B")
1.1141 + | Con3 ("a: A", "b: B", "d: data(A,B)")
1.1142 +\end{ttbox}
1.1143 +Because this datatype has two set parameters, $A$ and~$B$, the package
1.1144 +automatically supplies $\univ(A\un B)$ as its domain. The structural
1.1145 +induction rule has four minor premises, one per constructor, and only the last
1.1146 +has an induction hypothesis. (Details are left to the reader.)
1.1147 +
1.1148 +The constructors are defined by the equations
1.1149 +\begin{eqnarray*}
1.1150 + \Con_0 & \equiv & \Inl(\Inl(\emptyset)) \\
1.1151 + \Con_1(a) & \equiv & \Inl(\Inr(a)) \\
1.1152 + \Con_2(a,b) & \equiv & \Inr(\Inl(\pair{a,b})) \\
1.1153 + \Con_3(a,b,c) & \equiv & \Inr(\Inr(\pair{a,b,c})).
1.1154 +\end{eqnarray*}
1.1155 +The case analysis operator is
1.1156 +\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv
1.1157 + \case(\begin{array}[t]{@{}l}
1.1158 + \case(\lambda u.f_0,\; f_1),\, \\
1.1159 + \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
1.1160 + \end{array}
1.1161 +\]
1.1162 +This may look cryptic, but the case equations are trivial to verify.
1.1163 +
1.1164 +In the constructor definitions, the injections are balanced. A more naive
1.1165 +approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;
1.1166 +instead, each constructor has two injections. The difference here is small.
1.1167 +But the \textsc{zf} examples include a 60-element enumeration type, where each
1.1168 +constructor has 5 or~6 injections. The naive approach would require 1 to~59
1.1169 +injections; the definitions would be quadratic in size. It is like the
1.1170 +advantage of binary notation over unary.
1.1171 +
1.1172 +The result structure contains the case operator and constructor definitions as
1.1173 +the theorem list \verb|con_defs|. It contains the case equations, such as
1.1174 +\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]
1.1175 +as the theorem list \verb|case_eqns|. There is one equation per constructor.
1.1176 +
1.1177 +\subsection{Proving freeness theorems}
1.1178 +There are two kinds of freeness theorems:
1.1179 +\begin{itemize}
1.1180 +\item \defn{injectiveness} theorems, such as
1.1181 +\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
1.1182 +
1.1183 +\item \defn{distinctness} theorems, such as
1.1184 +\[ \Con_1(a) \not= \Con_2(a',b') \]
1.1185 +\end{itemize}
1.1186 +Since the number of such theorems is quadratic in the number of constructors,
1.1187 +the package does not attempt to prove them all. Instead it returns tools for
1.1188 +proving desired theorems --- either manually or during
1.1189 +simplification or classical reasoning.
1.1190 +
1.1191 +The theorem list \verb|free_iffs| enables the simplifier to perform freeness
1.1192 +reasoning. This works by incremental unfolding of constructors that appear in
1.1193 +equations. The theorem list contains logical equivalences such as
1.1194 +\begin{eqnarray*}
1.1195 + \Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\
1.1196 + \Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\
1.1197 + & \vdots & \\
1.1198 + \Inl(a)=\Inl(b) & \bimp & a=b \\
1.1199 + \Inl(a)=\Inr(b) & \bimp & {\tt False} \\
1.1200 + \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
1.1201 +\end{eqnarray*}
1.1202 +For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
1.1203 +
1.1204 +The theorem list \verb|free_SEs| enables the classical
1.1205 +reasoner to perform similar replacements. It consists of elimination rules
1.1206 +to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
1.1207 +assumptions.
1.1208 +
1.1209 +Such incremental unfolding combines freeness reasoning with other proof
1.1210 +steps. It has the unfortunate side-effect of unfolding definitions of
1.1211 +constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
1.1212 +be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs}
1.1213 +restores the defined constants.
1.1214 +
1.1215 +
1.1216 +\section{Related work}\label{related}
1.1217 +The use of least fixedpoints to express inductive definitions seems
1.1218 +obvious. Why, then, has this technique so seldom been implemented?
1.1219 +
1.1220 +Most automated logics can only express inductive definitions by asserting
1.1221 +axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if their
1.1222 +shell principle were removed. With \textsc{alf} the situation is more
1.1223 +complex; earlier versions of Martin-L\"of's type theory could (using
1.1224 +wellordering types) express datatype definitions, but the version underlying
1.1225 +\textsc{alf} requires new rules for each definition~\cite{dybjer91}. With Coq
1.1226 +the situation is subtler still; its underlying Calculus of Constructions can
1.1227 +express inductive definitions~\cite{huet88}, but cannot quite handle datatype
1.1228 +definitions~\cite{paulin-tlca}. It seems that researchers tried hard to
1.1229 +circumvent these problems before finally extending the Calculus with rule
1.1230 +schemes for strictly positive operators. Recently Gim{\'e}nez has extended
1.1231 +the Calculus of Constructions with inductive and coinductive
1.1232 +types~\cite{gimenez-codifying}, with mechanized support in Coq.
1.1233 +
1.1234 +Higher-order logic can express inductive definitions through quantification
1.1235 +over unary predicates. The following formula expresses that~$i$ belongs to the
1.1236 +least set containing~0 and closed under~$\succ$:
1.1237 +\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \]
1.1238 +This technique can be used to prove the Knaster-Tarski theorem, which (in its
1.1239 +general form) is little used in the Cambridge \textsc{hol} system.
1.1240 +Melham~\cite{melham89} describes the development. The natural numbers are
1.1241 +defined as shown above, but lists are defined as functions over the natural
1.1242 +numbers. Unlabelled trees are defined using G\"odel numbering; a labelled
1.1243 +tree consists of an unlabelled tree paired with a list of labels. Melham's
1.1244 +datatype package expresses the user's datatypes in terms of labelled trees.
1.1245 +It has been highly successful, but a fixedpoint approach might have yielded
1.1246 +greater power with less effort.
1.1247 +
1.1248 +Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the
1.1249 +Cambridge \textsc{hol} system with mutual recursion and infinitely-branching
1.1250 +trees. She retains many features of Melham's approach.
1.1251 +
1.1252 +Melham's inductive definition package~\cite{camilleri92} also uses
1.1253 +quantification over predicates. But instead of formalizing the notion of
1.1254 +monotone function, it requires definitions to consist of finitary rules, a
1.1255 +syntactic form that excludes many monotone inductive definitions.
1.1256 +
1.1257 +\textsc{pvs}~\cite{pvs-language} is another proof assistant based on
1.1258 +higher-order logic. It supports both inductive definitions and datatypes,
1.1259 +apparently by asserting axioms. Datatypes may not be iterated in general, but
1.1260 +may use recursion over the built-in $\lst$ type.
1.1261 +
1.1262 +The earliest use of least fixedpoints is probably Robin Milner's. Brian
1.1263 +Monahan extended this package considerably~\cite{monahan84}, as did I in
1.1264 +unpublished work.\footnote{The datatype package described in my \textsc{lcf}
1.1265 + book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts
1.1266 + axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant
1.1267 +fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of
1.1268 +continuous functions over domains. \textsc{lcf} is too weak to express
1.1269 +recursive predicates. The Isabelle package might be the first to be based on
1.1270 +the Knaster-Tarski theorem.
1.1271 +
1.1272 +
1.1273 +\section{Conclusions and future work}
1.1274 +Higher-order logic and set theory are both powerful enough to express
1.1275 +inductive definitions. A growing number of theorem provers implement one
1.1276 +of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive
1.1277 +definition package to write is one that asserts new axioms, not one that
1.1278 +makes definitions and proves theorems about them. But asserting axioms
1.1279 +could introduce unsoundness.
1.1280 +
1.1281 +The fixedpoint approach makes it fairly easy to implement a package for
1.1282 +(co)in\-duc\-tive definitions that does not assert axioms. It is efficient:
1.1283 +it processes most definitions in seconds and even a 60-constructor datatype
1.1284 +requires only a few minutes. It is also simple: The first working version took
1.1285 +under a week to code, consisting of under 1100 lines (35K bytes) of Standard
1.1286 +\textsc{ml}.
1.1287 +
1.1288 +In set theory, care is needed to ensure that the inductive definition yields
1.1289 +a set (rather than a proper class). This problem is inherent to set theory,
1.1290 +whether or not the Knaster-Tarski theorem is employed. We must exhibit a
1.1291 +bounding set (called a domain above). For inductive definitions, this is
1.1292 +often trivial. For datatype definitions, I have had to formalize much set
1.1293 +theory. To justify infinitely-branching datatype definitions, I have had to
1.1294 +develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem
1.1295 +that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all
1.1296 +$\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
1.1297 +The need for such efforts is not a drawback of the fixedpoint approach, for
1.1298 +the alternative is to take such definitions on faith.
1.1299 +
1.1300 +Care is also needed to ensure that the greatest fixedpoint really yields a
1.1301 +coinductive definition. In set theory, standard pairs admit only well-founded
1.1302 +constructions. Aczel's anti-foundation axiom~\cite{aczel88} could be used to
1.1303 +get non-well-founded objects, but it does not seem easy to mechanize.
1.1304 +Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
1.1305 +can be generalized to a variant notion of function. Elsewhere I have
1.1306 +proved that this simple approach works (yielding final coalgebras) for a broad
1.1307 +class of definitions~\cite{paulson-final}.
1.1308 +
1.1309 +Several large studies make heavy use of inductive definitions. L\"otzbeyer
1.1310 +and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
1.1311 +proving the equivalence between the operational and denotational semantics of
1.1312 +a simple imperative language. A single theory file contains three datatype
1.1313 +definitions (of arithmetic expressions, boolean expressions and commands) and
1.1314 +three inductive definitions (the corresponding operational rules). Using
1.1315 +different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
1.1316 +have both proved the Church-Rosser theorem; inductive definitions specify
1.1317 +several reduction relations on $\lambda$-terms. Recently, I have applied
1.1318 +inductive definitions to the analysis of cryptographic
1.1319 +protocols~\cite{paulson-markt}.
1.1320 +
1.1321 +To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
1.1322 +consistency of the dynamic and static semantics for a small functional
1.1323 +language. The example is due to Milner and Tofte~\cite{milner-coind}. It
1.1324 +concerns an extended correspondence relation, which is defined coinductively.
1.1325 +A codatatype definition specifies values and value environments in mutual
1.1326 +recursion. Non-well-founded values represent recursive functions. Value
1.1327 +environments are variant functions from variables into values. This one key
1.1328 +definition uses most of the package's novel features.
1.1329 +
1.1330 +The approach is not restricted to set theory. It should be suitable for any
1.1331 +logic that has some notion of set and the Knaster-Tarski theorem. I have
1.1332 +ported the (co)inductive definition package from Isabelle/\textsc{zf} to
1.1333 +Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95}
1.1334 +is investigating how to port the (co)datatype package. \textsc{hol}
1.1335 +represents sets by unary predicates; defining the corresponding types may
1.1336 +cause complications.
1.1337 +
1.1338 +
1.1339 +\begin{footnotesize}
1.1340 +\bibliographystyle{springer}
1.1341 +\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
1.1342 +\end{footnotesize}
1.1343 +%%%%%\doendnotes
1.1344 +
1.1345 +\ifshort\typeout{****Omitting appendices}
1.1346 +\else
1.1347 +\newpage
1.1348 +\appendix
1.1349 +\section{Inductive and coinductive definitions: users guide}
1.1350 +A theory file may contain any number of inductive and coinductive
1.1351 +definitions. They may be intermixed with other declarations; in
1.1352 +particular, the (co)inductive sets \defn{must} be declared separately as
1.1353 +constants, and may have mixfix syntax or be subject to syntax translations.
1.1354 +
1.1355 +The syntax is rather complicated. Please consult the examples above and the
1.1356 +theory files on the \textsc{zf} source directory.
1.1357 +
1.1358 +Each (co)inductive definition adds definitions to the theory and also proves
1.1359 +some theorems. Each definition creates an \textsc{ml} structure, which is a
1.1360 +substructure of the main theory structure.
1.1361 +
1.1362 +Inductive and datatype definitions can take up considerable storage. The
1.1363 +introduction rules are replicated in slightly different forms as fixedpoint
1.1364 +definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's
1.1365 +six definitions occupy over 600K in total. Defining the 60-constructor
1.1366 +datatype requires nearly 560K\@.
1.1367 +
1.1368 +\subsection{The result structure}
1.1369 +Many of the result structure's components have been discussed
1.1370 +in~\S\ref{basic-sec}; others are self-explanatory.
1.1371 +\begin{description}
1.1372 +\item[\tt thy] is the new theory containing the recursive sets.
1.1373 +
1.1374 +\item[\tt defs] is the list of definitions of the recursive sets.
1.1375 +
1.1376 +\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
1.1377 +
1.1378 +\item[\tt dom\_subset] is a theorem stating inclusion in the domain.
1.1379 +
1.1380 +\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
1.1381 +the recursive sets. The rules are also available individually, using the
1.1382 +names given them in the theory file.
1.1383 +
1.1384 +\item[\tt elim] is the elimination rule.
1.1385 +
1.1386 +\item[\tt mk\_cases] is a function to create simplified instances of {\tt
1.1387 +elim}, using freeness reasoning on some underlying datatype.
1.1388 +\end{description}
1.1389 +
1.1390 +For an inductive definition, the result structure contains two induction
1.1391 +rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter
1.1392 +rule is just {\tt True} unless more than one set is being defined.) For a
1.1393 +coinductive definition, it contains the rule \verb|coinduct|.
1.1394 +
1.1395 +Figure~\ref{def-result-fig} summarizes the two result signatures,
1.1396 +specifying the types of all these components.
1.1397 +
1.1398 +\begin{figure}
1.1399 +\begin{ttbox}
1.1400 +sig
1.1401 +val thy : theory
1.1402 +val defs : thm list
1.1403 +val bnd_mono : thm
1.1404 +val dom_subset : thm
1.1405 +val intrs : thm list
1.1406 +val elim : thm
1.1407 +val mk_cases : thm list -> string -> thm
1.1408 +{\it(Inductive definitions only)}
1.1409 +val induct : thm
1.1410 +val mutual_induct: thm
1.1411 +{\it(Coinductive definitions only)}
1.1412 +val coinduct : thm
1.1413 +end
1.1414 +\end{ttbox}
1.1415 +\hrule
1.1416 +\caption{The result of a (co)inductive definition} \label{def-result-fig}
1.1417 +\end{figure}
1.1418 +
1.1419 +\subsection{The syntax of a (co)inductive definition}
1.1420 +An inductive definition has the form
1.1421 +\begin{ttbox}
1.1422 +inductive
1.1423 + domains {\it domain declarations}
1.1424 + intrs {\it introduction rules}
1.1425 + monos {\it monotonicity theorems}
1.1426 + con_defs {\it constructor definitions}
1.1427 + type_intrs {\it introduction rules for type-checking}
1.1428 + type_elims {\it elimination rules for type-checking}
1.1429 +\end{ttbox}
1.1430 +A coinductive definition is identical, but starts with the keyword
1.1431 +{\tt coinductive}.
1.1432 +
1.1433 +The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
1.1434 +sections are optional. If present, each is specified as a string, which
1.1435 +must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply
1.1436 +inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger
1.1437 +\textsc{ml} error messages. You can then inspect the file on your directory.
1.1438 +
1.1439 +\begin{description}
1.1440 +\item[\it domain declarations] consist of one or more items of the form
1.1441 + {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
1.1442 + its domain.
1.1443 +
1.1444 +\item[\it introduction rules] specify one or more introduction rules in
1.1445 + the form {\it ident\/}~{\it string}, where the identifier gives the name of
1.1446 + the rule in the result structure.
1.1447 +
1.1448 +\item[\it monotonicity theorems] are required for each operator applied to
1.1449 + a recursive set in the introduction rules. There \defn{must} be a theorem
1.1450 + of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$
1.1451 + in an introduction rule!
1.1452 +
1.1453 +\item[\it constructor definitions] contain definitions of constants
1.1454 + appearing in the introduction rules. The (co)datatype package supplies
1.1455 + the constructors' definitions here. Most (co)inductive definitions omit
1.1456 + this section; one exception is the primitive recursive functions example
1.1457 + (\S\ref{primrec-sec}).
1.1458 +
1.1459 +\item[\it type\_intrs] consists of introduction rules for type-checking the
1.1460 + definition, as discussed in~\S\ref{basic-sec}. They are applied using
1.1461 + depth-first search; you can trace the proof by setting
1.1462 +
1.1463 + \verb|trace_DEPTH_FIRST := true|.
1.1464 +
1.1465 +\item[\it type\_elims] consists of elimination rules for type-checking the
1.1466 + definition. They are presumed to be safe and are applied as much as
1.1467 + possible, prior to the {\tt type\_intrs} search.
1.1468 +\end{description}
1.1469 +
1.1470 +The package has a few notable restrictions:
1.1471 +\begin{itemize}
1.1472 +\item The theory must separately declare the recursive sets as
1.1473 + constants.
1.1474 +
1.1475 +\item The names of the recursive sets must be identifiers, not infix
1.1476 +operators.
1.1477 +
1.1478 +\item Side-conditions must not be conjunctions. However, an introduction rule
1.1479 +may contain any number of side-conditions.
1.1480 +
1.1481 +\item Side-conditions of the form $x=t$, where the variable~$x$ does not
1.1482 + occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
1.1483 +\end{itemize}
1.1484 +
1.1485 +Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,
1.1486 +thanks to type-checking. There are no \texttt{domains}, \texttt{type\_intrs}
1.1487 +or \texttt{type\_elims} parts.
1.1488 +
1.1489 +
1.1490 +\section{Datatype and codatatype definitions: users guide}
1.1491 +This section explains how to include (co)datatype declarations in a theory
1.1492 +file. Please include {\tt Datatype} as a parent theory; this makes available
1.1493 +the definitions of $\univ$ and $\quniv$.
1.1494 +
1.1495 +
1.1496 +\subsection{The result structure}
1.1497 +The result structure extends that of (co)inductive definitions
1.1498 +(Figure~\ref{def-result-fig}) with several additional items:
1.1499 +\begin{ttbox}
1.1500 +val con_defs : thm list
1.1501 +val case_eqns : thm list
1.1502 +val free_iffs : thm list
1.1503 +val free_SEs : thm list
1.1504 +val mk_free : string -> thm
1.1505 +\end{ttbox}
1.1506 +Most of these have been discussed in~\S\ref{data-sec}. Here is a summary:
1.1507 +\begin{description}
1.1508 +\item[\tt con\_defs] is a list of definitions: the case operator followed by
1.1509 +the constructors. This theorem list can be supplied to \verb|mk_cases|, for
1.1510 +example.
1.1511 +
1.1512 +\item[\tt case\_eqns] is a list of equations, stating that the case operator
1.1513 +inverts each constructor.
1.1514 +
1.1515 +\item[\tt free\_iffs] is a list of logical equivalences to perform freeness
1.1516 +reasoning by rewriting. A typical application has the form
1.1517 +\begin{ttbox}
1.1518 +by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
1.1519 +\end{ttbox}
1.1520 +
1.1521 +\item[\tt free\_SEs] is a list of safe elimination rules to perform freeness
1.1522 +reasoning. It can be supplied to \verb|eresolve_tac| or to the classical
1.1523 +reasoner:
1.1524 +\begin{ttbox}
1.1525 +by (fast_tac (ZF_cs addSEs free_SEs) 1);
1.1526 +\end{ttbox}
1.1527 +
1.1528 +\item[\tt mk\_free] is a function to prove freeness properties, specified as
1.1529 +strings. The theorems can be expressed in various forms, such as logical
1.1530 +equivalences or elimination rules.
1.1531 +\end{description}
1.1532 +
1.1533 +The result structure also inherits everything from the underlying
1.1534 +(co)inductive definition, such as the introduction rules, elimination rule,
1.1535 +and (co)induction rule.
1.1536 +
1.1537 +
1.1538 +\subsection{The syntax of a (co)datatype definition}
1.1539 +A datatype definition has the form
1.1540 +\begin{ttbox}
1.1541 +datatype <={\it domain}
1.1542 + {\it datatype declaration} and {\it datatype declaration} and \ldots
1.1543 + monos {\it monotonicity theorems}
1.1544 + type_intrs {\it introduction rules for type-checking}
1.1545 + type_elims {\it elimination rules for type-checking}
1.1546 +\end{ttbox}
1.1547 +A codatatype definition is identical save that it starts with the keyword {\tt
1.1548 + codatatype}.
1.1549 +
1.1550 +The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are
1.1551 +optional. They are treated like their counterparts in a (co)inductive
1.1552 +definition, as described above. The package supplements your type-checking
1.1553 +rules (if any) with additional ones that should cope with any
1.1554 +finitely-branching (co)datatype definition.
1.1555 +
1.1556 +\begin{description}
1.1557 +\item[\it domain] specifies a single domain to use for all the mutually
1.1558 + recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are
1.1559 + omitted, the package supplies a domain automatically. Suppose the
1.1560 + definition involves the set parameters $A_1$, \ldots, $A_k$. Then
1.1561 + $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and
1.1562 + $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
1.1563 +
1.1564 + These choices should work for all finitely-branching (co)datatype
1.1565 + definitions. For examples of infinitely-branching datatypes,
1.1566 + see file {\tt ZF/ex/Brouwer.thy}.
1.1567 +
1.1568 +\item[\it datatype declaration] has the form
1.1569 +\begin{quote}
1.1570 + {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}
1.1571 + \ldots
1.1572 +\end{quote}
1.1573 +The {\it string\/} is the datatype, say {\tt"list(A)"}. Each
1.1574 +{\it constructor\/} has the form
1.1575 +\begin{quote}
1.1576 + {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}
1.1577 + {\it mixfix\/}
1.1578 +\end{quote}
1.1579 +The {\it name\/} specifies a new constructor while the {\it premises\/} its
1.1580 +typing conditions. The optional {\it mixfix\/} phrase may give
1.1581 +the constructor infix, for example.
1.1582 +
1.1583 +Mutually recursive {\it datatype declarations\/} are separated by the
1.1584 +keyword~{\tt and}.
1.1585 +\end{description}
1.1586 +
1.1587 +Isabelle/\textsc{hol}'s datatype definition package is (as of this writing)
1.1588 +entirely different from Isabelle/\textsc{zf}'s. The syntax is different, and
1.1589 +instead of making an inductive definition it asserts axioms.
1.1590 +
1.1591 +\paragraph*{Note.}
1.1592 +In the definitions of the constructors, the right-hand sides may overlap.
1.1593 +For instance, the datatype of combinators has constructors defined by
1.1594 +\begin{eqnarray*}
1.1595 + {\tt K} & \equiv & \Inl(\emptyset) \\
1.1596 + {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\
1.1597 + p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q}))
1.1598 +\end{eqnarray*}
1.1599 +Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the
1.1600 +longest right-hand sides are folded first.
1.1601 +
1.1602 +\fi
1.1603 +\end{document}