
diff -r 8d7d85e915b5 -r 02d98590454d LMCS-Paper/Paper.thy
--- 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 




