diff -r 4c5881455923 -r 9807d30c0e54 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jul 07 09:34:00 2010 +0100
+++ b/Paper/Paper.thy	Wed Jul 07 13:13:18 2010 +0100
@@ -26,7 +26,7 @@
   alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
-  fv ("fv'(_')" [100] 100) and
+  fv ("fa'(_')" [100] 100) and
   equal ("=") and
   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
   Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
@@ -43,7 +43,6 @@
 section {* Introduction *}
 
 text {*
-%%%  @{text "(1, (2, 3))"}
 
   So far, Nominal Isabelle provided a mechanism for constructing
   $\alpha$-equated terms, for example lambda-terms
@@ -358,7 +357,7 @@
   about them in a theorem prover would be a major pain.  \medskip
 
   \noindent
-  {\bf Contributions:}  We provide novel three definitions for when terms
+  {\bf Contributions:}  We provide three novel definitions for when terms
   involving general binders are $\alpha$-equivalent. These definitions are
   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
   proofs, we establish a reasoning infrastructure for $\alpha$-equated
@@ -424,7 +423,8 @@
   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 "p, q, \<dots>"} to stand for
-  permutations.  The sorts of atoms can be used to represent different kinds of
+  permutations. 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 type-variables in Core-Haskell.
   It is assumed that there is an infinite supply of atoms for each
   sort. However, in the interest of brevity, we shall restrict ourselves 
@@ -520,7 +520,7 @@
   \end{eqnarray}
   
   \noindent 
-  In some cases it can be difficult to characterise the support precisely, and
+  in some cases it can be difficult to characterise the support precisely, and
   only an approximation can be established (see \eqref{suppfun} above). Reasoning about
   such approximations can be simplified with the notion \emph{supports}, defined 
   as follows:
@@ -621,10 +621,10 @@
   @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
   the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
-  given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
+  given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
   set"}}, then @{text x} and @{text y} need to have the same set of free
-  variables; moreover there must be a permutation @{text p} such that {\it
-  (ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
+  atomss; moreover there must be a permutation @{text p} such that {\it
+  (ii)} @{text p} leaves the free atoms 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 equivalent terms. We also require that {\it (iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
@@ -632,9 +632,9 @@
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-              & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
-  @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+              & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+  @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
   @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   \end{array}
@@ -644,22 +644,22 @@
   Note that this relation depends on the permutation @{text
   "p"}; $\alpha$-equivalence between two pairs is then the relation where we
   existentially quantify over this @{text "p"}. Also note that the relation is
-  dependent on a free-variable function @{text "fv"} and a relation @{text
+  dependent on a free-atom function @{text "fa"} 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, @{text R} will be replaced by equality @{text "="} and we
-  will prove that @{text "fv"} is equal to @{text "supp"}.
+  will prove that @{text "fa"} is equal to @{text "supp"}.
 
   The definition in \eqref{alphaset} does not make any distinction between the
-  order of abstracted variables. If we want this, then we can define $\alpha$-equivalence 
+  order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence 
   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 
   as follows
   %
   \begin{equation}\label{alphalist}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             & @{term "fv(x) - (set as) = fv(y) - (set bs)"} & \mbox{\it (i)}\\
-  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+             & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
+  \wedge     & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
   \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
   \wedge     & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
   \end{array}
@@ -676,21 +676,21 @@
   %
   \begin{equation}\label{alphares}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
-  \wedge     & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+             & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
+  \wedge     & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
   \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
   \end{array}
   \end{equation}
 
   It might be useful to consider first some examples about how these definitions
   of $\alpha$-equivalence pan out in practice.  For this consider the case of
-  abstracting a set of variables over types (as in type-schemes). We set
-  @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
+  abstracting a set of atoms over types (as in type-schemes). We set
+  @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
   define
 
   \begin{center}
-  @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
+  @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
   \end{center}
 
   \noindent
@@ -946,13 +946,14 @@
   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
   %show this later with an example.
   
-  There are also some restrictions we need to impose on binding clauses. The
+  There are also some restrictions we need to impose on our binding clauses in comparison to
+  the ones of Ott. The
   main idea behind these restrictions is that we obtain a sensible notion of
-  $\alpha$-equivalence where it is ensured that within a given scope a 
-  variable occurence cannot be both bound and free at the same time.  The first
+  $\alpha$-equivalence where it is ensured that within a given scope an 
+  atom occurence cannot be both bound and free at the same time.  The first
   restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor (this ensures that the bound
-  variables of a body cannot be free at the same time by specifying an
+  atoms of a body cannot be free at the same time by specifying an
   alternative binder for the same body). For binders we distinguish between
   \emph{shallow} and \emph{deep} binders.  Shallow binders are just
   labels. The restriction we need to impose on them is that in case of
@@ -1068,9 +1069,9 @@
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the associated
-  notions of free-variables and $\alpha$-equivalence.
+  notions of free-atoms and $\alpha$-equivalence.
   
-  To make sure that variables bound by deep binders cannot be free at the
+  To make sure that atoms bound by deep binders cannot be free at the
   same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
 
@@ -1086,7 +1087,9 @@
 
   \noindent
   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
-  out different atoms to become bound, respectively be free, in @{text "p"}.
+  out different atoms to become bound, respectively be free, in @{text "p"}
+  (since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit 
+  such specifications).
   
   We also need to restrict the form of the binding functions in order 
   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
@@ -1107,7 +1110,7 @@
   (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
   later on.
   
-  In order to simplify our definitions of free variables and $\alpha$-equivalence, 
+  In order to simplify our definitions of free atoms and $\alpha$-equivalence, 
   we shall assume specifications 
   of term-calculi are implicitly \emph{completed}. By this we mean that  
   for every argument of a term-constructor that is \emph{not} 
@@ -1132,7 +1135,7 @@
   clauses and be sure to have captured all arguments of a term constructor. 
 *}
 
-section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
+section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
 
 text {*
   Having dealt with all syntax matters, the problem now is how we can turn
@@ -1141,7 +1144,7 @@
   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
   re-arranging the arguments of
   term-constructors so that binders and their bodies are next to each other will 
-  result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\<dots>x\<^isub>n=t\<^isub>n in s"}. 
+  result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. 
   Therefore we will first
   extract ``raw'' datatype definitions from the specification and then define 
   explicitly an $\alpha$-equivalence relation over them. We subsequently
@@ -1168,8 +1171,8 @@
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   non-empty and the types in the constructors only occur in positive 
   position (see \cite{Berghofer99} for an indepth description of the datatype package
-  in Isabelle/HOL). We then define the user-specified binding 
-  functions @{term "bn"} by recursion over the corresponding 
+  in Isabelle/HOL). We then define each of the user-specified binding 
+  function @{term "bn\<^isub>i"} by recursion over the corresponding 
   raw datatype. We can also easily define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
   %
@@ -1178,21 +1181,21 @@
   \end{equation}
 
   The first non-trivial step we have to perform is the generation of
-  free-variable functions from the specifications. For the 
-  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions
+  free-atom functions from the specifications. For the 
+  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
   %
   \begin{equation}\label{fvars}
-  @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
+  @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
   \end{equation}
 
   \noindent
   by mutual recursion.
-  We define these functions together with auxiliary free-variable functions for
+  We define these functions together with auxiliary free-atom functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
   %
   \begin{center}
-  @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
+  @{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
   \end{center}
 
   \noindent
@@ -1200,14 +1203,14 @@
   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
   that calculates those unbound atoms in a deep binder.
 
-  While the idea behind these free-variable functions is clear (they just
+  While the idea behind these free-atom functions is clear (they just
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given
   a term-constructor @{text "C"} of type @{text ty} and some associated
   binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
-  "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
-  "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding
-  clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar). 
+  "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
+  "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we define below what @{text "fa"} for a binding
+  clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar). 
   Suppose the binding clause @{text bc\<^isub>i} is of the form 
   %
   \begin{equation}
@@ -1225,20 +1228,20 @@
   then the free atoms of the binding clause @{text bc\<^isub>i} are given by
   %
   \begin{center}
-  @{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
+  @{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
   \end{center}
 
   \noindent
-  The set @{text D} is formally defined as
+  whereby the set @{text D} is formally defined as
   %
   \begin{center}
-  @{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+  @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
   \end{center} 
 
   \noindent
-  whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion 
-  (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types 
-  @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion 
+  (see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types 
+  @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
   In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
   for atom types to which shallow binders have to refer
   %
@@ -1262,7 +1265,7 @@
 
   \noindent 
   The set @{text "B'"} collects all free atoms in non-recursive deep
-  binders. Lets assume these binders in @{text "bc\<^isub>i"} are
+  binders. Let us assume these binders in @{text "bc\<^isub>i"} are
   %
   \begin{center}
   @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
@@ -1273,71 +1276,71 @@
   "d"}$_{1..q}$. The set @{text "B'"} is defined as
   %
   \begin{center}
-  @{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
+  @{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
   \end{center} 
 
   \noindent
-  This completes the definition of the free-variable functions.
+  This completes the definition of the free-atom functions.
 
   Note that for non-recursive deep binders, we have to add all atoms that are left 
-  unbound by the binding function @{text "bn"}. This is the purpose of the functions 
-  @{text "fv_bn"}, also defined by recursion. Assume the user specified 
+  unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this 
+  the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified 
   a @{text bn}-clause of the form
   %
   \begin{center}
-  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
+  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
   \end{center}
 
   \noindent
-  where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
+  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
   the arguments we calculate the free atoms as follows:
   %
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} 
-  (nothing gets bound in @{text "z\<^isub>i"}),\\
-  $\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
+  $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"} 
+  (that means nothing is bound in @{text "z\<^isub>i"}),\\
+  $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
   with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
   $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-  but without a recursive call
+  but without a recursive call.
   \end{tabular}
   \end{center}
 
   \noindent
-  For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+  For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
  
   To see how these definitions work in practice, let us reconsider the term-constructors 
   @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"} 
   from the example shown in \eqref{letrecs}. 
-  For them we define three free-variable functions, namely
-  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"} as follows:
+  For them we define three free-atom functions, namely
+  @{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\
-  @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
+  @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
+  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
 
-  @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+  @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
 
-  @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
+  @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
+  @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
   \end{tabular}
   \end{center}
 
   \noindent
-  To see the ``pattern'', recall that @{text ANil} and @{text "ACons"} have no
-  binding clause in the specification. The corresponding free-variable
-  function @{text "fv\<^bsub>assn\<^esub>"} therefore returns all atoms
+  To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
+  binding clause in the specification. The corresponding free-atom
+  function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
   occurring in an assignment. The binding only takes place in @{text Let} and
   @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
   that all atoms given by @{text "set (bn as)"} have to be bound in @{text
   t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
-  "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
+  "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
   free in @{text "as"}.  In contrast, in @{text "Let_rec"} we have a recursive
   binder where we want to also bind all occurrences of the atoms in @{text
   "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
-  @{text "set (bn as)"} from the union @{text "fv\<^bsub>trm\<^esub> t"} and @{text "fv\<^bsub>assn\<^esub> as"}. 
+  @{text "set (bn as)"} from the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. 
   
   An interesting point in this
   example is that a ``naked'' assignment does not bind any
@@ -1349,14 +1352,14 @@
   $\alpha$-equivalence.
 
   Next we define $\alpha$-equivalence relations for the raw types @{text
-  "ty"}$_{1..n}$. We call them 
+  "ty"}$_{1..n}$. We write them 
   %
   \begin{center}
   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. 
   \end{center}
 
   \noindent
-  Like with the free-variable functions, we also need to
+  Like with the free-atom functions, we also need to
   define auxiliary $\alpha$-equivalence relations 
   %
   \begin{center}
@@ -1366,13 +1369,13 @@
   \noindent
   for the binding functions @{text "bn"}$_{1..m}$, 
   To simplify our definitions we will use the following abbreviations for
-  equivalence relations and free-variable functions acting on pairs
+  equivalence relations and free-atom functions acting on pairs
 
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
   @{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
-  @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
+  @{text "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
   \end{tabular}
   \end{center}
 
@@ -1394,15 +1397,15 @@
 (*<*)
 consts alpha_ty ::'a
 consts alpha_trm ::'a
-consts fv_trm :: 'a
+consts fa_trm :: 'a
 consts alpha_trm2 ::'a
-consts fv_trm2 :: 'a
+consts fa_trm2 :: 'a
 notation (latex output) 
   alpha_ty ("\<approx>ty") and
   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
-  fv_trm ("fv\<^bsub>trm\<^esub>") and
+  fa_trm ("fa\<^bsub>trm\<^esub>") and
   alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
-  fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>") 
+  fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>") 
 (*>*)
 text {*
   *TBD below *
@@ -1419,18 +1422,18 @@
   \multicolumn{2}{@ {}l}{Shallow binders of the form 
   \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
   $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
-  @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then
+  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
+  @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
   \begin{center}
-  @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+  @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
   \end{center}\\
   \multicolumn{2}{@ {}l}{Deep binders of the form 
   \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 
   $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
-  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
-  @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders
+  @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
+  @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
   \begin{center}
-  @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
+  @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
   \end{center}\\
   $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
   \end{tabular}}
@@ -1472,9 +1475,9 @@
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+  {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
   \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+  {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
   \end{tabular}
   \end{center}
 
@@ -1532,8 +1535,8 @@
   "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain 
   definitions for the term-constructors @{text
   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
-  "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
-  "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+  "C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
+  "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
   "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the 
   user, since they are given in terms of the isomorphisms we obtained by 
   creating new types in Isabelle/HOL (recall the picture shown in the 
@@ -1619,25 +1622,25 @@
 
   \noindent
   for our infrastructure. In a similar fashion we can lift the equations
-  characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 
+  characterising the free-atom functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fa_bn\<AL>\<^isub>k"}, and the 
   binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these
   lifting are the properties:
   %
   \begin{equation}\label{fnresp}
   \mbox{%
   \begin{tabular}{l}
-  @{text "x \<approx>ty\<^isub>j y"} implies @{text "fv_ty\<^isub>j x = fv_ty\<^isub>j y"}\\
-  @{text "x \<approx>ty\<^isub>k y"} implies @{text "fv_bn\<^isub>k x = fv_bn\<^isub>k y"}\\
+  @{text "x \<approx>ty\<^isub>j y"} implies @{text "fa_ty\<^isub>j x = fa_ty\<^isub>j y"}\\
+  @{text "x \<approx>ty\<^isub>k y"} implies @{text "fa_bn\<^isub>k x = fa_bn\<^isub>k y"}\\
   @{text "x \<approx>ty\<^isub>k 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"}. Whereas the first
-  property is always true by the way we defined the free-variable
+  property is always true by the way we defined the free-atom
   functions for types, the second and third do \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 third property is just not true. However, our 
+  atom. Then the third property is just not true. However, our 
   restrictions imposed on the binding functions
   exclude this possibility.
 
@@ -1662,13 +1665,13 @@
   the lifting part of establishing the reasoning infrastructure. 
 
   By working now completely on the $\alpha$-equated level, we can first show that 
-  the free-variable functions and binding functions
+  the free-atom functions and binding functions
   are equivariant, namely
 
   \begin{center}
   \begin{tabular}{rcl}
-  @{text "p \<bullet> (fv_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fv_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
-  @{text "p \<bullet> (fv_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fv_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
+  @{text "p \<bullet> (fa_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fa_ty\<^sup>\<alpha> (p \<bullet> x)"}\\
+  @{text "p \<bullet> (fa_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fa_bn\<^sup>\<alpha> (p \<bullet> x)"}\\
   @{text "p \<bullet> (bn\<^sup>\<alpha> x)"}    & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}
   \end{tabular}
   \end{center}
@@ -1697,11 +1700,11 @@
   \noindent
   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>"}.
+  @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fa_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 
-  @{text "supp x\<^isub>i = fv_ty\<AL>\<^isub>i x\<^isub>i"} holds.
+  @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"} holds.
   \end{lemma}
 
   \begin{proof}
@@ -1846,7 +1849,7 @@
   \begin{lemma}\label{permutebn} 
   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
   {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}
-    @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+    @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
   \end{lemma}
 
   \begin{proof} 
@@ -1857,8 +1860,8 @@
   \noindent
   The first property states that a permutation applied to a binding function is
   equivalent to first permuting the binders and then calculating the bound
-  variables. The second amounts to the fact that permuting the binders has no 
-  effect on the free-variable function. The main point of this permutation
+  atoms. The second amounts to the fact that permuting the binders has no 
+  effect on the free-atom function. The main point of this permutation
   function, however, is that if we have a permutation that is fresh 
   for the support of an object @{text x}, then we can use this permutation 
   to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
@@ -2103,7 +2106,7 @@
 We can also see that
   %
   \begin{equation}\label{bnprop}
-  @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
+  @{text "fa_ty x  =  bn x \<union> fa_bn x"}.
   \end{equation}
 
   \noindent