--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Inductive/ind-defs.bbl Mon May 12 17:13:12 1997 +0200
@@ -0,0 +1,214 @@
+\begin{thebibliography}{10}
+
+\bibitem{abramsky90}
+Abramsky, S.,
+\newblock The lazy lambda calculus,
+\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
+ Addison-Wesley, 1977, pp.~65--116
+
+\bibitem{aczel77}
+Aczel, P.,
+\newblock An introduction to inductive definitions,
+\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
+ North-Holland, 1977, pp.~739--782
+
+\bibitem{aczel88}
+Aczel, P.,
+\newblock {\em Non-Well-Founded Sets},
+\newblock CSLI, 1988
+
+\bibitem{bm79}
+Boyer, R.~S., Moore, J.~S.,
+\newblock {\em A Computational Logic},
+\newblock Academic Press, 1979
+
+\bibitem{camilleri92}
+Camilleri, J., Melham, T.~F.,
+\newblock Reasoning with inductively defined relations in the {HOL} theorem
+ prover,
+\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
+
+\bibitem{davey&priestley}
+Davey, B.~A., Priestley, H.~A.,
+\newblock {\em Introduction to Lattices and Order},
+\newblock Cambridge Univ. Press, 1990
+
+\bibitem{dybjer91}
+Dybjer, P.,
+\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
+ set-theoretic semantics,
+\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ.
+ Press, 1991, pp.~280--306
+
+\bibitem{types94}
+Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
+\newblock {\em Types for Proofs and Programs: International Workshop {TYPES
+ '94}},
+\newblock LNCS 996. Springer, published 1995
+
+\bibitem{IMPS}
+Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
+\newblock {IMPS}: An interactive mathematical proof system,
+\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
+
+\bibitem{frost95}
+Frost, J.,
+\newblock A case study of co-induction in {Isabelle},
+\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995
+
+\bibitem{gimenez-codifying}
+Gim{\'e}nez, E.,
+\newblock Codifying guarded definitions with recursive schemes,
+\newblock In Dybjer et~al. \cite{types94}, pp.~39--59
+
+\bibitem{gunter-trees}
+Gunter, E.~L.,
+\newblock A broader class of trees for recursive type definitions for {HOL},
+\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG
+ '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,
+ pp.~141--154
+
+\bibitem{hennessy90}
+Hennessy, M.,
+\newblock {\em The Semantics of Programming Languages: An Elementary
+ Introduction Using Structural Operational Semantics},
+\newblock Wiley, 1990
+
+\bibitem{huet88}
+Huet, G.,
+\newblock Induction principles formalized in the {Calculus of Constructions},
+\newblock In {\em Programming of Future Generation Computers\/} (1988),
+ K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216
+
+\bibitem{melham89}
+Melham, T.~F.,
+\newblock Automating recursive type definitions in higher order logic,
+\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
+ Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386
+
+\bibitem{milner-ind}
+Milner, R.,
+\newblock How to derive inductions in {LCF},
+\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
+
+\bibitem{milner89}
+Milner, R.,
+\newblock {\em Communication and Concurrency},
+\newblock Prentice-Hall, 1989
+
+\bibitem{milner-coind}
+Milner, R., Tofte, M.,
+\newblock Co-induction in relational semantics,
+\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
+
+\bibitem{monahan84}
+Monahan, B.~Q.,
+\newblock {\em Data Type Proofs using Edinburgh {LCF}},
+\newblock PhD thesis, University of Edinburgh, 1984
+
+\bibitem{nipkow-CR}
+Nipkow, T.,
+\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
+\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/}
+ (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747
+
+\bibitem{pvs-language}
+Owre, S., Shankar, N., Rushby, J.~M.,
+\newblock {\em The {PVS} specification language},
+\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.
+ 1993,
+\newblock Beta release
+
+\bibitem{paulin-tlca}
+Paulin-Mohring, C.,
+\newblock Inductive definitions in the system {Coq}: Rules and properties,
+\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
+ J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
+
+\bibitem{paulson-markt}
+Paulson, L.~C.,
+\newblock Tool support for logics of programs,
+\newblock In {\em Mathematical Methods in Program Development: Summer School
+ Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer,
+\newblock In press
+
+\bibitem{paulson87}
+Paulson, L.~C.,
+\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
+\newblock Cambridge Univ. Press, 1987
+
+\bibitem{paulson-set-I}
+Paulson, L.~C.,
+\newblock Set theory for verification: {I}. {From} foundations to functions,
+\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
+
+\bibitem{paulson-isa-book}
+Paulson, L.~C.,
+\newblock {\em Isabelle: A Generic Theorem Prover},
+\newblock Springer, 1994,
+\newblock LNCS 828
+
+\bibitem{paulson-set-II}
+Paulson, L.~C.,
+\newblock Set theory for verification: {II}. {Induction} and recursion,
+\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
+
+\bibitem{paulson-coind}
+Paulson, L.~C.,
+\newblock Mechanizing coinduction and corecursion in higher-order logic,
+\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204
+
+\bibitem{paulson-final}
+Paulson, L.~C.,
+\newblock A concrete final coalgebra theorem for {ZF} set theory,
+\newblock In Dybjer et~al. \cite{types94}, pp.~120--139
+
+\bibitem{paulson-gr}
+Paulson, L.~C., Gr\c{a}bczewski, K.,
+\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
+\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
+
+\bibitem{pitts94}
+Pitts, A.~M.,
+\newblock A co-induction principle for recursively defined domains,
+\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
+
+\bibitem{rasmussen95}
+Rasmussen, O.,
+\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
+ experiment,
+\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
+ 1995
+
+\bibitem{saaltink-fme}
+Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
+\newblock An {EVES} data abstraction example,
+\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
+ J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
+
+\bibitem{slind-tfl}
+Slind, K.,
+\newblock Function definition in higher-order logic,
+\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
+ (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125
+
+\bibitem{szasz93}
+Szasz, N.,
+\newblock A machine checked proof that {Ackermann's} function is not primitive
+ recursive,
+\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
+ Univ. Press, 1993, pp.~317--338
+
+\bibitem{voelker95}
+V\"olker, N.,
+\newblock On the representation of datatypes in {Isabelle/HOL},
+\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
+ 1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
+ pp.~206--218
+
+\bibitem{winskel93}
+Winskel, G.,
+\newblock {\em The Formal Semantics of Programming Languages},
+\newblock MIT Press, 1993
+
+\end{thebibliography}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Inductive/ind-defs.tex Mon May 12 17:13:12 1997 +0200
@@ -0,0 +1,1600 @@
+\documentclass[12pt]{article}
+\usepackage{a4,latexsym,proof}
+
+\makeatletter
+\input{../rail.sty}
+\input{../iman.sty}
+\input{../extra.sty}
+\makeatother
+
+\newif\ifshort%''Short'' means a published version, not the documentation
+\shortfalse%%%%%\shorttrue
+
+\title{A Fixedpoint Approach to\\
+ (Co)Inductive and (Co)Datatype Definitions%
+ \thanks{J. Grundy and S. Thompson made detailed comments. Mads Tofte and
+ the referees were also helpful. The research was funded by the SERC
+ grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 ``Types''.}}
+
+\author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}\\
+ Computer Laboratory, University of Cambridge, England}
+\date{\today}
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\newcommand\sbs{\subseteq}
+\let\To=\Rightarrow
+
+%\newcommand\emph[1]{{\em#1\/}}
+\newcommand\defn[1]{{\bf#1}}
+%\newcommand\textsc[1]{{\sc#1}}
+%\newcommand\texttt[1]{{\tt#1}}
+
+\newcommand\pow{{\cal P}}
+%%%\let\pow=\wp
+\newcommand\RepFun{\hbox{\tt RepFun}}
+\newcommand\cons{\hbox{\tt cons}}
+\def\succ{\hbox{\tt succ}}
+\newcommand\split{\hbox{\tt split}}
+\newcommand\fst{\hbox{\tt fst}}
+\newcommand\snd{\hbox{\tt snd}}
+\newcommand\converse{\hbox{\tt converse}}
+\newcommand\domain{\hbox{\tt domain}}
+\newcommand\range{\hbox{\tt range}}
+\newcommand\field{\hbox{\tt field}}
+\newcommand\lfp{\hbox{\tt lfp}}
+\newcommand\gfp{\hbox{\tt gfp}}
+\newcommand\id{\hbox{\tt id}}
+\newcommand\trans{\hbox{\tt trans}}
+\newcommand\wf{\hbox{\tt wf}}
+\newcommand\nat{\hbox{\tt nat}}
+\newcommand\rank{\hbox{\tt rank}}
+\newcommand\univ{\hbox{\tt univ}}
+\newcommand\Vrec{\hbox{\tt Vrec}}
+\newcommand\Inl{\hbox{\tt Inl}}
+\newcommand\Inr{\hbox{\tt Inr}}
+\newcommand\case{\hbox{\tt case}}
+\newcommand\lst{\hbox{\tt list}}
+\newcommand\Nil{\hbox{\tt Nil}}
+\newcommand\Cons{\hbox{\tt Cons}}
+\newcommand\lstcase{\hbox{\tt list\_case}}
+\newcommand\lstrec{\hbox{\tt list\_rec}}
+\newcommand\length{\hbox{\tt length}}
+\newcommand\listn{\hbox{\tt listn}}
+\newcommand\acc{\hbox{\tt acc}}
+\newcommand\primrec{\hbox{\tt primrec}}
+\newcommand\SC{\hbox{\tt SC}}
+\newcommand\CONST{\hbox{\tt CONST}}
+\newcommand\PROJ{\hbox{\tt PROJ}}
+\newcommand\COMP{\hbox{\tt COMP}}
+\newcommand\PREC{\hbox{\tt PREC}}
+
+\newcommand\quniv{\hbox{\tt quniv}}
+\newcommand\llist{\hbox{\tt llist}}
+\newcommand\LNil{\hbox{\tt LNil}}
+\newcommand\LCons{\hbox{\tt LCons}}
+\newcommand\lconst{\hbox{\tt lconst}}
+\newcommand\lleq{\hbox{\tt lleq}}
+\newcommand\map{\hbox{\tt map}}
+\newcommand\term{\hbox{\tt term}}
+\newcommand\Apply{\hbox{\tt Apply}}
+\newcommand\termcase{\hbox{\tt term\_case}}
+\newcommand\rev{\hbox{\tt rev}}
+\newcommand\reflect{\hbox{\tt reflect}}
+\newcommand\tree{\hbox{\tt tree}}
+\newcommand\forest{\hbox{\tt forest}}
+\newcommand\Part{\hbox{\tt Part}}
+\newcommand\TF{\hbox{\tt tree\_forest}}
+\newcommand\Tcons{\hbox{\tt Tcons}}
+\newcommand\Fcons{\hbox{\tt Fcons}}
+\newcommand\Fnil{\hbox{\tt Fnil}}
+\newcommand\TFcase{\hbox{\tt TF\_case}}
+\newcommand\Fin{\hbox{\tt Fin}}
+\newcommand\QInl{\hbox{\tt QInl}}
+\newcommand\QInr{\hbox{\tt QInr}}
+\newcommand\qsplit{\hbox{\tt qsplit}}
+\newcommand\qcase{\hbox{\tt qcase}}
+\newcommand\Con{\hbox{\tt Con}}
+\newcommand\data{\hbox{\tt data}}
+
+\binperiod %%%treat . like a binary operator
+
+\begin{document}
+\pagestyle{empty}
+\begin{titlepage}
+\maketitle
+\begin{abstract}
+ This paper presents a fixedpoint approach to inductive definitions.
+ Instead of using a syntactic test such as ``strictly positive,'' the
+ approach lets definitions involve any operators that have been proved
+ monotone. It is conceptually simple, which has allowed the easy
+ implementation of mutual recursion and iterated definitions. It also
+ handles coinductive definitions: simply replace the least fixedpoint by a
+ greatest fixedpoint.
+
+ The method has been implemented in two of Isabelle's logics, \textsc{zf} set
+ theory and higher-order logic. It should be applicable to any logic in
+ which the Knaster-Tarski theorem can be proved. Examples include lists of
+ $n$ elements, the accessible part of a relation and the set of primitive
+ recursive functions. One example of a coinductive definition is
+ bisimulations for lazy lists. Recursive datatypes are examined in detail,
+ as well as one example of a \defn{codatatype}: lazy lists.
+
+ The Isabelle package has been applied in several large case studies,
+ including two proofs of the Church-Rosser theorem and a coinductive proof of
+ semantic consistency. The package can be trusted because it proves theorems
+ from definitions, instead of asserting desired properties as axioms.
+\end{abstract}
+%
+\bigskip
+\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
+\thispagestyle{empty}
+\end{titlepage}
+\tableofcontents\cleardoublepage\pagestyle{plain}
+
+\setcounter{page}{1}
+
+\section{Introduction}
+Several theorem provers provide commands for formalizing recursive data
+structures, like lists and trees. Robin Milner implemented one of the first
+of these, for Edinburgh \textsc{lcf}~\cite{milner-ind}. Given a description
+of the desired data structure, Milner's package formulated appropriate
+definitions and proved the characteristic theorems. Similar is Melham's
+recursive type package for the Cambridge \textsc{hol} system~\cite{melham89}.
+Such data structures are called \defn{datatypes}
+below, by analogy with datatype declarations in Standard~\textsc{ml}\@.
+Some logics take datatypes as primitive; consider Boyer and Moore's shell
+principle~\cite{bm79} and the Coq type theory~\cite{paulin-tlca}.
+
+A datatype is but one example of an \defn{inductive definition}. Such a
+definition~\cite{aczel77} specifies the least set~$R$ \defn{closed under}
+given rules: applying a rule to elements of~$R$ yields a result within~$R$.
+Inductive definitions have many applications. The collection of theorems in a
+logic is inductively defined. A structural operational
+semantics~\cite{hennessy90} is an inductive definition of a reduction or
+evaluation relation on programs. A few theorem provers provide commands for
+formalizing inductive definitions; these include Coq~\cite{paulin-tlca} and
+again the \textsc{hol} system~\cite{camilleri92}.
+
+The dual notion is that of a \defn{coinductive definition}. Such a definition
+specifies the greatest set~$R$ \defn{consistent with} given rules: every
+element of~$R$ can be seen as arising by applying a rule to elements of~$R$.
+Important examples include using bisimulation relations to formalize
+equivalence of processes~\cite{milner89} or lazy functional
+programs~\cite{abramsky90}. Other examples include lazy lists and other
+infinite data structures; these are called \defn{codatatypes} below.
+
+Not all inductive definitions are meaningful. \defn{Monotone} inductive
+definitions are a large, well-behaved class. Monotonicity can be enforced
+by syntactic conditions such as ``strictly positive,'' but this could lead to
+monotone definitions being rejected on the grounds of their syntactic form.
+More flexible is to formalize monotonicity within the logic and allow users
+to prove it.
+
+This paper describes a package based on a fixedpoint approach. Least
+fixedpoints yield inductive definitions; greatest fixedpoints yield
+coinductive definitions. Most of the discussion below applies equally to
+inductive and coinductive definitions, and most of the code is shared.
+
+The package supports mutual recursion and infinitely-branching datatypes and
+codatatypes. It allows use of any operators that have been proved monotone,
+thus accepting all provably monotone inductive definitions, including
+iterated definitions.
+
+The package has been implemented in
+Isabelle~\cite{paulson-markt,paulson-isa-book} using
+\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
+since been ported to Isabelle/\textsc{hol} (higher-order logic). The
+recursion equations are specified as introduction rules for the mutually
+recursive sets. The package transforms these rules into a mapping over sets,
+and attempts to prove that the mapping is monotonic and well-typed. If
+successful, the package makes fixedpoint definitions and proves the
+introduction, elimination and (co)induction rules. Users invoke the package
+by making simple declarations in Isabelle theory files.
+
+Most datatype packages equip the new datatype with some means of expressing
+recursive functions. This is the main omission from my package. Its
+fixedpoint operators define only recursive sets. The Isabelle/\textsc{zf}
+theory provides well-founded recursion~\cite{paulson-set-II}, which is harder
+to use than structural recursion but considerably more general.
+Slind~\cite{slind-tfl} has written a package to automate the definition of
+well-founded recursive functions in Isabelle/\textsc{hol}.
+
+\paragraph*{Outline.} Section~2 introduces the least and greatest fixedpoint
+operators. Section~3 discusses the form of introduction rules, mutual
+recursion and other points common to inductive and coinductive definitions.
+Section~4 discusses induction and coinduction rules separately. Section~5
+presents several examples, including a coinductive definition. Section~6
+describes datatype definitions. Section~7 presents related work.
+Section~8 draws brief conclusions. \ifshort\else The appendices are simple
+user's manuals for this Isabelle package.\fi
+
+Most of the definitions and theorems shown below have been generated by the
+package. I have renamed some variables to improve readability.
+
+\section{Fixedpoint operators}
+In set theory, the least and greatest fixedpoint operators are defined as
+follows:
+\begin{eqnarray*}
+ \lfp(D,h) & \equiv & \inter\{X\sbs D. h(X)\sbs X\} \\
+ \gfp(D,h) & \equiv & \union\{X\sbs D. X\sbs h(X)\}
+\end{eqnarray*}
+Let $D$ be a set. Say that $h$ is \defn{bounded by}~$D$ if $h(D)\sbs D$, and
+\defn{monotone below~$D$} if
+$h(A)\sbs h(B)$ for all $A$ and $B$ such that $A\sbs B\sbs D$. If $h$ is
+bounded by~$D$ and monotone then both operators yield fixedpoints:
+\begin{eqnarray*}
+ \lfp(D,h) & = & h(\lfp(D,h)) \\
+ \gfp(D,h) & = & h(\gfp(D,h))
+\end{eqnarray*}
+These equations are instances of the Knaster-Tarski theorem, which states
+that every monotonic function over a complete lattice has a
+fixedpoint~\cite{davey&priestley}. It is obvious from their definitions
+that $\lfp$ must be the least fixedpoint, and $\gfp$ the greatest.
+
+This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to
+prove. Showing monotonicity of~$h$ is trivial, in typical cases. We must
+also exhibit a bounding set~$D$ for~$h$. Frequently this is trivial, as when
+a set of theorems is (co)inductively defined over some previously existing set
+of formul{\ae}. Isabelle/\textsc{zf} provides suitable bounding sets for
+infinitely-branching (co)datatype definitions; see~\S\ref{univ-sec}. Bounding
+sets are also called \defn{domains}.
+
+The powerset operator is monotone, but by Cantor's theorem there is no
+set~$A$ such that $A=\pow(A)$. We cannot put $A=\lfp(D,\pow)$ because
+there is no suitable domain~$D$. But \S\ref{acc-sec} demonstrates
+that~$\pow$ is still useful in inductive definitions.
+
+\section{Elements of an inductive or coinductive definition}\label{basic-sec}
+Consider a (co)inductive definition of the sets $R_1$, \ldots,~$R_n$, in
+mutual recursion. They will be constructed from domains $D_1$,
+\ldots,~$D_n$, respectively. The construction yields not $R_i\sbs D_i$ but
+$R_i\sbs D_1+\cdots+D_n$, where $R_i$ is contained in the image of~$D_i$
+under an injection. Reasons for this are discussed
+elsewhere~\cite[\S4.5]{paulson-set-II}.
+
+The definition may involve arbitrary parameters $\vec{p}=p_1$,
+\ldots,~$p_k$. Each recursive set then has the form $R_i(\vec{p})$. The
+parameters must be identical every time they occur within a definition. This
+would appear to be a serious restriction compared with other systems such as
+Coq~\cite{paulin-tlca}. For instance, we cannot define the lists of
+$n$ elements as the set $\listn(A,n)$ using rules where the parameter~$n$
+varies. Section~\ref{listn-sec} describes how to express this set using the
+inductive definition package.
+
+To avoid clutter below, the recursive sets are shown as simply $R_i$
+instead of~$R_i(\vec{p})$.
+
+\subsection{The form of the introduction rules}\label{intro-sec}
+The body of the definition consists of the desired introduction rules. The
+conclusion of each rule must have the form $t\in R_i$, where $t$ is any term.
+Premises typically have the same form, but they can have the more general form
+$t\in M(R_i)$ or express arbitrary side-conditions.
+
+The premise $t\in M(R_i)$ is permitted if $M$ is a monotonic operator on
+sets, satisfying the rule
+\[ \infer{M(A)\sbs M(B)}{A\sbs B} \]
+The user must supply the package with monotonicity rules for all such premises.
+
+The ability to introduce new monotone operators makes the approach
+flexible. A suitable choice of~$M$ and~$t$ can express a lot. The
+powerset operator $\pow$ is monotone, and the premise $t\in\pow(R)$
+expresses $t\sbs R$; see \S\ref{acc-sec} for an example. The \emph{list of}
+operator is monotone, as is easily proved by induction. The premise
+$t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual
+recursion; see \S\ref{primrec-sec} and also my earlier
+paper~\cite[\S4.4]{paulson-set-II}.
+
+Introduction rules may also contain \defn{side-conditions}. These are
+premises consisting of arbitrary formul{\ae} not mentioning the recursive
+sets. Side-conditions typically involve type-checking. One example is the
+premise $a\in A$ in the following rule from the definition of lists:
+\[ \infer{\Cons(a,l)\in\lst(A)}{a\in A & l\in\lst(A)} \]
+
+\subsection{The fixedpoint definitions}
+The package translates the list of desired introduction rules into a fixedpoint
+definition. Consider, as a running example, the finite powerset operator
+$\Fin(A)$: the set of all finite subsets of~$A$. It can be
+defined as the least set closed under the rules
+\[ \emptyset\in\Fin(A) \qquad
+ \infer{\{a\}\un b\in\Fin(A)}{a\in A & b\in\Fin(A)}
+\]
+
+The domain in a (co)inductive definition must be some existing set closed
+under the rules. A suitable domain for $\Fin(A)$ is $\pow(A)$, the set of all
+subsets of~$A$. The package generates the definition
+\[ \Fin(A) \equiv \lfp(\pow(A), \,
+ \begin{array}[t]{r@{\,}l}
+ \lambda X. \{z\in\pow(A). & z=\emptyset \disj{} \\
+ &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in X)\})
+ \end{array}
+\]
+The contribution of each rule to the definition of $\Fin(A)$ should be
+obvious. A coinductive definition is similar but uses $\gfp$ instead
+of~$\lfp$.
+
+The package must prove that the fixedpoint operator is applied to a
+monotonic function. If the introduction rules have the form described
+above, and if the package is supplied a monotonicity theorem for every
+$t\in M(R_i)$ premise, then this proof is trivial.\footnote{Due to the
+ presence of logical connectives in the fixedpoint's body, the
+ monotonicity proof requires some unusual rules. These state that the
+ connectives $\conj$, $\disj$ and $\exists$ preserve monotonicity with respect
+ to the partial ordering on unary predicates given by $P\sqsubseteq Q$ if and
+ only if $\forall x.P(x)\imp Q(x)$.}
+
+The package returns its result as an \textsc{ml} structure, which consists of named
+components; we may regard it as a record. The result structure contains
+the definitions of the recursive sets as a theorem list called {\tt defs}.
+It also contains some theorems; {\tt dom\_subset} is an inclusion such as
+$\Fin(A)\sbs\pow(A)$, while {\tt bnd\_mono} asserts that the fixedpoint
+definition is monotonic.
+
+Internally the package uses the theorem {\tt unfold}, a fixedpoint equation
+such as
+\[
+ \begin{array}[t]{r@{\,}l}
+ \Fin(A) = \{z\in\pow(A). & z=\emptyset \disj{} \\
+ &(\exists a\,b. z=\{a\}\un b\conj a\in A\conj b\in \Fin(A))\}
+ \end{array}
+\]
+In order to save space, this theorem is not exported.
+
+
+\subsection{Mutual recursion} \label{mutual-sec}
+In a mutually recursive definition, the domain of the fixedpoint construction
+is the disjoint sum of the domain~$D_i$ of each~$R_i$, for $i=1$,
+\ldots,~$n$. The package uses the injections of the
+binary disjoint sum, typically $\Inl$ and~$\Inr$, to express injections
+$h_{1n}$, \ldots, $h_{nn}$ for the $n$-ary disjoint sum $D_1+\cdots+D_n$.
+
+As discussed elsewhere \cite[\S4.5]{paulson-set-II}, Isabelle/\textsc{zf} defines the
+operator $\Part$ to support mutual recursion. The set $\Part(A,h)$
+contains those elements of~$A$ having the form~$h(z)$:
+\[ \Part(A,h) \equiv \{x\in A. \exists z. x=h(z)\}. \]
+For mutually recursive sets $R_1$, \ldots,~$R_n$ with
+$n>1$, the package makes $n+1$ definitions. The first defines a set $R$ using
+a fixedpoint operator. The remaining $n$ definitions have the form
+\[ R_i \equiv \Part(R,h_{in}), \qquad i=1,\ldots, n. \]
+It follows that $R=R_1\un\cdots\un R_n$, where the $R_i$ are pairwise disjoint.
+
+
+\subsection{Proving the introduction rules}
+The user supplies the package with the desired form of the introduction
+rules. Once it has derived the theorem {\tt unfold}, it attempts
+to prove those rules. From the user's point of view, this is the
+trickiest stage; the proofs often fail. The task is to show that the domain
+$D_1+\cdots+D_n$ of the combined set $R_1\un\cdots\un R_n$ is
+closed under all the introduction rules. This essentially involves replacing
+each~$R_i$ by $D_1+\cdots+D_n$ in each of the introduction rules and
+attempting to prove the result.
+
+Consider the $\Fin(A)$ example. After substituting $\pow(A)$ for $\Fin(A)$
+in the rules, the package must prove
+\[ \emptyset\in\pow(A) \qquad
+ \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)}
+\]
+Such proofs can be regarded as type-checking the definition.\footnote{The
+ Isabelle/\textsc{hol} version does not require these proofs, as \textsc{hol}
+ has implicit type-checking.} The user supplies the package with
+type-checking rules to apply. Usually these are general purpose rules from
+the \textsc{zf} theory. They could however be rules specifically proved for a
+particular inductive definition; sometimes this is the easiest way to get the
+definition through!
+
+The result structure contains the introduction rules as the theorem list {\tt
+intrs}.
+
+\subsection{The case analysis rule}
+The elimination rule, called {\tt elim}, performs case analysis. It is a
+simple consequence of {\tt unfold}. There is one case for each introduction
+rule. If $x\in\Fin(A)$ then either $x=\emptyset$ or else $x=\{a\}\un b$ for
+some $a\in A$ and $b\in\Fin(A)$. Formally, the elimination rule for $\Fin(A)$
+is written
+\[ \infer{Q}{x\in\Fin(A) & \infer*{Q}{[x=\emptyset]}
+ & \infer*{Q}{[x=\{a\}\un b & a\in A &b\in\Fin(A)]_{a,b}} }
+\]
+The subscripted variables $a$ and~$b$ above the third premise are
+eigenvariables, subject to the usual ``not free in \ldots'' proviso.
+
+
+\section{Induction and coinduction rules}
+Here we must consider inductive and coinductive definitions separately. For
+an inductive definition, the package returns an induction rule derived
+directly from the properties of least fixedpoints, as well as a modified rule
+for mutual recursion. For a coinductive definition, the package returns a
+basic coinduction rule.
+
+\subsection{The basic induction rule}\label{basic-ind-sec}
+The basic rule, called {\tt induct}, is appropriate in most situations.
+For inductive definitions, it is strong rule induction~\cite{camilleri92}; for
+datatype definitions (see below), it is just structural induction.
+
+The induction rule for an inductively defined set~$R$ has the form described
+below. For the time being, assume that $R$'s domain is not a Cartesian
+product; inductively defined relations are treated slightly differently.
+
+The major premise is $x\in R$. There is a minor premise for each
+introduction rule:
+\begin{itemize}
+\item If the introduction rule concludes $t\in R_i$, then the minor premise
+is~$P(t)$.
+
+\item The minor premise's eigenvariables are precisely the introduction
+rule's free variables that are not parameters of~$R$. For instance, the
+eigenvariables in the $\Fin(A)$ rule below are $a$ and $b$, but not~$A$.
+
+\item If the introduction rule has a premise $t\in R_i$, then the minor
+premise discharges the assumption $t\in R_i$ and the induction
+hypothesis~$P(t)$. If the introduction rule has a premise $t\in M(R_i)$
+then the minor premise discharges the single assumption
+\[ t\in M(\{z\in R_i. P(z)\}). \]
+Because $M$ is monotonic, this assumption implies $t\in M(R_i)$. The
+occurrence of $P$ gives the effect of an induction hypothesis, which may be
+exploited by appealing to properties of~$M$.
+\end{itemize}
+The induction rule for $\Fin(A)$ resembles the elimination rule shown above,
+but includes an induction hypothesis:
+\[ \infer{P(x)}{x\in\Fin(A) & P(\emptyset)
+ & \infer*{P(\{a\}\un b)}{[a\in A & b\in\Fin(A) & P(b)]_{a,b}} }
+\]
+Stronger induction rules often suggest themselves. We can derive a rule for
+$\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$.
+The package provides rules for mutual induction and inductive relations. The
+Isabelle/\textsc{zf} theory also supports well-founded induction and recursion
+over datatypes, by reasoning about the \defn{rank} of a
+set~\cite[\S3.4]{paulson-set-II}.
+
+
+\subsection{Modified induction rules}
+
+If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$
+(however nested), then the corresponding predicate $P_i$ takes $m$ arguments.
+The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$;
+the conclusion becomes $P(z_1,\ldots,z_m)$. This simplifies reasoning about
+inductively defined relations, eliminating the need to express properties of
+$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$.
+Occasionally it may require you to split up the induction variable
+using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt
+ split} appears in the rule.
+
+The mutual induction rule is called {\tt
+mutual\_induct}. It differs from the basic rule in two respects:
+\begin{itemize}
+\item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$,
+\ldots,~$P_n$: one for each recursive set.
+
+\item There is no major premise such as $x\in R_i$. Instead, the conclusion
+refers to all the recursive sets:
+\[ (\forall z.z\in R_1\imp P_1(z))\conj\cdots\conj
+ (\forall z.z\in R_n\imp P_n(z))
+\]
+Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,
+\ldots,~$n$.
+\end{itemize}
+%
+If the domain of some $R_i$ is a Cartesian product, then the mutual induction
+rule is modified accordingly. The predicates are made to take $m$ separate
+arguments instead of a tuple, and the quantification in the conclusion is over
+the separate variables $z_1$, \ldots, $z_m$.
+
+\subsection{Coinduction}\label{coind-sec}
+A coinductive definition yields a primitive coinduction rule, with no
+refinements such as those for the induction rules. (Experience may suggest
+refinements later.) Consider the codatatype of lazy lists as an example. For
+suitable definitions of $\LNil$ and $\LCons$, lazy lists may be defined as the
+greatest set consistent with the rules
+\[ \LNil\in\llist(A) \qquad
+ \infer[(-)]{\LCons(a,l)\in\llist(A)}{a\in A & l\in\llist(A)}
+\]
+The $(-)$ tag stresses that this is a coinductive definition. A suitable
+domain for $\llist(A)$ is $\quniv(A)$; this set is closed under the variant
+forms of sum and product that are used to represent non-well-founded data
+structures (see~\S\ref{univ-sec}).
+
+The package derives an {\tt unfold} theorem similar to that for $\Fin(A)$.
+Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$
+is the greatest solution to this equation contained in $\quniv(A)$:
+\[ \infer{x\in\llist(A)}{x\in X & X\sbs \quniv(A) &
+ \infer*{
+ \begin{array}[b]{r@{}l}
+ z=\LNil\disj
+ \bigl(\exists a\,l.\, & z=\LCons(a,l) \conj a\in A \conj{}\\
+ & l\in X\un\llist(A) \bigr)
+ \end{array} }{[z\in X]_z}}
+\]
+This rule complements the introduction rules; it provides a means of showing
+$x\in\llist(A)$ when $x$ is infinite. For instance, if $x=\LCons(0,x)$ then
+applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$. (Here $\nat$
+is the set of natural numbers.)
+
+Having $X\un\llist(A)$ instead of simply $X$ in the third premise above
+represents a slight strengthening of the greatest fixedpoint property. I
+discuss several forms of coinduction rules elsewhere~\cite{paulson-coind}.
+
+The clumsy form of the third premise makes the rule hard to use, especially in
+large definitions. Probably a constant should be declared to abbreviate the
+large disjunction, and rules derived to allow proving the separate disjuncts.
+
+
+\section{Examples of inductive and coinductive definitions}\label{ind-eg-sec}
+This section presents several examples from the literature: the finite
+powerset operator, lists of $n$ elements, bisimulations on lazy lists, the
+well-founded part of a relation, and the primitive recursive functions.
+
+\subsection{The finite powerset operator}
+This operator has been discussed extensively above. Here is the
+corresponding invocation in an Isabelle theory file. Note that
+$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/\textsc{zf}.
+\begin{ttbox}
+Finite = Arith +
+consts Fin :: i=>i
+inductive
+ domains "Fin(A)" <= "Pow(A)"
+ intrs
+ emptyI "0 : Fin(A)"
+ consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
+ type_intrs "[empty_subsetI, cons_subsetI, PowI]"
+ type_elims "[make_elim PowD]"
+end
+\end{ttbox}
+Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the
+unary function symbol~$\Fin$, which is defined inductively. Its domain is
+specified as $\pow(A)$, where $A$ is the parameter appearing in the
+introduction rules. For type-checking, we supply two introduction
+rules:
+\[ \emptyset\sbs A \qquad
+ \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C}
+\]
+A further introduction rule and an elimination rule express both
+directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking
+involves mostly introduction rules.
+
+Like all Isabelle theory files, this one yields a structure containing the
+new theory as an \textsc{ml} value. Structure {\tt Finite} also has a
+substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we
+can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs}
+or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
+rule is {\tt Fin.induct}.
+
+
+\subsection{Lists of $n$ elements}\label{listn-sec}
+This has become a standard example of an inductive definition. Following
+Paulin-Mohring~\cite{paulin-tlca}, we could attempt to define a new datatype
+$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
+But her introduction rules
+\[ \hbox{\tt Niln}\in\listn(A,0) \qquad
+ \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}
+ {n\in\nat & a\in A & l\in\listn(A,n)}
+\]
+are not acceptable to the inductive definition package:
+$\listn$ occurs with three different parameter lists in the definition.
+
+The Isabelle version of this example suggests a general treatment of
+varying parameters. It uses the existing datatype definition of
+$\lst(A)$, with constructors $\Nil$ and~$\Cons$, and incorporates the
+parameter~$n$ into the inductive set itself. It defines $\listn(A)$ as a
+relation consisting of pairs $\pair{n,l}$ such that $n\in\nat$
+and~$l\in\lst(A)$ and $l$ has length~$n$. In fact, $\listn(A)$ is the
+converse of the length function on~$\lst(A)$. The Isabelle/\textsc{zf} introduction
+rules are
+\[ \pair{0,\Nil}\in\listn(A) \qquad
+ \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)}
+ {a\in A & \pair{n,l}\in\listn(A)}
+\]
+The Isabelle theory file takes, as parent, the theory~{\tt List} of lists.
+We declare the constant~$\listn$ and supply an inductive definition,
+specifying the domain as $\nat\times\lst(A)$:
+\begin{ttbox}
+ListN = List +
+consts listn :: i=>i
+inductive
+ domains "listn(A)" <= "nat*list(A)"
+ intrs
+ NilI "<0,Nil>: listn(A)"
+ ConsI "[| a: A; <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
+ type_intrs "nat_typechecks @ list.intrs"
+end
+\end{ttbox}
+The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$.
+Because $\listn(A)$ is a set of pairs, type-checking requires the
+equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. The
+package always includes the rules for ordered pairs.
+
+The package returns introduction, elimination and induction rules for
+$\listn$. The basic induction rule, {\tt listn.induct}, is
+\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) &
+ \infer*{P(\succ(n),\Cons(a,l))}
+ {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}}
+\]
+This rule lets the induction formula to be a
+binary property of pairs, $P(n,l)$.
+It is now a simple matter to prove theorems about $\listn(A)$, such as
+\[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \]
+\[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \]
+This latter result --- here $r``X$ denotes the image of $X$ under $r$
+--- asserts that the inductive definition agrees with the obvious notion of
+$n$-element list.
+
+A ``list of $n$ elements'' really is a list, namely an element of ~$\lst(A)$.
+It is subject to list operators such as append (concatenation). For example,
+a trivial induction on $\pair{m,l}\in\listn(A)$ yields
+\[ \infer{\pair{m\mathbin{+} m',\, l@l'}\in\listn(A)}
+ {\pair{m,l}\in\listn(A) & \pair{m',l'}\in\listn(A)}
+\]
+where $+$ denotes addition on the natural numbers and @ denotes append.
+
+\subsection{Rule inversion: the function {\tt mk\_cases}}
+The elimination rule, {\tt listn.elim}, is cumbersome:
+\[ \infer{Q}{x\in\listn(A) &
+ \infer*{Q}{[x = \pair{0,\Nil}]} &
+ \infer*{Q}
+ {\left[\begin{array}{l}
+ x = \pair{\succ(n),\Cons(a,l)} \\
+ a\in A \\
+ \pair{n,l}\in\listn(A)
+ \end{array} \right]_{a,l,n}}}
+\]
+The \textsc{ml} function {\tt listn.mk\_cases} generates simplified instances of
+this rule. It works by freeness reasoning on the list constructors:
+$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$. If
+$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt listn.mk\_cases}
+deduces the corresponding form of~$i$; this is called rule inversion.
+Here is a sample session:
+\begin{ttbox}
+listn.mk_cases list.con_defs "<i,Nil> : listn(A)";
+{\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
+listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";
+{\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
+{\out !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
+{\out |] ==> ?Q" : thm}
+\end{ttbox}
+Each of these rules has only two premises. In conventional notation, the
+second rule is
+\[ \infer{Q}{\pair{i, \Cons(a,l)}\in\listn(A) &
+ \infer*{Q}
+ {\left[\begin{array}{l}
+ a\in A \\ \pair{n,l}\in\listn(A) \\ i = \succ(n)
+ \end{array} \right]_{n}}}
+\]
+The package also has built-in rules for freeness reasoning about $0$
+and~$\succ$. So if $x$ is $\pair{0,l}$ or $\pair{\succ(i),l}$, then {\tt
+listn.mk\_cases} can deduce the corresponding form of~$l$.
+
+The function {\tt mk\_cases} is also useful with datatype definitions. The
+instance from the definition of lists, namely {\tt list.mk\_cases}, can
+prove that $\Cons(a,l)\in\lst(A)$ implies $a\in A $ and $l\in\lst(A)$:
+\[ \infer{Q}{\Cons(a,l)\in\lst(A) &
+ & \infer*{Q}{[a\in A &l\in\lst(A)]} }
+\]
+A typical use of {\tt mk\_cases} concerns inductive definitions of evaluation
+relations. Then rule inversion yields case analysis on possible evaluations.
+For example, Isabelle/\textsc{zf} includes a short proof of the
+diamond property for parallel contraction on combinators. Ole Rasmussen used
+{\tt mk\_cases} extensively in his development of the theory of
+residuals~\cite{rasmussen95}.
+
+
+\subsection{A coinductive definition: bisimulations on lazy lists}
+This example anticipates the definition of the codatatype $\llist(A)$, which
+consists of finite and infinite lists over~$A$. Its constructors are $\LNil$
+and~$\LCons$, satisfying the introduction rules shown in~\S\ref{coind-sec}.
+Because $\llist(A)$ is defined as a greatest fixedpoint and uses the variant
+pairing and injection operators, it contains non-well-founded elements such as
+solutions to $\LCons(a,l)=l$.
+
+The next step in the development of lazy lists is to define a coinduction
+principle for proving equalities. This is done by showing that the equality
+relation on lazy lists is the greatest fixedpoint of some monotonic
+operation. The usual approach~\cite{pitts94} is to define some notion of
+bisimulation for lazy lists, define equivalence to be the greatest
+bisimulation, and finally to prove that two lazy lists are equivalent if and
+only if they are equal. The coinduction rule for equivalence then yields a
+coinduction principle for equalities.
+
+A binary relation $R$ on lazy lists is a \defn{bisimulation} provided $R\sbs
+R^+$, where $R^+$ is the relation
+\[ \{\pair{\LNil,\LNil}\} \un
+ \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}.
+\]
+A pair of lazy lists are \defn{equivalent} if they belong to some
+bisimulation. Equivalence can be coinductively defined as the greatest
+fixedpoint for the introduction rules
+\[ \pair{\LNil,\LNil} \in\lleq(A) \qquad
+ \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)}
+ {a\in A & \pair{l,l'}\in \lleq(A)}
+\]
+To make this coinductive definition, the theory file includes (after the
+declaration of $\llist(A)$) the following lines:
+\begin{ttbox}
+consts lleq :: i=>i
+coinductive
+ domains "lleq(A)" <= "llist(A) * llist(A)"
+ intrs
+ LNil "<LNil,LNil> : lleq(A)"
+ LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
+ type_intrs "llist.intrs"
+\end{ttbox}
+The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking
+rules include the introduction rules for $\llist(A)$, whose
+declaration is discussed below (\S\ref{lists-sec}).
+
+The package returns the introduction rules and the elimination rule, as
+usual. But instead of induction rules, it returns a coinduction rule.
+The rule is too big to display in the usual notation; its conclusion is
+$x\in\lleq(A)$ and its premises are $x\in X$,
+${X\sbs\llist(A)\times\llist(A)}$ and
+\[ \infer*{z=\pair{\LNil,\LNil}\disj \bigl(\exists a\,l\,l'.\,
+ \begin{array}[t]{@{}l}
+ z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\
+ \pair{l,l'}\in X\un\lleq(A) \bigr)
+ \end{array}
+ }{[z\in X]_z}
+\]
+Thus if $x\in X$, where $X$ is a bisimulation contained in the
+domain of $\lleq(A)$, then $x\in\lleq(A)$. It is easy to show that
+$\lleq(A)$ is reflexive: the equality relation is a bisimulation. And
+$\lleq(A)$ is symmetric: its converse is a bisimulation. But showing that
+$\lleq(A)$ coincides with the equality relation takes some work.
+
+\subsection{The accessible part of a relation}\label{acc-sec}
+Let $\prec$ be a binary relation on~$D$; in short, $(\prec)\sbs D\times D$.
+The \defn{accessible} or \defn{well-founded} part of~$\prec$, written
+$\acc(\prec)$, is essentially that subset of~$D$ for which $\prec$ admits
+no infinite decreasing chains~\cite{aczel77}. Formally, $\acc(\prec)$ is
+inductively defined to be the least set that contains $a$ if it contains
+all $\prec$-predecessors of~$a$, for $a\in D$. Thus we need an
+introduction rule of the form
+\[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
+Paulin-Mohring treats this example in Coq~\cite{paulin-tlca}, but it causes
+difficulties for other systems. Its premise is not acceptable to the
+inductive definition package of the Cambridge \textsc{hol}
+system~\cite{camilleri92}. It is also unacceptable to the Isabelle package
+(recall \S\ref{intro-sec}), but fortunately can be transformed into the
+acceptable form $t\in M(R)$.
+
+The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
+$t\sbs R$. This in turn is equivalent to $\forall y\in t. y\in R$. To
+express $\forall y.y\prec a\imp y\in\acc(\prec)$ we need only find a
+term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is
+the inverse image of~$\{a\}$ under~$\prec$.
+
+The definition below follows this approach. Here $r$ is~$\prec$ and
+$\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a
+relation is the union of its domain and range.) Finally $r^{-}``\{a\}$
+denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt
+ Pow\_mono}, which asserts that $\pow$ is monotonic.
+\begin{ttbox}
+consts acc :: i=>i
+inductive
+ domains "acc(r)" <= "field(r)"
+ intrs
+ vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
+ monos "[Pow_mono]"
+\end{ttbox}
+The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For
+instance, $\prec$ is well-founded if and only if its field is contained in
+$\acc(\prec)$.
+
+As mentioned in~\S\ref{basic-ind-sec}, a premise of the form $t\in M(R)$
+gives rise to an unusual induction hypothesis. Let us examine the
+induction rule, {\tt acc.induct}:
+\[ \infer{P(x)}{x\in\acc(r) &
+ \infer*{P(a)}{\left[
+ \begin{array}{r@{}l}
+ r^{-}``\{a\} &\, \in\pow(\{z\in\acc(r).P(z)\}) \\
+ a &\, \in\field(r)
+ \end{array}
+ \right]_a}}
+\]
+The strange induction hypothesis is equivalent to
+$\forall y. \pair{y,a}\in r\imp y\in\acc(r)\conj P(y)$.
+Therefore the rule expresses well-founded induction on the accessible part
+of~$\prec$.
+
+The use of inverse image is not essential. The Isabelle package can accept
+introduction rules with arbitrary premises of the form $\forall
+\vec{y}.P(\vec{y})\imp f(\vec{y})\in R$. The premise can be expressed
+equivalently as
+\[ \{z\in D. P(\vec{y}) \conj z=f(\vec{y})\} \in \pow(R) \]
+provided $f(\vec{y})\in D$ for all $\vec{y}$ such that~$P(\vec{y})$. The
+following section demonstrates another use of the premise $t\in M(R)$,
+where $M=\lst$.
+
+\subsection{The primitive recursive functions}\label{primrec-sec}
+The primitive recursive functions are traditionally defined inductively, as
+a subset of the functions over the natural numbers. One difficulty is that
+functions of all arities are taken together, but this is easily
+circumvented by regarding them as functions on lists. Another difficulty,
+the notion of composition, is less easily circumvented.
+
+Here is a more precise definition. Letting $\vec{x}$ abbreviate
+$x_0,\ldots,x_{n-1}$, we can write lists such as $[\vec{x}]$,
+$[y+1,\vec{x}]$, etc. A function is \defn{primitive recursive} if it
+belongs to the least set of functions in $\lst(\nat)\to\nat$ containing
+\begin{itemize}
+\item The \defn{successor} function $\SC$, such that $\SC[y,\vec{x}]=y+1$.
+\item All \defn{constant} functions $\CONST(k)$, such that
+ $\CONST(k)[\vec{x}]=k$.
+\item All \defn{projection} functions $\PROJ(i)$, such that
+ $\PROJ(i)[\vec{x}]=x_i$ if $0\leq i<n$.
+\item All \defn{compositions} $\COMP(g,[f_0,\ldots,f_{m-1}])$,
+where $g$ and $f_0$, \ldots, $f_{m-1}$ are primitive recursive,
+such that
+\[ \COMP(g,[f_0,\ldots,f_{m-1}])[\vec{x}] =
+ g[f_0[\vec{x}],\ldots,f_{m-1}[\vec{x}]]. \]
+
+\item All \defn{recursions} $\PREC(f,g)$, where $f$ and $g$ are primitive
+ recursive, such that
+\begin{eqnarray*}
+ \PREC(f,g)[0,\vec{x}] & = & f[\vec{x}] \\
+ \PREC(f,g)[y+1,\vec{x}] & = & g[\PREC(f,g)[y,\vec{x}],\, y,\, \vec{x}].
+\end{eqnarray*}
+\end{itemize}
+Composition is awkward because it combines not two functions, as is usual,
+but $m+1$ functions. In her proof that Ackermann's function is not
+primitive recursive, Nora Szasz was unable to formalize this definition
+directly~\cite{szasz93}. So she generalized primitive recursion to
+tuple-valued functions. This modified the inductive definition such that
+each operation on primitive recursive functions combined just two functions.
+
+\begin{figure}
+\begin{ttbox}
+Primrec = List +
+consts
+ primrec :: i
+ SC :: i
+ \(\vdots\)
+defs
+ SC_def "SC == lam l:list(nat).list_case(0, \%x xs.succ(x), l)"
+ \(\vdots\)
+inductive
+ domains "primrec" <= "list(nat)->nat"
+ intrs
+ SC "SC : primrec"
+ CONST "k: nat ==> CONST(k) : primrec"
+ PROJ "i: nat ==> PROJ(i) : primrec"
+ COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
+ PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
+ monos "[list_mono]"
+ con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
+ type_intrs "nat_typechecks @ list.intrs @
+ [lam_type, list_case_type, drop_type, map_type,
+ apply_type, rec_type]"
+end
+\end{ttbox}
+\hrule
+\caption{Inductive definition of the primitive recursive functions}
+\label{primrec-fig}
+\end{figure}
+\def\fs{{\it fs}}
+
+Szasz was using \textsc{alf}, but Coq and \textsc{hol} would also have
+problems accepting this definition. Isabelle's package accepts it easily
+since $[f_0,\ldots,f_{m-1}]$ is a list of primitive recursive functions and
+$\lst$ is monotonic. There are five introduction rules, one for each of the
+five forms of primitive recursive function. Let us examine the one for
+$\COMP$:
+\[ \infer{\COMP(g,\fs)\in\primrec}{g\in\primrec & \fs\in\lst(\primrec)} \]
+The induction rule for $\primrec$ has one case for each introduction rule.
+Due to the use of $\lst$ as a monotone operator, the composition case has
+an unusual induction hypothesis:
+ \[ \infer*{P(\COMP(g,\fs))}
+ {[g\in\primrec & \fs\in\lst(\{z\in\primrec.P(z)\})]_{\fs,g}}
+\]
+The hypothesis states that $\fs$ is a list of primitive recursive functions,
+each satisfying the induction formula. Proving the $\COMP$ case typically
+requires structural induction on lists, yielding two subcases: either
+$\fs=\Nil$ or else $\fs=\Cons(f,\fs')$, where $f\in\primrec$, $P(f)$, and
+$\fs'$ is another list of primitive recursive functions satisfying~$P$.
+
+Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec}
+defines the constants $\SC$, $\CONST$, etc. These are not constructors of
+a new datatype, but functions over lists of numbers. Their definitions,
+most of which are omitted, consist of routine list programming. In
+Isabelle/\textsc{zf}, the primitive recursive functions are defined as a subset of
+the function set $\lst(\nat)\to\nat$.
+
+The Isabelle theory goes on to formalize Ackermann's function and prove
+that it is not primitive recursive, using the induction rule {\tt
+ primrec.induct}. The proof follows Szasz's excellent account.
+
+
+\section{Datatypes and codatatypes}\label{data-sec}
+A (co)datatype definition is a (co)inductive definition with automatically
+defined constructors and a case analysis operator. The package proves that
+the case operator inverts the constructors and can prove freeness theorems
+involving any pair of constructors.
+
+
+\subsection{Constructors and their domain}\label{univ-sec}
+A (co)inductive definition selects a subset of an existing set; a (co)datatype
+definition creates a new set. The package reduces the latter to the former.
+Isabelle/\textsc{zf} supplies sets having strong closure properties to serve
+as domains for (co)inductive definitions.
+
+Isabelle/\textsc{zf} defines the Cartesian product $A\times
+B$, containing ordered pairs $\pair{a,b}$; it also defines the
+disjoint sum $A+B$, containing injections $\Inl(a)\equiv\pair{0,a}$ and
+$\Inr(b)\equiv\pair{1,b}$. For use below, define the $m$-tuple
+$\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$
+if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$.
+
+A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be
+$h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.
+In a mutually recursive definition, all constructors for the set~$R_i$ have
+the outer form~$h_{in}$, where $h_{in}$ is the injection described
+in~\S\ref{mutual-sec}. Further nested injections ensure that the
+constructors for~$R_i$ are pairwise distinct.
+
+Isabelle/\textsc{zf} defines the set $\univ(A)$, which contains~$A$ and
+furthermore contains $\pair{a,b}$, $\Inl(a)$ and $\Inr(b)$ for $a$,
+$b\in\univ(A)$. In a typical datatype definition with set parameters
+$A_1$, \ldots, $A_k$, a suitable domain for all the recursive sets is
+$\univ(A_1\un\cdots\un A_k)$. This solves the problem for
+datatypes~\cite[\S4.2]{paulson-set-II}.
+
+The standard pairs and injections can only yield well-founded
+constructions. This eases the (manual!) definition of recursive functions
+over datatypes. But they are unsuitable for codatatypes, which typically
+contain non-well-founded objects.
+
+To support codatatypes, Isabelle/\textsc{zf} defines a variant notion of
+ordered pair, written~$\pair{a;b}$. It also defines the corresponding variant
+notion of Cartesian product $A\otimes B$, variant injections $\QInl(a)$
+and~$\QInr(b)$ and variant disjoint sum $A\oplus B$. Finally it defines the
+set $\quniv(A)$, which contains~$A$ and furthermore contains $\pair{a;b}$,
+$\QInl(a)$ and $\QInr(b)$ for $a$, $b\in\quniv(A)$. In a typical codatatype
+definition with set parameters $A_1$, \ldots, $A_k$, a suitable domain is
+$\quniv(A_1\un\cdots\un A_k)$. Details are published
+elsewhere~\cite{paulson-final}.
+
+\subsection{The case analysis operator}
+The (co)datatype package automatically defines a case analysis operator,
+called {\tt$R$\_case}. A mutually recursive definition still has only one
+operator, whose name combines those of the recursive sets: it is called
+{\tt$R_1$\_\ldots\_$R_n$\_case}. The case operator is analogous to those
+for products and sums.
+
+Datatype definitions employ standard products and sums, whose operators are
+$\split$ and $\case$ and satisfy the equations
+\begin{eqnarray*}
+ \split(f,\pair{x,y}) & = & f(x,y) \\
+ \case(f,g,\Inl(x)) & = & f(x) \\
+ \case(f,g,\Inr(y)) & = & g(y)
+\end{eqnarray*}
+Suppose the datatype has $k$ constructors $\Con_1$, \ldots,~$\Con_k$. Then
+its case operator takes $k+1$ arguments and satisfies an equation for each
+constructor:
+\[ R\hbox{\_case}(f_1,\ldots,f_k, {\tt Con}_i(\vec{x})) = f_i(\vec{x}),
+ \qquad i = 1, \ldots, k
+\]
+The case operator's definition takes advantage of Isabelle's representation of
+syntax in the typed $\lambda$-calculus; it could readily be adapted to a
+theorem prover for higher-order logic. If $f$ and~$g$ have meta-type $i\To i$
+then so do $\split(f)$ and $\case(f,g)$. This works because $\split$ and
+$\case$ operate on their last argument. They are easily combined to make
+complex case analysis operators. For example, $\case(f,\case(g,h))$ performs
+case analysis for $A+(B+C)$; let us verify one of the three equations:
+\[ \case(f,\case(g,h), \Inr(\Inl(b))) = \case(g,h,\Inl(b)) = g(b) \]
+Codatatype definitions are treated in precisely the same way. They express
+case operators using those for the variant products and sums, namely
+$\qsplit$ and~$\qcase$.
+
+\medskip
+
+To see how constructors and the case analysis operator are defined, let us
+examine some examples. Further details are available
+elsewhere~\cite{paulson-set-II}.
+
+
+\subsection{Example: lists and lazy lists}\label{lists-sec}
+Here is a declaration of the datatype of lists, as it might appear in a theory
+file:
+\begin{ttbox}
+consts list :: i=>i
+datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")
+\end{ttbox}
+And here is a declaration of the codatatype of lazy lists:
+\begin{ttbox}
+consts llist :: i=>i
+codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
+\end{ttbox}
+
+Each form of list has two constructors, one for the empty list and one for
+adding an element to a list. Each takes a parameter, defining the set of
+lists over a given set~$A$. Each is automatically given the appropriate
+domain: $\univ(A)$ for $\lst(A)$ and $\quniv(A)$ for $\llist(A)$. The default
+can be overridden.
+
+\ifshort
+Now $\lst(A)$ is a datatype and enjoys the usual induction rule.
+\else
+Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt
+ list.induct}:
+\[ \infer{P(x)}{x\in\lst(A) & P(\Nil)
+ & \infer*{P(\Cons(a,l))}{[a\in A & l\in\lst(A) & P(l)]_{a,l}} }
+\]
+Induction and freeness yield the law $l\not=\Cons(a,l)$. To strengthen this,
+Isabelle/\textsc{zf} defines the rank of a set and proves that the standard
+pairs and injections have greater rank than their components. An immediate
+consequence, which justifies structural recursion on lists
+\cite[\S4.3]{paulson-set-II}, is
+\[ \rank(l) < \rank(\Cons(a,l)). \]
+\par
+\fi
+But $\llist(A)$ is a codatatype and has no induction rule. Instead it has
+the coinduction rule shown in \S\ref{coind-sec}. Since variant pairs and
+injections are monotonic and need not have greater rank than their
+components, fixedpoint operators can create cyclic constructions. For
+example, the definition
+\[ \lconst(a) \equiv \lfp(\univ(a), \lambda l. \LCons(a,l)) \]
+yields $\lconst(a) = \LCons(a,\lconst(a))$.
+
+\ifshort
+\typeout{****SHORT VERSION}
+\typeout{****Omitting discussion of constructors!}
+\else
+\medskip
+It may be instructive to examine the definitions of the constructors and
+case operator for $\lst(A)$. The definitions for $\llist(A)$ are similar.
+The list constructors are defined as follows:
+\begin{eqnarray*}
+ \Nil & \equiv & \Inl(\emptyset) \\
+ \Cons(a,l) & \equiv & \Inr(\pair{a,l})
+\end{eqnarray*}
+The operator $\lstcase$ performs case analysis on these two alternatives:
+\[ \lstcase(c,h) \equiv \case(\lambda u.c, \split(h)) \]
+Let us verify the two equations:
+\begin{eqnarray*}
+ \lstcase(c, h, \Nil) & = &
+ \case(\lambda u.c, \split(h), \Inl(\emptyset)) \\
+ & = & (\lambda u.c)(\emptyset) \\
+ & = & c\\[1ex]
+ \lstcase(c, h, \Cons(x,y)) & = &
+ \case(\lambda u.c, \split(h), \Inr(\pair{x,y})) \\
+ & = & \split(h, \pair{x,y}) \\
+ & = & h(x,y)
+\end{eqnarray*}
+\fi
+
+
+\ifshort
+\typeout{****Omitting mutual recursion example!}
+\else
+\subsection{Example: mutual recursion}
+In mutually recursive trees and forests~\cite[\S4.5]{paulson-set-II}, trees
+have the one constructor $\Tcons$, while forests have the two constructors
+$\Fnil$ and~$\Fcons$:
+\begin{ttbox}
+consts tree, forest, tree_forest :: i=>i
+datatype "tree(A)" = Tcons ("a: A", "f: forest(A)")
+and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
+\end{ttbox}
+The three introduction rules define the mutual recursion. The
+distinguishing feature of this example is its two induction rules.
+
+The basic induction rule is called {\tt tree\_forest.induct}:
+\[ \infer{P(x)}{x\in\TF(A) &
+ \infer*{P(\Tcons(a,f))}
+ {\left[\begin{array}{l} a\in A \\
+ f\in\forest(A) \\ P(f)
+ \end{array}
+ \right]_{a,f}}
+ & P(\Fnil)
+ & \infer*{P(\Fcons(t,f))}
+ {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
+ f\in\forest(A) \\ P(f)
+ \end{array}
+ \right]_{t,f}} }
+\]
+This rule establishes a single predicate for $\TF(A)$, the union of the
+recursive sets. Although such reasoning is sometimes useful
+\cite[\S4.5]{paulson-set-II}, a proper mutual induction rule should establish
+separate predicates for $\tree(A)$ and $\forest(A)$. The package calls this
+rule {\tt tree\_forest.mutual\_induct}. Observe the usage of $P$ and $Q$ in
+the induction hypotheses:
+\[ \infer{(\forall z. z\in\tree(A)\imp P(z)) \conj
+ (\forall z. z\in\forest(A)\imp Q(z))}
+ {\infer*{P(\Tcons(a,f))}
+ {\left[\begin{array}{l} a\in A \\
+ f\in\forest(A) \\ Q(f)
+ \end{array}
+ \right]_{a,f}}
+ & Q(\Fnil)
+ & \infer*{Q(\Fcons(t,f))}
+ {\left[\begin{array}{l} t\in\tree(A) \\ P(t) \\
+ f\in\forest(A) \\ Q(f)
+ \end{array}
+ \right]_{t,f}} }
+\]
+Elsewhere I describe how to define mutually recursive functions over trees and
+forests \cite[\S4.5]{paulson-set-II}.
+
+Both forest constructors have the form $\Inr(\cdots)$,
+while the tree constructor has the form $\Inl(\cdots)$. This pattern would
+hold regardless of how many tree or forest constructors there were.
+\begin{eqnarray*}
+ \Tcons(a,l) & \equiv & \Inl(\pair{a,l}) \\
+ \Fnil & \equiv & \Inr(\Inl(\emptyset)) \\
+ \Fcons(a,l) & \equiv & \Inr(\Inr(\pair{a,l}))
+\end{eqnarray*}
+There is only one case operator; it works on the union of the trees and
+forests:
+\[ {\tt tree\_forest\_case}(f,c,g) \equiv
+ \case(\split(f),\, \case(\lambda u.c, \split(g)))
+\]
+\fi
+
+
+\subsection{Example: a four-constructor datatype}
+A bigger datatype will illustrate some efficiency
+refinements. It has four constructors $\Con_0$, \ldots, $\Con_3$, with the
+corresponding arities.
+\begin{ttbox}
+consts data :: [i,i] => i
+datatype "data(A,B)" = Con0
+ | Con1 ("a: A")
+ | Con2 ("a: A", "b: B")
+ | Con3 ("a: A", "b: B", "d: data(A,B)")
+\end{ttbox}
+Because this datatype has two set parameters, $A$ and~$B$, the package
+automatically supplies $\univ(A\un B)$ as its domain. The structural
+induction rule has four minor premises, one per constructor, and only the last
+has an induction hypothesis. (Details are left to the reader.)
+
+The constructors are defined by the equations
+\begin{eqnarray*}
+ \Con_0 & \equiv & \Inl(\Inl(\emptyset)) \\
+ \Con_1(a) & \equiv & \Inl(\Inr(a)) \\
+ \Con_2(a,b) & \equiv & \Inr(\Inl(\pair{a,b})) \\
+ \Con_3(a,b,c) & \equiv & \Inr(\Inr(\pair{a,b,c})).
+\end{eqnarray*}
+The case analysis operator is
+\[ {\tt data\_case}(f_0,f_1,f_2,f_3) \equiv
+ \case(\begin{array}[t]{@{}l}
+ \case(\lambda u.f_0,\; f_1),\, \\
+ \case(\split(f_2),\; \split(\lambda v.\split(f_3(v)))) )
+ \end{array}
+\]
+This may look cryptic, but the case equations are trivial to verify.
+
+In the constructor definitions, the injections are balanced. A more naive
+approach is to define $\Con_3(a,b,c)$ as $\Inr(\Inr(\Inr(\pair{a,b,c})))$;
+instead, each constructor has two injections. The difference here is small.
+But the \textsc{zf} examples include a 60-element enumeration type, where each
+constructor has 5 or~6 injections. The naive approach would require 1 to~59
+injections; the definitions would be quadratic in size. It is like the
+advantage of binary notation over unary.
+
+The result structure contains the case operator and constructor definitions as
+the theorem list \verb|con_defs|. It contains the case equations, such as
+\[ {\tt data\_case}(f_0,f_1,f_2,f_3,\Con_3(a,b,c)) = f_3(a,b,c), \]
+as the theorem list \verb|case_eqns|. There is one equation per constructor.
+
+\subsection{Proving freeness theorems}
+There are two kinds of freeness theorems:
+\begin{itemize}
+\item \defn{injectiveness} theorems, such as
+\[ \Con_2(a,b) = \Con_2(a',b') \bimp a=a' \conj b=b' \]
+
+\item \defn{distinctness} theorems, such as
+\[ \Con_1(a) \not= \Con_2(a',b') \]
+\end{itemize}
+Since the number of such theorems is quadratic in the number of constructors,
+the package does not attempt to prove them all. Instead it returns tools for
+proving desired theorems --- either manually or during
+simplification or classical reasoning.
+
+The theorem list \verb|free_iffs| enables the simplifier to perform freeness
+reasoning. This works by incremental unfolding of constructors that appear in
+equations. The theorem list contains logical equivalences such as
+\begin{eqnarray*}
+ \Con_0=c & \bimp & c=\Inl(\Inl(\emptyset)) \\
+ \Con_1(a)=c & \bimp & c=\Inl(\Inr(a)) \\
+ & \vdots & \\
+ \Inl(a)=\Inl(b) & \bimp & a=b \\
+ \Inl(a)=\Inr(b) & \bimp & {\tt False} \\
+ \pair{a,b} = \pair{a',b'} & \bimp & a=a' \conj b=b'
+\end{eqnarray*}
+For example, these rewrite $\Con_1(a)=\Con_1(b)$ to $a=b$ in four steps.
+
+The theorem list \verb|free_SEs| enables the classical
+reasoner to perform similar replacements. It consists of elimination rules
+to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the
+assumptions.
+
+Such incremental unfolding combines freeness reasoning with other proof
+steps. It has the unfortunate side-effect of unfolding definitions of
+constructors in contexts such as $\exists x.\Con_1(a)=x$, where they should
+be left alone. Calling the Isabelle tactic {\tt fold\_tac con\_defs}
+restores the defined constants.
+
+
+\section{Related work}\label{related}
+The use of least fixedpoints to express inductive definitions seems
+obvious. Why, then, has this technique so seldom been implemented?
+
+Most automated logics can only express inductive definitions by asserting
+axioms. Little would be left of Boyer and Moore's logic~\cite{bm79} if their
+shell principle were removed. With \textsc{alf} the situation is more
+complex; earlier versions of Martin-L\"of's type theory could (using
+wellordering types) express datatype definitions, but the version underlying
+\textsc{alf} requires new rules for each definition~\cite{dybjer91}. With Coq
+the situation is subtler still; its underlying Calculus of Constructions can
+express inductive definitions~\cite{huet88}, but cannot quite handle datatype
+definitions~\cite{paulin-tlca}. It seems that researchers tried hard to
+circumvent these problems before finally extending the Calculus with rule
+schemes for strictly positive operators. Recently Gim{\'e}nez has extended
+the Calculus of Constructions with inductive and coinductive
+types~\cite{gimenez-codifying}, with mechanized support in Coq.
+
+Higher-order logic can express inductive definitions through quantification
+over unary predicates. The following formula expresses that~$i$ belongs to the
+least set containing~0 and closed under~$\succ$:
+\[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \]
+This technique can be used to prove the Knaster-Tarski theorem, which (in its
+general form) is little used in the Cambridge \textsc{hol} system.
+Melham~\cite{melham89} describes the development. The natural numbers are
+defined as shown above, but lists are defined as functions over the natural
+numbers. Unlabelled trees are defined using G\"odel numbering; a labelled
+tree consists of an unlabelled tree paired with a list of labels. Melham's
+datatype package expresses the user's datatypes in terms of labelled trees.
+It has been highly successful, but a fixedpoint approach might have yielded
+greater power with less effort.
+
+Elsa Gunter~\cite{gunter-trees} reports an ongoing project to generalize the
+Cambridge \textsc{hol} system with mutual recursion and infinitely-branching
+trees. She retains many features of Melham's approach.
+
+Melham's inductive definition package~\cite{camilleri92} also uses
+quantification over predicates. But instead of formalizing the notion of
+monotone function, it requires definitions to consist of finitary rules, a
+syntactic form that excludes many monotone inductive definitions.
+
+\textsc{pvs}~\cite{pvs-language} is another proof assistant based on
+higher-order logic. It supports both inductive definitions and datatypes,
+apparently by asserting axioms. Datatypes may not be iterated in general, but
+may use recursion over the built-in $\lst$ type.
+
+The earliest use of least fixedpoints is probably Robin Milner's. Brian
+Monahan extended this package considerably~\cite{monahan84}, as did I in
+unpublished work.\footnote{The datatype package described in my \textsc{lcf}
+ book~\cite{paulson87} does {\it not\/} make definitions, but merely asserts
+ axioms.} \textsc{lcf} is a first-order logic of domain theory; the relevant
+fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of
+continuous functions over domains. \textsc{lcf} is too weak to express
+recursive predicates. The Isabelle package might be the first to be based on
+the Knaster-Tarski theorem.
+
+
+\section{Conclusions and future work}
+Higher-order logic and set theory are both powerful enough to express
+inductive definitions. A growing number of theorem provers implement one
+of these~\cite{IMPS,saaltink-fme}. The easiest sort of inductive
+definition package to write is one that asserts new axioms, not one that
+makes definitions and proves theorems about them. But asserting axioms
+could introduce unsoundness.
+
+The fixedpoint approach makes it fairly easy to implement a package for
+(co)in\-duc\-tive definitions that does not assert axioms. It is efficient:
+it processes most definitions in seconds and even a 60-constructor datatype
+requires only a few minutes. It is also simple: The first working version took
+under a week to code, consisting of under 1100 lines (35K bytes) of Standard
+\textsc{ml}.
+
+In set theory, care is needed to ensure that the inductive definition yields
+a set (rather than a proper class). This problem is inherent to set theory,
+whether or not the Knaster-Tarski theorem is employed. We must exhibit a
+bounding set (called a domain above). For inductive definitions, this is
+often trivial. For datatype definitions, I have had to formalize much set
+theory. To justify infinitely-branching datatype definitions, I have had to
+develop a theory of cardinal arithmetic~\cite{paulson-gr}, such as the theorem
+that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for all
+$\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
+The need for such efforts is not a drawback of the fixedpoint approach, for
+the alternative is to take such definitions on faith.
+
+Care is also needed to ensure that the greatest fixedpoint really yields a
+coinductive definition. In set theory, standard pairs admit only well-founded
+constructions. Aczel's anti-foundation axiom~\cite{aczel88} could be used to
+get non-well-founded objects, but it does not seem easy to mechanize.
+Isabelle/\textsc{zf} instead uses a variant notion of ordered pairing, which
+can be generalized to a variant notion of function. Elsewhere I have
+proved that this simple approach works (yielding final coalgebras) for a broad
+class of definitions~\cite{paulson-final}.
+
+Several large studies make heavy use of inductive definitions. L\"otzbeyer
+and Sandner have formalized two chapters of a semantics book~\cite{winskel93},
+proving the equivalence between the operational and denotational semantics of
+a simple imperative language. A single theory file contains three datatype
+definitions (of arithmetic expressions, boolean expressions and commands) and
+three inductive definitions (the corresponding operational rules). Using
+different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
+have both proved the Church-Rosser theorem; inductive definitions specify
+several reduction relations on $\lambda$-terms. Recently, I have applied
+inductive definitions to the analysis of cryptographic
+protocols~\cite{paulson-markt}.
+
+To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
+consistency of the dynamic and static semantics for a small functional
+language. The example is due to Milner and Tofte~\cite{milner-coind}. It
+concerns an extended correspondence relation, which is defined coinductively.
+A codatatype definition specifies values and value environments in mutual
+recursion. Non-well-founded values represent recursive functions. Value
+environments are variant functions from variables into values. This one key
+definition uses most of the package's novel features.
+
+The approach is not restricted to set theory. It should be suitable for any
+logic that has some notion of set and the Knaster-Tarski theorem. I have
+ported the (co)inductive definition package from Isabelle/\textsc{zf} to
+Isabelle/\textsc{hol} (higher-order logic). V\"olker~\cite{voelker95}
+is investigating how to port the (co)datatype package. \textsc{hol}
+represents sets by unary predicates; defining the corresponding types may
+cause complications.
+
+
+\begin{footnotesize}
+\bibliographystyle{springer}
+\bibliography{string-abbrv,atp,theory,funprog,isabelle,crossref}
+\end{footnotesize}
+%%%%%\doendnotes
+
+\ifshort\typeout{****Omitting appendices}
+\else
+\newpage
+\appendix
+\section{Inductive and coinductive definitions: users guide}
+A theory file may contain any number of inductive and coinductive
+definitions. They may be intermixed with other declarations; in
+particular, the (co)inductive sets \defn{must} be declared separately as
+constants, and may have mixfix syntax or be subject to syntax translations.
+
+The syntax is rather complicated. Please consult the examples above and the
+theory files on the \textsc{zf} source directory.
+
+Each (co)inductive definition adds definitions to the theory and also proves
+some theorems. Each definition creates an \textsc{ml} structure, which is a
+substructure of the main theory structure.
+
+Inductive and datatype definitions can take up considerable storage. The
+introduction rules are replicated in slightly different forms as fixedpoint
+definitions, elimination rules and induction rules. L\"otzbeyer and Sandner's
+six definitions occupy over 600K in total. Defining the 60-constructor
+datatype requires nearly 560K\@.
+
+\subsection{The result structure}
+Many of the result structure's components have been discussed
+in~\S\ref{basic-sec}; others are self-explanatory.
+\begin{description}
+\item[\tt thy] is the new theory containing the recursive sets.
+
+\item[\tt defs] is the list of definitions of the recursive sets.
+
+\item[\tt bnd\_mono] is a monotonicity theorem for the fixedpoint operator.
+
+\item[\tt dom\_subset] is a theorem stating inclusion in the domain.
+
+\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
+the recursive sets. The rules are also available individually, using the
+names given them in the theory file.
+
+\item[\tt elim] is the elimination rule.
+
+\item[\tt mk\_cases] is a function to create simplified instances of {\tt
+elim}, using freeness reasoning on some underlying datatype.
+\end{description}
+
+For an inductive definition, the result structure contains two induction
+rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter
+rule is just {\tt True} unless more than one set is being defined.) For a
+coinductive definition, it contains the rule \verb|coinduct|.
+
+Figure~\ref{def-result-fig} summarizes the two result signatures,
+specifying the types of all these components.
+
+\begin{figure}
+\begin{ttbox}
+sig
+val thy : theory
+val defs : thm list
+val bnd_mono : thm
+val dom_subset : thm
+val intrs : thm list
+val elim : thm
+val mk_cases : thm list -> string -> thm
+{\it(Inductive definitions only)}
+val induct : thm
+val mutual_induct: thm
+{\it(Coinductive definitions only)}
+val coinduct : thm
+end
+\end{ttbox}
+\hrule
+\caption{The result of a (co)inductive definition} \label{def-result-fig}
+\end{figure}
+
+\subsection{The syntax of a (co)inductive definition}
+An inductive definition has the form
+\begin{ttbox}
+inductive
+ domains {\it domain declarations}
+ intrs {\it introduction rules}
+ monos {\it monotonicity theorems}
+ con_defs {\it constructor definitions}
+ type_intrs {\it introduction rules for type-checking}
+ type_elims {\it elimination rules for type-checking}
+\end{ttbox}
+A coinductive definition is identical, but starts with the keyword
+{\tt coinductive}.
+
+The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
+sections are optional. If present, each is specified as a string, which
+must be a valid \textsc{ml} expression of type {\tt thm list}. It is simply
+inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger
+\textsc{ml} error messages. You can then inspect the file on your directory.
+
+\begin{description}
+\item[\it domain declarations] consist of one or more items of the form
+ {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
+ its domain.
+
+\item[\it introduction rules] specify one or more introduction rules in
+ the form {\it ident\/}~{\it string}, where the identifier gives the name of
+ the rule in the result structure.
+
+\item[\it monotonicity theorems] are required for each operator applied to
+ a recursive set in the introduction rules. There \defn{must} be a theorem
+ of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$
+ in an introduction rule!
+
+\item[\it constructor definitions] contain definitions of constants
+ appearing in the introduction rules. The (co)datatype package supplies
+ the constructors' definitions here. Most (co)inductive definitions omit
+ this section; one exception is the primitive recursive functions example
+ (\S\ref{primrec-sec}).
+
+\item[\it type\_intrs] consists of introduction rules for type-checking the
+ definition, as discussed in~\S\ref{basic-sec}. They are applied using
+ depth-first search; you can trace the proof by setting
+
+ \verb|trace_DEPTH_FIRST := true|.
+
+\item[\it type\_elims] consists of elimination rules for type-checking the
+ definition. They are presumed to be safe and are applied as much as
+ possible, prior to the {\tt type\_intrs} search.
+\end{description}
+
+The package has a few notable restrictions:
+\begin{itemize}
+\item The theory must separately declare the recursive sets as
+ constants.
+
+\item The names of the recursive sets must be identifiers, not infix
+operators.
+
+\item Side-conditions must not be conjunctions. However, an introduction rule
+may contain any number of side-conditions.
+
+\item Side-conditions of the form $x=t$, where the variable~$x$ does not
+ occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
+\end{itemize}
+
+Isabelle/\textsc{hol} uses a simplified syntax for inductive definitions,
+thanks to type-checking. There are no \texttt{domains}, \texttt{type\_intrs}
+or \texttt{type\_elims} parts.
+
+
+\section{Datatype and codatatype definitions: users guide}
+This section explains how to include (co)datatype declarations in a theory
+file. Please include {\tt Datatype} as a parent theory; this makes available
+the definitions of $\univ$ and $\quniv$.
+
+
+\subsection{The result structure}
+The result structure extends that of (co)inductive definitions
+(Figure~\ref{def-result-fig}) with several additional items:
+\begin{ttbox}
+val con_defs : thm list
+val case_eqns : thm list
+val free_iffs : thm list
+val free_SEs : thm list
+val mk_free : string -> thm
+\end{ttbox}
+Most of these have been discussed in~\S\ref{data-sec}. Here is a summary:
+\begin{description}
+\item[\tt con\_defs] is a list of definitions: the case operator followed by
+the constructors. This theorem list can be supplied to \verb|mk_cases|, for
+example.
+
+\item[\tt case\_eqns] is a list of equations, stating that the case operator
+inverts each constructor.
+
+\item[\tt free\_iffs] is a list of logical equivalences to perform freeness
+reasoning by rewriting. A typical application has the form
+\begin{ttbox}
+by (asm_simp_tac (ZF_ss addsimps free_iffs) 1);
+\end{ttbox}
+
+\item[\tt free\_SEs] is a list of safe elimination rules to perform freeness
+reasoning. It can be supplied to \verb|eresolve_tac| or to the classical
+reasoner:
+\begin{ttbox}
+by (fast_tac (ZF_cs addSEs free_SEs) 1);
+\end{ttbox}
+
+\item[\tt mk\_free] is a function to prove freeness properties, specified as
+strings. The theorems can be expressed in various forms, such as logical
+equivalences or elimination rules.
+\end{description}
+
+The result structure also inherits everything from the underlying
+(co)inductive definition, such as the introduction rules, elimination rule,
+and (co)induction rule.
+
+
+\subsection{The syntax of a (co)datatype definition}
+A datatype definition has the form
+\begin{ttbox}
+datatype <={\it domain}
+ {\it datatype declaration} and {\it datatype declaration} and \ldots
+ monos {\it monotonicity theorems}
+ type_intrs {\it introduction rules for type-checking}
+ type_elims {\it elimination rules for type-checking}
+\end{ttbox}
+A codatatype definition is identical save that it starts with the keyword {\tt
+ codatatype}.
+
+The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are
+optional. They are treated like their counterparts in a (co)inductive
+definition, as described above. The package supplements your type-checking
+rules (if any) with additional ones that should cope with any
+finitely-branching (co)datatype definition.
+
+\begin{description}
+\item[\it domain] specifies a single domain to use for all the mutually
+ recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are
+ omitted, the package supplies a domain automatically. Suppose the
+ definition involves the set parameters $A_1$, \ldots, $A_k$. Then
+ $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and
+ $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition.
+
+ These choices should work for all finitely-branching (co)datatype
+ definitions. For examples of infinitely-branching datatypes,
+ see file {\tt ZF/ex/Brouwer.thy}.
+
+\item[\it datatype declaration] has the form
+\begin{quote}
+ {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|}
+ \ldots
+\end{quote}
+The {\it string\/} is the datatype, say {\tt"list(A)"}. Each
+{\it constructor\/} has the form
+\begin{quote}
+ {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)}
+ {\it mixfix\/}
+\end{quote}
+The {\it name\/} specifies a new constructor while the {\it premises\/} its
+typing conditions. The optional {\it mixfix\/} phrase may give
+the constructor infix, for example.
+
+Mutually recursive {\it datatype declarations\/} are separated by the
+keyword~{\tt and}.
+\end{description}
+
+Isabelle/\textsc{hol}'s datatype definition package is (as of this writing)
+entirely different from Isabelle/\textsc{zf}'s. The syntax is different, and
+instead of making an inductive definition it asserts axioms.
+
+\paragraph*{Note.}
+In the definitions of the constructors, the right-hand sides may overlap.
+For instance, the datatype of combinators has constructors defined by
+\begin{eqnarray*}
+ {\tt K} & \equiv & \Inl(\emptyset) \\
+ {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\
+ p{\tt\#}q & \equiv & \Inr(\Inl(\pair{p,q}))
+\end{eqnarray*}
+Unlike in previous versions of Isabelle, \verb|fold_tac| now ensures that the
+longest right-hand sides are folded first.
+
+\fi
+\end{document}