# HG changeset patch # User lcp # Date 778850936 -7200 # Node ID 5b1a0e50c79a6da05c6cf3a61d968d26511ad263 # Parent 550292083e66a5eefcd17b822ea96fb9359c526a documentation of theory sections (co)inductive and (co)datatype diff -r 550292083e66 -r 5b1a0e50c79a doc-src/ind-defs.tex --- a/doc-src/ind-defs.tex Tue Sep 06 13:10:38 1994 +0200 +++ b/doc-src/ind-defs.tex Tue Sep 06 13:28:56 1994 +0200 @@ -87,8 +87,8 @@ \binperiod %%%treat . like a binary operator \begin{document} -%CADE%\pagestyle{empty} -%CADE%\begin{titlepage} +\pagestyle{empty} +\begin{titlepage} \maketitle \begin{abstract} This paper presents a fixedpoint approach to inductive definitions. @@ -110,10 +110,10 @@ are simple user's manuals for this Isabelle/ZF package.\fi \end{abstract} % -%CADE%\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} -%CADE%\thispagestyle{empty} -%CADE%\end{titlepage} -%CADE%\tableofcontents\cleardoublepage\pagestyle{headings} +\bigskip\centerline{Copyright \copyright{} \number\year{} by Lawrence C. Paulson} +\thispagestyle{empty} +\end{titlepage} +\tableofcontents\cleardoublepage\pagestyle{plain} \section{Introduction} Several theorem provers provide commands for formalizing recursive data @@ -446,8 +446,9 @@ \ldots,~$n$. \item If the domain of some $R_i$ is the Cartesian product -$A_1\times\cdots\times A_m$, then the corresponding predicate $P_i$ takes $m$ -arguments and the corresponding conjunct of the conclusion is + $A_1\times\cdots\times A_m$ (associated to the right), then the + corresponding predicate $P_i$ takes $m$ arguments and the corresponding + conjunct of the conclusion is \[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) \] \end{itemize} @@ -498,26 +499,25 @@ of a relation, and the primitive recursive functions. \subsection{The finite powerset operator} -This operator has been discussed extensively above. Here -is the corresponding ML invocation (note that $\cons(a,b)$ abbreviates -$\{a\}\un b$ in Isabelle/ZF): +This operator has been discussed extensively above. Here is the +corresponding invocation in an Isabelle theory file. Note that +$\cons(a,b)$ abbreviates $\{a\}\un b$ in Isabelle/ZF. \begin{ttbox} -structure Fin = Inductive_Fun - (val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)] - val thy_name = "Fin" - val rec_doms = [("Fin","Pow(A)")] - val sintrs = ["0 : Fin(A)", - "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] - val monos = [] - val con_defs = [] - val type_intrs = [empty_subsetI, cons_subsetI, PowI] - val type_elims = [make_elim PowD]); +Finite = Arith + +consts Fin :: "i=>i" +inductive + domains "Fin(A)" <= "Pow(A)" + intrs + emptyI "0 : Fin(A)" + consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" + type_intrs "[empty_subsetI, cons_subsetI, PowI]" + type_elims "[make_elim PowD]" +end \end{ttbox} -We apply the functor {\tt Inductive\_Fun} to a structure describing the -desired inductive definition. The parent theory~{\tt thy} is obtained from -{\tt Arith.thy} by adding the unary function symbol~$\Fin$. Its domain is +Theory {\tt Finite} extends the parent theory {\tt Arith} by declaring the +unary function symbol~$\Fin$, which is defined inductively. Its domain is specified as $\pow(A)$, where $A$ is the parameter appearing in the -introduction rules. For type-checking, the structure supplies introduction +introduction rules. For type-checking, we supply two introduction rules: \[ \emptyset\sbs A \qquad \infer{\{a\}\un B\sbs C}{a\in C & B\sbs C} @@ -526,12 +526,12 @@ directions of the equivalence $A\in\pow(B)\bimp A\sbs B$. Type-checking involves mostly introduction rules. -ML is Isabelle's top level, so such functor invocations can take place at -any time. The result structure is declared with the name~{\tt Fin}; we can -refer to the $\Fin(A)$ introduction rules as {\tt Fin.intrs}, the induction -rule as {\tt Fin.induct} and so forth. There are plans to integrate the -package better into Isabelle so that users can place inductive definitions -in Isabelle theory files instead of applying functors. +Like all Isabelle theory files, this one yields a structure containing the +new theory as an \ML{} value. Structure {\tt Finite} also has a +substructure, called~{\tt Fin}. After declaring \hbox{\tt open Finite;} we +can refer to the $\Fin(A)$ introduction rules as the list {\tt Fin.intrs} +or individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction +rule is {\tt Fin.induct}. \subsection{Lists of $n$ elements}\label{listn-sec} @@ -546,24 +546,6 @@ are not acceptable to the inductive definition package: $\listn$ occurs with three different parameter lists in the definition. -\begin{figure} -\begin{ttbox} -structure ListN = Inductive_Fun - (val thy = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)] - val thy_name = "ListN" - val rec_doms = [("listn", "nat*list(A)")] - val sintrs = - ["<0,Nil>: listn(A)", - "[| a: A; : listn(A) |] ==> : listn(A)"] - val monos = [] - val con_defs = [] - val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] - val type_elims = []); -\end{ttbox} -\hrule -\caption{Defining lists of $n$ elements} \label{listn-fig} -\end{figure} - The Isabelle/ZF 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 @@ -576,13 +558,24 @@ \infer{\pair{\succ(n),\Cons(a,l)}\in\listn(A)} {a\in A & \pair{n,l}\in\listn(A)} \] -Figure~\ref{listn-fig} presents the ML invocation. A theory of lists, -extended with a declaration of $\listn$, is the parent theory. The domain -is specified as $\nat\times\lst(A)$. The type-checking rules include those -for 0, $\succ$, $\Nil$ and $\Cons$. Because $\listn(A)$ is a set of pairs, -type-checking also requires introduction and elimination rules to express -both directions of the equivalence $\pair{a,b}\in A\times B \bimp a\in A -\conj b\in B$. +The Isabelle theory file takes, as parent, the theory~{\tt List} of lists. +We declare the constant~$\listn$ and supply an inductive definition, +specifying the domain as $\nat\times\lst(A)$: +\begin{ttbox} +ListN = List + +consts listn ::"i=>i" +inductive + domains "listn(A)" <= "nat*list(A)" + intrs + NilI "<0,Nil> : listn(A)" + ConsI "[| a: A; : listn(A) |] ==> : listn(A)" + type_intrs "nat_typechecks @ list.intrs" +end +\end{ttbox} +The type-checking rules include those for 0, $\succ$, $\Nil$ and $\Cons$. +Because $\listn(A)$ is a set of pairs, type-checking requires the +equivalence $\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$; the +package always includes the necessary rules. The package returns introduction, elimination and induction rules for $\listn$. The basic induction rule, {\tt ListN.induct}, is @@ -687,25 +680,21 @@ \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} {a\in A & \pair{l,l'}\in \lleq(A)} \] -To make this coinductive definition, we invoke \verb|CoInductive_Fun|: +To make this coinductive definition, the theory file includes (after the +declaration of $\llist(A)$) the following lines: \begin{ttbox} -structure LList_Eq = CoInductive_Fun - (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)] - val thy_name = "LList_Eq" - val rec_doms = [("lleq", "llist(A) * llist(A)")] - val sintrs = - [" : lleq(A)", - "[| a:A; : lleq(A) |] ==> : lleq(A)"] - val monos = [] - val con_defs = [] - val type_intrs = LList.intrs - val type_elims = []); +consts lleq :: "i=>i" +coinductive + domains "lleq(A)" <= "llist(A) * llist(A)" + intrs + LNil " : lleq(A)" + LCons "[| a:A; : lleq(A) |] ==> : lleq(A)" + type_intrs "llist.intrs" \end{ttbox} Again, {\tt addconsts} declares a constant for $\lleq$ in the parent theory. The domain of $\lleq(A)$ is $\llist(A)\times\llist(A)$. The type-checking -rules include the introduction rules for lazy lists as well as rules -for both directions of the equivalence -$\pair{a,b}\in A\times B \bimp a\in A \conj b\in B$. +rules include the introduction rules for $\llist(A)$, whose +declaration is discussed below (\S\ref{lists-sec}). The package returns the introduction rules and the elimination rule, as usual. But instead of induction rules, it returns a coinduction rule. @@ -749,21 +738,20 @@ term~$t$ such that $y\in t$ if and only if $y\prec a$. A suitable $t$ is the inverse image of~$\{a\}$ under~$\prec$. -The ML invocation below follows this approach. Here $r$ is~$\prec$ and +The theory file below follows this approach. Here $r$ is~$\prec$ and $\field(r)$ refers to~$D$, the domain of $\acc(r)$. (The field of a -relation is the union of its domain and range.) Finally -$r^{-}``\{a\}$ denotes the inverse image of~$\{a\}$ under~$r$. The package is -supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic. +relation is the union of its domain and range.) Finally $r^{-}``\{a\}$ +denotes the inverse image of~$\{a\}$ under~$r$. We supply the theorem {\tt + Pow\_mono}, which asserts that $\pow$ is monotonic. \begin{ttbox} -structure Acc = Inductive_Fun - (val thy = WF.thy |> add_consts [("acc","i=>i",NoSyn)] - val thy_name = "Acc" - val rec_doms = [("acc", "field(r)")] - val sintrs = ["[| r-``\{a\}:\,Pow(acc(r)); a:\,field(r) |] ==> a:\,acc(r)"] - val monos = [Pow_mono] - val con_defs = [] - val type_intrs = [] - val type_elims = []); +Acc = WF + +consts acc :: "i=>i" +inductive + domains "acc(r)" <= "field(r)" + intrs + vimage "[| r-``\{a\}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)" + monos "[Pow_mono]" +end \end{ttbox} The Isabelle theory proceeds to prove facts about $\acc(\prec)$. For instance, $\prec$ is well-founded if and only if its field is contained in @@ -831,20 +819,28 @@ \begin{figure} \begin{ttbox} -structure Primrec = Inductive_Fun - (val thy = Primrec0.thy - val thy_name = "Primrec" - val rec_doms = [("primrec", "list(nat)->nat")] - val sintrs = - ["SC : primrec", - "k: nat ==> CONST(k) : primrec", - "i: nat ==> PROJ(i) : primrec", - "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec", - "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"] - val monos = [list_mono] - val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def] - val type_intrs = pr0_typechecks - val type_elims = []); +Primrec = List + +consts + primrec :: "i" + SC :: "i" + \(\vdots\) +defs + SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)" + \(\vdots\) +inductive + domains "primrec" <= "list(nat)->nat" + intrs + SC "SC : primrec" + CONST "k: nat ==> CONST(k) : primrec" + PROJ "i: nat ==> PROJ(i) : primrec" + COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec" + PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec" + monos "[list_mono]" + con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]" + type_intrs "nat_typechecks @ list.intrs @ \ttback +\ttback [lam_type, list_case_type, drop_type, map_type, \ttback +\ttback apply_type, rec_type]" +end \end{ttbox} \hrule \caption{Inductive definition of the primitive recursive functions} @@ -869,10 +865,10 @@ 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 ML invocation. Theory {\tt - Primrec0.thy} defines the constants $\SC$, $\CONST$, etc. These are not -constructors of a new datatype, but functions over lists of numbers. Their -definitions, which are omitted, consist of routine list programming. In +Figure~\ref{primrec-fig} presents the theory file. Theory {\tt Primrec} +defines the constants $\SC$, $\CONST$, etc. These are not constructors of +a new datatype, but functions over lists of numbers. Their definitions, +most of which are omitted, consist of routine list programming. In Isabelle/ZF, the primitive recursive functions are defined as a subset of the function set $\lst(\nat)\to\nat$. @@ -996,57 +992,39 @@ examine some examples. These include lists and trees/forests, which I have discussed extensively in another paper~\cite{paulson-set-II}. -\begin{figure} + +\subsection{Example: lists and lazy lists}\label{lists-sec} +Here is a theory file that declares the datatype of lists: \begin{ttbox} -structure List = Datatype_Fun - (val thy = Univ.thy - val thy_name = "List" - val rec_specs = [("list", "univ(A)", - [(["Nil"], "i", NoSyn), - (["Cons"], "[i,i]=>i", NoSyn)])] - val rec_styp = "i=>i" - val sintrs = ["Nil : list(A)", - "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"] - val monos = [] - val type_intrs = datatype_intrs - val type_elims = datatype_elims); +List = Univ + +consts list :: "i=>i" +datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") +end \end{ttbox} -\hrule -\caption{Defining the datatype of lists} \label{list-fig} - -\medskip +And here is the theory file that declares the codatatype of lazy lists: \begin{ttbox} -structure LList = CoDatatype_Fun - (val thy = QUniv.thy - val thy_name = "LList" - val rec_specs = [("llist", "quniv(A)", - [(["LNil"], "i", NoSyn), - (["LCons"], "[i,i]=>i", NoSyn)])] - val rec_styp = "i=>i" - val sintrs = ["LNil : llist(A)", - "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"] - val monos = [] - val type_intrs = codatatype_intrs - val type_elims = codatatype_elims); +LList = QUniv + +consts llist :: "i=>i" +codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)") +end \end{ttbox} -\hrule -\caption{Defining the codatatype of lazy lists} \label{llist-fig} -\end{figure} - -\subsection{Example: lists and lazy lists} -Figures \ref{list-fig} and~\ref{llist-fig} present the ML definitions of -lists and lazy lists, respectively. They highlight the (many) similarities -and (few) differences between datatype and codatatype definitions. +They highlight the (many) similarities and (few) differences between +datatype and codatatype definitions.\footnote{The real theory files contain + many more declarations, mainly of functions over lists; the declaration + of lazy lists is followed by the coinductive definition of lazy list + equality.} 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 uses the appropriate domain from a Isabelle/ZF theory: \begin{itemize} -\item $\lst(A)$ specifies domain $\univ(A)$ and parent theory {\tt Univ.thy}. +\item $\lst(A)$ requires the parent theory {\tt Univ}. The package + automatically uses the domain $\univ(A)$ (the default choice can be + overridden). -\item $\llist(A)$ specifies domain $\quniv(A)$ and parent theory {\tt -QUniv.thy}. +\item $\llist(A)$ requires the parent theory {\tt QUniv}. The package + automatically uses the domain $\quniv(A)$. \end{itemize} Since $\lst(A)$ is a datatype, it enjoys a structural induction rule, {\tt @@ -1095,36 +1073,18 @@ & = & h(x,y) \end{eqnarray*} -\begin{figure} -\begin{ttbox} -structure TF = Datatype_Fun - (val thy = Univ.thy - val thy_name = "TF" - val rec_specs = [("tree", "univ(A)", - [(["Tcons"], "[i,i]=>i", NoSyn)]), - ("forest", "univ(A)", - [(["Fnil"], "i", NoSyn), - (["Fcons"], "[i,i]=>i", NoSyn)])] - val rec_styp = "i=>i" - val sintrs = - ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", - "Fnil : forest(A)", - "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"] - val monos = [] - val type_intrs = datatype_intrs - val type_elims = datatype_elims); -\end{ttbox} -\hrule -\caption{Defining the datatype of trees and forests} \label{tf-fig} -\end{figure} - \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 -$\Fnil$ and~$\Fcons$. Figure~\ref{tf-fig} presents the ML -definition. It has much in common with that of $\lst(A)$, including its -use of $\univ(A)$ for the domain and {\tt Univ.thy} for the parent theory. +$\Fnil$ and~$\Fcons$: +\begin{ttbox} +TF = List + +consts tree, forest, tree_forest :: "i=>i" +datatype "tree(A)" = Tcons ("a: A", "f: forest(A)") +and "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") +end +\end{ttbox} The three introduction rules define the mutual recursion. The distinguishing feature of this example is its two induction rules. @@ -1183,37 +1143,22 @@ \case(\split(f),\, \case(\lambda u.c, \split(g))) \end{eqnarray*} -\begin{figure} -\begin{ttbox} -structure Data = Datatype_Fun - (val thy = Univ.thy - val thy_name = "Data" - val rec_specs = [("data", "univ(A Un B)", - [(["Con0"], "i", NoSyn), - (["Con1"], "i=>i", NoSyn), - (["Con2"], "[i,i]=>i", NoSyn), - (["Con3"], "[i,i,i]=>i", NoSyn)])] - val rec_styp = "[i,i]=>i" - val sintrs = - ["Con0 : data(A,B)", - "[| a: A |] ==> Con1(a) : data(A,B)", - "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", - "[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"] - val monos = [] - val type_intrs = datatype_intrs - val type_elims = datatype_elims); -\end{ttbox} -\hrule -\caption{Defining the four-constructor sample datatype} \label{data-fig} -\end{figure} \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. Figure~\ref{data-fig} presents the ML definition. -Because this datatype has two set parameters, $A$ and~$B$, it specifies -$\univ(A\un B)$ as its domain. The structural induction rule has four -minor premises, one per constructor: +constructors $\Con_0$, \ldots, $\Con_3$, with the corresponding arities. +\begin{ttbox} +Data = Univ + +consts data :: "[i,i] => i" +datatype "data(A,B)" = Con0 + | Con1 ("a: A") + | Con2 ("a: A", "b: B") + | Con3 ("a: A", "b: B", "d: data(A,B)") +end +\end{ttbox} +Because this datatype has two set parameters, $A$ and~$B$, the package +automatically supplies $\univ(A\un B)$ as its domain. The structural +induction rule has four minor premises, one per constructor: \[ \infer{P(x)}{x\in\data(A,B) & P(\Con_0) & \infer*{P(\Con_1(a))}{[a\in A]_a} & @@ -1392,9 +1337,14 @@ \newpage \appendix \section{Inductive and coinductive definitions: users guide} -The ML functors \verb|Inductive_Fun| and \verb|CoInductive_Fun| build -inductive and coinductive definitions, respectively. This section describes -how to invoke them. +A theory file may contain any number of inductive and coinductive +definitions. They may be intermixed with other declarations; in +particular, the (co)inductive sets {\bf must} be declared separately as +constants, and may have mixfix syntax or be subject to syntax translations. + +Each (co)inductive definition adds definitions to the theory and also +proves some theorems. Each definition creates an ML structure, which is a +substructure of the main theory structure. \subsection{The result structure} Many of the result structure's components have been discussed @@ -1412,7 +1362,8 @@ \item[\tt dom\_subset] is a theorem stating inclusion in the domain. \item[\tt intrs] is the list of introduction rules, now proved as theorems, for -the recursive sets. +the recursive sets. The rules are also available individually, using the +names given them in the theory file. \item[\tt elim] is the elimination rule. @@ -1447,66 +1398,63 @@ \end{ttbox} \hrule \caption{The result of a (co)inductive definition} \label{def-result-fig} - -\medskip -\begin{ttbox} -sig -val thy : theory -val thy_name : string -val rec_doms : (string*string) list -val sintrs : string list -val monos : thm list -val con_defs : thm list -val type_intrs : thm list -val type_elims : thm list -end -\end{ttbox} -\hrule -\caption{The argument of a (co)inductive definition} \label{def-arg-fig} \end{figure} -\subsection{The argument structure} -Both \verb|Inductive_Fun| and \verb|CoInductive_Fun| take the same argument -structure (Figure~\ref{def-arg-fig}). Its components are as follows: -\begin{description} -\item[\tt thy] is the definition's parent theory, which {\it must\/} -declare constants for the recursive sets. +\subsection{The syntax of a (co)inductive definition} +An inductive definition has the form +\begin{ttbox} +inductive + domains {\it domain declarations} + intrs {\it introduction rules} + monos {\it monotonicity theorems} + con_defs {\it constructor definitions} + type_intrs {\it introduction rules for type-checking} + type_elims {\it elimination rules for type-checking} +\end{ttbox} +A coinductive definition is identical save that it starts with the keyword +{\tt coinductive}. -\item[\tt thy\_name] is a string, informing Isabelle's theory database of - the name you will give to the result structure. - -\item[\tt rec\_doms] is a list of pairs, associating the name of each recursive -set with its domain. +The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims} +sections are optional. If present, each is specified as a string, which +must be a valid ML expression of type {\tt thm list}. It is simply +inserted into the {\tt .thy.ML} file; if it is ill-formed, it will trigger +ML error messages. You can then inspect the file on your directory. -\item[\tt sintrs] specifies the desired introduction rules as strings. +\begin{description} +\item[\it domain declarations] consist of one or more items of the form + {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with + its domain. -\item[\tt monos] consists of monotonicity theorems for each operator applied -to a recursive set in the introduction rules. +\item[\it introduction rules] specify one or more introduction rules in + the form {\it ident\/}~{\it string}, where the identifier gives the name of + the rule in the result structure. -\item[\tt con\_defs] contains definitions of constants appearing in the -introduction rules. The (co)datatype package supplies the constructors' -definitions here. Most direct calls of \verb|Inductive_Fun| or -\verb|CoInductive_Fun| pass the empty list; one exception is the primitive -recursive functions example (\S\ref{primrec-sec}). +\item[\it monotonicity theorems] are required for each operator applied to + a recursive set in the introduction rules. There {\bf must} be a theorem + of the form $A\sbs B\Imp M(A)\sbs M(B)$, for each premise $t\in M(R_i)$ + in an introduction rule! -\item[\tt type\_intrs] consists of introduction rules for type-checking the +\item[\it constructor definitions] contain definitions of constants + appearing in the introduction rules. The (co)datatype package supplies + the constructors' definitions here. Most (co)inductive definitions omit + this section; one exception is the primitive recursive functions example + (\S\ref{primrec-sec}). + +\item[\it type\_intrs] consists of introduction rules for type-checking the definition, as discussed in~\S\ref{basic-sec}. They are applied using depth-first search; you can trace the proof by setting + \verb|trace_DEPTH_FIRST := true|. -\item[\tt type\_elims] consists of elimination rules for type-checking the -definition. They are presumed to be `safe' and are applied as much as -possible, prior to the {\tt type\_intrs} search. +\item[\it type\_elims] consists of elimination rules for type-checking the + definition. They are presumed to be `safe' and are applied as much as + possible, prior to the {\tt type\_intrs} search. \end{description} + The package has a few notable restrictions: \begin{itemize} -\item The parent theory, {\tt thy}, must declare the recursive sets as - constants. You can extend a theory with new constants using {\tt - addconsts}, as illustrated in~\S\ref{ind-eg-sec}. If the inductive - definition also requires new concrete syntax, then it is simpler to - express the parent theory using a theory file. It is often convenient to - define an infix syntax for relations, say $a\prec b$ for $\pair{a,b}\in - R$. +\item The theory must separately declare the recursive sets as + constants. \item The names of the recursive sets must be identifiers, not infix operators. @@ -1517,16 +1465,14 @@ \section{Datatype and codatatype definitions: users guide} -The ML functors \verb|Datatype_Fun| and \verb|CoDatatype_Fun| define datatypes -and codatatypes, invoking \verb|Datatype_Fun| and -\verb|CoDatatype_Fun| to make the underlying (co)inductive definitions. +This section explains how to include (co)datatype declarations in a theory +file. \subsection{The result structure} The result structure extends that of (co)inductive definitions (Figure~\ref{def-result-fig}) with several additional items: \begin{ttbox} -val con_thy : theory val con_defs : thm list val case_eqns : thm list val free_iffs : thm list @@ -1535,11 +1481,6 @@ \end{ttbox} Most of these have been discussed in~\S\ref{data-sec}. Here is a summary: \begin{description} -\item[\tt con\_thy] is a new theory containing definitions of the -(co)datatype's constructors and case operator. It also declares the -recursive sets as constants, so that it may serve as the parent -theory for the (co)inductive definition. - \item[\tt con\_defs] is a list of definitions: the case operator followed by the constructors. This theorem list can be supplied to \verb|mk_cases|, for example. @@ -1570,74 +1511,60 @@ and (co)induction rule. -\begin{figure} +\subsection{The syntax of a (co)datatype definition} +A datatype definition has the form \begin{ttbox} -sig -val thy : theory -val thy_name : string -val rec_specs : (string * string * (string list*string)list) list -val rec_styp : string -val sintrs : string list -val monos : thm list -val type_intrs: thm list -val type_elims: thm list -end +datatype <={\it domain} + {\it datatype declaration} and {\it datatype declaration} and \ldots + monos {\it monotonicity theorems} + type_intrs {\it introduction rules for type-checking} + type_elims {\it elimination rules for type-checking} \end{ttbox} -\hrule -\caption{The argument of a (co)datatype definition} \label{data-arg-fig} -\end{figure} +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 ZF source +directory. -\subsection{The argument structure} -Both (co)datatype functors take the same argument structure -(Figure~\ref{data-arg-fig}). It does not extend that for (co)inductive -definitions, but shares several components and passes them uninterpreted to -\verb|Datatype_Fun| or \verb|CoDatatype_Fun|. The new components are as -follows: -\begin{description} -\item[\tt thy] is the (co)datatype's parent theory. It {\it must not\/} -declare constants for the recursive sets. Recall that (co)inductive -definitions have the opposite restriction. +The {\tt monos}, {\tt type\_intrs} and {\tt type\_elims} sections are +optional. They are treated like their counterparts in a (co)inductive +definition, as described above. The package supplements your type-checking +rules (if any) with additional ones that should cope with any +finitely-branching (co)datatype definition. -\item[\tt rec\_specs] is a list of triples of the form ({\it recursive set\/}, -{\it domain\/}, {\it constructors\/}) for each mutually recursive set. {\it -Constructors\/} is a list of the form (names, type, mixfix). The mixfix -component is usually {\tt NoSyn}, specifying no special syntax for the -constructor; other useful possibilities are {\tt Infixl}~$p$ and {\tt - Infixr}~$p$, specifying an infix operator of priority~$p$. -Section~\ref{data-sec} presents examples. +\begin{description} +\item[\it domain] specifies a single domain to use for all the mutually + recursive (co)datatypes. If it (and the preceeding~{\tt <=}) are + omitted, the package supplies a domain automatically. Suppose the + definition involves the set parameters $A_1$, \ldots, $A_k$. Then + $\univ(A_1\un\cdots\un A_k)$ is used for a datatype definition and + $\quniv(A_1\un\cdots\un A_k)$ is used for a codatatype definition. + + These choices should work for all finitely-branching (co)datatype + definitions. For examples of infinitely-branching datatype + definitions, see the file {\tt ZF/ex/Brouwer.thy}. -\item[\tt rec\_styp] is the common meta-type of the mutually recursive sets, -specified as a string. They must all have the same type because all must -take the same parameters. +\item[\it datatype declaration] has the form +\begin{quote} + {\it string\/} {\tt =} {\it constructor} {\tt|} {\it constructor} {\tt|} + \ldots +\end{quote} +The {\it string\/} is the datatype, say {\tt"list(A)"}. Each +{\it constructor\/} has the form +\begin{quote} + {\it name\/} {\tt(} {\it premise} {\tt,} {\it premise} {\tt,} \ldots {\tt)} + {\it mixfix\/} +\end{quote} +The {\it name\/} specifies a new constructor while the {\it premises\/} its +typing conditions. The optional {\it mixfix\/} phrase may give +the constructor infix, for example. + +Mutually recursive {\it datatype declarations\/} are separated by the +keyword~{\tt and}. \end{description} -The choice of domain is usually simple. Isabelle/ZF defines the set -$\univ(A)$, which contains~$A$ and is closed under the standard Cartesian -products and disjoint sums \cite[\S4.2]{paulson-set-II}. In a typical -datatype definition with set parameters $A_1$, \ldots, $A_k$, a suitable -domain for all the recursive sets is $\univ(A_1\un\cdots\un A_k)$. For a -codatatype definition, the set -$\quniv(A)$ contains~$A$ and is closed under the variant Cartesian products -and disjoint sums; the appropriate domain is -$\quniv(A_1\un\cdots\un A_k)$. -The {\tt sintrs} specify the introduction rules, which govern the recursive -structure of the datatype. Introduction rules may involve monotone -operators and side-conditions to express things that go beyond the usual -notion of datatype. The theorem lists {\tt monos}, {\tt type\_intrs} and -{\tt type\_elims} should contain precisely what is needed for the -underlying (co)inductive definition. Isabelle/ZF defines lists of -type-checking rules that can be supplied for the latter two components: -\begin{itemize} -\item {\tt datatype\_intrs} and {\tt datatype\_elims} are rules -for $\univ(A)$. -\item {\tt codatatype\_intrs} and {\tt codatatype\_elims} are -rules for $\quniv(A)$. -\end{itemize} -In typical definitions, these theorem lists need not be supplemented with -other theorems. - -The constructor definitions' right-hand sides can overlap. A -simple example is the datatype for the combinators, whose constructors are +\paragraph*{Note.} +In the definitions of the constructors, the right-hand sides may overlap. +For instance, the datatype of combinators has constructors defined by \begin{eqnarray*} {\tt K} & \equiv & \Inl(\emptyset) \\ {\tt S} & \equiv & \Inr(\Inl(\emptyset)) \\