# HG changeset patch # User Christian Urban # Date 1269961140 -7200 # Node ID 0c3c66f5c0e7e7e4f725c7b607ed82a95b38907c # Parent a3ef7fba983ff0139532c41503e21bff9827170f removed "raw" distinction diff -r a3ef7fba983f -r 0c3c66f5c0e7 Paper/Paper.thy --- a/Paper/Paper.thy Tue Mar 30 15:09:26 2010 +0200 +++ b/Paper/Paper.thy Tue Mar 30 16:59:00 2010 +0200 @@ -222,7 +222,7 @@ where no clause for variables is given. Arguably, such specifications make some sense in the context of Coq's type theory (which Ott supports), but not at all in a HOL-based environment where every datatype must have a non-empty - set-theoretic model. + set-theoretic model \cite{Berghofer99}. Another reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning @@ -844,21 +844,20 @@ \end{equation} \noindent - since for finite sets, @{text "S"}, we have - @{thm (concl) supp_finite_atom_set[no_vars]}). + since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}. - Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof - of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we - can define and prove properties about them conveniently on the Isabelle/HOL level, - but also use them in what follows next when we deal with binding in specifications - of term-calculi. + Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof + of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we + can define and prove them aconveniently on the Isabelle/HOL level, + but also use them in what follows next when we deal with binding in + specifications of term-calculi. *} section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *} text {* Our choice of syntax for specifications of term-calculi is influenced by the existing - datatype package of Isabelle/HOL and by the syntax of the Ott-tool + datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool \cite{ott-jfp}. A specification is a collection of (possibly mutual recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots, @{text ty}$^\alpha_n$, and an associated collection @@ -902,8 +901,8 @@ whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the corresponding argument a \emph{recursive argument}. The labels annotated on - the types are optional and can be used in the (possibly empty) list of - \emph{binding clauses}. These clauses indicate the binders and their scope of + the types are optional. Their purpose is to be used in the (possibly empty) list of + \emph{binding clauses}, which indicate the binders and their scope in a term-constructor. They come in three \emph{modes}: @@ -920,7 +919,7 @@ of binders (the order does not matter, but the cardinality does) and the last is for sets of binders (with vacuous binders preserving alpha-equivalence). - In addition we distinguish between \emph{shallow} binders and \emph{deep} + In addition we distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\; \isacommand{in}\; {\it label'} (similar for the other two modes). The restriction we impose on shallow binders is that the {\it label} must either @@ -932,18 +931,18 @@ \begin{center} \begin{tabular}{@ {}cc@ {}} \begin{tabular}{@ {}l@ {\hspace{-1mm}}} - \isacommand{nominal\_datatype} {\it lam} =\\ - \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\ - \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\ - \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\ - \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ + \isacommand{nominal\_datatype} @{text lam} =\\ + \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\ + \hspace{5mm}$\mid$~@{text "App lam lam"}\\ + \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\ + \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} - \isacommand{nominal\_datatype} {\it ty} =\\ - \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\ - \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\ - \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\ - \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\ + \isacommand{nominal\_datatype}~@{text ty} =\\ + \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ + \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ + \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\ + \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} \end{tabular} \end{center} @@ -955,9 +954,9 @@ \begin{center} \begin{tabular}{ll} - \it {\rm Foo} x::name y::name t::lam & \it - \isacommand{bind}\;x\;\isacommand{in}\;t,\; - \isacommand{bind}\;y\;\isacommand{in}\;t + @{text "Foo x::name y::name t::lam"} & + \isacommand{bind} @{text x} \isacommand{in} @{text t},\; + \isacommand{bind} @{text y} \isacommand{in} @{text t} \end{tabular} \end{center} @@ -979,27 +978,27 @@ \begin{center} \begin{tabular}{l} - \isacommand{nominal\_datatype} {\it trm} =\\ - \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\ - \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\ - \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} - \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\ - \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} - \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\ - \isacommand{and} {\it pat} =\\ - \hspace{5mm}\phantom{$\mid$} PNil\\ - \hspace{5mm}$\mid$ PVar\;{\it name}\\ - \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\ - \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\ - \isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\ - \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\ - \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\ + \isacommand{nominal\_datatype} @{text trm} =\\ + \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\ + \hspace{5mm}$\mid$~@{term "App trm trm"}\\ + \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} + \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ + \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} + \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ + \isacommand{and} @{text pat} =\\ + \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\ + \hspace{5mm}$\mid$~@{text "PVar name"}\\ + \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ + \isacommand{with}~@{text "bn::pat \ atom list"}\\ + \isacommand{where}~@{text "bn(PNil) = []"}\\ + \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ + \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\ \end{tabular} \end{center} \noindent In this specification the function @{text "bn"} determines which atoms of @{text p} are - bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"} + bound in the argument @{text "t"}. Note that in the second last clause the function @{text "atom"} coerces a name into the generic atom type of Nominal Isabelle. This allows us to treat binders of different atom type uniformly. @@ -1011,16 +1010,19 @@ the empty set or empty list (as in case PNil), a singleton set or singleton list containing an atom (case PVar), or unions of atom sets or appended atom lists (case PTup). This restriction will simplify proofs later on. - The the most drastic restriction we have to impose on deep binders is that + + The most drastic restriction we have to impose on deep binders is that we cannot have ``overlapping'' deep binders. Consider for example the term-constructors: \begin{center} \begin{tabular}{ll} - \it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; - \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\ - \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\; - \isacommand{bind}\;bn(p)\;\isacommand{in}\;t + @{text "Foo p::pat q::pat t::trm"} & + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\; + \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\ + @{text "Foo' x::name p::pat t::trm"} & + \isacommand{bind} @{text x} \isacommand{in} @{text t},\; + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} \end{tabular} \end{center} @@ -1037,10 +1039,12 @@ \begin{center} \begin{tabular}{ll} - \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; - \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\ - \it {\rm Bar}$'$p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\; - \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\ + @{text "Bar p::pat t::trm s::trm"} & + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\; + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\ + @{text "Bar' p::pat t::trm"} & + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text p},\; + \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ \end{tabular} \end{center} @@ -1049,7 +1053,7 @@ Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}. Whenever such a binding clause is present, we will call the binder \emph{recursive}. - To see the purpose for this, consider ``plain'' Lets and Let\_recs: + To see the purpose for this, compare ``plain'' Lets and Let\_recs: \begin{center} \begin{tabular}{@ {}l@ {}} @@ -1083,36 +1087,40 @@ term-constructors so that binders and their bodies are next to each other, and then use the type constructors @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first - extract datatype definitions from the specification and then define an - alpha-equivalence relation over them. + extract datatype definitions from the specification and then define + independently an alpha-equivalence relation over them. The datatype definition can be obtained by just stripping off the binding clauses and the labels on the types. We also have to invent new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} - given by user. In our implementation we just use an affix like + given by user. In our implementation we just use an affix @{text "_raw"}. + For the purpose of the paper we just use superscripts to indicate a + notion defined over alpha-equivalence classes and leave out the superscript + for the corresponding notion on the ``raw'' level. So for example: \begin{center} - @{text "ty\<^sup>\ \ ty_raw"} \hspace{7mm} @{text "C\<^sup>\ \ C_raw"} + @{text "ty\<^sup>\ \ ty"} \hspace{7mm} @{text "C\<^sup>\ \ C"} \end{center} \noindent The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are non-empty and the types in the constructors only occur in positive - position (see \cite{} for an indepth explanation of the datatype package + position (see \cite{Berghofer99} for an indepth explanation of the datatype package in Isabelle/HOL). We then define the user-specified binding functions by primitive recursion over the raw datatypes. We can also easily define a permutation operation by primitive recursion so that for each - term constructor @{text "C_raw ty\<^isub>1 \ ty\<^isub>n"} we have that + term constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"} we have that \begin{center} - @{text "p \ (C_raw x\<^isub>1 \ x\<^isub>n) \ C_raw (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} + @{text "p \ (C x\<^isub>1 \ x\<^isub>n) \ C (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} \end{center} - \noindent - From this definition we can easily show that the raw datatypes are - all permutation types (Def ??) by a simple structural induction over - the @{text "ty_raw"}s. + % TODO: we did not define permutation types + %\noindent + %From this definition we can easily show that the raw datatypes are + %all permutation types (Def ??) by a simple structural induction over + %the @{text "ty"}s. The first non-trivial step we have to perform is the generation free-variable functions from the specifications. Given types @{text "ty\<^isub>1, \, ty\<^isub>n"} @@ -1136,8 +1144,8 @@ that are not bound in a term constructor, but because of the rather complicated binding mechanisms the details are somewhat involved. - Given a term-constructor @{text "C_raw ty\<^isub>1 \ ty\<^isub>n"}, of type @{text ty} together with - some binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \ x\<^isub>n)"} will be + Given a term-constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"}, of type @{text ty} together with + some binding clauses, the function @{text "fv_ty (C x\<^isub>1 \ x\<^isub>n)"} will be the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}. From the binding clause of this term constructor, we can determine whether the argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also @@ -1184,7 +1192,7 @@ @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the omission of the arguments present in @{text "bn"}. - For a binding function clause @{text "bn (C_raw x\<^isub>1 \ x\<^isub>n) = rhs"}, + For a binding function clause @{text "bn (C x\<^isub>1 \ x\<^isub>n) = rhs"}, we define @{text "fv_bn"} to be the union of the values calculated for @{text "x\<^isub>j"} as follows: @@ -1219,8 +1227,8 @@ @{text "\bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \ ty\<^isub>i\<^isub>1 \ bool \ \bn\<^isub>n :: ty\<^isub>i\<^isub>m \ ty\<^isub>i\<^isub>m \ bool"} \end{center} - Given a term-constructor @{text "C_raw ty\<^isub>1 \ ty\<^isub>n"}, of a type @{text ty}, two instances - of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \ x\<^isub>n \ C_raw y\<^isub>1 \ y\<^isub>n"} if there + Given a term-constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"}, of a type @{text ty}, two instances + of this constructor are alpha-equivalent @{text "C x\<^isub>1 \ x\<^isub>n \ C y\<^isub>1 \ y\<^isub>n"} if there exist permutations @{text "\\<^isub>1 \ \\<^isub>p"} (one for each bound argument) such that the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds. For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if: @@ -1254,8 +1262,8 @@ for their respective types, the difference is that they ommit checking the arguments that are bound. We assumed that there are no bindings in the type on which the binding function is defined so, there are no permutations involved. For a binding function clause - @{text "bn (C_raw x\<^isub>1 \ x\<^isub>n) = rhs"}, two instances of the constructor are equivalent - @{text "C_raw x\<^isub>1 \ x\<^isub>n \ C_raw y\<^isub>1 \ y\<^isub>n"} if: + @{text "bn (C x\<^isub>1 \ x\<^isub>n) = rhs"}, two instances of the constructor are equivalent + @{text "C x\<^isub>1 \ x\<^isub>n \ C y\<^isub>1 \ y\<^isub>n"} if: \begin{center} \begin{tabular}{cp{7cm}} $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\ diff -r a3ef7fba983f -r 0c3c66f5c0e7 Paper/document/root.bib --- a/Paper/document/root.bib Tue Mar 30 15:09:26 2010 +0200 +++ b/Paper/document/root.bib Tue Mar 30 16:59:00 2010 +0200 @@ -1,3 +1,14 @@ +@InProceedings{Berghofer99, + author = {S.~Berghofer and M.~Wenzel}, + title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in + {F}ormal-{L}ogic {E}ngineering}, + booktitle = {Proc.~of the 12th International Conference Theorem Proving in + Higher Order Logics (TPHOLs)}, + pages = {19--36}, + year = 1999, + number = 1690, + series = {LNCS} +} @InProceedings{CoreHaskell, author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},