--- a/doc-src/ind-defs.tex Fri Sep 09 11:57:49 1994 +0200
+++ b/doc-src/ind-defs.tex Fri Sep 09 12:25:56 1994 +0200
@@ -100,14 +100,15 @@
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. 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. \ifCADE\else 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
+ The method has been implemented in two of Isabelle's logics, 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. \ifCADE\else 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
+ package.\fi
\end{abstract}
%
\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
@@ -118,7 +119,7 @@
\section{Introduction}
Several theorem provers provide commands for formalizing recursive data
structures, like lists and trees. Examples include Boyer and Moore's shell
-principle~\cite{bm79} and Melham's recursive type package for the HOL
+principle~\cite{bm79} and Melham's recursive type package for the Cambridge HOL
system~\cite{melham89}. Such data structures are called {\bf datatypes}
below, by analogy with {\tt datatype} definitions in Standard~ML\@.
@@ -151,21 +152,22 @@
\item It allows reference to any operators that have been proved monotone.
Thus it accepts all provably monotone inductive definitions, including
iterated definitions.
-\item It accepts a wide class of datatype definitions, though at present
- restricted to finite branching.
+\item It accepts a wide class of datatype definitions, including those with
+ infinite branching.
\item It handles coinductive and codatatype definitions. Most of
the discussion below applies equally to inductive and coinductive
definitions, and most of the code is shared. To my knowledge, this is
the only package supporting coinductive definitions.
\item Definitions may be mutually recursive.
\end{itemize}
-The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set
-theory \cite{paulson-set-I,paulson-set-II}. However, the fixedpoint
-approach is independent of Isabelle. 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
+The package has been implemented in Isabelle~\cite{isabelle-intro} using ZF
+set theory \cite{paulson-set-I,paulson-set-II}; part of it has since been
+ported to Isabelle's higher-order logic. However, the fixedpoint approach is
+independent of Isabelle. 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. The package consists of several Standard ML
functors~\cite{paulson91}; it accepts its argument and returns its result
as ML structures.\footnote{This use of ML modules is not essential; the
@@ -184,7 +186,7 @@
presents several examples, including a coinductive definition. Section~6
describes datatype definitions. Section~7 presents related work.
Section~8 draws brief conclusions. \ifCADE\else The appendices are simple
-user's manuals for this Isabelle/ZF package.\fi
+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.
@@ -355,11 +357,13 @@
\[ \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. The user
-supplies the package with type-checking rules to apply. Usually these are
-general purpose rules from the 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!
+Such proofs can be regarded as type-checking the definition.\footnote{The
+ Isabelle/HOL version does not require these proofs, as HOL has implicit
+ type-checking.} The user supplies the package with type-checking rules to
+apply. Usually these are general purpose rules from the 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}.
@@ -546,7 +550,7 @@
are not acceptable to the inductive definition package:
$\listn$ occurs with three different parameter lists in the definition.
-The Isabelle/ZF version of this example suggests a general treatment of
+The Isabelle version of this example suggests a general treatment of
varying parameters. Here, we use the existing datatype definition of
$\lst(A)$, with constructors $\Nil$ and~$\Cons$. Then incorporate the
parameter~$n$ into the inductive set itself, defining $\listn(A)$ as a
@@ -726,11 +730,11 @@
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{paulin92}, but it causes
-difficulties for other systems. Its premise does not conform to
-the structure of introduction rules for HOL's inductive definition
-package~\cite{camilleri92}. It is also unacceptable to Isabelle package
-(\S\ref{intro-sec}), but fortunately can be transformed into the acceptable
-form $t\in M(R)$.
+difficulties for other systems. Its premise is not acceptable to the
+inductive definition package of the Cambridge HOL
+system~\cite{camilleri92}. It is also unacceptable to 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
@@ -1265,13 +1269,13 @@
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, but it is
-little used in the HOL system. Melham~\cite{melham89} clearly describes
-the development. The natural numbers are defined as shown above, but lists
-are defined as functions over the natural numbers. Unlabelled
+little used in the Cambridge HOL system. Melham~\cite{melham89} clearly
+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 would have yielded greater
+highly successful, but a fixedpoint approach might have yielded greater
functionality with less effort.
Melham's inductive definition package~\cite{camilleri92} uses
@@ -1285,13 +1289,11 @@
package considerably~\cite{monahan84}, as did I in unpublished
work.\footnote{The datatype package described in my LCF
book~\cite{paulson87} does {\it not\/} make definitions, but merely
- asserts axioms. I justified this shortcut on grounds of efficiency:
- existing packages took tens of minutes to run. Such an explanation would
- not do today.}
+ asserts axioms.}
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. LCF is too weak to express recursive predicates.
-Thus it would appear that the Isabelle/ZF package is the first to be based
+Thus it would appear that the Isabelle package is the first to be based
on the Knaster-Tarski Theorem.
@@ -1315,17 +1317,19 @@
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. I intend to formalize cardinal arithmetic and the
-$\aleph$-sequence to handle datatype definitions that have infinite
-branching. The need for such efforts is not a drawback of the fixedpoint
+much set theory. To justify infinitely branching datatype definitions, I
+have had to develop a theory of cardinal arithmetic, 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.
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
-intend to use the Isabelle/ZF package as the basis for a higher-order logic
-one, using Isabelle/HOL\@. The necessary theory is already
-mechanized~\cite{paulson-coind}. HOL represents sets by unary predicates;
-defining the corresponding types may cause complications.
+have ported the (co)inductive definition package from Isabelle/ZF to
+Isabelle/HOL (higher-order logic). I hope to port the (co)datatype package
+later. HOL represents sets by unary predicates; defining the corresponding
+types may cause complications.
\bibliographystyle{springer}
@@ -1461,6 +1465,9 @@
\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}