--- a/doc-src/ind-defs.bbl Wed Jul 17 15:04:48 1996 +0200
+++ b/doc-src/ind-defs.bbl Wed Jul 17 15:25:50 1996 +0200
@@ -3,8 +3,8 @@
\bibitem{abramsky90}
Abramsky, S.,
\newblock The lazy lambda calculus,
-\newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner,
- Ed. Addison-Wesley, 1977, pp.~65--116
+\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
+ Addison-Wesley, 1977, pp.~65--116
\bibitem{aczel77}
Aczel, P.,
@@ -37,8 +37,14 @@
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
+\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.,
@@ -50,6 +56,18 @@
\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
@@ -60,14 +78,13 @@
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
+ 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
+ Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386
\bibitem{milner-ind}
Milner, R.,
@@ -92,10 +109,17 @@
\bibitem{nipkow-CR}
Nipkow, T.,
\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
-\newblock In {\em Automated Deduction --- {CADE}-13\/} (1996), M.~McRobbie,
+\newblock In {\em Automated Deduction --- {CADE}-13\/} (1996), M.~McRobbie
J.~Slaney, Eds., LNAI, Springer, p.~?,
\newblock in press
+\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{paulin92}
Paulin-Mohring, C.,
\newblock Inductive definitions in the system {Coq}: Rules and properties,
@@ -131,9 +155,7 @@
\bibitem{paulson-final}
Paulson, L.~C.,
\newblock A concrete final coalgebra theorem for {ZF} set theory,
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
- '94}\/} (published 1995), P.~Dybjer, B.~Nordstr{\"om},, J.~Smith, Eds., LNCS
- 996, Springer, pp.~120--139
+\newblock In Dybjer et~al. \cite{types94}, pp.~120--139
\bibitem{paulson-gr}
Paulson, L.~C., Gr\c{a}bczewski, K.,
@@ -157,7 +179,7 @@
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
+ J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
\bibitem{slind-tfl}
Slind, K.,
@@ -170,7 +192,7 @@
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
+\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
Univ. Press, 1993, pp.~317--338
\bibitem{voelker95}
--- a/doc-src/ind-defs.tex Wed Jul 17 15:04:48 1996 +0200
+++ b/doc-src/ind-defs.tex Wed Jul 17 15:25:50 1996 +0200
@@ -1,6 +1,6 @@
\documentstyle[a4,alltt,iman,extra,proof209,12pt]{article}
\newif\ifshort
-\shortfalse
+\shortfalse%%%%%\shorttrue
\title{A Fixedpoint Approach to\\
(Co)Inductive and (Co)Datatype Definitions%
@@ -20,6 +20,7 @@
\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
@@ -99,10 +100,9 @@
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 other conveniences. It also
+ implementation of mutual recursion and iterated definitions. It also
handles coinductive definitions: simply replace the least fixedpoint by a
- greatest fixedpoint. This represents the first automated support for
- coinductive definitions.
+ 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
@@ -114,7 +114,8 @@
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.
+ semantic consistency. The package can be trusted because it proves theorems
+ from definitions, instead of asserting desired properties as axioms.
\end{abstract}
%
\bigskip
@@ -162,8 +163,7 @@
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. To my
-knowledge, this is the only package supporting coinductive definitions.
+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,
@@ -224,9 +224,9 @@
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}.
+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
@@ -426,12 +426,12 @@
\[ \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 Isabelle/\textsc{zf} theory defines the \defn{rank} of a
-set~\cite[\S3.4]{paulson-set-II}, which supports well-founded induction and
-recursion over datatypes. The package proves a rule for mutual induction, and
-modifies the default rule if~$R$ is a relation.
+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}
@@ -534,7 +534,7 @@
\[ \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 the two
+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.
@@ -559,10 +559,10 @@
$\listn$ occurs with three different parameter lists in the definition.
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
-relation. It consists of pairs $\pair{n,l}$ such that $n\in\nat$
+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
@@ -604,14 +604,13 @@
--- asserts that the inductive definition agrees with the obvious notion of
$n$-element list.
-Unlike in Coq, the definition does not declare a new datatype. A ``list of
-$n$ elements'' really is a list and 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)}
+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 $+$ here denotes addition on the natural numbers and @ denotes append.
+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:
@@ -738,7 +737,7 @@
Paulin-Mohring treats this example in Coq~\cite{paulin92}, 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 Isabelle package
+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)$.
@@ -869,12 +868,13 @@
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
-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$.
+ {[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
@@ -934,7 +934,8 @@
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)$.
+$\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,
@@ -971,8 +972,8 @@
\medskip
To see how constructors and the case analysis operator are defined, let us
-examine some examples. These include lists and trees/forests, which I have
-discussed extensively in another paper~\cite{paulson-set-II}.
+examine some examples. Further details are available
+elsewhere~\cite{paulson-set-II}.
\subsection{Example: lists and lazy lists}\label{lists-sec}
@@ -990,24 +991,27 @@
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 requires {\tt Datatype} as a parent theory;
-this makes available the definitions of $\univ$ and $\quniv$. Each is
-automatically given the appropriate domain: $\univ(A)$ for $\lst(A)$ and
-$\quniv(A)$ for $\llist(A)$. The default can be overridden.
+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
+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)). \]
-
-Since $\llist(A)$ is a codatatype, it has no induction rule. Instead it has
+\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
@@ -1015,13 +1019,17 @@
\[ \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 & = & \Inl(\emptyset) \\
- \Cons(a,l) & = & \Inr(\pair{a,l})
+ \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)) \]
@@ -1036,8 +1044,12 @@
& = & \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
@@ -1091,19 +1103,22 @@
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) & = & \Inl(\pair{a,l}) \\
- \Fnil & = & \Inr(\Inl(\emptyset)) \\
- \Fcons(a,l) & = & \Inr(\Inr(\pair{a,l}))
+ \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))) \]
+ \case(\split(f),\, \case(\lambda u.c, \split(g)))
+\]
+\fi
-\subsection{A four-constructor datatype}
-Finally let us consider a fairly general datatype. It has four
-constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities.
+\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
@@ -1116,14 +1131,14 @@
induction rule has four minor premises, one per constructor, and only the last
has an induction hypothesis. (Details are left to the reader.)
-The constructor definitions are
+The constructors are defined by the equations
\begin{eqnarray*}
- \Con_0 & = & \Inl(\Inl(\emptyset)) \\
- \Con_1(a) & = & \Inl(\Inr(a)) \\
- \Con_2(a,b) & = & \Inr(\Inl(\pair{a,b})) \\
- \Con_3(a,b,c) & = & \Inr(\Inr(\pair{a,b,c})).
+ \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 operator is
+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),\, \\
@@ -1133,13 +1148,12 @@
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 difference between the binary and unary
-numeral systems.
+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
@@ -1190,16 +1204,18 @@
obvious. Why, then, has this technique so seldom been implemented?
Most automated logics can only express inductive definitions by asserting
-new 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
+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{paulin92}. It seems that
-researchers tried hard to circumvent these problems before finally
-extending the Calculus with rule schemes for strictly positive operators.
+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{paulin92}. 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
@@ -1215,11 +1231,20 @@
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}
@@ -1251,7 +1276,7 @@
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
+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$.
@@ -1302,7 +1327,7 @@
\end{footnotesize}
%%%%%\doendnotes
-\ifshort\typeout{****Omitting appendices from short version!}
+\ifshort\typeout{****Omitting appendices}
\else
\newpage
\appendix
@@ -1312,6 +1337,9 @@
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.
@@ -1439,10 +1467,15 @@
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.
+file. Please include {\tt Datatype} as a parent theory; this makes available
+the definitions of $\univ$ and $\quniv$.
\subsection{The result structure}
@@ -1496,10 +1529,8 @@
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 syntax is rather complicated; please consult the
-examples above (\S\ref{lists-sec}) and the theory files on the \textsc{zf} source
-directory.
+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
@@ -1538,6 +1569,10 @@
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