--- a/LMCS-Paper/Paper.thy Wed Sep 07 12:38:32 2011 +0100
+++ b/LMCS-Paper/Paper.thy Thu Sep 08 11:21:03 2011 +0100
@@ -30,6 +30,8 @@
fv ("fa'(_')" [100] 100) and
equal ("=") and
alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
+ alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and
+ alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and
Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
Abs_lst ("[_]\<^bsub>list\<^esub>._") and
Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
@@ -94,7 +96,7 @@
binders by iterating single binders, this leads to a rather clumsy
formalisation of W. The need of iterating single binders is also one reason
why Nominal Isabelle and similar theorem provers that only provide
- mechanisms for binding single variables has not fared extremely well with
+ mechanisms for binding single variables have not fared extremely well with
the more advanced tasks in the POPLmark challenge \cite{challenge05},
because also there one would like to bind multiple variables at once.
@@ -123,8 +125,8 @@
give a general binding mechanism and associated notion of alpha-equivalence
that can be used to faithfully represent this kind of binding in Nominal
Isabelle. The difficulty of finding the right notion for alpha-equivalence
- can be appreciated in this case by considering that the definition given by
- Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
+ can be appreciated in this case by considering that the definition given for
+ type-schemes by Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
However, the notion of alpha-equivalence that is preserved by vacuous
binders is not always wanted. For example in terms like
@@ -361,7 +363,7 @@
Figure~\ref{corehas}). This term language involves patterns that have lists
of type-, coercion- and term-variables, all of which are bound in @{text
"\<CASE>"}-expressions. In these patterns we do not know in advance how many
- variables need to be bound. Another example is the algorithm W
+ variables need to be bound. Another example is the algorithm W,
which includes multiple binders in type-schemes.\medskip
\noindent
@@ -432,7 +434,7 @@
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,
+ c, \<dots>"} to stand for atoms and @{text "\<pi>, \<pi>\<^isub>1, \<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
@@ -449,7 +451,7 @@
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
- operation is defined over the type-hierarchy \cite{HuffmanUrban10};
+ operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
for example permutations acting on products, lists, sets, functions and booleans are
given by:
@@ -610,7 +612,9 @@
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 "\<pi> \<bullet> x = x"}.
+ @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. Note that @{term "supp x \<sharp>* \<pi>"}
+ is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also use the other
+ `direction' in Propositions \ref{supppermeq} and \ref{avoiding}.
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
@@ -732,15 +736,15 @@
abstract a single atom.
In the rest of this section we are going to introduce three abstraction
- types. For this we define
+ types. For this we define the relations
\begin{equation}
- \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)"}\\
+ \begin{array}{r}
+ @{term "alpha_abs_set (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}\\
+ @{term "alpha_abs_res (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, y)"}\\
+ @{term "alpha_abs_lst (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, y)"}\\
\end{array}
- \end{equation}
+ \end{equation}\smallskip
\noindent
We can show that these relations are equivalence
@@ -748,32 +752,35 @@
\begin{lem}\label{alphaeq}
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
- and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if
+ and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant.
+ %, and if
%@{term "abs_set (as, x) (bs, y)"} then also
%@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
\end{lem}
\begin{proof}
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
+ a permutation @{text "\<pi>"} 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.
+ proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
+ @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} holds provided
+ @{term "abs_set (as, x) (bs, y)"}.
+
\end{proof}
\noindent
This lemma allows us to use our quotient package for introducing
- new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
+ 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
- \begin{center}
- @{term "Abs_set as x"}, \hspace{5mm}
- @{term "Abs_res as x"} and \hspace{5mm}
- @{term "Abs_lst as x"},
- \end{center}
+ \[
+ @{term "Abs_set as x"} \hspace{10mm}
+ @{term "Abs_res as x"} \hspace{10mm}
+ @{term "Abs_lst as x"}
+ \]\smallskip
\noindent
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
@@ -784,37 +791,33 @@
\begin{thm}[Support of Abstractions]\label{suppabs}
Assuming @{text x} has finite support, then
- \begin{center}
- \begin{tabular}{l}
- @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$
- @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\
- @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$
- @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}
- \end{tabular}
- \end{center}
+ \[
+ \begin{array}{l@ {\;=\;}l}
+ @{thm (lhs) supp_Abs(1)[no_vars]} & @{thm (rhs) supp_Abs(1)[no_vars]}\\
+ @{thm (lhs) supp_Abs(2)[no_vars]} & @{thm (rhs) supp_Abs(2)[no_vars]}\\
+ @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} &
+ @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\
+ \end{array}
+ \]\smallskip
\end{thm}
\noindent
This theorem states that the bound names do not appear in the support.
- For brevity we omit the proof and again refer the reader to
- our formalisation in Isabelle/HOL.
+ Below we will show the first equation. The others follow by similar
+ arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
- \noindent
- Below we will show the first equation. The others
- follow by similar arguments. By definition of the abstraction type @{text "abs_set"}
- we have
\begin{equation}\label{abseqiff}
@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\;
- @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
- \end{equation}
+ @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
+ \end{equation}\smallskip
\noindent
and also
\begin{equation}\label{absperm}
- @{thm permute_Abs[no_vars]}
- \end{equation}
+ @{thm permute_Abs(1)[where p="\<pi>", no_vars]}
+ \end{equation}\smallskip
\noindent
The second fact derives from the definition of permutations acting on pairs