Updated for existence of HOL version and infinitely
authorlcp
Fri Sep 09 12:25:56 1994 +0200 (1994-09-09)
changeset 597ebf373c17ee2
parent 596 cffb278ec83e
child 598 2457042caac8
Updated for existence of HOL version and infinitely
branching datatypes
doc-src/ind-defs.tex
     1.1 --- a/doc-src/ind-defs.tex	Fri Sep 09 11:57:49 1994 +0200
     1.2 +++ b/doc-src/ind-defs.tex	Fri Sep 09 12:25:56 1994 +0200
     1.3 @@ -100,14 +100,15 @@
     1.4    greatest fixedpoint.  This represents the first automated support for
     1.5    coinductive definitions.
     1.6  
     1.7 -  The method has been implemented in Isabelle's formalization of ZF set
     1.8 -  theory.  It should be applicable to any logic in which the Knaster-Tarski
     1.9 -  Theorem can be proved.  Examples include lists of $n$ elements, the
    1.10 -  accessible part of a relation and the set of primitive recursive
    1.11 -  functions.  One example of a coinductive definition is bisimulations for
    1.12 -  lazy lists.  \ifCADE\else Recursive datatypes are examined in detail, as
    1.13 -  well as one example of a {\bf codatatype}: lazy lists.  The appendices
    1.14 -  are simple user's manuals for this Isabelle/ZF package.\fi
    1.15 +  The method has been implemented in two of Isabelle's logics, ZF set theory
    1.16 +  and higher-order logic.  It should be applicable to any logic in which
    1.17 +  the Knaster-Tarski Theorem can be proved.  Examples include lists of $n$
    1.18 +  elements, the accessible part of a relation and the set of primitive
    1.19 +  recursive functions.  One example of a coinductive definition is
    1.20 +  bisimulations for lazy lists.  \ifCADE\else Recursive datatypes are
    1.21 +  examined in detail, as well as one example of a {\bf codatatype}: lazy
    1.22 +  lists.  The appendices are simple user's manuals for this Isabelle
    1.23 +  package.\fi
    1.24  \end{abstract}
    1.25  %
    1.26  \bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    1.27 @@ -118,7 +119,7 @@
    1.28  \section{Introduction}
    1.29  Several theorem provers provide commands for formalizing recursive data
    1.30  structures, like lists and trees.  Examples include Boyer and Moore's shell
    1.31 -principle~\cite{bm79} and Melham's recursive type package for the HOL
    1.32 +principle~\cite{bm79} and Melham's recursive type package for the Cambridge HOL
    1.33  system~\cite{melham89}.  Such data structures are called {\bf datatypes}
    1.34  below, by analogy with {\tt datatype} definitions in Standard~ML\@.
    1.35  
    1.36 @@ -151,21 +152,22 @@
    1.37  \item It allows reference to any operators that have been proved monotone.
    1.38    Thus it accepts all provably monotone inductive definitions, including
    1.39    iterated definitions.
    1.40 -\item It accepts a wide class of datatype definitions, though at present
    1.41 -  restricted to finite branching.
    1.42 +\item It accepts a wide class of datatype definitions, including those with
    1.43 +  infinite branching.
    1.44  \item It handles coinductive and codatatype definitions.  Most of
    1.45    the discussion below applies equally to inductive and coinductive
    1.46    definitions, and most of the code is shared.  To my knowledge, this is
    1.47    the only package supporting coinductive definitions.
    1.48  \item Definitions may be mutually recursive.
    1.49  \end{itemize}
    1.50 -The package is implemented in Isabelle~\cite{isabelle-intro}, using ZF set
    1.51 -theory \cite{paulson-set-I,paulson-set-II}.  However, the fixedpoint
    1.52 -approach is independent of Isabelle.  The recursion equations are specified
    1.53 -as introduction rules for the mutually recursive sets.  The package
    1.54 -transforms these rules into a mapping over sets, and attempts to prove that
    1.55 -the mapping is monotonic and well-typed.  If successful, the package
    1.56 -makes fixedpoint definitions and proves the introduction, elimination and
    1.57 +The package has been implemented in Isabelle~\cite{isabelle-intro} using ZF
    1.58 +set theory \cite{paulson-set-I,paulson-set-II}; part of it has since been
    1.59 +ported to Isabelle's higher-order logic.  However, the fixedpoint approach is
    1.60 +independent of Isabelle.  The recursion equations are specified as
    1.61 +introduction rules for the mutually recursive sets.  The package transforms
    1.62 +these rules into a mapping over sets, and attempts to prove that the
    1.63 +mapping is monotonic and well-typed.  If successful, the package makes
    1.64 +fixedpoint definitions and proves the introduction, elimination and
    1.65  (co)induction rules.  The package consists of several Standard ML
    1.66  functors~\cite{paulson91}; it accepts its argument and returns its result
    1.67  as ML structures.\footnote{This use of ML modules is not essential; the
    1.68 @@ -184,7 +186,7 @@
    1.69  presents several examples, including a coinductive definition.  Section~6
    1.70  describes datatype definitions.  Section~7 presents related work.
    1.71  Section~8 draws brief conclusions.  \ifCADE\else The appendices are simple
    1.72 -user's manuals for this Isabelle/ZF package.\fi
    1.73 +user's manuals for this Isabelle package.\fi
    1.74  
    1.75  Most of the definitions and theorems shown below have been generated by the
    1.76  package.  I have renamed some variables to improve readability.
    1.77 @@ -355,11 +357,13 @@
    1.78  \[  \emptyset\in\pow(A)  \qquad 
    1.79      \infer{\{a\}\un b\in\pow(A)}{a\in A & b\in\pow(A)} 
    1.80  \]
    1.81 -Such proofs can be regarded as type-checking the definition.  The user
    1.82 -supplies the package with type-checking rules to apply.  Usually these are
    1.83 -general purpose rules from the ZF theory.  They could however be rules
    1.84 -specifically proved for a particular inductive definition; sometimes this is
    1.85 -the easiest way to get the definition through!
    1.86 +Such proofs can be regarded as type-checking the definition.\footnote{The
    1.87 +  Isabelle/HOL version does not require these proofs, as HOL has implicit
    1.88 +  type-checking.}  The user supplies the package with type-checking rules to
    1.89 +apply.  Usually these are general purpose rules from the ZF theory.  They
    1.90 +could however be rules specifically proved for a particular inductive
    1.91 +definition; sometimes this is the easiest way to get the definition
    1.92 +through!
    1.93  
    1.94  The result structure contains the introduction rules as the theorem list {\tt
    1.95  intrs}.
    1.96 @@ -546,7 +550,7 @@
    1.97  are not acceptable to the inductive definition package:
    1.98  $\listn$ occurs with three different parameter lists in the definition.
    1.99  
   1.100 -The Isabelle/ZF version of this example suggests a general treatment of
   1.101 +The Isabelle version of this example suggests a general treatment of
   1.102  varying parameters.  Here, we use the existing datatype definition of
   1.103  $\lst(A)$, with constructors $\Nil$ and~$\Cons$.  Then incorporate the
   1.104  parameter~$n$ into the inductive set itself, defining $\listn(A)$ as a
   1.105 @@ -726,11 +730,11 @@
   1.106  introduction rule of the form 
   1.107  \[ \infer{a\in\acc(\prec)}{\forall y.y\prec a\imp y\in\acc(\prec)} \]
   1.108  Paulin-Mohring treats this example in Coq~\cite{paulin92}, but it causes
   1.109 -difficulties for other systems.  Its premise does not conform to 
   1.110 -the structure of introduction rules for HOL's inductive definition
   1.111 -package~\cite{camilleri92}.  It is also unacceptable to Isabelle package
   1.112 -(\S\ref{intro-sec}), but fortunately can be transformed into the acceptable
   1.113 -form $t\in M(R)$.
   1.114 +difficulties for other systems.  Its premise is not acceptable to the
   1.115 +inductive definition package of the Cambridge HOL
   1.116 +system~\cite{camilleri92}.  It is also unacceptable to Isabelle package
   1.117 +(recall \S\ref{intro-sec}), but fortunately can be transformed into the
   1.118 +acceptable form $t\in M(R)$.
   1.119  
   1.120  The powerset operator is monotonic, and $t\in\pow(R)$ is equivalent to
   1.121  $t\sbs R$.  This in turn is equivalent to $\forall y\in t. y\in R$.  To
   1.122 @@ -1265,13 +1269,13 @@
   1.123  least set containing~0 and closed under~$\succ$:
   1.124  \[ \forall P. P(0)\conj (\forall x.P(x)\imp P(\succ(x))) \imp P(i) \] 
   1.125  This technique can be used to prove the Knaster-Tarski Theorem, but it is
   1.126 -little used in the HOL system.  Melham~\cite{melham89} clearly describes
   1.127 -the development.  The natural numbers are defined as shown above, but lists
   1.128 -are defined as functions over the natural numbers.  Unlabelled
   1.129 +little used in the Cambridge HOL system.  Melham~\cite{melham89} clearly
   1.130 +describes the development.  The natural numbers are defined as shown above,
   1.131 +but lists are defined as functions over the natural numbers.  Unlabelled
   1.132  trees are defined using G\"odel numbering; a labelled tree consists of an
   1.133  unlabelled tree paired with a list of labels.  Melham's datatype package
   1.134  expresses the user's datatypes in terms of labelled trees.  It has been
   1.135 -highly successful, but a fixedpoint approach would have yielded greater
   1.136 +highly successful, but a fixedpoint approach might have yielded greater
   1.137  functionality with less effort.
   1.138  
   1.139  Melham's inductive definition package~\cite{camilleri92} uses
   1.140 @@ -1285,13 +1289,11 @@
   1.141  package considerably~\cite{monahan84}, as did I in unpublished
   1.142  work.\footnote{The datatype package described in my LCF
   1.143    book~\cite{paulson87} does {\it not\/} make definitions, but merely
   1.144 -  asserts axioms.  I justified this shortcut on grounds of efficiency:
   1.145 -  existing packages took tens of minutes to run.  Such an explanation would
   1.146 -  not do today.}
   1.147 +  asserts axioms.}
   1.148  LCF is a first-order logic of domain theory; the relevant fixedpoint
   1.149  theorem is not Knaster-Tarski but concerns fixedpoints of continuous
   1.150  functions over domains.  LCF is too weak to express recursive predicates.
   1.151 -Thus it would appear that the Isabelle/ZF package is the first to be based
   1.152 +Thus it would appear that the Isabelle package is the first to be based
   1.153  on the Knaster-Tarski Theorem.
   1.154  
   1.155  
   1.156 @@ -1315,17 +1317,19 @@
   1.157  theory, whether or not the Knaster-Tarski Theorem is employed.  We must
   1.158  exhibit a bounding set (called a domain above).  For inductive definitions,
   1.159  this is often trivial.  For datatype definitions, I have had to formalize
   1.160 -much set theory.  I intend to formalize cardinal arithmetic and the
   1.161 -$\aleph$-sequence to handle datatype definitions that have infinite
   1.162 -branching.  The need for such efforts is not a drawback of the fixedpoint
   1.163 +much set theory.  To justify infinitely branching datatype definitions, I
   1.164 +have had to develop a theory of cardinal arithmetic, such as the theorem
   1.165 +that if $\kappa$ is an infinite cardinal and $|X(\alpha)| \le \kappa$ for
   1.166 +all $\alpha<\kappa$ then $|\union\sb{\alpha<\kappa} X(\alpha)| \le \kappa$.
   1.167 +The need for such efforts is not a drawback of the fixedpoint
   1.168  approach, for the alternative is to take such definitions on faith.
   1.169  
   1.170  The approach is not restricted to set theory.  It should be suitable for
   1.171  any logic that has some notion of set and the Knaster-Tarski Theorem.  I
   1.172 -intend to use the Isabelle/ZF package as the basis for a higher-order logic
   1.173 -one, using Isabelle/HOL\@.  The necessary theory is already
   1.174 -mechanized~\cite{paulson-coind}.  HOL represents sets by unary predicates;
   1.175 -defining the corresponding types may cause complications.
   1.176 +have ported the (co)inductive definition package from Isabelle/ZF to
   1.177 +Isabelle/HOL (higher-order logic).  I hope to port the (co)datatype package
   1.178 +later.  HOL represents sets by unary predicates; defining the corresponding
   1.179 +types may cause complications.
   1.180  
   1.181  
   1.182  \bibliographystyle{springer}
   1.183 @@ -1461,6 +1465,9 @@
   1.184  
   1.185  \item Side-conditions must not be conjunctions.  However, an introduction rule
   1.186  may contain any number of side-conditions.
   1.187 +
   1.188 +\item Side-conditions of the form $x=t$, where the variable~$x$ does not
   1.189 +  occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
   1.190  \end{itemize}
   1.191  
   1.192