diff -r d5b223b9c2bb -r a5501c9fad9b Paper/Paper.thy --- a/Paper/Paper.thy Wed Mar 24 19:50:42 2010 +0100 +++ b/Paper/Paper.thy Thu Mar 25 07:21:41 2010 +0100 @@ -528,30 +528,30 @@ section {* Alpha-Equivalence and Free Variables *} text {* - Our specifications for term-calculi are heavily - inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is - a collection of (possibly mutual recursive) type declarations, say - $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an - associated collection of binding functions, say - $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle - for such specifications is rougly as follows: + Our specifications for term-calculi are heavily inspired by the existing + datatype package of Isabelle/HOL 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 + of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text + bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is + rougly as follows: % \begin{equation}\label{scheme} \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l} type \mbox{declaration part} & $\begin{cases} \mbox{\begin{tabular}{l} - \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\ - \isacommand{and} $ty^\alpha_2 = \ldots$\\ + \isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\ + \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\ $\ldots$\\ - \isacommand{and} $ty^\alpha_n = \ldots$\\ + \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ \end{tabular}} \end{cases}$\\ binding \mbox{function part} & $\begin{cases} \mbox{\begin{tabular}{l} - \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$ - $\ldots$\\ + \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\ \isacommand{where}\\ $\ldots$\\ \end{tabular}} @@ -560,22 +560,22 @@ \end{equation} \noindent - Every type declaration $ty^\alpha_i$ consists of a collection of + Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of term-constructors, each of which comes with a list of labelled types that stand for the types of the arguments of the term-constructor. - For example a term-constructor $C^\alpha$ might have + For example a term-constructor @{text "C\<^sup>\"} might have \begin{center} - $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ + @{text "C\<^sup>\ label\<^isub>1::ty"}$'_1$ @{text "\ label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"} \end{center} \noindent - whereby some of the $ty'_k$ (or their components) are contained in the collection - of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the + 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 the scope of - the binders in a term-constructor. They come in three \emph{modes} + \emph{binding clauses}. These clauses indicate the binders and their scope of + in a term-constructor. They come in three \emph{modes}: \begin{center} @@ -588,17 +588,17 @@ \noindent The first mode is for binding lists of atoms (the order of binders matters); the second is for sets - of binders (the order does not matter, but cardinality does) and the last is for + 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} binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\; - \isacommand{in}\; {\it another\_label} (similar for the other two modes). The + \isacommand{in}\; {\it label'} (similar for the other two modes). The restriction we impose on shallow binders is that the {\it label} must either refer to a type that is an atom type or to a type that is a finite set or - list of an atom type. For example the specifications for lambda-terms, where - a single name is bound, and type-schemes, where a finite set of names is - bound, use shallow binders (the type \emph{name} is an atom type): + list of an atom type. Two examples for the use of shallow binders are the + specification of lambda-terms, where a single name is bound, and of + type-schemes, where a finite set of names is bound: \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -620,12 +620,13 @@ \end{center} \noindent + Note that in this specification \emph{name} refers to an atom type. If we have shallow binders that ``share'' a body, for instance $t$ in - the term-constructor Foo$_0$ + the following term-constructor \begin{center} \begin{tabular}{ll} - \it {\rm Foo}$_0$ x::name y::name t::lam & \it + \it {\rm Foo} x::name y::name t::lam & \it \isacommand{bind}\;x\;\isacommand{in}\;t,\; \isacommand{bind}\;y\;\isacommand{in}\;t \end{tabular} @@ -633,19 +634,19 @@ \noindent then we have to make sure the modes of the binders agree. We cannot - have in the first binding clause the mode \isacommand{bind} and in the second - \isacommand{bind\_set}. + have, for instance, in the first binding clause the mode \isacommand{bind} + and in the second \isacommand{bind\_set}. A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms in one argument of the term-constructor, which can be bound in other arguments and also in the same argument (we will - call such binders \emph{recursive}). + call such binders \emph{recursive}, see below). The binding functions are expected to return either a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can be defined by primitive recursion over the corresponding type; the equations must be given in the binding function part of the scheme shown in \eqref{scheme}. For example for a calculus containing lets - with tuple patterns, you might declare + with tuple patterns, you might specify \begin{center} \begin{tabular}{l} @@ -657,52 +658,59 @@ \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$} PNo\\ - \hspace{5mm}$\mid$ PVr\;{\it name}\\ - \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\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} $bn(\textrm{PNil}) = []$\\ - \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\ - \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\ + \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)$\\ \end{tabular} \end{center} \noindent - In this specification the function $atom$ coerces a name into the generic - atom type of Nominal Isabelle. This allows us to treat binders of different - atom type uniformly. As will shortly become clear, we cannot return an atom in a - binding function that also is bound in the term-constructor. In the present - version of Nominal Isabelle, we adopted the restriction the Ott-tool imposes - on the binding functions, namely a binding function can only return the - empty set (case PNil), a singleton set containing an atom (case PVar) or - unions of atom sets (case PPrd). Moreover, as with shallow binders, deep - binders with shared body need to have the same binding mode. Finally, 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: + 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"} + coerces a name into the generic atom type of Nominal Isabelle. This allows + us to treat binders of different atom type uniformly. + + As will shortly become clear, we cannot return an atom in a binding function + that is also bound in the corresponding term-constructor. That means in the + example above that the term-constructors PVar and PTup must not have a + binding clause. In the present version of Nominal Isabelle, we also adopted + the restriction from the Ott-tool that binding functions can only return: + 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 + we cannot have ``overlapping'' deep binders. Consider for example the + term-constructors: \begin{center} \begin{tabular}{ll} - \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; + \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}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\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 \end{tabular} \end{center} \noindent - In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms - from $q$ in $t$. As a result we have no way to determine whether the binder came from the - binding function in $p$ or $q$. Similarly in the second case: - the binder $bn(p)$ overlaps with the shallow binder $x$. We must exclude such specifiactions, - as we will not be able to represent them using the general binders described in - Section \ref{sec:binders}. However the following two term-constructors are allowed: + In the first case we bind all atoms from the pattern @{text p} in @{text t} + and also all atoms from @{text q} in @{text t}. As a result we have no way + to determine whether the binder came from the binding function @{text + "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder + @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why + we must exclude such specifiactions is that they cannot be represent by + the general binders described in Section \ref{sec:binders}. However + the following two term-constructors are allowed \begin{center} \begin{tabular}{ll} - \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; + \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}$_2$ p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\; + \it {\rm Bar}$'$p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\; \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\ \end{tabular} \end{center} @@ -710,15 +718,19 @@ \noindent since there is no overlap of binders. - Let us come back one more time to the specification of simultaneous lets. - A specification for them looks as follows: + Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}. + Whenver 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: \begin{center} - \begin{tabular}{l} + \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype} {\it trm} =\\ \hspace{5mm}\phantom{$\mid$}\ldots\\ \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\ + \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm} + \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}, + \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\ \isacommand{and} {\it assn} =\\ \hspace{5mm}\phantom{$\mid$} ANil\\ \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\ @@ -729,65 +741,77 @@ \end{center} \noindent - The intention with this specification is to bind all variables - from the assignments inside the body @{text t}. However one might - like to consider the variant where the variables are not just - bound in @{term t}, but also in the assignments themselves. In - this case we need to specify + The difference is that with Let we only want to bind the atoms @{text + "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms + inside the assignment. This requires recursive binders and also has + consequences for the free variable function and alpha-equivalence relation, + which we are going to explain in the rest of this section. + + Having dealt with all syntax matters, the problem now is how we can turn + specifications into actual type definitions in Isabelle/HOL and then + establish a reasoning infrastructure for them. Because of the problem + Pottier and Cheney pointed out, we cannot in general re-arrange arguments of + 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-equiavlence 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 \begin{center} - \begin{tabular}{l} - Let\_rec\;{\it a::assn}\; {\it t::trm} - \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}, - \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\ - \end{tabular} + @{text "ty\<^sup>\ \ ty_raw"} \hspace{7mm} @{text "C\<^sup>\ \ C_raw"} \end{center} \noindent - where we bind also in @{text a} all the atoms @{text bn} returns. In this - case we will say the binder is a \emph{recursive binder}. - - Having dealt with all syntax matters, the problem now is how we can turn - specifications into actual type - definitions in Isabelle/HOL and then establish a reasoning infrastructure - for them. Because of the problem Pottier and Cheney pointed out, we cannot - in general re-arrange arguments of term-constructors so that binders and - their bodies next to each other, an 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-equiavlence relation over them. - - The datatype definition can be obtained by just stripping of the - binding clauses and the labels on the types. We also have to invent - new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$ - given by user. We just use an affix like + 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 explanataion 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 \begin{center} - $ty^\alpha \mapsto ty\_raw \qquad C^\alpha \mapsto C\_raw$ + @{text "p \ (C_raw x\<^isub>1 \ x\<^isub>n) \ C_raw (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} \end{center} \noindent - The datatype definition can be made, provided the usual conditions hold: - the datatypes must be non-empty and they must only occur in positive - position (see \cite{}). We then consider the user-specified binding - functions and define them by primitive recursion over the raw datatypes. + 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. + + The first non-trivial step we have to perform is the generatation free-variable + functions from the specifications. Given types @{text "ty\<^isub>1, \, ty\<^isub>n"} + we need to define the free-variable functions + + \begin{center} + @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \ atom set \ fv_ty\<^isub>n :: ty\<^isub>n \ atom set"} + \end{center} + + \noindent + and given binding functions @{text "bn_ty\<^isub>1, \, bn_ty\<^isub>m"} we also need to define + the free-variable functions - The first non-trivial step we have to generate free-variable - functions from the specifications. The basic idea is to collect - all atoms that are not bound, but because of the rather complicated - binding mechanisms the details are somewhat involved. - There are two kinds of free-variable functions: one corresponds to types, - written $\fv\_ty$, and the other corresponds to binding functions, - written $\fv\_bn$. They have to be defined at the same time, since there can - be dependencies between them. + \begin{center} + @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \ atom set \ fv_bn_ty\<^isub>m :: ty\<^isub>m \ atom set"} + \end{center} - Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with - some binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be - the union of the values generated for each argument, say $x_i$ with type $ty_i$. - By the binding clause we know whether the argument $x_i$ is a shallow or deep - binder and in the latter case also whether it is a recursive or non-recursive - of a binder. In these cases we return as value: + \noindent + The basic idea behind these free-variable functions is to collect all atoms + 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 + 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 + whether it is a recursive or non-recursive of a binder. In these cases the value is: \begin{center} \begin{tabular}{cp{7cm}} @@ -798,12 +822,13 @@ \end{center} \noindent - The binding clause will also give us whether the argument @{term "x\<^isub>i"} is - a body of one or more abstractions. There are two cases: either the + In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of + one or more abstractions. There are two cases: either the corresponding binders are all shallow or there is a single deep binder. In the former case we build the union of all shallow binders; in the later case we just take set or list of atoms the specified binding - function returns. Below use @{text "bnds"} to stand for them. + function returns. Let @{text "bnds"} be an abbreviation of the bound + atoms. Then the value is given by: \begin{center} \begin{tabular}{cp{7cm}} @@ -816,13 +841,37 @@ \end{center} \noindent - If the argument is neither a binder, nor a body, then it is defined as - the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms + If the argument is neither a binder, nor a body of an abstraction, then the + value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms are abstracted. + TODO + + Given a clause of a binding function of the form + + \begin{center} + @{text "bn_ty (C_raw x\<^isub>1 \ x\<^isub>n) = rhs"} + \end{center} + + \noindent + then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the + union of the values calculated for the @{text "x\<^isub>j"} as follows: + + \begin{center} + \begin{tabular}{cp{7cm}} + $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\ + $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} + with the recursive call @{text "bn_ty x\<^isub>j"}\\ + $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ + $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ + $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ + $\bullet$ & @{term "{}"} otherwise + \end{tabular} + \end{center} + *} - +section {* The Lifting of Definitions and Properties *} text {* Restrictions