--- 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 "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}
representing alpha-equivalence classes of pairs of type
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
@@ -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>\<alpha>"} might be specified with
\[
- @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;$} @{text "binding_clauses"}
+ @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> 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 \<Rightarrow> 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 "\<equiv>"} & @{text "{atom a}"}\\
@{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
@{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\<equiv>"} & @{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 \<equiv> {atom a | a \<in> 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 \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> 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)\\