author lcp Wed Dec 01 13:00:04 1993 +0100 (1993-12-01) changeset 179 ceb948cefb93 parent 178 afbb13cb34ca child 180 8962c2b0dc2b
minor corrections
 doc-src/ind-defs.tex file | annotate | diff | revisions
     1.1 --- a/doc-src/ind-defs.tex	Wed Dec 01 12:48:47 1993 +0100
1.2 +++ b/doc-src/ind-defs.tex	Wed Dec 01 13:00:04 1993 +0100
1.3 @@ -1,4 +1,5 @@
1.4  \documentstyle[12pt,a4,proof,lcp,alltt,amssymbols]{article}
1.5 +\hyphenation{data-type}
1.6  %CADE version should use 11pt and the Springer style
1.9 @@ -97,7 +98,6 @@
1.10  \newcommand\Con{{\tt Con}}
1.11  \newcommand\data{{\tt data}}
1.12
1.13 -\sloppy
1.14  \binperiod     %%%treat . like a binary operator
1.15
1.16  \begin{document}
1.17 @@ -106,19 +106,18 @@
1.18  \maketitle
1.19  \begin{abstract}
1.20    Several theorem provers provide commands for formalizing recursive
1.21 -  datatypes and/or inductively defined sets.  This paper presents a new
1.22 -  approach, based on fixedpoint definitions.  It is unusually general:
1.23 -  it admits all monotone inductive definitions.  It is conceptually simple,
1.24 -  which has allowed the easy implementation of mutual recursion and other
1.25 -  conveniences.  It also handles coinductive definitions: simply replace
1.26 -  the least fixedpoint by a greatest fixedpoint.  This represents the first
1.27 -  automated support for coinductive definitions.
1.28 +  data\-types or inductively defined sets.  This paper presents a new
1.29 +  approach, based on fixedpoint definitions.  It is unusually general: it
1.30 +  admits all provably monotone inductive definitions.  It is conceptually
1.31 +  simple, which has allowed the easy implementation of mutual recursion and
1.32 +  other conveniences.  It also handles coinductive definitions: simply
1.33 +  replace the least fixedpoint by a greatest fixedpoint.  This represents
1.34 +  the first automated support for coinductive definitions.
1.35
1.36    The method has been implemented in Isabelle's formalization of ZF set
1.37 -  theory.  It should
1.38 -  be applicable to any logic in which the Knaster-Tarski Theorem can be
1.39 -  proved.  The paper briefly describes a method of formalizing
1.40 -  non-well-founded data structures in standard ZF set theory.
1.41 +  theory.  It should be applicable to any logic in which the Knaster-Tarski
1.42 +  Theorem can be proved.  The paper briefly describes a method of
1.43 +  formalizing non-well-founded data structures in standard ZF set theory.
1.44
1.45    Examples include lists of $n$ elements, the accessible part of a relation
1.46    and the set of primitive recursive functions.  One example of a
1.47 @@ -229,8 +228,8 @@
1.48  This fixedpoint theory is simple.  The Knaster-Tarski theorem is easy to
1.49  prove.  Showing monotonicity of~$h$ is trivial, in typical cases.  We must
1.50  also exhibit a bounding set~$D$ for~$h$.  Sometimes this is trivial, as
1.51 -when a set of theorems'' is (co)inductively defined over some previously
1.52 -existing set of formulae.''  But defining the bounding set for
1.53 +when a set of theorems' is (co)inductively defined over some previously
1.54 +existing set of formulae.'  But defining the bounding set for
1.55  (co)datatype definitions requires some effort; see~\S\ref{univ-sec} below.
1.56
1.57
1.58 @@ -534,10 +533,10 @@
1.59  as {\tt Fin.induct}, and so forth.
1.60
1.61  \subsection{Lists of $n$ elements}\label{listn-sec}
1.62 -This has become a standard example in the
1.63 -literature.  Following Paulin-Mohring~\cite{paulin92}, we could attempt to
1.64 -define a new datatype $\listn(A,n)$, for lists of length~$n$, as an $n$-indexed
1.65 -family of sets.  But her introduction rules
1.66 +This has become a standard example of an inductive definition.  Following
1.67 +Paulin-Mohring~\cite{paulin92}, we could attempt to define a new datatype
1.68 +$\listn(A,n)$, for lists of length~$n$, as an $n$-indexed family of sets.
1.69 +But her introduction rules
1.70  ${\tt Niln}\in\listn(A,0) \qquad 1.71 \infer{{\tt Consn}(n,a,l)\in\listn(A,\succ(n))} 1.72 {n\in\nat & a\in A & l\in\listn(A,n)} 1.73 @@ -628,11 +627,11 @@ 1.74 \pair{n,l}\in\listn(A) 1.75 \end{array} \right]_{a,l,n}}} 1.76$
1.77 -The ML function {\tt ListN.mk\_cases} generates simplified instances of this
1.78 -rule.  It works by freeness reasoning on the list constructors: $\Cons$ is
1.79 -injective and $\Cons(a,l)\not=\Nil$. If $x$ is $\pair{i,\Nil}$ or
1.80 -$\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases} deduces the corresponding
1.81 -form of~$i$.  For example,
1.82 +The ML function {\tt ListN.mk\_cases} generates simplified instances of
1.83 +this rule.  It works by freeness reasoning on the list constructors:
1.84 +$\Cons(a,l)$ is injective in its two arguments and differs from~$\Nil$.  If
1.85 +$x$ is $\pair{i,\Nil}$ or $\pair{i,\Cons(a,l)}$ then {\tt ListN.mk\_cases}
1.86 +deduces the corresponding form of~$i$.  For example,
1.87  \begin{ttbox}
1.88  ListN.mk_cases List.con_defs "<i,Cons(a,l)> : listn(A)"
1.89  \end{ttbox}
1.90 @@ -947,9 +946,10 @@
1.91
1.92  \subsection{The case analysis operator}
1.93  The (co)datatype package automatically defines a case analysis operator,
1.94 -called {\tt$R$\_case}.  A mutually recursive definition still has only
1.95 -one operator, called {\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is
1.96 -analogous to those for products and sums.
1.97 +called {\tt$R$\_case}.  A mutually recursive definition still has only one
1.98 +operator, whose name combines those of the recursive sets: it is called
1.99 +{\tt$R_1$\_\ldots\_$R_n$\_case}.  The case operator is analogous to those
1.100 +for products and sums.
1.101
1.102  Datatype definitions employ standard products and sums, whose operators are
1.103  $\split$ and $\case$ and satisfy the equations
1.104 @@ -1519,7 +1519,7 @@
1.105
1.106  The result structure also inherits everything from the underlying
1.107  (co)inductive definition, such as the introduction rules, elimination rule,
1.108 -and induction/coinduction rule.
1.109 +and (co)induction rule.
1.110
1.111
1.112  \begin{figure}
1.113 @@ -1576,16 +1576,16 @@
1.114  $\quniv(A_1\un\cdots\un A_k)$.
1.115
1.116  The {\tt sintrs} specify the introduction rules, which govern the recursive
1.117 -structure of the datatype.  Introduction rules may involve monotone operators
1.118 -and side-conditions to express things that go beyond the usual notion of
1.119 -datatype.  The theorem lists {\tt monos}, {\tt type\_intrs} and {\tt
1.120 -type\_elims} should contain precisely what is needed for the underlying
1.121 -(co)inductive definition.  Isabelle/ZF defines theorem lists that can be
1.122 -defined for the latter two components:
1.123 +structure of the datatype.  Introduction rules may involve monotone
1.124 +operators and side-conditions to express things that go beyond the usual
1.125 +notion of datatype.  The theorem lists {\tt monos}, {\tt type\_intrs} and
1.126 +{\tt type\_elims} should contain precisely what is needed for the
1.127 +underlying (co)inductive definition.  Isabelle/ZF defines lists of
1.128 +type-checking rules that can be supplied for the latter two components:
1.129  \begin{itemize}
1.130 -\item {\tt datatype\_intrs} and {\tt datatype\_elims} are type-checking rules
1.131 +\item {\tt datatype\_intrs} and {\tt datatype\_elims} are rules
1.132  for $\univ(A)$.
1.133 -\item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are type-checking
1.134 +\item {\tt co\_datatype\_intrs} and {\tt co\_datatype\_elims} are
1.135  rules for $\quniv(A)$.
1.136  \end{itemize}
1.137  In typical definitions, these theorem lists need not be supplemented with