minor corrections
authorlcp
Wed Dec 01 13:00:04 1993 +0100 (1993-12-01)
changeset 179ceb948cefb93
parent 178 afbb13cb34ca
child 180 8962c2b0dc2b
minor corrections
doc-src/ind-defs.tex
     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.7  \newif\ifCADE
     1.8  \CADEfalse
     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