# HG changeset patch # User Christian Urban # Date 1315734133 -3600 # Node ID 21674aea64e001a3075732cce4af7c79bbc67145 # Parent c5de60da0bcf0f95b176d4e1ab9f5cb5e6de8c58 more on paper diff -r c5de60da0bcf -r 21674aea64e0 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Sat Sep 10 00:03:42 2011 +0100 +++ b/LMCS-Paper/Paper.thy Sun Sep 11 10:42:13 2011 +0100 @@ -284,7 +284,7 @@ a new type by identifying a non-empty subset of an existing type. The construction we perform in Isabelle/HOL can be illustrated by the following picture: - \[ + \begin{equation}\label{picture} \mbox{\begin{tikzpicture}[scale=1.1] %\draw[step=2mm] (-4,-1) grid (4,1); @@ -306,7 +306,7 @@ \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism}; \end{tikzpicture}} - \]\smallskip + \end{equation}\smallskip \noindent We take as the starting point a definition of raw terms (defined as a @@ -494,7 +494,7 @@ definition for the notion of the ``set of free variables of an object @{text "x"}''. This notion, written @{term "supp x"}, is general in the sense that it applies not only to lambda-terms (alpha-equated or not), but also to lists, - products, sets and even functions. The definition depends only on the + products, sets and even functions. Its definition depends only on the permutation operation and on the notion of equality defined for the type of @{text x}, namely: @@ -750,7 +750,8 @@ abstract a single atom. In the rest of this section we are going to show that the alpha-equivalences really - lead to abstractions where some atoms are bound. For this we are going to introduce + lead to abstractions where some atoms are bound (more precisely removed from the + support). For this we are going to introduce three abstraction types that are quotients with respect to the relations \begin{equation} @@ -766,7 +767,6 @@ with @{term "supp"} and the relation @{text R} with equality. We can show the following properties: - \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$ and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. @@ -785,7 +785,8 @@ \end{proof} \noindent - This lemma allows us to use our quotient package for introducing + Recall the picture shown in \eqref{picture} about new types in HOL. + The lemma above allows us to use our quotient package for introducing new types @{text "\ abs\<^bsub>set\<^esub>"}, @{text "\ abs\<^bsub>set+\<^esub>"} and @{text "\ abs\<^bsub>list\<^esub>"} representing alpha-equivalence classes of pairs of type @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} @@ -896,7 +897,7 @@ This is because for every finite sets of atoms, say @{text "bs"}, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes - Theorem~\ref{suppabs}. + the first equation of Theorem~\ref{suppabs}. The method of first considering abstractions of the form @{term "Abs_set as x"} etc is motivated by the fact that we can conveniently establish at the @@ -947,7 +948,8 @@ term-constructor @{text "C\<^sup>\"} might be specified with \[ - @{text "C\<^sup>\ label\<^isub>1::ty"}\mbox{$'_1$} @{text "\ label\<^isub>l::ty"}\mbox{$'_l\;\;$} @{text "binding_clauses"} + @{text "C\<^sup>\ label\<^isub>1::ty"}\mbox{$'_1$} @{text "\ label\<^isub>l::ty"}\mbox{$'_l\;\;\;\;\;$} + @{text "binding_clauses"} \]\smallskip \noindent @@ -1092,7 +1094,7 @@ into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows us to treat binders of different atom type uniformly. - As said above, for deep binders we allow binding clauses such as + For deep binders we allow binding clauses such as \[\mbox{ \begin{tabular}{ll} @@ -1156,29 +1158,29 @@ terms. The main restriction is that we cannot return an atom in a binding function that is also bound in the corresponding term-constructor. Consider again the specification for @{text "trm"} and a contrived - version for assignments, @{text "assn"}: + version for assignments @{text "assn"}: \begin{equation}\label{bnexp} \mbox{% \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ \isacommand{and} @{text "assn"} $=$\\ - \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ - \hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"} + \hspace{5mm}\phantom{$\mid$}~@{text "ANil'"}\\ + \hspace{5mm}$\mid$~@{text "ACons' x::name y::name t::trm assn"} \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\ \isacommand{binder} @{text "bn::assn \ atom list"}\\ - \isacommand{where}~@{text "bn(ANil) = []"}\\ - \hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\ + \isacommand{where}~@{text "bn(ANil') = []"}\\ + \hspace{5mm}$\mid$~@{text "bn(ACons' x y t as) = [atom x] @ bn(as)"}\\ \end{tabular}} \end{equation}\smallskip \noindent - In this example the term constructor @{text "ACons"} contains a binding + In this example the term constructor @{text "ACons'"} contains a binding clause, and also is used in the definition of the binding function. The restriction we have to impose is that the binding function can only return free atoms, that is the ones that are not mentioned in a binding clause. Therefore @{text "y"} cannot be used in the binding function @{text "bn"} - (since it is bound in @{text "ACons"} by the binding clause), but @{text x} + (since it is bound in @{text "ACons'"} by the binding clause), but @{text x} can (since it is a free atom). This restriction is sufficient for lifting the binding function to alpha-equated terms. If we would permit that @{text "bn"} can also return @{text "y"}, then it would not be respectful and therefore @@ -1186,9 +1188,9 @@ In the version of Nominal Isabelle described here, we also adopted the restriction from the Ott-tool that binding functions can only return: the - empty set or empty list (as in case @{text ANil}), a singleton set or + empty set or empty list (as in case @{text ANil'}), a singleton set or singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or - unions of atom sets or appended atom lists (case @{text ACons}). This + unions of atom sets or appended atom lists (case @{text ACons'}). This restriction will simplify some automatic definitions and proofs later on. In order to simplify our definitions of free atoms and alpha-equivalence, @@ -1248,7 +1250,7 @@ in Isabelle/HOL). We subsequently define each of the user-specified binding functions @{term "bn"}$_{1..m}$ by recursion over the corresponding - raw datatype. We can also easily define permutation operations by + raw datatype. We also define permutation operations by recursion so that for each term constructor @{text "C"} we have that \begin{equation}\label{ceqvt} @@ -1257,7 +1259,7 @@ The first non-trivial step we have to perform is the generation of \emph{free-atom functions} from the specification.\footnote{Admittedly, the - details of our definitions are somewhat involved. However they are still + details of our definitions will be somewhat involved. However they are still conceptually simple in comparison with the ``positional'' approach taken in Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and \emph{partial equivalence relations} over sets of occurences.} For the @@ -1321,7 +1323,7 @@ where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason - for the latter choice is that @{text "ty"}$_i$ is not a type that is part of the specification, and + for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and we assume @{text supp} is the generic notion that characterises the free variables of a type (in fact in the next section we will show that the free-variable functions we define here, are equal to the support once lifted to alpha-equivalence classes). @@ -1329,28 +1331,28 @@ In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions for atom types to which shallow binders may refer\\[-4mm] - \[\mbox{ + \begin{equation}\label{bnaux}\mbox{ \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\"} & @{text "{atom a}"}\\ @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\"} & @{text "atoms as"}\\ @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\"} & @{text "atoms (set as)"} \end{tabular}} - \]\smallskip + \end{equation}\smallskip \noindent Like the function @{text atom}, the function @{text "atoms"} coerces a set of atoms to a set of the generic atom type. It is defined as @{text "atoms as \ {atom a | a \ as}"}. - The set @{text B} is then formally defined as + The set @{text B} in \eqref{fadef} is then formally defined as \begin{equation}\label{bdef} @{text "B \ bn_ty\<^isub>1 b\<^isub>1 \ ... \ bn_ty\<^isub>p b\<^isub>p"} \end{equation}\smallskip \noindent - where we use the auxiliary binding functions for shallow binders (that means - when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or - @{text "atom list"}). The set @{text "B'"} collects all free atoms in + where we use the auxiliary binding functions from \eqref{bnaux} for shallow + binders (that means when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or + @{text "atom list"}). The set @{text "B'"} in \eqref{fadef} collects all free atoms in non-recursive deep binders. Let us assume these binders in the binding clause @{text "bc\<^isub>i"} are @@ -1359,8 +1361,8 @@ \]\smallskip \noindent - with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see - \eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies + with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and + none of the @{text "l"}$_{1..r}$ being among the bodies @{text "d"}$_{1..q}$. The set @{text "B'"} is defined as \begin{equation}\label{bprimedef} @@ -1368,11 +1370,11 @@ \end{equation}\smallskip \noindent - This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$. + This completes all clauses for the free-atom functions @{text "fa_ty"}$_{1..n}$. Note that for non-recursive deep binders, we have to add in \eqref{fadef} the set of atoms that are left unbound by the binding functions @{text - "bn"}$_{1..m}$, see also the definition in \eqref{bprimedef}. We used for + "bn"}$_{1..m}$. We used for the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The definition for those functions needs to be extracted from the clauses the user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text @@ -1391,7 +1393,8 @@ $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\ & (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\ $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"} - with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\smallskip\\ + with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\ + & (that means whatever is ``left over'' from the @{text "bn"}-function is free)\smallskip\\ $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}, but without a recursive call\\ & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\