diff -r 54becd55d83a -r e78cd33a246f Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 26 18:44:47 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 26 22:02:59 2010 +0100
@@ -6,8 +6,6 @@
 consts
   fv :: "'a \<Rightarrow> 'b"
   abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-  Abs_lst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
-  Abs_res :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 
 definition
  "equal \<equiv> (op =)" 
@@ -19,9 +17,9 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and
-  alpha_lst ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and
-  alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and
+  alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
+  alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
+  alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   fv ("fv'(_')" [100] 100) and
   equal ("=") and
@@ -412,9 +410,9 @@
   \noindent
   For a proof see \cite{HuffmanUrban10}.
 
-  \begin{property}
-  @{thm[mode=IfThen] at_set_avoiding[no_vars]}
-  \end{property}
+  %\begin{property}
+  %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
+  %\end{property}
 
 *}
 
@@ -444,8 +442,8 @@
   variables; moreover there must be a permutation @{text p} such that {\it
   ii)} it leaves the free variables 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 equal terms. We also require {\it iv)} that
-  @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The
+  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
+  @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it i)} to {\it iv)} can be stated formally as follows:
   %
   \begin{equation}\label{alphaset}
@@ -502,7 +500,8 @@
   \end{equation}
 
   \begin{exmple}\rm
-  It might be useful to consider some examples for how these definitions pan out in practise.
+  It might be useful to consider some examples for how these definitions of alpha-equivalence
+  pan out in practise.
   For this consider the case of abstracting a set of variables over types (as in type-schemes). 
   We set @{text R} to be the equality and for @{text "fv(T)"} we define
 
@@ -556,55 +555,53 @@
 
 
   In the rest of this section we are going to introduce a type- and term-constructor 
-  for abstractions. For this we define 
+  for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$ 
+  and $\approx_{\textit{abs\_res}}$)
   %
   \begin{equation}
   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
   \end{equation}
   
   \noindent
-  Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these 
-  relations are equivalence relations and equivariant 
+  We can show that these relations are equivalence relations and equivariant 
   (we only show the $\approx_{\textit{abs\_set}}$-case).
 
-  \begin{lemma}
+  \begin{lemma}\label{alphaeq}
   $\approx_{\textit{abs\_set}}$ is an equivalence
-  relations, and if @{term "abs_set (as, x) (bs, x)"} then also
-  @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}.
+  relations, 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)"}.
   \end{lemma}
 
   \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 the conditions are then by simple
+  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
   calculations. 
   \end{proof}
 
+  \noindent 
+  We are also define the following two auxiliary functions taking a pair
+  as argument.
+  %
+  \begin{equation}\label{aux}
+  \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+  @{text "aux (as, x)"}      & @{text "\<equiv>"} & @{text "supp x - as"}\\
+  @{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"}
+  \end{array}
+  \end{equation}
+  
   \noindent
-  The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and 
-  $\approx_{\textit{abs\_res}}$) will be crucial below: 
-
-  \begin{lemma}
-  @{thm[mode=IfThen] alpha_abs_swap[no_vars]}
-  \end{lemma}
+  The point of these two functions is that they are preserved under
+  alpha-equivalence, that means for instance
+  %
+  \begin{equation}\label{auxpreserved}
+  @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\; 
+  @{term "aux (as, x) = aux (bs, y)"}
+  \end{equation}
 
-  \begin{proof}
-  This lemma is straightforward by observing that the assumptions give us
-  @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
-  is equivariant.
-  \end{proof}
-
-  \noindent 
-  We are also define the following  
-
-  @{text "aux (as, x) \<equiv> supp x - as"}
-
-  
-
-  \noindent
-  This allows us to use our quotient package and introduce new types
-  @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+  Lemma \ref{alphaeq} allows us to use our quotient package and introduce 
+  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   representing the alpha-equivalence classes. Elements in these types 
   we will, respectively, write as:
 
@@ -614,6 +611,28 @@
   @{term "Abs_res as x"}
   \end{center}
 
+  \noindent
+  By definition we have 
+
+  \begin{center}
+  @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\; 
+  @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  \end{center}
+
+
+  \noindent
+  The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and 
+  $\approx_{\textit{abs\_res}}$) will be crucial below: 
+
+  \begin{lemma}
+  @{thm[mode=IfThen] abs_swap1(1)[no_vars]}
+  \end{lemma}
+
+  \begin{proof}
+  This lemma is straightforward by observing that the assumptions give us
+  @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
+  is equivariant.
+  \end{proof}
 
   \begin{lemma}
   $supp ([as]set. x) = supp x - as$ 
@@ -1000,6 +1019,13 @@
 text {*
   Complication when the single scopedness restriction is lifted (two 
   overlapping permutations)
+
+
+  The formalisation presented here will eventually become part of the 
+  Isabelle distribution, but for the moment it can be downloaded from 
+  the Mercurial repository linked at 
+  \href{http://isabelle.in.tum.de/nominal/download}
+  {http://isabelle.in.tum.de/nominal/download}.\medskip
 *}
 
 text {*