author lcp Wed, 01 Dec 1993 13:00:04 +0100 changeset 179 ceb948cefb93 parent 178 afbb13cb34ca child 180 8962c2b0dc2b
minor corrections
 doc-src/ind-defs.tex file | annotate | diff | comparison | revisions
--- a/doc-src/ind-defs.tex	Wed Dec 01 12:48:47 1993 +0100
+++ b/doc-src/ind-defs.tex	Wed Dec 01 13:00:04 1993 +0100
@@ -1,4 +1,5 @@
\documentstyle[12pt,a4,proof,lcp,alltt,amssymbols]{article}
+\hyphenation{data-type}
%CADE version should use 11pt and the Springer style
@@ -97,7 +98,6 @@
\newcommand\Con{{\tt Con}}
\newcommand\data{{\tt data}}

-\sloppy
\binperiod     %%%treat . like a binary operator

\begin{document}
@@ -106,19 +106,18 @@
\maketitle
\begin{abstract}
Several theorem provers provide commands for formalizing recursive
-  datatypes and/or inductively defined sets.  This paper presents a new
-  approach, based on fixedpoint definitions.  It is unusually general:
-  it admits all monotone inductive definitions.  It is conceptually simple,
-  which has allowed the easy implementation of mutual recursion and other
-  conveniences.  It also handles coinductive definitions: simply replace
-  the least fixedpoint by a greatest fixedpoint.  This represents the first
-  automated support for coinductive definitions.
+  data\-types or inductively defined sets.  This paper presents a new
+  approach, based on fixedpoint definitions.  It is unusually general: it
+  admits all provably monotone inductive definitions.  It is conceptually
+  simple, which has allowed the easy implementation of mutual recursion and
+  other conveniences.  It also handles coinductive definitions: simply
+  replace the least fixedpoint by a greatest fixedpoint.  This represents
+  the first automated support for coinductive definitions.

The method has been implemented in Isabelle's formalization of ZF set
-  theory.  It should
-  be applicable to any logic in which the Knaster-Tarski Theorem can be
-  proved.  The paper briefly describes a method of formalizing
-  non-well-founded data structures in standard ZF set theory.
+  theory.  It should be applicable to any logic in which the Knaster-Tarski
+  Theorem can be proved.  The paper briefly describes a method of
+  formalizing non-well-founded data structures in standard ZF set theory.

Examples include lists of $n$ elements, the accessible part of a relation
and the set of primitive recursive functions.  One example of a
@@ -229,8 +228,8 @@
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$.  Sometimes this is trivial, as
-when a set of theorems'' is (co)inductively defined over some previously
-existing set of formulae.''  But defining the bounding set for
+when a set of theorems' is (co)inductively defined over some previously
+existing set of formulae.'  But defining the bounding set for
(co)datatype definitions requires some effort; see~\S\ref{univ-sec} below.

@@ -534,10 +533,10 @@
as {\tt Fin.induct}, and so forth.

\subsection{Lists of $n$ elements}\label{listn-sec}
-This has become a standard example in the
-literature.  Following Paulin-Mohring~\cite{paulin92}, 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
+This has become a standard example of an inductive definition.  Following
+Paulin-Mohring~\cite{paulin92}, 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
${\tt Niln}\in\listn(A,0) \qquad \infer{{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} {n\in\nat & a\in A & l\in\listn(A,n)} @@ -628,11 +627,11 @@ \pair{n,l}\in\listn(A) \end{array} \right]_{a,l,n}}}$
-The ML function {\tt ListN.mk\_cases} generates simplified instances of this
-rule.  It works by freeness reasoning on the list constructors: $\Cons$ is
-injective and $\Cons(a,l)\not=\Nil$. If $x$ is $\pair{i,\Nil}$ or
-$\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} deduces the corresponding
-form of~$i$.  For example,
+The 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$.  For example,
\begin{ttbox}
ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)"
\end{ttbox}
@@ -947,9 +946,10 @@

\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, called {\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is
-analogous to those for products and sums.
+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
@@ -1519,7 +1519,7 @@

The result structure also inherits everything from the underlying
(co)inductive definition, such as the introduction rules, elimination rule,
-and induction/coinduction rule.
+and (co)induction rule.

\begin{figure}
@@ -1576,16 +1576,16 @@
$\quniv(A_1\un\cdots\un A_k)$.

The {\tt sintrs} specify the introduction rules, which govern the recursive
-structure of the datatype.  Introduction rules may involve monotone operators
-and side-conditions to express things that go beyond the usual notion of
-datatype.  The theorem lists {\tt monos}, {\tt type\_intrs} and {\tt
-type\_elims} should contain precisely what is needed for the underlying
-(co)inductive definition.  Isabelle/ZF defines theorem lists that can be
-defined for the latter two components:
+structure of the datatype.  Introduction rules may involve monotone
+operators and side-conditions to express things that go beyond the usual
+notion of datatype.  The theorem lists {\tt monos}, {\tt type\_intrs} and
+{\tt type\_elims} should contain precisely what is needed for the
+underlying (co)inductive definition.  Isabelle/ZF defines lists of
+type-checking rules that can be supplied for the latter two components:
\begin{itemize}
-\item {\tt datatype\_intrs} and {\tt datatype\_elims} are type-checking rules
+\item {\tt datatype\_intrs} and {\tt datatype\_elims} are rules
for $\univ(A)$.
-\item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are type-checking
+\item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are
rules for $\quniv(A)$.
\end{itemize}
In typical definitions, these theorem lists need not be supplemented with