--- a/Paper/Paper.thy	Tue Mar 30 13:58:07 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 15:07:42 2010 +0200
@@ -28,7 +28,7 @@
   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
   Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
-  supp_gen ("aux _" [1000] 100)
+  supp_gen ("aux _" [1000] 10)
 (*>*)
 
 
@@ -556,17 +556,17 @@
   \end{property}
 
   \begin{property}
-  For a finite set @{text xs} and a finitely supported @{text x} with
-  @{term "xs \<sharp>* x"} and also a finitely supported @{text c}, there
-  exists a permutation @{text p} such that @{term "(p \<bullet> xs) \<sharp>* c"} and
+  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"}.
   \end{property}
 
   \noindent
-  The idea behind the second property is that given a finite set @{text xs}
+  The idea behind the second property is that given a finite set @{text as}
   of binders (being bound in @{text x} which is ensured by the
-  assumption @{term "xs \<sharp>* x"}), then there exists a permutation @{text p} such that
-  the renamed binders @{term "p \<bullet> xs"} avoid the @{text c} (which can be arbitrarily chosen
+  assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
+  the renamed binders @{term "p \<bullet> as"} avoid the @{text c} (which can be arbitrarily chosen
   as long as it is finitely supported) and also does not affect anything
   in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
@@ -625,7 +625,7 @@
   dependent on a free-variable function @{text "fv"} 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, $R$ will be replaced by equality @{text "="} and for raw terms we
+  the latter case, $R$ will be replaced by equality @{text "="} and we
   will prove that @{text "fv"} is equal to the support of @{text
   x} and @{text y}.
 
@@ -759,9 +759,10 @@
   \end{center}
 
   \noindent
-  indicating that a set or list is abstracted in @{text x}. We will call the types
-  \emph{abstraction types} and their elements \emph{abstractions}. The important 
-  property we need is a characterisation for the support of abstractions, namely
+  indicating that a set or list @{text as} is abstracted in @{text x}. We will
+  call the types \emph{abstraction types} and their elements
+  \emph{abstractions}. The important property we need is a characterisation
+  for the support of abstractions, namely:
 
   \begin{thm}[Support of Abstractions]\label{suppabs} 
   Assuming @{text x} has finite support, then\\[-6mm] 
@@ -769,13 +770,13 @@
   \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}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)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+  @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
   \end{thm}
 
   \noindent
-  We will only show the first equation as the others 
+  We will show below the first equation as the others 
   follow similar arguments. By definition of the abstraction type @{text "abs_set"} 
   we have 
   %
@@ -792,34 +793,33 @@
   \end{equation}
 
   \noindent
-  The last fact derives from the definition of permutations acting on pairs 
-  (see \eqref{permute}) and alpha-equivalence being equivariant (see Lemma~\ref{alphaeq}).
-
-  With these two facts at our disposal, we can show the following lemma 
-  about swapping two atoms.
+  The second fact derives from the definition of permutations acting on pairs 
+  (see \eqref{permute}) and alpha-equivalence being equivariant 
+  (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
+  the following lemma about swapping two atoms.
   
   \begin{lemma}
-  @{thm[mode=IfThen] abs_swap1(1)[no_vars]}
+  @{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
   \end{lemma}
 
   \begin{proof}
-  By using \eqref{abseqiff}, this lemma is straightforward when observing that 
-  the assumptions give us
-  @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
-  and set difference are equivariant.
+  By using \eqref{abseqiff}, this lemma is straightforward when observing that
+  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}
+  and that @{text supp} and set difference are equivariant.
   \end{proof}
 
   \noindent
-  This lemma gives us
+  This lemma allows us to show
   %
   \begin{equation}\label{halfone}
   @{thm abs_supports(1)[no_vars]}
   \end{equation}
   
   \noindent
-  which with Property~\ref{supportsprop} gives us one half of
-  Thm~\ref{suppabs}. The other half is a bit more involved. For this we use a
-  trick from \cite{Pitts04} and first define an auxiliary function
+  which by Property~\ref{supportsprop} gives us ``one half'' of
+  Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
+  it, we use a trick from \cite{Pitts04} and first define an auxiliary 
+  function taking an abstraction as argument
   %
   \begin{center}
   @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
@@ -827,32 +827,31 @@
   
   \noindent
   Using the second equation in \eqref{equivariance}, we can show that 
-  @{term "supp_gen"} is equivariant and therefore has empty support. This 
-  in turn means
+  @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
+  (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. 
+  This in turn means
   %
   \begin{center}
-  @{thm (prem 1) aux_fresh(1)[where bs="as", no_vars]}
-  \;\;implies\;\;
-  @{thm (concl) aux_fresh(1)[where bs="as", no_vars]}
+  @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
   \end{center}
 
   \noindent
-  using \eqref{suppfun}. Since @{term "supp x"} is by definition equal 
-  to @{term "{a. \<not> a \<sharp> x}"} we can establish that
+  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set
+  we further obtain
   %
   \begin{equation}\label{halftwo}
   @{thm (concl) supp_abs_subset1(1)[no_vars]}
   \end{equation}
 
   \noindent
-  provided @{text x} has finite support (the precondition we need in order to show 
-  that for a finite set of atoms, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}).
+  since for finite sets, @{text "S"}, we have 
+  @{thm (concl) supp_finite_atom_set[no_vars]}).
 
   Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
   of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we 
   can define and prove properties about them conveniently on the Isabelle/HOL level,
-  and in addition can use them in what
-  follows next when we have to deal with binding in specifications of term-calculi. 
+  but also use them in what follows next when we deal with binding in specifications 
+  of term-calculi. 
 *}
 
 section {* Alpha-Equivalence and Free Variables *}