\documentstyle[12pt,a4,proof,iman,alltt]{article}

 \documentstyle[a4,proof,iman,extra,times]{llncs}

 \hyphenation{data-type}

 %Repetition in the two sentences that begin ``The powerset operator''

 %CADE version should use 11pt and the Springer style

 \CADEfalse

 \CADEtrue

 \title{A Fixedpoint Approach to Implementing (Co)Inductive

 \title{A Fixedpoint Approach to Implementing\\ 

    Definitions\thanks{Jim Grundy and Simon Thompson made detailed comments on

   (Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed

    a draft.  Research funded by the SERC (grants GR/G53279,

     comments; the referees were also helpful.  Research funded by

     GR/H40570) and by the ESPRIT Basic Research Action 6453 `Types'.}}

     SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453

     `Types'.}}

 \author{{\em Lawrence C. Paulson}\\ 

         Computer Laboratory, University of Cambridge}

 \author{Lawrence C. Paulson\\{\tt lcp@cl.cam.ac.uk}}

 \institute{Computer Laboratory, University of Cambridge, England}

 %%%\newcommand\Pow{{\tt Pow}}

 \newcommand\pow{{\cal P}}

 \let\pow=\wp

 %%%\let\pow=\wp

 \newcommand\RepFun{{\tt RepFun}}

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

 \newcommand\cons{{\tt cons}}

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

 \def\succ{{\tt succ}}

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

 \newcommand\split{{\tt split}}

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

 \newcommand\fst{{\tt fst}}

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

 \newcommand\snd{{\tt snd}}

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

 \newcommand\converse{{\tt converse}}

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

 \newcommand\domain{{\tt domain}}

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

 \newcommand\range{{\tt range}}

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

 \newcommand\field{{\tt field}}

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

 \newcommand\bndmono{\hbox{\tt bnd\_mono}}

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

 \newcommand\lfp{{\tt lfp}}

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

 \newcommand\gfp{{\tt gfp}}

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

 \newcommand\id{{\tt id}}

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

 \newcommand\trans{{\tt trans}}

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

 \newcommand\wf{{\tt wf}}

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

 \newcommand\wfrec{\hbox{\tt wfrec}}

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

 \newcommand\nat{{\tt nat}}

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

 \newcommand\natcase{\hbox{\tt nat\_case}}

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

 \newcommand\transrec{{\tt transrec}}

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

 \newcommand\rank{{\tt rank}}

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

 \newcommand\univ{{\tt univ}}

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

 \newcommand\Vrec{{\tt Vrec}}

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

 \newcommand\Inl{{\tt Inl}}

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

 \newcommand\Inr{{\tt Inr}}

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

 \newcommand\case{{\tt case}}

 \newcommand\lst{{\tt list}}

 \newcommand\Nil{{\tt Nil}}

 \newcommand\Cons{{\tt Cons}}

 \newcommand\length{{\tt length}}

 \newcommand\length{\hbox{\tt length}}

 \newcommand\listn{{\tt listn}}

 \newcommand\listn{\hbox{\tt listn}}

 \newcommand\acc{{\tt acc}}

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

 \newcommand\primrec{{\tt primrec}}

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

 \newcommand\SC{{\tt SC}}

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

 \newcommand\CONST{{\tt CONST}}

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

 \newcommand\PROJ{{\tt PROJ}}

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

 \newcommand\COMP{{\tt COMP}}

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

 \newcommand\PREC{{\tt PREC}}

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

 \newcommand\quniv{{\tt quniv}}

 \newcommand\quniv{\hbox{\tt quniv}}

 \newcommand\llist{{\tt llist}}

 \newcommand\llist{\hbox{\tt llist}}

 \newcommand\LNil{{\tt LNil}}

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

 \newcommand\LCons{{\tt LCons}}

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

 \newcommand\lconst{{\tt lconst}}

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

 \newcommand\lleq{{\tt lleq}}

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

 \newcommand\map{{\tt map}}

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

 \newcommand\term{{\tt term}}

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

 \newcommand\Apply{{\tt Apply}}

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

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

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

 \newcommand\rev{{\tt rev}}

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

 \newcommand\reflect{{\tt reflect}}

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

 \newcommand\tree{{\tt tree}}

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

 \newcommand\forest{{\tt forest}}

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

 \newcommand\Part{{\tt Part}}

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

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

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

 \newcommand\Tcons{{\tt Tcons}}

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

 \newcommand\Fcons{{\tt Fcons}}

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

 \newcommand\Fnil{{\tt Fnil}}

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

 \newcommand\Fin{{\tt Fin}}

 \newcommand\Fin{\hbox{\tt Fin}}

 \newcommand\QInl{{\tt QInl}}

 \newcommand\QInl{\hbox{\tt QInl}}

 \newcommand\QInr{{\tt QInr}}

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

 \newcommand\qsplit{{\tt qsplit}}

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

 \newcommand\qcase{{\tt qcase}}

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

 \newcommand\Con{{\tt Con}}

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

 \newcommand\data{{\tt data}}

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

 \pagestyle{empty}

 %CADE%\pagestyle{empty}

 \begin{titlepage}

 %CADE%\begin{titlepage}

   Several theorem provers provide commands for formalizing recursive

   This paper presents a fixedpoint approach to inductive definitions.

   data\-types or inductively defined sets.  This paper presents a new

   Instead of using a syntactic test such as `strictly positive,' the

   approach, based on fixedpoint definitions.  It is unusually general: it

   approach lets definitions involve any operators that have been proved

   admits all provably monotone inductive definitions.  It is conceptually

   monotone.  It is conceptually simple, which has allowed the easy

   simple, which has allowed the easy implementation of mutual recursion and

   implementation of mutual recursion and other conveniences.  It also

   other conveniences.  It also handles coinductive definitions: simply

   handles coinductive definitions: simply replace the least fixedpoint by a

   replace the least fixedpoint by a greatest fixedpoint.  This represents

   greatest fixedpoint.  This represents the first automated support for

   the first automated support for coinductive definitions.

   coinductive definitions.

   Theorem can be proved.  The paper briefly describes a method of

   Theorem can be proved.  Examples include lists of $n$ elements, the

   formalizing non-well-founded data structures in standard ZF set theory.

   accessible part of a relation and the set of primitive recursive

   functions.  One example of a coinductive definition is bisimulations for

   Examples include lists of $n$ elements, the accessible part of a relation

   lazy lists.  \ifCADE\else Recursive datatypes are examined in detail, as

   and the set of primitive recursive functions.  One example of a

   well as one example of a {\bf codatatype}: lazy lists.  The appendices

   coinductive definition is bisimulations for lazy lists.  \ifCADE\else

   are simple user's manuals for this Isabelle/ZF package.\fi

   Recursive datatypes are examined in detail, as well as one example of a

   {\bf codatatype}: lazy lists.  The appendices are simple user's manuals

   for this Isabelle/ZF package.\fi

 \begin{center} Copyright \copyright{} \number\year{} by Lawrence C. Paulson

 %CADE%\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}

 \end{center}

 %CADE%\thispagestyle{empty} 

 \thispagestyle{empty} 

 %CADE%\end{titlepage}

 \end{titlepage}

 %CADE%\tableofcontents\cleardoublepage\pagestyle{headings}

 \tableofcontents

 \cleardoublepage

 \pagenumbering{arabic}\pagestyle{headings}

 Most existing implementations of datatype and inductive definitions accept

 Not all inductive definitions are meaningful.  {\bf Monotone} inductive

 an artificially narrow class of inputs, and are not easily extended.  The

 definitions are a large, well-behaved class.  Monotonicity can be enforced

 shell principle and Coq's inductive definition rules are built into the

 by syntactic conditions such as `strictly positive,' but this could lead to

 underlying logic.  Melham's packages derive datatypes and inductive

 monotone definitions being rejected on the grounds of their syntactic form.

 definitions from specialized constructions in higher-order logic.

 More flexible is to formalize monotonicity within the logic and allow users

 to prove it.

 coinductive definitions.  The package is uniquely powerful:

 coinductive definitions.  The package has several advantages:

 \item It accepts the largest natural class of inductive definitions, namely

 \item It allows reference to any operators that have been proved monotone.

   all that are provably monotone.

   Thus it accepts all provably monotone inductive definitions, including

 \item It accepts a wide class of datatype definitions.

   iterated definitions.

 \item It accepts a wide class of datatype definitions, though at present

   restricted to finite branching.

 as ML structures.

 as ML structures.\footnote{This use of ML modules is not essential; the

   package could also be implemented as a function on records.}

 recursive functions.  This is the main thing lacking from my package.  Its

 recursive functions.  This is the main omission from my package.  Its

 fixedpoint operators define recursive sets, not recursive functions.  But

 fixedpoint operators define only recursive sets.  To define recursive

 the Isabelle/ZF theory provides well-founded recursion and other logical

 functions, the Isabelle/ZF theory provides well-founded recursion and other

 tools to simplify this task~\cite{paulson-set-II}.

 logical tools~\cite{paulson-set-II}.

 {\bf Outline.}  \S2 briefly introduces the least and greatest fixedpoint

 {\bf Outline.} Section~2 introduces the least and greatest fixedpoint

 operators.  \S3 discusses the form of introduction rules, mutual recursion and

 operators.  Section~3 discusses the form of introduction rules, mutual

 other points common to inductive and coinductive definitions.  \S4 discusses

 recursion and other points common to inductive and coinductive definitions.

 induction and coinduction rules separately.  \S5 presents several examples,

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

 including a coinductive definition.  \S6 describes datatype definitions, while

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

 \S7 draws brief conclusions.  \ifCADE\else The appendices are simple user's

 describes datatype definitions.  Section~7 presents related work.

 manuals for this Isabelle/ZF package.\fi

 Section~8 draws brief conclusions.  \ifCADE\else The appendices are simple

 user's manuals for this Isabelle/ZF package.\fi

 These equations are instances of the Knaster-Tarski theorem, which states

 These equations are instances of the Knaster-Tarski Theorem, which states

 This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to

 This fixedpoint theory is simple.  The Knaster-Tarski Theorem is easy to

 also exhibit a bounding set~$D$ for~$h$.  Sometimes this is trivial, as

 also exhibit a bounding set~$D$ for~$h$.  Frequently this is trivial, as

 existing set of `formulae.'  But defining the bounding set for

 existing set of `formulae.'  Isabelle/ZF provides a suitable bounding set

 (co)datatype definitions requires some effort; see~\S\ref{univ-sec} below.

 for finitely branching (co)datatype definitions; see~\S\ref{univ-sec}

 below.  Bounding sets are also called {\bf 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.

 mutual recursion.  They will be constructed from previously existing sets

 mutual recursion.  They will be constructed from domains $D_1$,

 $D_1$, \ldots,~$D_n$, respectively, which are called their {\bf domains}. 

 \ldots,~$D_n$, respectively.  The construction yields not $R_i\sbs D_i$ but

 The construction yields not $R_i\sbs D_i$ but $R_i\sbs D_1+\cdots+D_n$, where

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

 $R_i$ is contained in the image of~$D_i$ under an

 under an injection.  Reasons for this are discussed

 injection.  Reasons for this are discussed

 varies.  \S\ref{listn-sec} describes how to express this set using the

 varies.  Section~\ref{listn-sec} describes how to express this set using the

 Because any monotonic $M$ may appear in premises, the criteria for an

 The ability to introduce new monotone operators makes the approach

 acceptable definition is semantic rather than syntactic.  A suitable choice

 flexible.  A suitable choice of~$M$ and~$t$ can express a lot.  The

 of~$M$ and~$t$ can express a lot.  The powerset operator $\pow$ is

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

 monotone, and the premise $t\in\pow(R)$ expresses $t\sbs R$; see

 expresses $t\sbs R$; see \S\ref{acc-sec} for an example.  The `list of'

 \S\ref{acc-sec} for an example.  The `list of' operator is monotone, as is

 operator is monotone, as is easily proved by induction.  The premise

 easily proved by induction.  The premise $t\in\lst(R)$ avoids having to

 $t\in\lst(R)$ avoids having to encode the effect of~$\lst(R)$ using mutual

 encode the effect of~$\lst(R)$ using mutual recursion; see \S\ref{primrec-sec}

 recursion; see \S\ref{primrec-sec} and also my earlier

 and also my earlier paper~\cite[\S4.4]{paulson-set-II}.

 paper~\cite[\S4.4]{paulson-set-II}.

 The result structure contains the definitions of the recursive sets as a theorem

 The package returns its result as an ML structure, which consists of named

 list called {\tt defs}.  It also contains, as the theorem {\tt unfold}, a

 components; we may regard it as a record.  The result structure contains

 fixedpoint equation such as 

 the definitions of the recursive sets as a theorem list called {\tt defs}.

 It also contains, as the theorem {\tt unfold}, a fixedpoint equation such

 as

 \subsection{The elimination rule}

 \subsection{The case analysis rule}

 The elimination rule, called {\tt elim}, performs case analysis: a

 The elimination rule, called {\tt elim}, performs case analysis.  There is one

 This rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else

 The subscripted variables $a$ and~$b$ above the third premise are

 eigenvariables, subject to the usual `not free in \ldots' proviso.

 The rule states that if $x\in\Fin(A)$ then either $x=\emptyset$ or else

 \ifCADE\typeout{****Omitting mk_cases from CADE version!}\else

 The package also returns a function for generating simplified instances of

 The package also returns a function {\tt mk\_cases}, for generating simplified

 the case analysis rule.  It works for datatypes and for inductive

 instances of the elimination rule.  However, {\tt mk\_cases} only works for

 definitions involving datatypes, such as an inductively defined relation

 datatypes and for inductive definitions involving datatypes, such as an

 between lists.  It instantiates {\tt elim} with a user-supplied term then

 inductively defined relation between lists.  It instantiates {\tt elim}

 simplifies the cases using freeness of the underlying datatype.  The

 with a user-supplied term, then simplifies the cases using the freeness of

 simplified rules perform `rule inversion' on the inductive definition.

 the underlying datatype.

 Section~\S\ref{mkcases} presents an example.

 See \S\ref{mkcases} for an example.

 \fi

 Stronger induction rules often suggest themselves.  In the case of

 Stronger induction rules often suggest themselves.  We can derive a rule

 $\Fin(A)$, the Isabelle/ZF theory proceeds to derive a rule whose third

 for $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in

 premise discharges the extra assumption $a\not\in b$.  Most special induction

 b$.  The Isabelle/ZF theory defines the {\bf rank} of a

 rules must be proved manually, but the package proves a rule for mutual

 set~\cite[\S3.4]{paulson-set-II}, which supports well-founded induction and

 induction and inductive relations.

 recursion over datatypes.  The package proves a rule for mutual induction

 and inductive relations.

 Proving the premises simultaneously establishes $P_i(z)$ for $z\in

 Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$,

 R_i$ and $i=1$, \ldots,~$n$.

 \ldots,~$n$.

 Then it proves the theorem {\tt co\_induct}, which expresses that $\llist(A)$

 Then it proves the theorem {\tt coinduct}, which expresses that $\llist(A)$

       \begin{array}[t]{@{}l}

             z=\LCons(a,l) \conj a\in A \conj l\in X\un\llist(A) \bigr)}

         z=\LCons(a,l) \conj a\in A \conj{}\\

            {[z\in X]_z}}

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

 %     \begin{array}[t]{@{}l}

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

 %       z=\LCons(a,l) \conj a\in A \conj{}\\

 %       l\in X\un\llist(A) \bigr)

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

 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  Here $\nat$

 applying the rule with $X=\{x\}$ proves $x\in\llist(\nat)$.  (Here $\nat$

 is the set of natural numbers.

 is the set of natural numbers.)

  (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];

  (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]

   val rec_doms = [("Fin","Pow(A)")];

   val rec_doms   = [("Fin","Pow(A)")]

   val sintrs = 

   val sintrs     = ["0 : Fin(A)",

           ["0 : Fin(A)",

                     "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]

            "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];

   val monos      = []

   val monos = [];

   val con_defs   = []

   val con_defs = [];

   val type_intrs = [empty_subsetI, cons_subsetI, PowI]

   val type_intrs = [empty_subsetI, cons_subsetI, PowI];

 The parent theory is obtained from {\tt Arith.thy} by adding the unary

 We apply the functor {\tt Inductive\_Fun} to a structure describing the

 function symbol~$\Fin$.  Its domain is specified as $\pow(A)$, where $A$ is

 desired inductive definition.  The parent theory~{\tt thy} is obtained from

 the parameter appearing in the introduction rules.  For type-checking, the

 {\tt Arith.thy} by adding the unary function symbol~$\Fin$.  Its domain is

 package supplies the introduction rules:

 specified as $\pow(A)$, where $A$ is the parameter appearing in the

 introduction rules.  For type-checking, the structure supplies introduction

 rules:

 involves mostly introduction rules.  When the package returns, we can refer

 involves mostly introduction rules.  

 to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction rule

 as {\tt Fin.induct}, and so forth.

 ML is Isabelle's top level, so such functor invocations can take place at

 any time.  The result structure is declared with the name~{\tt Fin}; we can

 refer to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction

 rule as {\tt Fin.induct} and so forth.  There are plans to integrate the

 package better into Isabelle so that users can place inductive definitions

 in Isabelle theory files instead of applying functors.

 \[ {\tt Niln}\in\listn(A,0)  \qquad

 \[ \hbox{\tt Niln}\in\listn(A,0)  \qquad

    \infer{{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}

    \infer{\hbox{\tt Consn}(n,a,l)\in\listn(A,\succ(n))}

 \begin{small}

 \begin{ttbox}

 \begin{verbatim}

  (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];

  (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]

   val rec_doms = [("listn", "nat*list(A)")];

   val rec_doms   = [("listn", "nat*list(A)")]

   val sintrs = 

   val sintrs     = 

       ["<0,Nil> : listn(A)",

         ["<0,Nil>: listn(A)",

        "[| a: A;  <n,l> : listn(A) |] ==> 

          "[| a: A;  <n,l>: listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"]

         <succ(n), Cons(a,l)> : listn(A)"];

   val monos      = []

   val monos = [];

   val con_defs   = []

   val con_defs = [];

   val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]

   val type_intrs = nat_typechecks @ List.intrs @ [SigmaI];

 \end{verbatim}

 \end{ttbox}

 \end{small}

 There is an obvious way of handling this particular example, which may suggest

 The Isabelle/ZF version of this example suggests a general treatment of

 a general approach to varying parameters.  Here, we can take advantage of an

 varying parameters.  Here, we use the existing datatype definition of

 existing datatype definition of $\lst(A)$, with constructors $\Nil$

 $\lst(A)$, with constructors $\Nil$ and~$\Cons$.  Then incorporate the

 and~$\Cons$.  Then incorporate the number~$n$ into the inductive set itself,

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

 defining $\listn(A)$ as a relation.  It consists of pairs $\pair{n,l}$ such

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

 that $n\in\nat$ and~$l\in\lst(A)$ and $l$ has length~$n$.  In fact,

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

 $\listn(A)$ turns out to be the converse of the length function on~$\lst(A)$. 

 converse of the length function on~$\lst(A)$.  The Isabelle/ZF introduction

 The Isabelle/ZF introduction rules are

 rules are

 \ifCADE\typeout{****Omitting mk_cases from CADE version!}

 \subsection{A demonstration of rule inversion}\label{mkcases}

 \else

 \subsection{A demonstration of {\tt mk\_cases}}\label{mkcases}

 deduces the corresponding form of~$i$.  For example,

 deduces the corresponding form of~$i$;  this is called rule inversion.  For

 example, 

 The function {\tt mk\_cases} is also useful with datatype definitions

 The function {\tt mk\_cases} is also useful with datatype definitions.  The

 themselves.  The version from the definition of lists, namely {\tt

 instance from the definition of lists, namely {\tt List.mk\_cases}, can

 List.mk\_cases}, can prove the rule

 prove the rule

 The most important uses of {\tt mk\_cases} concern inductive definitions of

 A typical use of {\tt mk\_cases} concerns inductive definitions of

 evaluation relations.  Then {\tt mk\_cases} supports case analysis on

 evaluation relations.  Then rule inversion yields case analysis on possible

 possible evaluations, for example to prove that evaluation is

 evaluations.  For example, the Isabelle/ZF theory includes a short proof

 functional.

 of the diamond property for parallel contraction on combinators.

 \fi  %CADE

 (val thy = LList.thy addconsts [(["lleq"],"i=>i")];

  (val thy = LList.thy addconsts [(["lleq"],"i=>i")]

  val rec_doms = [("lleq", "llist(A) * llist(A)")];

   val rec_doms   = [("lleq", "llist(A) * llist(A)")]

  val sintrs = 

   val sintrs     = 

    ["<LNil, LNil> : lleq(A)",

        ["<LNil, LNil> : lleq(A)",

     "[| a:A; <l,l'>: lleq(A) |] ==> 

         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"]

      <LCons(a,l), LCons(a,l')>: lleq(A)"];

   val monos      = []

  val monos = [];

   val con_defs   = []

  val con_defs = [];

   val type_intrs = LList.intrs @ [SigmaI]

  val type_intrs = LList.intrs @ [SigmaI];

   val type_elims = [SigmaE2]);

  val type_elims = [SigmaE2]);

       \begin{array}[t]{@{}l}

       z=\pair{\LCons(a,l),\LCons(a,l')} \conj 

         z=\pair{\LCons(a,l),\LCons(a,l')} \conj a\in A \conj{}\\

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

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

 %     \begin{array}[t]{@{}l}

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

 %       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}

  (val thy = WF.thy addconsts [(["acc"],"i=>i")];

  (val thy        = WF.thy addconsts [(["acc"],"i=>i")]

   val rec_doms = [("acc", "field(r)")];

   val rec_doms   = [("acc", "field(r)")]

   val sintrs = 

   val sintrs     = ["[| r-``\{a\}:\,Pow(acc(r)); a:\,field(r) |] ==> a:\,acc(r)"]

       ["[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"];

   val monos      = [Pow_mono]

   val monos = [Pow_mono];

   val con_defs   = []

   val con_defs = [];

   val type_intrs = []

   val type_intrs = [];

 \begin{small}\begin{verbatim}

 \begin{ttbox}

  (val thy = Primrec0.thy;

  (val thy        = Primrec0.thy

   val rec_doms = [("primrec", "list(nat)->nat")];

   val rec_doms   = [("primrec", "list(nat)->nat")]

   val ext = None;

   val sintrs     = 

   val sintrs = 

         ["SC : primrec",

       ["SC : primrec",

          "k: nat ==> CONST(k) : primrec",

        "k: nat ==> CONST(k) : primrec",

          "i: nat ==> PROJ(i) : primrec",

        "i: nat ==> PROJ(i) : primrec",

          "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",

        "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",

          "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]

        "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"];

   val monos      = [list_mono]

   val monos = [list_mono];

   val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]

   val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];

   val type_intrs = pr0_typechecks

   val type_intrs = pr0_typechecks;

 \end{verbatim}\end{small}

 \end{ttbox}

 the five forms of primitive recursive function.  Note the one for $\COMP$:

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

 $\COMP$: 

   Primrec0.thy} defines the constants $\SC$, etc.; their definitions

   Primrec0.thy} defines the constants $\SC$, $\CONST$, etc.  These are not

 consist of routine list programming and are omitted.  The Isabelle theory

 constructors of a new datatype, but functions over lists of numbers.  Their

 goes on to formalize Ackermann's function and prove that it is not

 definitions, which are omitted, consist of routine list programming.  In

 primitive recursive, using the induction rule {\tt Primrec.induct}.  The

 Isabelle/ZF, the primitive recursive functions are defined as a subset of

 proof follows Szasz's excellent account.

 the function set $\lst(\nat)\to\nat$.

 ALF and Coq treat inductive definitions as datatypes, with a new

 The Isabelle theory goes on to formalize Ackermann's function and prove

 constructor for each introduction rule.  This forced Szasz to define a

 that it is not primitive recursive, using the induction rule {\tt

 small programming language for the primitive recursive functions, and then

   Primrec.induct}.  The proof follows Szasz's excellent account.

 define their semantics.  But the Isabelle/ZF formulation defines the

 primitive recursive functions directly as a subset of the function set

 $\lst(\nat)\to\nat$.  This saves a step and conforms better to mathematical

 tradition.

 defined constructors and a case analysis operator.  The package proves that the

 defined constructors and a case analysis operator.  The package proves that

 case operator inverts the constructors, and can also prove freeness theorems

 the case operator inverts the constructors and can prove freeness theorems

 Conceptually, our two forms of definition are distinct: a (co)inductive

 Conceptually, our two forms of definition are distinct.  A (co)inductive

 definition selects a subset of an existing set, but a (co)datatype

 definition selects a subset of an existing set; a (co)datatype definition

 definition creates a new set.  But the package reduces the latter to the

 creates a new set.  But the package reduces the latter to the former.  A

 former.  A set having strong closure properties must serve as the domain

 set having strong closure properties must serve as the domain of the

 of the (co)inductive definition.  Constructing this set requires some

 (co)inductive definition.  Constructing this set requires some theoretical

 theoretical effort.  Consider first datatypes and then codatatypes.

 effort, which must be done anyway to show that (co)datatypes exist.  It is

 not obvious that standard set theory is suitable for defining codatatypes.

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

 $\pair{x_1,\ldots,x_m}$ is 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$.

 $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

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

 $h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$.

 and~$\QInr(b)$, and variant disjoint sum $A\oplus B$.  Finally it defines

 and~$\QInr(b)$ and variant disjoint sum $A\oplus B$.  Finally it defines

 standard ZF set theory\footnote{No reference is available.  Variant pairs

 standard ZF set theory~\cite{paulson-final} is an alternative to adopting

   are defined by $\pair{a;b}\equiv (a+b) \equiv (\{0\}\times a) \un

 Aczel's Anti-Foundation Axiom~\cite{aczel88}.

   (\{1\}\times b)$, where $\times$ is the Cartesian product for standard

   ordered pairs.  Now

   $\pair{a;b}$ is injective and monotonic in its two arguments.

   Non-well-founded constructions, such as infinite lists, are constructed

   as least fixedpoints; the bounding set typically has the form

   $\univ(a_1\un\cdots\un a_k)$, where $a_1$, \ldots, $a_k$ are specified

   elements of the construction.}

 is an alternative to adopting Aczel's Anti-Foundation

 Axiom~\cite{aczel88}.

 \medskip

 \ifCADE The package has processed all the datatypes discussed in my earlier

 paper~\cite{paulson-set-II} and the codatatype of lazy lists.  Space

 \ifCADE The package has processed all the datatypes discussed in

 limitations preclude discussing these examples here, but they are

 my earlier paper~\cite{paulson-set-II} and the codatatype of lazy lists.

 distributed with Isabelle.  

 Space limitations preclude discussing these examples here, but they are

 \typeout{****Omitting datatype examples from CADE version!} \else

 distributed with Isabelle.  \typeout{****Omitting datatype examples from

   CADE version!} \else

  (val thy = Univ.thy;

  (val thy        = Univ.thy

   val rec_specs = 

   val rec_specs  = [("list", "univ(A)",

       [("list", "univ(A)",

                       [(["Nil"],    "i"), 

           [(["Nil"],    "i"), 

                        (["Cons"],   "[i,i]=>i")])]

            (["Cons"],   "[i,i]=>i")])];

   val rec_styp   = "i=>i"

   val rec_styp = "i=>i";

   val ext        = None

   val ext = None;

   val sintrs     = ["Nil : list(A)",

   val sintrs = 

                     "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]

       ["Nil : list(A)",

   val monos      = []

        "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];

   val type_intrs = datatype_intrs

   val monos = [];

   val type_intrs = datatype_intrs;

  (val thy = QUniv.thy;

  (val thy        = QUniv.thy

   val rec_specs = 

   val rec_specs  = [("llist", "quniv(A)",

       [("llist", "quniv(A)",

                       [(["LNil"],   "i"), 

           [(["LNil"],   "i"), 

                        (["LCons"],  "[i,i]=>i")])]

            (["LCons"],  "[i,i]=>i")])];

   val rec_styp   = "i=>i"

   val rec_styp = "i=>i";

   val ext        = None

   val ext = None;

   val sintrs     = ["LNil : llist(A)",

   val sintrs = 

                     "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]

       ["LNil : llist(A)",

   val monos      = []

        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];

   val type_intrs = codatatype_intrs

   val monos = [];

   val type_intrs = codatatype_intrs;

 \begin{small}

 \begin{ttbox}

 \begin{verbatim}

  (val thy = Univ.thy;

  (val thy        = Univ.thy

   val rec_specs = 

   val rec_specs  = [("tree", "univ(A)",

       [("tree", "univ(A)",

                        [(["Tcons"],  "[i,i]=>i")]),

           [(["Tcons"],  "[i,i]=>i")]),

                     ("forest", "univ(A)",

        ("forest", "univ(A)",

                        [(["Fnil"],   "i"),

           [(["Fnil"],   "i"),

                         (["Fcons"],  "[i,i]=>i")])]

            (["Fcons"],  "[i,i]=>i")])];

   val rec_styp   = "i=>i"

   val rec_styp = "i=>i";

   val ext        = None

   val ext = None;

   val sintrs     = 

   val sintrs = 

         ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",

           ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",

          "Fnil : forest(A)",

            "Fnil : forest(A)",

          "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]

            "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];

   val monos      = []

   val monos = [];

   val type_intrs = datatype_intrs

   val type_intrs = datatype_intrs;

 \end{verbatim}

 \end{ttbox}

 \end{small}

 \begin{small}

 \begin{ttbox}

 \begin{verbatim}

  (val thy = Univ.thy;

  (val thy        = Univ.thy

   val rec_specs = 

   val rec_specs  = [("data", "univ(A Un B)",

       [("data", "univ(A Un B)",

                        [(["Con0"],   "i"),

           [(["Con0"],   "i"),

                         (["Con1"],   "i=>i"),

            (["Con1"],   "i=>i"),

                         (["Con2"],   "[i,i]=>i"),

            (["Con2"],   "[i,i]=>i"),

                         (["Con3"],   "[i,i,i]=>i")])]

            (["Con3"],   "[i,i,i]=>i")])];

   val rec_styp   = "[i,i]=>i"

   val rec_styp = "[i,i]=>i";

   val ext        = None

   val ext = None;

   val sintrs     = 

   val sintrs = 

         ["Con0 : data(A,B)",

           ["Con0 : data(A,B)",

          "[| a: A |] ==> Con1(a) : data(A,B)",

            "[| a: A |] ==> Con1(a) : data(A,B)",

          "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",

            "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",

          "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]

            "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];

   val monos      = []

   val monos = [];

   val type_intrs = datatype_intrs

   val type_intrs = datatype_intrs;

 \end{verbatim}

 \end{ttbox}

 \end{small}

 to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$, and so forth, in the

 to replace $\Con_0=c$ by $c=\Inl(\Inl(\emptyset))$ and so forth, in the

 The fixedpoint approach makes it easy to implement a powerful

 Higher-order logic and set theory are both powerful enough to express

 package for inductive and coinductive definitions.  It is efficient: it

 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)inductive definitions that does not assert axioms.  It is efficient: it

 any logic that has some notion of set and the Knaster-Tarski Theorem.

 any logic that has some notion of set and the Knaster-Tarski Theorem.  I

 Indeed, Melham's inductive definition package for the HOL

 intend to use the Isabelle/ZF package as the basis for a higher-order logic

 system~\cite{camilleri92} implicitly proves this theorem.

 one, using Isabelle/HOL\@.  The necessary theory is already

 Datatype and codatatype definitions furthermore require a particular set

 closed under a suitable notion of ordered pair.  I intend to use the

 Isabelle/ZF package as the basis for a higher-order logic one, using

 Isabelle/HOL\@.  The necessary theory is already

 defining the corresponding types may cause complication.

 defining the corresponding types may cause complications.

 \bibliographystyle{plain}

 \bibliographystyle{springer}

 \bibliography{atp,theory,funprog,isabelle}

 \bibliography{string-abbrv,atp,theory,funprog,isabelle}

 \item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are

 \item {\tt codatatype\_intrs} and {\tt codatatype\_elims} are