# HG changeset patch # User lcp # Date 775480886 -7200 # Node ID 990d2573efa629d27f600b4d0e889775138b7cb4 # Parent 3fc829fa81d299ab2f27838d17fb237ad63a21f9 revised for new theory system: removal of ext, addition of thy_name diff -r 3fc829fa81d2 -r 990d2573efa6 doc-src/ind-defs.tex --- a/doc-src/ind-defs.tex Fri Jul 29 11:09:45 1994 +0200 +++ b/doc-src/ind-defs.tex Fri Jul 29 13:21:26 1994 +0200 @@ -1,6 +1,6 @@ -\documentstyle[a4,proof,iman,extra,times]{llncs} +\documentstyle[a4,proof,iman,extra,12pt]{llncs} \newif\ifCADE -\CADEtrue +\CADEfalse \title{A Fixedpoint Approach to Implementing\\ (Co)Inductive Definitions\thanks{J. Grundy and S. Thompson made detailed @@ -503,7 +503,8 @@ $\{a\}\un b$ in Isabelle/ZF): \begin{ttbox} structure Fin = Inductive_Fun - (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] + (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)"] @@ -548,7 +549,8 @@ \begin{figure} \begin{ttbox} structure ListN = Inductive_Fun - (val thy = ListFn.thy addconsts [(["listn"],"i=>i")] + (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)", @@ -556,7 +558,7 @@ val monos = [] val con_defs = [] val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] - val type_elims = [SigmaE2]); + val type_elims = []); \end{ttbox} \hrule \caption{Defining lists of $n$ elements} \label{listn-fig} @@ -688,15 +690,16 @@ To make this coinductive definition, we invoke \verb|CoInductive_Fun|: \begin{ttbox} structure LList_Eq = CoInductive_Fun - (val thy = LList.thy addconsts [(["lleq"],"i=>i")] + (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 @ [SigmaI] - val type_elims = [SigmaE2]); + val type_intrs = LList.intrs + val type_elims = []); \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 @@ -753,7 +756,8 @@ supplied the theorem {\tt Pow\_mono}, which asserts that $\pow$ is monotonic. \begin{ttbox} structure Acc = Inductive_Fun - (val thy = WF.thy addconsts [(["acc"],"i=>i")] + (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] @@ -829,6 +833,7 @@ \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", @@ -995,11 +1000,11 @@ \begin{ttbox} structure List = Datatype_Fun (val thy = Univ.thy + val thy_name = "List" val rec_specs = [("list", "univ(A)", - [(["Nil"], "i"), - (["Cons"], "[i,i]=>i")])] + [(["Nil"], "i", NoSyn), + (["Cons"], "[i,i]=>i", NoSyn)])] val rec_styp = "i=>i" - val ext = None val sintrs = ["Nil : list(A)", "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"] val monos = [] @@ -1013,11 +1018,11 @@ \begin{ttbox} structure LList = CoDatatype_Fun (val thy = QUniv.thy + val thy_name = "LList" val rec_specs = [("llist", "quniv(A)", - [(["LNil"], "i"), - (["LCons"], "[i,i]=>i")])] + [(["LNil"], "i", NoSyn), + (["LCons"], "[i,i]=>i", NoSyn)])] val rec_styp = "i=>i" - val ext = None val sintrs = ["LNil : llist(A)", "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"] val monos = [] @@ -1094,13 +1099,13 @@ \begin{ttbox} structure TF = Datatype_Fun (val thy = Univ.thy + val thy_name = "TF" val rec_specs = [("tree", "univ(A)", - [(["Tcons"], "[i,i]=>i")]), + [(["Tcons"], "[i,i]=>i", NoSyn)]), ("forest", "univ(A)", - [(["Fnil"], "i"), - (["Fcons"], "[i,i]=>i")])] + [(["Fnil"], "i", NoSyn), + (["Fcons"], "[i,i]=>i", NoSyn)])] val rec_styp = "i=>i" - val ext = None val sintrs = ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", "Fnil : forest(A)", @@ -1182,13 +1187,13 @@ \begin{ttbox} structure Data = Datatype_Fun (val thy = Univ.thy + val thy_name = "Data" val rec_specs = [("data", "univ(A Un B)", - [(["Con0"], "i"), - (["Con1"], "i=>i"), - (["Con2"], "[i,i]=>i"), - (["Con3"], "[i,i,i]=>i")])] + [(["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 ext = None val sintrs = ["Con0 : data(A,B)", "[| a: A |] ==> Con1(a) : data(A,B)", @@ -1447,6 +1452,7 @@ \begin{ttbox} sig val thy : theory +val thy_name : string val rec_doms : (string*string) list val sintrs : string list val monos : thm list @@ -1466,6 +1472,9 @@ \item[\tt thy] is the definition's parent theory, which {\it must\/} declare constants for the recursive sets. +\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. @@ -1565,9 +1574,9 @@ \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 ext : Syntax.sext option val sintrs : string list val monos : thm list val type_intrs: thm list @@ -1582,8 +1591,8 @@ 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: +\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 @@ -1591,18 +1600,15 @@ \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). See the discussion and -examples in~\S\ref{data-sec}. +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. \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[\tt ext] is an optional syntax extension, usually omitted by writing -{\tt None}. You can supply mixfix syntax for the constructors by supplying -\begin{ttbox} -Some (Syntax.simple_sext [{\it mixfix declarations\/}]) -\end{ttbox} \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