nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:c5de60da0bcf
+:21674aea64e0
 specification we will need to construct type(s) containing as elements the
 alpha-equated terms. To do so, we use the standard HOL-technique of defining
 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);
 \draw[very thick] (0.7,0.4) circle (4.25mm);
 \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
 \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
 \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
 datatype in Isabelle/HOL); then identify the alpha-equivalence classes in
 the type of sets of raw terms according to our alpha-equivalence relation,
 The most original aspect of the nominal logic work of Pitts is a general
 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:
 \begin{equation}\label{suppdef}
 @{thm supp_def[no_vars, THEN eq_reflection]}
 (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 shown that all three notions of alpha-equivalence coincide, if we only
 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}
 \begin{array}{r}
 @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
 \noindent
 Note that in these relation we replaced the free-atom function @{text "fa"}
 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.
 \end{lem}
 operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
 (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
 \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>"}
 (in the third case).
 The elements in these types will be, respectively, written as
 \noindent
 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
 Isabelle/HOL level properties about them.  It would be extremely laborious
 to write custom ML-code that derives automatically such properties for every
 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 @{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
 whereby some of the @{text ty}$'_{1..l}$ (or their components) can be
 contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in
 the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
 second-last @{text bn}-clause the function @{text "atom"} coerces a name
 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}
 @{text "Bar p::pat t::trm"} &
 \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
 We also need to restrict the form of the binding functions in order to
 ensure the @{text "bn"}-functions can be defined for alpha-equated
 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}\phantom{$\mid$}~@{text "ANil'"}\\
-\hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"}
+\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) = []"}\\
+\isacommand{where}~@{text "bn(ANil') = []"}\\
-\hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\
+\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
 cannot be lifted.
 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,
 we shall assume specifications
 of term-calculi are implicitly \emph{completed}. By this we mean that
 non-empty and the types in the constructors only occur in positive
 position (see \cite{Berghofer99} for an in-depth description of the datatype package
 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}
 @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
 \end{equation}\smallskip
 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
 \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 \noindent
 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).
 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
+where we use the auxiliary binding functions from \eqref{bnaux} for shallow
-when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
+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
+@{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
 \[
 \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
 \]\smallskip
 \noindent
-with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see
+with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and
-\eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies
+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}
 @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
 \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
 bn}-clause of the form
 \[\mbox{
 \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
 $\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)\\
 \end{tabular}}
 \]\smallskip

changeset 3008	21674aea64e0
parent 3007	c5de60da0bcf
child 3009	41c1e98c686f