--- a/LMCS-Paper/Paper.thy Tue Sep 06 12:18:02 2011 +0100
+++ b/LMCS-Paper/Paper.thy Wed Sep 07 12:38:32 2011 +0100
@@ -101,7 +101,7 @@
Binding multiple variables has interesting properties that cannot be captured
easily by iterating single binders. For example in the case of type-schemes we do not
want to make a distinction about the order of the bound variables. Therefore
- we would like to regard below the first pair of type-schemes as alpha-equivalent,
+ we would like to regard in \eqref{ex1} below the first pair of type-schemes as alpha-equivalent,
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
the second pair should \emph{not} be alpha-equivalent:
@@ -378,7 +378,7 @@
The main improvement over Ott is that we introduce three binding modes
(only one is present in Ott), provide formalised definitions for alpha-equivalence and
for free variables of our terms, and also derive a reasoning infrastructure
- for our specifications from ``first principles''.
+ for our specifications from ``first principles'' inside a theorem prover.
\begin{figure}
@@ -431,14 +431,14 @@
to aid the description of what follows.
Two central notions in the nominal logic work are sorted atoms and
- sort-respecting permutations of atoms. We will use the letters @{text "a,
- b, c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for
- permutations. The purpose of atoms is to represent variables, be they bound or free.
- The sorts of atoms can be used to represent different kinds of
- variables, such as the term-, coercion- and type-variables in Core-Haskell.
- It is assumed that there is an infinite supply of atoms for each
- sort. In the interest of brevity, we shall restrict ourselves
- in what follows to only one sort of atoms.
+ sort-respecting permutations of atoms. We will use the letters @{text "a, b,
+ c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for permutations,
+ which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to
+ represent variables, be they bound or free. The sorts of atoms can be used
+ to represent different kinds of variables, such as the term-, coercion- and
+ type-variables in Core-Haskell. It is assumed that there is an infinite
+ supply of atoms for each sort. In the interest of brevity, we shall restrict
+ ourselves in what follows to only one sort of atoms.
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
@@ -487,7 +487,7 @@
\begin{equation}\label{suppdef}
@{thm supp_def[no_vars, THEN eq_reflection]}
- \end{equation}
+ \end{equation}\smallskip
\noindent
There is also the derived notion for when an atom @{text a} is \emph{fresh}
@@ -508,7 +508,7 @@
\begin{prop}\label{swapfreshfresh}
If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
- then @{thm (concl) swap_fresh_fresh[no_vars]}
+ then @{thm (concl) swap_fresh_fresh[no_vars]}.
\end{prop}
While often the support of an object can be relatively easily
@@ -539,7 +539,7 @@
notion \emph{supports}, defined as follows:
\begin{defi}
- A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+ A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b}
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
\end{defi}
@@ -548,8 +548,10 @@
two properties.
\begin{prop}\label{supportsprop}
- Given a set @{text "as"} of atoms.
- {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+ Given a set @{text "as"} of atoms.\\
+ {\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]}
+ and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then
+ @{thm (concl) supp_is_subset[where S="as", no_vars]}.\\
{\it (ii)} @{thm supp_supports[no_vars]}.
\end{prop}
@@ -558,17 +560,17 @@
it is required that every permutation leaves @{text f} unchanged, that is
\begin{equation}\label{equivariancedef}
- @{term "\<forall>p. p \<bullet> f = f"}
- \end{equation}
+ @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
+ \end{equation}\smallskip
\noindent or equivalently that a permutation applied to the application
@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
- functions @{text f}, we have for all permutations @{text p}:
+ functions @{text f}, we have for all permutations @{text "\<pi>"}:
\begin{equation}\label{equivariance}
- @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
- @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
- \end{equation}
+ @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
+ @{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+ \end{equation}\smallskip
\noindent
From property \eqref{equivariancedef} and the definition of @{text supp}, we
@@ -577,7 +579,7 @@
that
\begin{center}
- @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+ @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
\end{center}
Using freshness, the nominal logic work provides us with general means for renaming
@@ -585,35 +587,34 @@
\noindent
While in the older version of Nominal Isabelle, we used extensively
- Property~\ref{swapfreshfresh}
- this property to rename single binders, it this property
+ Property~\ref{swapfreshfresh} to rename single binders, this property
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
\begin{prop}\label{supppermeq}
- @{thm[mode=IfThen] supp_perm_eq[no_vars]}
+ @{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}
\end{prop}
\begin{prop}\label{avoiding}
For a finite set @{text as} and a finitely supported @{text x} with
@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
- exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
- @{term "supp x \<sharp>* p"}.
+ exists a permutation @{text "\<pi>"} such that @{term "(\<pi> \<bullet> as) \<sharp>* c"} and
+ @{term "supp x \<sharp>* \<pi>"}.
\end{prop}
\noindent
The idea behind the second property is that given a finite set @{text as}
of binders (being bound, or fresh, in @{text x} is ensured by the
- assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
- the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
- as long as it is finitely supported) and also @{text "p"} does not affect anything
- in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
+ assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
+ the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
+ as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
+ in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last
fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
- @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
+ @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
Most properties given in this section are described in detail in \cite{HuffmanUrban10}
and all are formalised in Isabelle/HOL. In the next sections we will make
- extensive use of these properties in order to define alpha-equivalence in
+ use of these properties in order to define alpha-equivalence in
the presence of multiple binders.
*}
@@ -628,7 +629,7 @@
In order to keep our work with deriving the reasoning infrastructure
manageable, we will wherever possible state definitions and perform proofs
- on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. that
+ on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
generates them anew for each specification.
To that end, we will consider
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
@@ -641,48 +642,48 @@
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
- atoms; moreover there must be a permutation @{text p} such that {\it
- (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
+ atoms; moreover there must be a permutation @{text \<pi>} such that {\it
+ (ii)} @{text \<pi>} leaves the free atoms of @{text x} and @{text y} unchanged, but
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
- @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
+ @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
- %
- \begin{equation}\label{alphaset}
- \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
- \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} &
- \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"} \\
- \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* p"} &
- \mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"} \\
- \end{array}
- \end{equation}
- %
+
+ \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
+ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
+ @{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\
+ & \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
+ & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"} \\
+ & \mbox{\it (iv)} & @{term "(\<pi> \<bullet> as) = bs"} \\
+ \end{tabular}
+ \end{defi}
+
\noindent
Note that this relation depends on the permutation @{text
- "p"}; alpha-equivalence between two pairs is then the relation where we
- existentially quantify over this @{text "p"}. Also note that the relation is
+ "\<pi>"}; alpha-equivalence between two pairs is then the relation where we
+ existentially quantify over this @{text "\<pi>"}. Also note that the relation is
dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
$\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
the latter case, @{text R} will be replaced by equality @{text "="} and we
will prove that @{text "fa"} is equal to @{text "supp"}.
- The definition in \eqref{alphaset} does not make any distinction between the
+ Definition \ref{alphaset} does not make any distinction between the
order of abstracted atoms. If we want this, then we can define alpha-equivalence
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
as follows
- %
- \begin{equation}\label{alphalist}
- \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
- \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"} &
- \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
- \mbox{\it (ii)} & @{term "(fa(x) - set as) \<sharp>* p"} &
- \mbox{\it (iv)} & @{term "(p \<bullet> as) = bs"}\\
- \end{array}
- \end{equation}
- %
+
+ \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
+ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
+ @{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ & \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\
+ & \mbox{\it (ii)} & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
+ & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
+ & \mbox{\it (iv)} & @{term "(\<pi> \<bullet> as) = bs"}\\
+ \end{tabular}
+ \end{defi}
+
\noindent
where @{term set} is the function that coerces a list of atoms into a set of atoms.
Now the last clause ensures that the order of the binders matters (since @{text as}
@@ -690,38 +691,39 @@
If we do not want to make any difference between the order of binders \emph{and}
also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop
- condition {\it (iv)} in \eqref{alphaset}:
- %
- \begin{equation}\label{alphares}
- \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
- \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"} &
- \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
- \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* p"}\\
- \end{array}
- \end{equation}
+ condition {\it (iv)} in Definition~\ref{alphaset}:
+
+ \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
+ \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
+ @{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ & \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\
+ & \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
+ & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
+ \end{tabular}
+ \end{defi}
+
It might be useful to consider first some examples how these definitions
of alpha-equivalence pan out in practice. For this consider the case of
abstracting a set of atoms over types (as in type-schemes). We set
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
define
- %
- \begin{center}
+
+ \[
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
- \end{center}
+ \]\smallskip
\noindent
Now recall the examples shown in \eqref{ex1} and
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
@{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
- $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to
+ $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
since there is no permutation that makes the lists @{text "[x, y]"} and
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$
- @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+ @{text "({x, y}, x)"} which holds by taking @{text "\<pi>"} to be the identity
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
@@ -731,15 +733,18 @@
In the rest of this section we are going to introduce three abstraction
types. For this we define
- %
+
\begin{equation}
- @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
+ \begin{array}{l}
+ @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, x)"}\\
+ @{term "abs_res (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, x)"}\\
+ @{term "abs_lst (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, x)"}\\
+ \end{array}
\end{equation}
\noindent
- (similarly for $\approx_{\,\textit{abs\_set+}}$
- and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
- relations. %% and equivariant.
+ We can show that these relations are equivalence
+ relations and equivariant.
\begin{lem}\label{alphaeq}
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
@@ -749,10 +754,10 @@
\end{lem}
\begin{proof}
- Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
- a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
- of transitivity, we have two permutations @{text p} and @{text q}, and for the
- proof obligation use @{text "q + p"}. All conditions are then by simple
+ Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
+ a permutation @{text p} and for the proof obligation take @{term "- \<pi>"}. In case
+ of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
+ proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. All conditions are then by simple
calculations.
\end{proof}