--- a/Paper/Paper.thy	Fri Apr 02 06:45:50 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 07:30:25 2010 +0200
@@ -1465,8 +1465,8 @@
 text {*
   Having made all necessary definitions for raw terms, we can start
   introducing the reasoning infrastructure for the alpha-equated types the
-  user specified. We sketch in this section the facts we need for establishing
-  this reasoning infrastructure. We first have to show that the
+  user originally specified. We sketch in this section the facts we need for establishing
+  this reasoning infrastructure. First we have to show that the
   alpha-equivalence relations defined in the previous section are indeed
   equivalence relations.
 
@@ -1485,18 +1485,18 @@
 
   \noindent 
   We can feed this lemma into our quotient package and obtain new types @{text
-  "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text
-  "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text
+  "ty"}$^\alpha_{1..n}$ representing alpha-equated terms. We also obtain 
+  definitions for the term-constructors @{text
   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
-  "C"}$_{1..m}$. Similarly for the free-variable functions @{text
+  "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
-  "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the 
-  user, since the are formulated in terms of the isomorphisms we obtained by 
+  "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the 
+  user, since the are given in terms of the isomorphisms we obtained by 
   creating new types in Isabelle/HOL (recall the picture shown in the 
   Introduction).
 
-  The first useful property about term-constructors 
-  is to know that they are distinct, that is
+  The first useful property to the user is the fact that term-constructors are 
+  distinct, that is
   %
   \begin{equation}\label{distinctalpha}
   \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 
@@ -1508,39 +1508,39 @@
   for the raw term-constructors
   %
   \begin{equation}\label{distinctraw}
-  @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;\not\approx@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
+  \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}
   \end{equation}
 
   \noindent
-  In order to generate \eqref{distinctalpha} from this fact, the quotient
+  In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 
-  are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}.
-  This means, given @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
-  @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, we have to show that
+  are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
+  Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
+  @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, then respectfulness amounts to showing
   
   \begin{center}
   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
   \end{center}  
 
   \noindent
-  under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
-  and  @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by 
-  analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish an
-  auxiliary fact: given a binding function @{text bn} defined for the type @{text ty}
-  we have that
-
+  are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
+  and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments. We can prove this by 
+  analysing the definition of @{text "\<approx>ty"}. For this to succeed we have to establish 
+  the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 
+  for the type @{text ty\<^isub>i}, we have that
+  %
   \begin{center}
-  @{text "x \<approx>ty y"} implies @{text "x \<approx>bn y"}
+  @{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"}
   \end{center}
 
   \noindent
-  This can be established by induction on the definition of @{text "\<approx>ty"}. 
+  This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. 
    
   Having established respectfulness for every raw term-constructor, the 
-  quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
-  In fact we can lift any fact from the raw level to the alpha-equated level that
-  apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The 
-  induction principles derived by the datatype package of Isabelle/HOL for @{text
+  quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
+  In fact we can from now on lift any fact from the raw level to the alpha-equated level that
+  apart from variables only contains the raw term-constructors. The 
+  induction principles derived by the datatype package in Isabelle/HOL for teh types @{text
   "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
   induction principles that establish
 
@@ -1549,8 +1549,9 @@
   \end{center} 
 
   \noindent
-  for every @{text "y\<^isub>i"} under the assumption we specified the types
-  @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of these induction principles look
+  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
+  defined over the types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of 
+  these induction principles look
   as follows
 
   \begin{center}
@@ -1561,10 +1562,11 @@
   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
   Next we lift the permutation operations defined in \eqref{ceqvt} for
   the raw term-constructors @{text "C"}. These facts contain, in addition 
-  to the term-constructors, also permutations operations. Therefore
-  we have to know that permutation operations are respectful 
-  w.r.t.~alpha-equivalence, which amounts to knowing that the 
-  alpha-equivalence relations are equivariant, which we established 
+  to the term-constructors, also permutations operations. In order to make the 
+  lifting to go through, 
+  we have to know that the permutation operations are respectful 
+  w.r.t.~alpha-equivalence. This amounts to showing that the 
+  alpha-equivalence relations are equivariant, which we already established 
   in Lemma~\ref{equiv}. As a result we can add the equations
   
   \begin{equation}\label{ceqvt}
@@ -1573,25 +1575,28 @@
 
   \noindent
   to our infrastructure. In a similar fashion we can lift the equations
-  characterising our free-variable functions and the binding functions. 
-  The necessary respectfulness lemmas are
+  characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and the 
+  binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for this
+  lifting are the two properties:
   %
   \begin{equation}\label{fnresp}
   \mbox{%
   \begin{tabular}{l}
-  @{text "x \<approx>ty y"} implies @{text "fv_ty x = fv_ty y"}\\
-  @{text "x \<approx>ty y"} implies @{text "bn x = bn y"}
+  @{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\
+  @{text "x \<approx>ty\<^isub>j y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}
   \end{tabular}}
   \end{equation}
 
   \noindent
-  which can be established by induction on @{text "\<approx>ty"}. While the first
-  kind of lemma is always ensured by way of how we defined the free variable
-  functions, the second does not hold in general. It only if the @{text bn}-functions 
-  do not return any atom that is also bound. Hence our restriction imposed
-  on the binding functions that excludes this possibility. 
+  which can be established by induction on @{text "\<approx>ty"}. Whereas the first
+  property is always true by the way how we defined the free-variable
+  functions, the second does \emph{not} hold in general. There is, in principle, 
+  the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
+  variable. Then the second property is just not true. However, our 
+  restrictions imposed on the binding functions
+  exclude this possibility.
 
-  Having the facts \eqref{fnresp} at our disposal, we can finally lift the
+  Having the facts \eqref{fnresp} at our disposal, we can lift the
   definitions that characterise when two terms of the form
 
   \begin{center}
@@ -1607,13 +1612,13 @@
   \end{center}
 
   \noindent
-  We call these conditions as \emph{quasi-injectivity}. Except for one definition we have
-  to lift in the next section, this completes
+  We call these conditions as \emph{quasi-injectivity}. Except for one function, which
+  we have to lift in the next section, this stage completes
   the lifting part of establishing the reasoning infrastructure. From
-  now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only
-  reason with @{text "ty\<AL>\<^bsub>1..n\<^esub>"}
+  now on, we can almost completely ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only
+  reason about @{text "ty\<AL>\<^bsub>1..n\<^esub>"}.
 
-  We can first show that the free-variable function and binding functions
+  We can first show that the free-variable functions and binding functions
   are equivariant, namely
 
   \begin{center}
@@ -1624,18 +1629,18 @@
   \end{center}
 
   \noindent
-  These facts can be established by structural induction over the @{text x}.
+  These two properties can be established by structural induction over the @{text x}.
 
   Until now we have not yet derived any fact about the support of the 
   alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can
   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
 
   \begin{center}
-  @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+  @{text "supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}.
   \end{center}
  
   \noindent
-  holds. This together with Property~\ref{supportsprobs} allows us to show
+  This together with Property~\ref{supportsprop} allows us to show
  
 
   \begin{center}
@@ -1643,11 +1648,12 @@
   \end{center}
 
   \noindent
-  by mutual structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types 
+  by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types 
   @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in 
   @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\<AL>\<^bsub>1..n\<^esub>"}.
 
-  \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that 
+  \begin{lemma} 
+  For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that 
   @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.
   \end{lemma}