summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/ind-defs.tex

changeset 179 | ceb948cefb93 |

parent 130 | c035b6b9eafc |

child 181 | 9c2db771f224 |

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