
diff -r 3c8d3aaf292c -r 8d7d85e915b5 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Sep 06 12:18:02 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Wed Sep 07 12:38:32 2011 +0100
@@ -101,7 +101,7 @@
   Binding multiple variables has interesting properties that cannot be captured
   easily by iterating single binders. For example in the case of type-schemes we do not
   want to make a distinction about the order of the bound variables. Therefore
-  we would like to regard below the first pair of type-schemes as alpha-equivalent,
+  we would like to regard in \eqref{ex1} below  the first pair of type-schemes as alpha-equivalent,
   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
   the second pair should \emph{not} be alpha-equivalent:
 
@@ -378,7 +378,7 @@
   The main improvement over Ott is that we introduce three binding modes
   (only one is present in Ott), provide formalised definitions for alpha-equivalence and 
   for free variables of our terms, and also derive a reasoning infrastructure
-  for our specifications from ``first principles''.
+  for our specifications from ``first principles'' inside a theorem prover.
 
 
   \begin{figure}
@@ -431,14 +431,14 @@
   to aid the description of what follows. 
 
   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. 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. In the interest of brevity, we shall restrict ourselves 
-  in what follows to only one sort of atoms.
+  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,
+  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
+  type-variables in Core-Haskell.  It is assumed that there is an infinite
+  supply of atoms for each sort. In the interest of brevity, we shall restrict
+  ourselves in what follows to only one sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 
@@ -487,7 +487,7 @@
   
   \begin{equation}\label{suppdef}
   @{thm supp_def[no_vars, THEN eq_reflection]}
-  \end{equation}
+  \end{equation}\smallskip
 
   \noindent
   There is also the derived notion for when an atom @{text a} is \emph{fresh}
@@ -508,7 +508,7 @@
   
   \begin{prop}\label{swapfreshfresh}
   If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
-  then @{thm (concl) swap_fresh_fresh[no_vars]}
+  then @{thm (concl) swap_fresh_fresh[no_vars]}.
   \end{prop}
   
   While often the support of an object can be relatively easily 
@@ -539,7 +539,7 @@
   notion \emph{supports}, defined as follows:
   
   \begin{defi}
-  A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+  A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b}
   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
   \end{defi}
   
@@ -548,8 +548,10 @@
   two properties.
   
   \begin{prop}\label{supportsprop}
-  Given a set @{text "as"} of atoms.
-  {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+  Given a set @{text "as"} of atoms.\\
+  {\it (i)} If @{thm (prem 1) supp_is_subset[where S="as", no_vars]}
+  and @{thm (prem 2) supp_is_subset[where S="as", no_vars]} then 
+  @{thm (concl) supp_is_subset[where S="as", no_vars]}.\\
   {\it (ii)} @{thm supp_supports[no_vars]}.
   \end{prop}
   
@@ -558,17 +560,17 @@
   it is required that every permutation leaves @{text f} unchanged, that is
   
   \begin{equation}\label{equivariancedef}
-  @{term "\<forall>p. p \<bullet> f = f"}
-  \end{equation}
+  @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}
+  \end{equation}\smallskip
   
   \noindent or equivalently that a permutation applied to the application
   @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-  functions @{text f}, we have for all permutations @{text p}:
+  functions @{text f}, we have for all permutations @{text "\<pi>"}:
   
   \begin{equation}\label{equivariance}
-  @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
-  @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
-  \end{equation}
+  @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
+  @{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+  \end{equation}\smallskip
    
   \noindent
   From property \eqref{equivariancedef} and the definition of @{text supp}, we 
@@ -577,7 +579,7 @@
   that
   
   \begin{center}
-  @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+  @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
   \end{center}
   
   Using freshness, the nominal logic work provides us with general means for renaming 
@@ -585,35 +587,34 @@
   
   \noindent
   While in the older version of Nominal Isabelle, we used extensively 
-  Property~\ref{swapfreshfresh}
-  this property to rename single binders, it this property 
+  Property~\ref{swapfreshfresh} to rename single binders, this property 
   proved too unwieldy for dealing with multiple binders. For such binders the 
   following generalisations turned out to be easier to use.
 
   \begin{prop}\label{supppermeq}
-  @{thm[mode=IfThen] supp_perm_eq[no_vars]}
+  @{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}
   \end{prop}
 
   \begin{prop}\label{avoiding}
   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"}.
+  exists a permutation @{text "\<pi>"} such that @{term "(\<pi> \<bullet> as) \<sharp>* c"} and
+  @{term "supp x \<sharp>* \<pi>"}.
   \end{prop}
 
   \noindent
   The idea behind the second property is that given a finite set @{text as}
   of binders (being bound, or fresh, in @{text x} is ensured by the
-  assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
-  the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-  as long as it is finitely supported) and also @{text "p"} does not affect anything
-  in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
+  assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
+  the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
+  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 "p \<bullet> x = x"}.
+  @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
 
   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 
-  extensive use of these properties in order to define alpha-equivalence in 
+  use of these properties in order to define alpha-equivalence in 
   the presence of multiple binders.
 *}
 
@@ -628,7 +629,7 @@
 
   In order to keep our work with deriving the reasoning infrastructure
   manageable, we will wherever possible state definitions and perform proofs
-  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code.  that
+  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
   generates them anew for each specification. 
   To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
@@ -641,48 +642,48 @@
   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
   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
-  atoms; 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
+  atoms; moreover there must be a permutation @{text \<pi>} such that {\it
+  (ii)} @{text \<pi>} 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
+  @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
-  %
-  \begin{equation}\label{alphaset}
-  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-       \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
-       \mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
-       \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} & 
-       \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\ 
-  \end{array}
-  \end{equation}
-  %
+
+  \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
+  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
+  @{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"} 
+       & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
+       & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
+       & \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\
+       & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"} \\ 
+  \end{tabular}
+  \end{defi}
+ 
   \noindent
   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
+  "\<pi>"}; alpha-equivalence between two pairs is then the relation where we
+  existentially quantify over this @{text "\<pi>"}. Also note that the relation is
   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 "fa"} is equal to @{text "supp"}.
 
-  The definition in \eqref{alphaset} does not make any distinction between the
+  Definition \ref{alphaset} does not make any distinction between the
   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}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-         \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & 
-         \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-         \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
-         \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
-  \end{array}
-  \end{equation}
-  %
+  
+  \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
+  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
+  @{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+         & \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ 
+         & \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
+         & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
+         & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"}\\
+  \end{tabular}
+  \end{defi}
+  
   \noindent
   where @{term set} is the function that coerces a list of atoms into a set of atoms.
   Now the last clause ensures that the order of the binders matters (since @{text as}
@@ -690,38 +691,39 @@
 
   If we do not want to make any difference between the order of binders \emph{and}
   also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop 
-  condition {\it (iv)} in \eqref{alphaset}:
-  %
-  \begin{equation}\label{alphares}
-  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} & 
-             \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-             \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
-  \end{array}
-  \end{equation}
+  condition {\it (iv)} in Definition~\ref{alphaset}:
+
+  \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
+  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
+  @{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+             & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
+             & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
+             & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
+  \end{tabular}
+  \end{defi}
+
 
   It might be useful to consider first some examples how these definitions
   of alpha-equivalence pan out in practice.  For this consider the case of
   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 "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}
+  \]\smallskip
 
   \noindent
   Now recall the examples shown in \eqref{ex1} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
   @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
-  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to
+  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
   since there is no permutation that makes the lists @{text "[x, y]"} and
   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
   unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$
-  @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+  @{text "({x, y}, x)"} which holds by taking @{text "\<pi>"} to be the identity
   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
@@ -731,15 +733,18 @@
 
   In the rest of this section we are going to introduce three abstraction 
   types. For this we define 
-  %
+
   \begin{equation}
-  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
+  \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)"}\\
+  \end{array}
   \end{equation}
   
   \noindent
-  (similarly for $\approx_{\,\textit{abs\_set+}}$ 
-  and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
-  relations. %% and equivariant.
+  We can show that these relations are equivalence 
+  relations and equivariant.
 
   \begin{lem}\label{alphaeq} 
   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
@@ -749,10 +754,10 @@
   \end{lem}
 
   \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 conditions are then by simple
+  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 
+  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. 
   \end{proof}
 




