
diff -r e842807d8268 -r a33e96e62a2b LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Mon Sep 12 21:48:26 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Tue Sep 13 09:30:34 2011 +0200
@@ -463,17 +463,19 @@
   the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}, 
   and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
   operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
-  for example permutations acting on products, lists, sets, functions and booleans are
-  given by:
+  for example permutations acting on atoms, products, lists, permutations, sets, 
+  functions and booleans are given by:
   
   \begin{equation}\label{permute}
   \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
   \begin{tabular}{@ {}l@ {}}
+  @{text "\<pi> \<bullet> a \<equiv> \<pi> a"}\\
   @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
   @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
+  @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
   @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
   @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
@@ -623,11 +625,13 @@
   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 "\<pi> \<bullet> x = x"}. Note that @{term "supp x \<sharp>* \<pi>"}
+  @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. 
+
+  Note that @{term "supp x \<sharp>* \<pi>"}
   is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate 
   Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the 
   reasoning infrastructure of Nominal Isabelle is set up so that it provides more
-  automation for the original formulation.
+  automation for the formulation given above.
 
   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 
@@ -707,7 +711,8 @@
   and @{text bs} are lists of atoms).
 
   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 
+  also allow vacuous binders, that means according to Pitts \emph{restrict} names
+  \cite{Pitts04}, then we keep sets of binders, but drop 
   condition {\it (iv)} in Definition~\ref{alphaset}:
 
   \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
@@ -756,9 +761,9 @@
 
   \begin{equation}
   \begin{array}{r}
-  @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
-  @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\
-  @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
+  @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\
+  @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\
+  @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
   \end{array}
   \end{equation}\smallskip
   
@@ -768,20 +773,24 @@
   the following properties:
 
   \begin{lem}\label{alphaeq} 
-  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
-  and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant. 
+  The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, 
+  $\approx_{\,\textit{set+}}^{=, \textit{supp}}$
+  and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are 
+  equivalence relations and equivariant. 
   \end{lem}
 
   \begin{proof}
   Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
-  a permutation @{text "\<pi>"} 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"}. Equivariance means
-  @{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided 
-  \mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the
-  definitions and `pull out' the permutations, which is possible since all
-  operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
-  (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
+  a permutation @{text "\<pi>"} 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"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
+  \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
+  "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. To show this, we need to
+  unfold the definitions and `pull out' the permutations, which is possible
+  since all operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"},
+  are equivariant (see \cite{HuffmanUrban10}). Finally we apply the
+  permutation operation on booleans.
   \end{proof}
 
   \noindent
@@ -1080,7 +1089,7 @@
   to be defined by recursion over the corresponding type; the equations
   must be given in the binding function part of the scheme shown in
   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
-  tuple patterns might be specified as:
+  tuple patterns may be specified as:
 
   \begin{equation}\label{letpat}
   \mbox{%
@@ -1105,7 +1114,7 @@
 
   \noindent
   In this specification the function @{text "bn"} determines which atoms of
-  the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
+  the pattern @{text p} (fifth line) are bound in the argument @{text "t"}. Note that in the
   second-last @{text bn}-clause the function @{text "atom"} coerces a name
   into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
   allows us to treat binders of different atom type uniformly.
@@ -1191,8 +1200,8 @@
   \end{equation}\smallskip
 
   \noindent
-  In this example the term constructor @{text "ACons'"} has four arguments and
-  contains a binding clause. This constructor is also used in the definition
+  In this example the term constructor @{text "ACons'"} has four arguments with
+  a binding clause for two of them. This constructor is also used in the definition
   of the binding function. The restriction we have to impose is that the
   binding function can only return free atoms, that is the ones that are not
   mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the
@@ -1274,10 +1283,10 @@
   \end{equation}\smallskip
 
   The first non-trivial step we have to perform is the generation of
-  \emph{free-atom functions} from the specification.\footnote{Admittedly, the
+  \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
   details of our definitions will be somewhat involved. However they are still
   conceptually simple in comparison with the ``positional'' approach taken in
-  Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and
+  Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and
   \emph{partial equivalence relations} over sets of occurences.} For the
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 
@@ -1562,13 +1571,14 @@
 
   \noindent
   In this case we define a premise @{text P} using the relation
-  $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
-  $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other
+  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly
+  $\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and 
+  $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other
   binding modes). This premise defines alpha-equivalence of two abstractions
   involving multiple binders. As above, we first build the tuples @{text "D"} and
   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
   compound alpha-relation @{text "R"} (shown in \eqref{rempty}). 
-  For $\approx_{\,\textit{set}}$  we also need
+  For $\approx_{\,\textit{set}}^{R, fa}$  we also need
   a compound free-atom function for the bodies defined as
   
   \[
@@ -1651,10 +1661,12 @@
   \noindent
   This completes the definition of alpha-equivalence. As a sanity check, we can show
   that the premises of empty binding clauses are a special case of the clauses for 
-  non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
+  non-empty ones (we just have to unfold the definition of 
+  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ and take @{text "0"}
   for the existentially quantified permutation).
 
-  Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
+  Again let us take a look at a concrete example for these definitions. For 
+  teh specification given in \eqref{letrecs}
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$ with the following clauses:
 
@@ -1684,7 +1696,7 @@
   \]\smallskip
 
   \noindent
-  Note the difference between  $\approx_{\textit{assn}}$ and
+  Notice the difference between  $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of 
   the components in an assignment that are \emph{not} bound. This is needed in the 
   clause for @{text "Let"} (which has
@@ -1692,6 +1704,9 @@
   The underlying reason is that the terms inside an assignment are not meant 
   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
   because there all components of an assignment are ``under'' the binder. 
+  Note also that in case of more than one body (e.g.~@{text "Let_rec"}-case)
+  we need to parametrise the relation $\approx_{\textit{list}}$ with compound
+  equivalence relations and compund free-atom functions.
 *}
 
 section {* Establishing the Reasoning Infrastructure *}
@@ -2371,7 +2386,7 @@
   have proved that our definitions lead to alpha-equated terms, whose support
   is as expected (that means bound names are removed from the support). We
   also showed that our specifications lift from a raw type to a type of
-  alpha-equivalence classes. For this we were able to establish then every
+  alpha-equivalence classes. For this we had to establish (automatically) that every
   term-constructor and function is repectful w.r.t.~alpha-equivalence.
 
   Although we were heavily inspired by the syntax of Ott, its definition of
@@ -2401,7 +2416,7 @@
   ``spread'' over two arguments; in the second term-constructor we have two
   independent bodies in which the same variables are bound. As a result we
   have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
-  make @{text "(a, b)"} equal with @{text "(a, b)"} and @{text "(b, a)"}, but
+  make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but
   there are two permutations so that we can make @{text "(a, b)"} and @{text
   "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
   a)"} with the other.}
@@ -2445,11 +2460,11 @@
   it defines an equivalence relation. A complete reasoning infrastructure is
   well beyond the purposes of his language. Similar work for Haskell with
   similar results was reported by Cheney \cite{Cheney05a} and more recently 
-  by ???
+  by Weirich et al \cite{WeirichYorgeySheard11}.
 
   In a slightly different domain (programming with dependent types),
-  Altenkirch et al present a calculus with a notion of alpha-equivalence
-  related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}.
+  Altenkirch et al \cite{Altenkirch10} present a calculus with a notion of
+  alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
   Their definition is similar to the one by Pottier, except that it has a more
   operational flavour and calculates a partial (renaming) map. In this way,
   the definition can deal with vacuous binders. However, to our best
@@ -2474,8 +2489,7 @@
   type-schemes and approximately a dozen of other typical examples from
   programming language research~\cite{SewellBestiary}. The code will
   eventually become part of the next Isabelle distribution.\footnote{It 
-  can be downloaded already from the Mercurial repository linked at
-  \href{http://isabelle.in.tum.de/nominal/download}
+  can be downloaded from \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.}
 
   We have left out a discussion about how functions can be defined over




