
diff -r 9d8ebeded16f -r 9832641ed955 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jul 16 03:22:24 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 16 04:58:46 2010 +0100
@@ -1689,7 +1689,7 @@
   any bound atoms. In Ott, in contrast, the user may 
   define @{text "bn"}$_{1..m}$ so that they return bound
   atoms and in this case the third implication is \emph{not} true. A 
-  result is that the lifing of the corresponding binding functions to $\alpha$-equated
+  result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
   terms is impossible.
 
   Having established respectfulness for the raw term-constructors, the 
@@ -1728,7 +1728,7 @@
   to our infrastructure. In a similar fashion we can lift the defining equations
   of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
   @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-  "bn\<AL>"}$_{1..m}$ and of the size functions @{text "size_ty\<AL>"}$_{1..n}$.
+  "bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
   The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
   by the datatype package of Isabelle/HOL.
 
@@ -1772,17 +1772,17 @@
   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
 
   \begin{center}
-  @{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
+  @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
   \end{center}
  
   \noindent
-  holds. This together with Property~\ref{supportsprop} allows us to show
-  for every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, 
+  holds. This together with Property~\ref{supportsprop} allows us to prove
+  that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, 
   namely @{text "finite (supp x)"}. This can be again shown by induction 
   over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of 
   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
-  This important fact provides evidence that our notions of free-atoms and 
-  $\alpha$-equivalence are correct.
+  This fact is important in a nominal setting, but also provides evidence 
+  that our notions of free-atoms and $\alpha$-equivalence are correct.
 
   \begin{lemma} 
   For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -1797,12 +1797,12 @@
   \end{proof}
 
   \noindent
-  To sum up, we can established automatically a reasoning infrastructure
+  To sum up this section, we can established automatically a reasoning infrastructure
   for the types @{text "ty\<AL>"}$_{1..n}$ 
   by first lifting definitions from the raw level to the quotient level and
   then by establishing facts about these lifted definitions. All necessary proofs
   are generated automatically by custom ML-code. This code can deal with 
-  specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
+  specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
 
   \begin{figure}[t!]
   \begin{boxedminipage}{\linewidth}
@@ -1880,9 +1880,10 @@
 text {*
   In the previous section we were able to provide induction principles that 
   allow us to perform structural inductions over $\alpha$-equated terms. 
-  We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+  We call such induction principles \emph{weak}, because in case of the 
+  term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
   the induction hypothesis requires us to establish the implications \eqref{weakprem}.
-  The problem with these implications is that in general they are not easy to establish.
+  The problem with these implications is that in general they are difficult to establish.
   The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} 
   (for example we cannot assume the variable convention for them).
 
@@ -1898,8 +1899,21 @@
 
   Given a binding function @{text "bn"} we define an auxiliary permutation 
   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
-  Assuming a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
-  we define @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"} with @{text "y\<^isub>i"} determined as follows:
+  Assuming a clause of @{text bn} is given as 
+  %
+  \begin{center}
+  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
+  \end{center}
+
+  \noindent 
+  then we define 
+  %
+  \begin{center}
+  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
+  \end{center}
+  
+  \noindent
+  with @{text "y\<^isub>i"} determined as follows:
   %
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1915,8 +1929,8 @@
 
   \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 "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.
+  {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
+    @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
   \end{lemma}
 
   \begin{proof} 
@@ -1933,18 +1947,21 @@
   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 
   @{text "Let"} term-constructor from the example shown 
-  \eqref{letpat} this means for a permutation @{text "r"}:
+  in \eqref{letpat} this means for a permutation @{text "r"}
   %
   \begin{equation}\label{renaming}
   \begin{array}{l}
   \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
-  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bnpat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
   \end{array}
   \end{equation}
 
   \noindent
-  This fact will be crucial when establishing the strong induction principles. 
-  In our running example about @{text "Let"}, they state that instead 
+  This fact will be crucial when establishing the strong induction principles below.
+
+ 
+  In our running example about @{text "Let"}, the strong induction
+  principle means that instead 
   of establishing the implication 
   %
   \begin{center}
@@ -1966,7 +1983,7 @@
   \noindent 
   While this implication contains an additional argument, namely @{text c}, and 
   also additional universal quantifications, it is usually easier to establish.
-  The reason is that we can make the freshness 
+  The reason is that we have the freshness 
   assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
   chosen by the user as long as it has finite support.
 
@@ -1976,7 +1993,7 @@
   %
   \begin{equation}\label{hyps}
   @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
-  @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+  @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
   \end{equation} 
 
   \noindent
@@ -1996,38 +2013,35 @@
   \begin{center}
   \begin{tabular}{l}
   @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-  \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+  \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
   \end{tabular}
   \end{center}
 
   \noindent
   So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-  establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
+  establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
   To do so, we will use the implication \eqref{strong} of the strong induction
   principle, which requires us to discharge
   the following four proof obligations:
   %
   \begin{center}
   \begin{tabular}{rl}
-  {\it i)} &   @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-  {\it ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-  {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-  {\it iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
+  {\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+  {\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+  {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+  {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it i)}; the 
+  The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
   others from the induction hypotheses in \eqref{hyps} (in the fourth case
   we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
 
   Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
-  This completes the proof showing that the strong induction principle derives from
-  the weak induction principle. For the moment we can derive the difficult cases of 
-  the strong induction principles only by hand, but they are very schematic 
-  so that with little effort we can even derive them for 
-  Core-Haskell given in Figure~\ref{nominalcorehas}. 
+  This completes the proof showing that the weak induction principles imply 
+  the strong induction principles. 
 *}
 
 
@@ -2073,7 +2087,7 @@
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose from
   the need to ``unbind'' variables. This can be done in one step with our
-  general binders, but needs a cumbersome
+  general binders described in this paper, but needs a cumbersome
   iteration with single binders. The resulting formal reasoning turned out to
   be rather unpleasant. The hope is that the extension presented in this paper
   is a substantial improvement.
@@ -2097,11 +2111,11 @@
   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
   covers cases of binders depending on other binders, which just do not make
   sense for our $\alpha$-equated terms. Third, it allows empty types that have no
-  meaning in a HOL-based theorem prover. We also had to generalise slightly their 
+  meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 
   binding clauses. In Ott you specify binding clauses with a single body; we 
   allow more than one. We have to do this, because this makes a difference 
   for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and 
-  \isacommand{bind\_res}. For example
+  \isacommand{bind\_res}. Consider the examples
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@@ -2114,7 +2128,7 @@
   \end{center}
 
   \noindent
-  in the first term-constructor we have a single
+  In the first term-constructor we have a single
   body that happens to be ``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
@@ -2153,11 +2167,11 @@
   In a slightly different domain (programming with dependent types), the 
   paper \cite{Altenkirch10} presents a calculus with a notion of 
   $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
-  The corresponding definition is similar to the one by Pottier, except that it
+  The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
   has a more operational flavour and calculates a partial (renaming) map. 
-  In this way Altenkirch et al can deal with vacuous binders. However, to our
-  best knowledge, no concrete mathematical result concerning their notion
-  of equality has been proved.    
+  In this way, the definition can deal with vacuous binders. However, to our
+  best knowledge, no concrete mathematical result concerning this
+  definition of $\alpha$-equivalence has been proved.    
 *}
 
 section {* Conclusion *}
@@ -2167,8 +2181,11 @@
   general binders, that is term-constructors having multiple bound 
   variables. For this extension we introduced novel definitions of 
   $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
-  We have tried out the extension with terms from Core-Haskell and our code
-  will become part of the Isabelle distribution.\footnote{For the moment
+  To specify general binders we used the syntax from Ott, but modified 
+  it so that it makes sense in our context of $\alpha$-equated terms.
+  We have tried out the extension with terms from Core-Haskell, type-schemes 
+  and the lambda-calculus, and our code
+  will eventually become part of the next Isabelle distribution.\footnote{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}.}
@@ -2181,7 +2198,7 @@
   definitions to equivariant functions (for such functions it is possible to
   provide more automation).
 
-  There are some restrictions we imposed in this paper, that we would like to lift in
+  There are some restrictions we imposed in this paper that we would like to lift in
   future work. One is the exclusion of nested datatype definitions. Nested
   datatype definitions allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
@@ -2189,7 +2206,7 @@
   achieve this, we need a slightly more clever implementation than we have at the moment. 
 
   A more interesting line of investigation is whether we can go beyond the 
-  simple-minded form for binding functions that we adopted from Ott. At the moment, binding
+  simple-minded form of binding functions that we adopted from Ott. At the moment, binding
   functions can only return the empty set, a singleton atom set or unions
   of atom sets (similarly for lists). It remains to be seen whether 
   properties like




