doc-src/ind-defs.tex
author oheimb
Sat Feb 15 16:10:00 1997 +0100 (1997-02-15)
changeset 2628 1fe7c9f599c2
parent 2219 5687d7dec139
child 2974 bb55cab416af
permissions -rw-r--r--
description of del(eq)congs, safe and unsafe solver
     1 \documentstyle[a4,alltt,iman,extra,proof209,12pt]{article}
     2 \newif\ifshort%''Short'' means a published version, not the documentation
     3 \shortfalse%%%%%\shorttrue
     4 
     5 \title{A Fixedpoint Approach to\\ 
     6   (Co)Inductive and (Co)Datatype Definitions%
     7 \thanks{J. Grundy and S. Thompson made detailed
     8     comments; the referees were also helpful.  Research funded by
     9     SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453
    10     ``Types''.}}
    11 
    12 \author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
    13         Computer Laboratory, University of Cambridge, England}
    14 \date{\today} 
    15 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    16 
    17 \newcommand\sbs{\subseteq}
    18 \let\To=\Rightarrow
    19 
    20 \newcommand\emph[1]{{\em#1\/}}
    21 \newcommand\defn[1]{{\bf#1}}
    22 \newcommand\textsc[1]{{\sc#1}}
    23 \newcommand\texttt[1]{{\tt#1}}
    24 
    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}}
    52 \newcommand\lstcase{\hbox{\tt list\_case}}
    53 \newcommand\lstrec{\hbox{\tt list\_rec}}
    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}}
    63 
    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}}
    83 \newcommand\TFcase{\hbox{\tt TF\_case}}
    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}}
    91 
    92 \binperiod     %%%treat . like a binary operator
    93 
    94 \begin{document}
    95 \pagestyle{empty}
    96 \begin{titlepage}
    97 \maketitle 
    98 \begin{abstract}
    99   This paper presents a fixedpoint approach to inductive definitions.
   100   Instead of using a syntactic test such as ``strictly positive,'' the
   101   approach lets definitions involve any operators that have been proved
   102   monotone.  It is conceptually simple, which has allowed the easy
   103   implementation of mutual recursion and iterated definitions.  It also
   104   handles coinductive definitions: simply replace the least fixedpoint by a
   105   greatest fixedpoint.  
   106 
   107   The method has been implemented in two of Isabelle's logics, \textsc{zf} set
   108   theory and higher-order logic.  It should be applicable to any logic in
   109   which the Knaster-Tarski theorem can be proved.  Examples include lists of
   110   $n$ elements, the accessible part of a relation and the set of primitive
   111   recursive functions.  One example of a coinductive definition is
   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 Church-Rosser theorem and a coinductive proof of
   117   semantic consistency.  The package can be trusted because it proves theorems
   118   from definitions, instead of asserting desired properties as axioms.
   119 \end{abstract}
   120 %
   121 \bigskip
   122 \centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
   123 \thispagestyle{empty} 
   124 \end{titlepage}
   125 \tableofcontents\cleardoublepage\pagestyle{plain}
   126 
   127 \setcounter{page}{1}
   128 
   129 \section{Introduction}
   130 Several theorem provers provide commands for formalizing recursive data
   131 structures, like lists and trees.  Robin Milner implemented one of the first
   132 of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}.  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
   139 principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
   140 
   141 A datatype is but one example of an \defn{inductive definition}.  This
   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
   147 Coq~\cite{paulin-tlca} and again the \textsc{hol} system~\cite{camilleri92}.
   148 
   149 The dual notion is that of a \defn{coinductive definition}.  This specifies
   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
   154 are called \defn{codatatypes} below.
   155 
   156 Not all inductive definitions are meaningful.  \defn{Monotone} inductive
   157 definitions are a large, well-behaved class.  Monotonicity can be enforced
   158 by syntactic conditions such as ``strictly positive,'' but this could lead to
   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.
   162 
   163 This paper describes a package based on a fixedpoint approach.  Least
   164 fixedpoints yield inductive definitions; greatest fixedpoints yield
   165 coinductive definitions.  Most of the discussion below applies equally to
   166 inductive and coinductive definitions, and most of the code is shared.  
   167 
   168 The package supports mutual recursion and infinitely-branching datatypes and
   169 codatatypes.  It allows use of any operators that have been proved monotone,
   170 thus accepting all provably monotone inductive definitions, including
   171 iterated definitions.
   172 
   173 The package has been implemented in
   174 Isabelle~\cite{paulson-markt,paulson-isa-book} using 
   175 \textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
   176 since been ported to Isabelle/\textsc{hol} (higher-order 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 well-typed.  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.
   183 
   184 Most datatype packages equip the new datatype with some means of expressing
   185 recursive functions.  This is the main omission from my package.  Its
   186 fixedpoint operators define only recursive sets.  The Isabelle/\textsc{zf}
   187 theory provides well-founded recursion~\cite{paulson-set-II}, which is harder
   188 to use than structural recursion but considerably more general.
   189 Slind~\cite{slind-tfl} has written a package to automate the definition of
   190 well-founded recursive functions in Isabelle/\textsc{hol}.
   191 
   192 \paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint
   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.
   198 Section~8 draws brief conclusions.  \ifshort\else The appendices are simple
   199 user's manuals for this Isabelle package.\fi
   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*}   
   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
   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*}   
   219 These equations are instances of the Knaster-Tarski theorem, which states
   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 
   224 This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
   225 prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
   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
   228 of formul{\ae}.  Isabelle/\textsc{zf} provides suitable bounding sets for
   229 infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}.  Bounding
   230 sets are also called \defn{domains}.
   231 
   232 The powerset operator is monotone, but by Cantor's theorem there is no
   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{acc-sec} demonstrates
   235 that~$\pow$ is still useful in inductive definitions.
   236 
   237 \section{Elements of an inductive or coinductive definition}\label{basic-sec}
   238 Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
   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
   243 elsewhere~\cite[\S4.5]{paulson-set-II}.
   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
   249 Coq~\cite{paulin-tlca}.  For instance, we cannot define the lists of
   250 $n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
   251 varies.  Section~\ref{listn-sec} describes how to express this set using the
   252 inductive definition package.
   253 
   254 To avoid clutter below, the recursive sets are shown as simply $R_i$
   255 instead of~$R_i(\vec{p})$.
   256 
   257 \subsection{The form of the introduction rules}\label{intro-sec}
   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 side-conditions.
   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} \]
   266 The user must supply the package with monotonicity rules for all such premises.
   267 
   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)$
   271 expresses $t\sbs R$; see \S\ref{acc-sec} for an example.  The \emph{list of}
   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{primrec-sec} and also my earlier
   275 paper~\cite[\S4.4]{paulson-set-II}.
   276 
   277 Introduction rules may also contain \defn{side-conditions}.  These are
   278 premises consisting of arbitrary formul{\ae} not mentioning the recursive
   279 sets. Side-conditions typically involve type-checking.  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
   285 definition.  Consider, as a running example, the finite powerset operator
   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 
   292 The domain in a (co)inductive definition must be some existing set closed
   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
   295 \[  \Fin(A) \equiv \lfp(\pow(A), \,
   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}
   300 \]
   301 The contribution of each rule to the definition of $\Fin(A)$ should be
   302 obvious.  A coinductive definition is similar but uses $\gfp$ instead
   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
   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
   313   only if $\forall x.P(x)\imp Q(x)$.}
   314 
   315 The package returns its result as an \textsc{ml} structure, which consists of named
   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}.
   318 It also contains some theorems; {\tt dom\_subset} is an inclusion such as 
   319 $\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
   320 definition is monotonic.
   321 
   322 Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
   323 such as
   324 \[
   325   \begin{array}[t]{r@{\,}l}
   326      \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\
   327              &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
   328   \end{array}
   329 \]
   330 In order to save space, this theorem is not exported.  
   331 
   332 
   333 \subsection{Mutual recursion} \label{mutual-sec}
   334 In a mutually recursive definition, the domain of the fixedpoint construction
   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
   338 $h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
   339 
   340 As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the
   341 operator $\Part$ to support mutual recursion.  The set $\Part(A,h)$
   342 contains those elements of~$A$ having the form~$h(z)$:
   343 \[ \Part(A,h)  \equiv \{x\in A. \exists z. x=h(z)\}. \]   
   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
   347 \[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n.  \] 
   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}
   352 The user supplies the package with the desired form of the introduction
   353 rules.  Once it has derived the theorem {\tt unfold}, it attempts
   354 to prove those rules.  From the user's point of view, this is the
   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 \]
   366 Such proofs can be regarded as type-checking the definition.\footnote{The
   367   Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}
   368   has implicit type-checking.} The user supplies the package with
   369 type-checking 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!
   373 
   374 The result structure contains the introduction rules as the theorem list {\tt
   375 intrs}.
   376 
   377 \subsection{The case analysis rule}
   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
   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 \]
   386 The subscripted variables $a$ and~$b$ above the third premise are
   387 eigenvariables, subject to the usual ``not free in \ldots'' proviso.
   388 
   389 
   390 \section{Induction and coinduction rules}
   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.
   396 
   397 \subsection{The basic induction rule}\label{basic-ind-sec}
   398 The basic rule, called {\tt induct}, is appropriate in most situations.
   399 For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
   400 datatype definitions (see below), it is just structural induction.  
   401 
   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 
   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
   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$.
   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}
   425 The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
   426 but includes an induction hypothesis:
   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 \] 
   430 Stronger induction rules often suggest themselves.  We can derive a rule for
   431 $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.
   432 The package provides rules for mutual induction and inductive relations.  The
   433 Isabelle/\textsc{zf} theory also supports well-founded induction and recursion
   434 over datatypes, by reasoning about the \defn{rank} of a
   435 set~\cite[\S3.4]{paulson-set-II}.
   436 
   437 
   438 \subsection{Modified induction rules}
   439 
   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 
   450 The mutual induction rule is called {\tt
   451 mutual\_induct}.  It differs from the basic rule in two respects:
   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 \]
   461 Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
   462 \ldots,~$n$.
   463 \end{itemize}
   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$.
   469 
   470 \subsection{Coinduction}\label{coind-sec}
   471 A coinductive definition yields a primitive coinduction rule, with no
   472 refinements such as those for the induction rules.  (Experience may suggest
   473 refinements later.)  Consider the codatatype of lazy lists as an example.  For
   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 \]
   479 The $(-)$ tag stresses that this is a coinductive definition.  A suitable
   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 non-well-founded data
   482 structures (see~\S\ref{univ-sec}).
   483 
   484 The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$. 
   485 Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
   486 is the greatest solution to this equation contained in $\quniv(A)$:
   487 \[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
   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}}
   494 \]
   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
   497 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  (Here $\nat$
   498 is the set of natural numbers.)
   499 
   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
   502 discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
   503 
   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 
   508 
   509 \section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
   510 This section presents several examples from the literature: the finite
   511 powerset operator, lists of $n$ elements, bisimulations on lazy lists, the
   512 well-founded part of a relation, and the primitive recursive functions.
   513 
   514 \subsection{The finite powerset operator}
   515 This operator has been discussed extensively above.  Here is the
   516 corresponding invocation in an Isabelle theory file.  Note that
   517 $\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.
   518 \begin{ttbox}
   519 Finite = Arith + 
   520 consts      Fin :: i=>i
   521 inductive
   522   domains   "Fin(A)" <= "Pow(A)"
   523   intrs
   524     emptyI  "0 : Fin(A)"
   525     consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
   526   type_intrs "[empty_subsetI, cons_subsetI, PowI]"
   527   type_elims "[make_elim PowD]"
   528 end
   529 \end{ttbox}
   530 Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
   531 unary function symbol~$\Fin$, which is defined inductively.  Its domain is
   532 specified as $\pow(A)$, where $A$ is the parameter appearing in the
   533 introduction rules.  For type-checking, we supply two introduction
   534 rules:
   535 \[ \emptyset\sbs A              \qquad
   536    \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
   537 \]
   538 A further introduction rule and an elimination rule express both
   539 directions of the equivalence $A\in\pow(B)\bimp A\sbs B$.  Type-checking
   540 involves mostly introduction rules.  
   541 
   542 Like all Isabelle theory files, this one yields a structure containing the
   543 new theory as an \textsc{ml} value.  Structure {\tt Finite} also has a
   544 substructure, called~{\tt Fin}.  After declaring \hbox{\tt open Finite;} we
   545 can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
   546 or individually as {\tt Fin.emptyI} and {\tt Fin.consI}.  The induction
   547 rule is {\tt Fin.induct}.
   548 
   549 
   550 \subsection{Lists of $n$ elements}\label{listn-sec}
   551 This has become a standard example of an inductive definition.  Following
   552 Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
   553 $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
   554 But her introduction rules
   555 \[ \hbox{\tt Niln}\in\listn(A,0)  \qquad
   556    \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
   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 
   562 The Isabelle version of this example suggests a general treatment of
   563 varying parameters.  It uses the existing datatype definition of
   564 $\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the
   565 parameter~$n$ into the inductive set itself.  It defines $\listn(A)$ as a
   566 relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$
   567 and~$l\in\lst(A)$ and $l$ has length~$n$.  In fact, $\listn(A)$ is the
   568 converse of the length function on~$\lst(A)$.  The Isabelle/\textsc{zf} introduction
   569 rules are
   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 \]
   574 The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
   575 We declare the constant~$\listn$ and supply an inductive definition,
   576 specifying the domain as $\nat\times\lst(A)$:
   577 \begin{ttbox}
   578 ListN = List +
   579 consts  listn :: i=>i
   580 inductive
   581   domains   "listn(A)" <= "nat*list(A)"
   582   intrs
   583     NilI  "<0,Nil>: listn(A)"
   584     ConsI "[| a: A;  <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
   585   type_intrs "nat_typechecks @ list.intrs"
   586 end
   587 \end{ttbox}
   588 The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
   589 Because $\listn(A)$ is a set of pairs, type-checking requires the
   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.
   592 
   593 The package returns introduction, elimination and induction rules for
   594 $\listn$.  The basic induction rule, {\tt listn.induct}, is
   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))}
   597                 {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
   598 \]
   599 This rule lets the induction formula to be a 
   600 binary property of pairs, $P(n,l)$.  
   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\} \]
   604 This latter result --- here $r``X$ denotes the image of $X$ under $r$
   605 --- asserts that the inductive definition agrees with the obvious notion of
   606 $n$-element list.  
   607 
   608 A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.
   609 It is subject to list operators such as append (concatenation).  For example,
   610 a trivial induction on $\pair{m,l}\in\listn(A)$ yields
   611 \[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
   612          {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)} 
   613 \]
   614 where $+$ denotes addition on the natural numbers and @ denotes append.
   615 
   616 \subsection{Rule inversion: the function {\tt mk\_cases}}
   617 The elimination rule, {\tt listn.elim}, is cumbersome:
   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 \]
   627 The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of
   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
   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: 
   633 \begin{ttbox}
   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}
   640 \end{ttbox}
   641 Each of these rules has only two premises.  In conventional notation, the
   642 second rule is
   643 \[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) & 
   644           \infer*{Q}
   645              {\left[\begin{array}{l}
   646                a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)
   647                \end{array} \right]_{n}}}
   648 \]
   649 The package also has built-in rules for freeness reasoning about $0$
   650 and~$\succ$.  So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
   651 listn.mk\_cases} can deduce the corresponding form of~$l$. 
   652 
   653 The function {\tt mk\_cases} is also useful with datatype definitions.  The
   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)$:
   656 \[ \infer{Q}{\Cons(a,l)\in\lst(A) & 
   657                  & \infer*{Q}{[a\in A &l\in\lst(A)]} }
   658 \]
   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 
   666 
   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$
   670 and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.  
   671 Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
   672 pairing and injection operators, it contains non-well-founded elements such as
   673 solutions to $\LCons(a,l)=l$.
   674 
   675 The next step in the development of lazy lists is to define a coinduction
   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
   681 only if they are equal.  The coinduction rule for equivalence then yields a
   682 coinduction principle for equalities.
   683 
   684 A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs
   685 R^+$, where $R^+$ is the relation
   686 \[ \{\pair{\LNil,\LNil}\} \un 
   687    \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
   688 \]
   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
   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)}
   695 \]
   696 To make this coinductive definition, the theory file includes (after the
   697 declaration of $\llist(A)$) the following lines:
   698 \begin{ttbox}
   699 consts    lleq :: i=>i
   700 coinductive
   701   domains "lleq(A)" <= "llist(A) * llist(A)"
   702   intrs
   703     LNil  "<LNil,LNil> : lleq(A)"
   704     LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
   705   type_intrs  "llist.intrs"
   706 \end{ttbox}
   707 The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$.  The type-checking
   708 rules include the introduction rules for $\llist(A)$, whose 
   709 declaration is discussed below (\S\ref{lists-sec}).
   710 
   711 The package returns the introduction rules and the elimination rule, as
   712 usual.  But instead of induction rules, it returns a coinduction rule.
   713 The rule is too big to display in the usual notation; its conclusion is
   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'.\,
   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}  
   721     }{[z\in X]_z}
   722 \]
   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
   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
   727 $\lleq(A)$ coincides with the equality relation takes some work.
   728 
   729 \subsection{The accessible part of a relation}\label{acc-sec}
   730 Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
   731 The \defn{accessible} or \defn{well-founded} part of~$\prec$, written
   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)} \]
   738 Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
   739 difficulties for other systems.  Its premise is not acceptable to the
   740 inductive definition package of the Cambridge \textsc{hol}
   741 system~\cite{camilleri92}.  It is also unacceptable to the Isabelle package
   742 (recall \S\ref{intro-sec}), but fortunately can be transformed into the
   743 acceptable form $t\in M(R)$.
   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 
   751 The definition below follows this approach.  Here $r$ is~$\prec$ and
   752 $\field(r)$ refers to~$D$, the domain of $\acc(r)$.  (The field of a
   753 relation is the union of its domain and range.)  Finally $r^{-}``\{a\}$
   754 denotes the inverse image of~$\{a\}$ under~$r$.  We supply the theorem {\tt
   755   Pow\_mono}, which asserts that $\pow$ is monotonic.
   756 \begin{ttbox}
   757 consts    acc :: i=>i
   758 inductive
   759   domains "acc(r)" <= "field(r)"
   760   intrs
   761     vimage  "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
   762   monos     "[Pow_mono]"
   763 \end{ttbox}
   764 The Isabelle theory proceeds to prove facts about $\acc(\prec)$.  For
   765 instance, $\prec$ is well-founded if and only if its field is contained in
   766 $\acc(\prec)$.  
   767 
   768 As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
   769 gives rise to an unusual induction hypothesis.  Let us examine the
   770 induction rule, {\tt acc.induct}:
   771 \[ \infer{P(x)}{x\in\acc(r) &
   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}}
   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 well-founded 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 
   788 \[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \] 
   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{primrec-sec}
   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_{n-1}$, we can write lists such as $[\vec{x}]$,
   802 $[y+1,\vec{x}]$, etc.  A function is \defn{primitive recursive} if it
   803 belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
   804 \begin{itemize}
   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
   807   $\CONST(k)[\vec{x}]=k$. 
   808 \item All \defn{projection} functions $\PROJ(i)$, such that
   809   $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$. 
   810 \item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$, 
   811 where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
   812 such that
   813 \[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] = 
   814    g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \] 
   815 
   816 \item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
   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 tuple-valued functions.  This modified the inductive definition such that
   828 each operation on primitive recursive functions combined just two functions.
   829 
   830 \begin{figure}
   831 \begin{ttbox}
   832 Primrec = List +
   833 consts
   834   primrec :: i
   835   SC      :: i
   836   \(\vdots\)
   837 defs
   838   SC_def    "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
   839   \(\vdots\)
   840 inductive
   841   domains "primrec" <= "list(nat)->nat"
   842   intrs
   843     SC       "SC : primrec"
   844     CONST    "k: nat ==> CONST(k) : primrec"
   845     PROJ     "i: nat ==> PROJ(i) : primrec"
   846     COMP     "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
   847     PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   848   monos      "[list_mono]"
   849   con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
   850   type_intrs "nat_typechecks @ list.intrs @                      
   851               [lam_type, list_case_type, drop_type, map_type,    
   852                apply_type, rec_type]"
   853 end
   854 \end{ttbox}
   855 \hrule
   856 \caption{Inductive definition of the primitive recursive functions} 
   857 \label{primrec-fig}
   858 \end{figure}
   859 \def\fs{{\it fs}} 
   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_{m-1}]$ 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$:
   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))}
   872           {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}} 
   873 \]
   874 The hypothesis states that $\fs$ is a list of primitive recursive functions,
   875 each satisfying the induction formula.  Proving the $\COMP$ case typically
   876 requires structural induction on lists, yielding two subcases: either
   877 $\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and
   878 $\fs'$ is another list of primitive recursive functions satisfying~$P$.
   879 
   880 Figure~\ref{primrec-fig} presents the theory file.  Theory {\tt Primrec}
   881 defines the constants $\SC$, $\CONST$, etc.  These are not constructors of
   882 a new datatype, but functions over lists of numbers.  Their definitions,
   883 most of which are omitted, consist of routine list programming.  In
   884 Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of
   885 the function set $\lst(\nat)\to\nat$.
   886 
   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
   889   primrec.induct}.  The proof follows Szasz's excellent account.
   890 
   891 
   892 \section{Datatypes and codatatypes}\label{data-sec}
   893 A (co)datatype definition is a (co)inductive definition with automatically
   894 defined constructors and a case analysis operator.  The package proves that
   895 the case operator inverts the constructors and can prove freeness theorems
   896 involving any pair of constructors.
   897 
   898 
   899 \subsection{Constructors and their domain}\label{univ-sec}
   900 A (co)inductive definition selects a subset of an existing set; a (co)datatype
   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
   903 as domains for (co)inductive definitions.
   904 
   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 
   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$.
   914 In a mutually recursive definition, all constructors for the set~$R_i$ have
   915 the outer form~$h_{in}$, where $h_{in}$ is the injection described
   916 in~\S\ref{mutual-sec}.  Further nested injections ensure that the
   917 constructors for~$R_i$ are pairwise distinct.  
   918 
   919 Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and
   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]{paulson-set-II}.
   925 
   926 The standard pairs and injections can only yield well-founded
   927 constructions.  This eases the (manual!) definition of recursive functions
   928 over datatypes.  But they are unsuitable for codatatypes, which typically
   929 contain non-well-founded objects.
   930 
   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
   933 notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
   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
   938 $\quniv(A_1\un\cdots\un A_k)$.  Details are published
   939 elsewhere~\cite{paulson-final}.
   940 
   941 \subsection{The case analysis operator}
   942 The (co)datatype package automatically defines a case analysis operator,
   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.
   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:
   958 \[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),
   959     \qquad i = 1, \ldots, k
   960 \]
   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 higher-order logic.  If $f$ and~$g$ have meta-type $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) \]
   969 Codatatype definitions are treated in precisely the same way.  They express
   970 case operators using those for the variant products and sums, namely
   971 $\qsplit$ and~$\qcase$.
   972 
   973 \medskip
   974 
   975 To see how constructors and the case analysis operator are defined, let us
   976 examine some examples.  Further details are available
   977 elsewhere~\cite{paulson-set-II}.
   978 
   979 
   980 \subsection{Example: lists and lazy lists}\label{lists-sec}
   981 Here is a declaration of the datatype of lists, as it might appear in a theory
   982 file:
   983 \begin{ttbox} 
   984 consts  list :: i=>i
   985 datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
   986 \end{ttbox}
   987 And here is a declaration of the codatatype of lazy lists:
   988 \begin{ttbox}
   989 consts  llist :: i=>i
   990 codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
   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
   995 lists over a given set~$A$.  Each is automatically given the appropriate
   996 domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$.  The default
   997 can be overridden.
   998 
   999 \ifshort
  1000 Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
  1001 \else
  1002 Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
  1003   list.induct}:
  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,
  1008 Isabelle/\textsc{zf} defines the rank of a set and proves that the standard
  1009 pairs and injections have greater rank than their components.  An immediate
  1010 consequence, which justifies structural recursion on lists
  1011 \cite[\S4.3]{paulson-set-II}, is
  1012 \[ \rank(l) < \rank(\Cons(a,l)). \]
  1013 \par
  1014 \fi
  1015 But $\llist(A)$ is a codatatype and has no induction rule.  Instead it has
  1016 the coinduction rule shown in \S\ref{coind-sec}.  Since variant pairs and
  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
  1020 \[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]
  1021 yields $\lconst(a) = \LCons(a,\lconst(a))$.
  1022 
  1023 \ifshort
  1024 \typeout{****SHORT VERSION}
  1025 \typeout{****Omitting discussion of constructors!}
  1026 \else
  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*}
  1032   \Nil       & \equiv & \Inl(\emptyset) \\
  1033   \Cons(a,l) & \equiv & \Inr(\pair{a,l})
  1034 \end{eqnarray*}
  1035 The operator $\lstcase$ performs case analysis on these two alternatives:
  1036 \[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]
  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) \\
  1042      & = & c\\[1ex]
  1043     \lstcase(c, h, \Cons(x,y)) & = & 
  1044        \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
  1045      & = & \split(h, \pair{x,y}) \\
  1046      & = & h(x,y)
  1047 \end{eqnarray*} 
  1048 \fi
  1049 
  1050 
  1051 \ifshort
  1052 \typeout{****Omitting mutual recursion example!}
  1053 \else
  1054 \subsection{Example: mutual recursion}
  1055 In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
  1056 have the one constructor $\Tcons$, while forests have the two constructors
  1057 $\Fnil$ and~$\Fcons$:
  1058 \begin{ttbox}
  1059 consts  tree, forest, tree_forest    :: i=>i
  1060 datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
  1061 and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
  1062 \end{ttbox}
  1063 The three introduction rules define the mutual recursion.  The
  1064 distinguishing feature of this example is its two induction rules.
  1065 
  1066 The basic induction rule is called {\tt tree\_forest.induct}:
  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)
  1074      & \infer*{P(\Fcons(t,f))}
  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
  1081 recursive sets.  Although such reasoning is sometimes useful
  1082 \cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
  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:
  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)
  1094      & \infer*{Q(\Fcons(t,f))}
  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 \] 
  1100 Elsewhere I describe how to define mutually recursive functions over trees and
  1101 forests \cite[\S4.5]{paulson-set-II}.
  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*}
  1107   \Tcons(a,l)  & \equiv & \Inl(\pair{a,l}) \\
  1108   \Fnil        & \equiv & \Inr(\Inl(\emptyset)) \\
  1109   \Fcons(a,l)  & \equiv & \Inr(\Inr(\pair{a,l}))
  1110 \end{eqnarray*} 
  1111 There is only one case operator; it works on the union of the trees and
  1112 forests:
  1113 \[ {\tt tree\_forest\_case}(f,c,g) \equiv 
  1114     \case(\split(f),\, \case(\lambda u.c, \split(g))) 
  1115 \]
  1116 \fi
  1117 
  1118 
  1119 \subsection{Example: a four-constructor datatype}
  1120 A bigger datatype will illustrate some efficiency 
  1121 refinements.  It has four constructors $\Con_0$, \ldots, $\Con_3$, with the
  1122 corresponding arities.
  1123 \begin{ttbox}
  1124 consts    data :: [i,i] => i
  1125 datatype  "data(A,B)" = Con0
  1126                       | Con1 ("a: A")
  1127                       | Con2 ("a: A", "b: B")
  1128                       | Con3 ("a: A", "b: B", "d: data(A,B)")
  1129 \end{ttbox}
  1130 Because this datatype has two set parameters, $A$ and~$B$, the package
  1131 automatically supplies $\univ(A\un B)$ as its domain.  The structural
  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.)
  1134 
  1135 The constructors are defined by the equations
  1136 \begin{eqnarray*}
  1137   \Con_0         & \equiv & \Inl(\Inl(\emptyset)) \\
  1138   \Con_1(a)      & \equiv & \Inl(\Inr(a)) \\
  1139   \Con_2(a,b)    & \equiv & \Inr(\Inl(\pair{a,b})) \\
  1140   \Con_3(a,b,c)  & \equiv & \Inr(\Inr(\pair{a,b,c})).
  1141 \end{eqnarray*} 
  1142 The case analysis operator is
  1143 \[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv 
  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} 
  1148 \]
  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
  1152 approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;
  1153 instead, each constructor has two injections.  The difference here is small.
  1154 But the \textsc{zf} examples include a 60-element enumeration type, where each
  1155 constructor has 5 or~6 injections.  The naive approach would require 1 to~59
  1156 injections; the definitions would be quadratic in size.  It is like the
  1157 advantage of binary notation over unary.
  1158 
  1159 The result structure contains the case operator and constructor definitions as
  1160 the theorem list \verb|con_defs|. It contains the case equations, such as 
  1161 \[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]
  1162 as the theorem list \verb|case_eqns|.  There is one equation per constructor.
  1163 
  1164 \subsection{Proving freeness theorems}
  1165 There are two kinds of freeness theorems:
  1166 \begin{itemize}
  1167 \item \defn{injectiveness} theorems, such as
  1168 \[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
  1169 
  1170 \item \defn{distinctness} theorems, such as
  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
  1175 proving desired theorems --- either manually or during
  1176 simplification or classical reasoning.
  1177 
  1178 The theorem list \verb|free_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                     \\
  1186   \Inl(a)=\Inr(b)   & \bimp &  {\tt False}             \\
  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 \verb|free_SEs| enables the classical
  1192 reasoner to perform similar replacements.  It consists of elimination rules
  1193 to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
  1194 assumptions.
  1195 
  1196 Such incremental unfolding combines freeness reasoning with other proof
  1197 steps.  It has the unfortunate side-effect 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.
  1201 
  1202 
  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
  1208 axioms.  Little would be left of Boyer and Moore's logic~\cite{bm79} if their
  1209 shell principle were removed.  With \textsc{alf} the situation is more
  1210 complex; earlier versions of Martin-L\"of's type theory could (using
  1211 wellordering types) express datatype definitions, but the version underlying
  1212 \textsc{alf} requires new rules for each definition~\cite{dybjer91}.  With Coq
  1213 the situation is subtler still; its underlying Calculus of Constructions can
  1214 express inductive definitions~\cite{huet88}, but cannot quite handle datatype
  1215 definitions~\cite{paulin-tlca}.  It seems that researchers tried hard to
  1216 circumvent these problems before finally extending the Calculus with rule
  1217 schemes for strictly positive operators.  Recently Gim{\'e}nez has extended
  1218 the Calculus of Constructions with inductive and coinductive
  1219 types~\cite{gimenez-codifying}, with mechanized support in Coq.
  1220 
  1221 Higher-order 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) \] 
  1225 This technique can be used to prove the Knaster-Tarski 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.
  1234 
  1235 Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the
  1236 Cambridge \textsc{hol} system with mutual recursion and infinitely-branching
  1237 trees.  She retains many features of Melham's approach.
  1238 
  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.
  1243 
  1244 \textsc{pvs}~\cite{pvs-language} is another proof assistant based on
  1245 higher-order logic.  It supports both inductive definitions and datatypes,
  1246 apparently by asserting axioms.  Datatypes may not be iterated in general, but
  1247 may use recursion over the built-in $\lst$ type.
  1248 
  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 first-order logic of domain theory; the relevant
  1254 fixedpoint theorem is not Knaster-Tarski 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 Knaster-Tarski theorem.
  1258 
  1259 
  1260 \section{Conclusions and future work}
  1261 Higher-order 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,saaltink-fme}.  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
  1269 (co)in\-duc\-tive definitions that does not assert axioms.  It is efficient:
  1270 it processes most definitions in seconds and even a 60-constructor 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 Knaster-Tarski 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
  1280 theory.  To justify infinitely-branching datatype definitions, I have had to
  1281 develop a theory of cardinal arithmetic~\cite{paulson-gr}, 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 well-founded
  1289 constructions.  Aczel's anti-foundation axiom~\cite{aczel88} could be used to
  1290 get non-well-founded 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{paulson-final}.
  1295 
  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{nipkow-CR} and Rasmussen~\cite{rasmussen95}
  1303 have both proved the Church-Rosser 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{paulson-markt}. 
  1307 
  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{milner-coind}.  It
  1311 concerns an extended correspondence relation, which is defined coinductively.
  1312 A codatatype definition specifies values and value environments in mutual
  1313 recursion.  Non-well-founded 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.
  1316 
  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 Knaster-Tarski theorem.  I have
  1319 ported the (co)inductive definition package from Isabelle/\textsc{zf} to
  1320 Isabelle/\textsc{hol} (higher-order 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.
  1324 
  1325 
  1326 \begin{footnotesize}
  1327 \bibliographystyle{springer}
  1328 \bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
  1329 \end{footnotesize}
  1330 %%%%%\doendnotes
  1331 
  1332 \ifshort\typeout{****Omitting appendices}
  1333 \else
  1334 \newpage
  1335 \appendix
  1336 \section{Inductive and coinductive definitions: users guide}
  1337 A theory file may contain any number of inductive and coinductive
  1338 definitions.  They may be intermixed with other declarations; in
  1339 particular, the (co)inductive sets \defn{must} be declared separately as
  1340 constants, and may have mixfix syntax or be subject to syntax translations.
  1341 
  1342 The syntax is rather complicated.  Please consult the examples above and the
  1343 theory files on the \textsc{zf} source directory.  
  1344 
  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
  1347 substructure of the main theory structure.
  1348 
  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 60-constructor
  1353 datatype requires nearly 560K\@.
  1354 
  1355 \subsection{The result structure}
  1356 Many of the result structure's components have been discussed
  1357 in~\S\ref{basic-sec}; others are self-explanatory.
  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
  1368 the recursive sets.  The rules are also available individually, using the
  1369 names given them in the theory file. 
  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 
  1377 For an inductive definition, the result structure contains two induction
  1378 rules, {\tt induct} and \verb|mutual_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 \verb|coinduct|.
  1381 
  1382 Figure~\ref{def-result-fig} summarizes the two result signatures,
  1383 specifying the types of all these components.
  1384 
  1385 \begin{figure}
  1386 \begin{ttbox}
  1387 sig
  1388 val thy          : theory
  1389 val defs         : thm list
  1390 val bnd_mono     : thm
  1391 val dom_subset   : thm
  1392 val intrs        : thm list
  1393 val elim         : thm
  1394 val mk_cases     : thm list -> string -> thm
  1395 {\it(Inductive definitions only)} 
  1396 val induct       : thm
  1397 val mutual_induct: thm
  1398 {\it(Coinductive definitions only)}
  1399 val coinduct    : thm
  1400 end
  1401 \end{ttbox}
  1402 \hrule
  1403 \caption{The result of a (co)inductive definition} \label{def-result-fig}
  1404 \end{figure}
  1405 
  1406 \subsection{The syntax of a (co)inductive definition}
  1407 An inductive definition has the form
  1408 \begin{ttbox}
  1409 inductive
  1410   domains    {\it domain declarations}
  1411   intrs      {\it introduction rules}
  1412   monos      {\it monotonicity theorems}
  1413   con_defs   {\it constructor definitions}
  1414   type_intrs {\it introduction rules for type-checking}
  1415   type_elims {\it elimination rules for type-checking}
  1416 \end{ttbox}
  1417 A coinductive definition is identical, but starts with the keyword
  1418 {\tt coinductive}.  
  1419 
  1420 The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
  1421 sections are optional.  If present, each is specified as a string, which
  1422 must be a valid \textsc{ml} expression of type {\tt thm list}.  It is simply
  1423 inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger
  1424 \textsc{ml} error messages.  You can then inspect the file on your directory.
  1425 
  1426 \begin{description}
  1427 \item[\it domain declarations] consist of one or more items of the form
  1428   {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
  1429   its domain.
  1430 
  1431 \item[\it introduction rules] specify one or more introduction rules in
  1432   the form {\it ident\/}~{\it string}, where the identifier gives the name of
  1433   the rule in the result structure.
  1434 
  1435 \item[\it monotonicity theorems] are required for each operator applied to
  1436   a recursive set in the introduction rules.  There \defn{must} be a theorem
  1437   of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$
  1438   in an introduction rule!
  1439 
  1440 \item[\it constructor definitions] contain definitions of constants
  1441   appearing in the introduction rules.  The (co)datatype package supplies
  1442   the constructors' definitions here.  Most (co)inductive definitions omit
  1443   this section; one exception is the primitive recursive functions example
  1444   (\S\ref{primrec-sec}).
  1445 
  1446 \item[\it type\_intrs] consists of introduction rules for type-checking the
  1447   definition, as discussed in~\S\ref{basic-sec}.  They are applied using
  1448   depth-first search; you can trace the proof by setting
  1449 
  1450   \verb|trace_DEPTH_FIRST := true|.
  1451 
  1452 \item[\it type\_elims] consists of elimination rules for type-checking the
  1453   definition.  They are presumed to be safe and are applied as much as
  1454   possible, prior to the {\tt type\_intrs} search.
  1455 \end{description}
  1456 
  1457 The package has a few notable restrictions:
  1458 \begin{itemize}
  1459 \item The theory must separately declare the recursive sets as
  1460   constants.
  1461 
  1462 \item The names of the recursive sets must be identifiers, not infix
  1463 operators.  
  1464 
  1465 \item Side-conditions must not be conjunctions.  However, an introduction rule
  1466 may contain any number of side-conditions.
  1467 
  1468 \item Side-conditions of the form $x=t$, where the variable~$x$ does not
  1469   occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
  1470 \end{itemize}
  1471 
  1472 Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,
  1473 thanks to type-checking.  There are no \texttt{domains}, \texttt{type\_intrs}
  1474 or \texttt{type\_elims} parts.
  1475 
  1476 
  1477 \section{Datatype and codatatype definitions: users guide}
  1478 This section explains how to include (co)datatype declarations in a theory
  1479 file.  Please include {\tt Datatype} as a parent theory; this makes available
  1480 the definitions of $\univ$ and $\quniv$.
  1481 
  1482 
  1483 \subsection{The result structure}
  1484 The result structure extends that of (co)inductive definitions
  1485 (Figure~\ref{def-result-fig}) with several additional items:
  1486 \begin{ttbox}
  1487 val con_defs  : thm list
  1488 val case_eqns : thm list
  1489 val free_iffs : thm list
  1490 val free_SEs  : thm list
  1491 val mk_free   : string -> thm
  1492 \end{ttbox}
  1493 Most of these have been discussed in~\S\ref{data-sec}.  Here is a summary:
  1494 \begin{description}
  1495 \item[\tt con\_defs] is a list of definitions: the case operator followed by
  1496 the constructors.  This theorem list can be supplied to \verb|mk_cases|, for
  1497 example.
  1498 
  1499 \item[\tt case\_eqns] is a list of equations, stating that the case operator
  1500 inverts each constructor.
  1501 
  1502 \item[\tt free\_iffs] is a list of logical equivalences to perform freeness
  1503 reasoning by rewriting.  A typical application has the form
  1504 \begin{ttbox}
  1505 by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
  1506 \end{ttbox}
  1507 
  1508 \item[\tt free\_SEs] is a list of safe elimination rules to perform freeness
  1509 reasoning.  It can be supplied to \verb|eresolve_tac| or to the classical
  1510 reasoner:
  1511 \begin{ttbox} 
  1512 by (fast_tac (ZF_cs addSEs free_SEs) 1);
  1513 \end{ttbox}
  1514 
  1515 \item[\tt mk\_free] is a function to prove freeness properties, specified as
  1516 strings.  The theorems can be expressed in various forms, such as logical
  1517 equivalences or elimination rules.
  1518 \end{description}
  1519 
  1520 The result structure also inherits everything from the underlying
  1521 (co)inductive definition, such as the introduction rules, elimination rule,
  1522 and (co)induction rule.
  1523 
  1524 
  1525 \subsection{The syntax of a (co)datatype definition}
  1526 A datatype definition has the form
  1527 \begin{ttbox}
  1528 datatype <={\it domain}
  1529  {\it datatype declaration} and {\it datatype declaration} and \ldots
  1530   monos      {\it monotonicity theorems}
  1531   type_intrs {\it introduction rules for type-checking}
  1532   type_elims {\it elimination rules for type-checking}
  1533 \end{ttbox}
  1534 A codatatype definition is identical save that it starts with the keyword {\tt
  1535   codatatype}.
  1536 
  1537 The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are
  1538 optional.  They are treated like their counterparts in a (co)inductive
  1539 definition, as described above.  The package supplements your type-checking
  1540 rules (if any) with additional ones that should cope with any
  1541 finitely-branching (co)datatype definition.
  1542 
  1543 \begin{description}
  1544 \item[\it domain] specifies a single domain to use for all the mutually
  1545   recursive (co)datatypes.  If it (and the preceeding~{\tt <=}) are
  1546   omitted, the package supplies a domain automatically.  Suppose the
  1547   definition involves the set parameters $A_1$, \ldots, $A_k$.  Then
  1548   $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and
  1549   $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
  1550 
  1551   These choices should work for all finitely-branching (co)datatype
  1552   definitions.  For examples of infinitely-branching datatypes, 
  1553   see file {\tt ZF/ex/Brouwer.thy}.
  1554 
  1555 \item[\it datatype declaration] has the form
  1556 \begin{quote}
  1557  {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}
  1558  \ldots 
  1559 \end{quote}
  1560 The {\it string\/} is the datatype, say {\tt"list(A)"}.  Each
  1561 {\it constructor\/} has the form 
  1562 \begin{quote}
  1563  {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}
  1564  {\it mixfix\/}
  1565 \end{quote}
  1566 The {\it name\/} specifies a new constructor while the {\it premises\/} its
  1567 typing conditions.  The optional {\it mixfix\/} phrase may give
  1568 the constructor infix, for example.
  1569 
  1570 Mutually recursive {\it datatype declarations\/} are separated by the
  1571 keyword~{\tt and}.
  1572 \end{description}
  1573 
  1574 Isabelle/\textsc{hol}'s datatype definition package is (as of this writing)
  1575 entirely different from Isabelle/\textsc{zf}'s.  The syntax is different, and
  1576 instead of making an inductive definition it asserts axioms.
  1577 
  1578 \paragraph*{Note.}
  1579 In the definitions of the constructors, the right-hand sides may overlap.
  1580 For instance, the datatype of combinators has constructors defined by
  1581 \begin{eqnarray*}
  1582   {\tt K} & \equiv & \Inl(\emptyset) \\
  1583   {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\
  1584   p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q})) 
  1585 \end{eqnarray*}
  1586 Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the
  1587 longest right-hand sides are folded first.
  1588 
  1589 \fi
  1590 \end{document}