
diff -r 6c131c089ce2 -r 6b3e8602edcf Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Nov 21 02:17:19 2010 +0000
+++ b/Paper/Paper.thy	Wed Nov 24 01:08:48 2010 +0000
@@ -274,7 +274,7 @@
 
   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   terms is nearly always taken for granted, establishing it automatically in
-  the Isabelle/HOL is a rather non-trivial task. For every
+  Isabelle/HOL is a rather non-trivial task. For every
   specification we will need to construct type(s) containing as elements the
   $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
   a new type by identifying a non-empty subset of an existing type.  The
@@ -441,10 +441,9 @@
   b, c, \<dots>"} to stand for atoms and @{text "p, q, \<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.
+  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 
+  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 
@@ -457,7 +456,7 @@
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   operation is defined over the type-hierarchy \cite{HuffmanUrban10};
-  for example permutations acting on products, lists, sets, functions and booleans is
+  for example permutations acting on products, lists, sets, functions and booleans are
   given by:
   %
   %\begin{equation}\label{permute}
@@ -1429,7 +1428,7 @@
   %\noindent
   for the binding functions @{text "bn"}$_{1..m}$, 
   To simplify our definitions we will use the following abbreviations for
-  \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
+  \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples.
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1619,7 +1618,7 @@
   Note 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 
-  in the clause for @{text "Let"} (which is has
+  clause for @{text "Let"} (which has
   a non-recursive binder). 
   %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"}, 
@@ -1834,7 +1833,7 @@
   \end{proof}
 
   \noindent
-  To sum up this section, we can established automatically a reasoning infrastructure
+  To sum up this section, we can establish 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
@@ -1949,7 +1948,7 @@
   In \cite{UrbanTasson05} we showed how the weaker induction principles imply
   the stronger ones. This was done by some quite complicated, nevertheless automated,
   induction proofs. In this paper we simplify this work by leveraging the automated proof
-  methods from the function package of Isabelle/HOL generates. 
+  methods from the function package of Isabelle/HOL. 
   The reasoning principle these methods employ is well-founded induction. 
   To use them in our setting, we have to discharge
   two proof obligations: one is that we have
@@ -2032,8 +2031,8 @@
   \noindent
   Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
   @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
-  is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. T
-  hese facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+  is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. 
+  These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
   completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
   principle.
   
@@ -2203,7 +2202,7 @@
   de-Bruijn representation), but to different bound variables. A similar idea
   has been recently explored for general binders in the locally nameless
   approach to binding \cite{chargueraud09}.  There, de-Bruijn indices consist
-  of two numbers, one referring to the place where a variable is bound and the
+  of two numbers, one referring to the place where a variable is bound, and the
   other to which variable is bound. The reasoning infrastructure for both
   representations of bindings comes for free in theorem provers like Isabelle/HOL or
   Coq, since the corresponding term-calculi can be implemented as ``normal''
@@ -2250,8 +2249,9 @@
   $\alpha$-equivalence of terms that can be specified in Ott.  This definition is
   rather different from ours, not using any nominal techniques.  To our
   knowledge there is also no concrete mathematical result concerning this
-  notion of $\alpha$-equivalence.  A definition for the notion of free variables
-  is in Ott work in progress.
+  notion of $\alpha$-equivalence.  Also the definition for the 
+  notion of free variables
+  is work in progress.
 
   Although we were heavily inspired by the syntax of Ott,
   its definition of $\alpha$-equivalence is unsuitable for our extension of




