
diff -r 10e476d6f4b8 -r 204a488c71c6 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Sep 20 14:44:50 2011 +0900
+++ b/LMCS-Paper/Paper.thy	Tue Sep 20 09:17:29 2011 +0200
@@ -235,7 +235,7 @@
   assn} as follows
 
   \[
-  @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{10mm} 
+  @{text "bn(\<ANIL>) ="}~@{term "{}"} \hspace{10mm} 
   @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 
   \]\smallskip
 
@@ -261,7 +261,7 @@
   \cite{Berghofer99}.  Another reason is that we establish the reasoning
   infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a
   reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or
-  `raw', terms. While our alpha-equated terms and the raw terms produced by
+  `raw', terms. While our alpha-equated terms and the `raw' terms produced by
   Ott use names for bound variables, there is a key difference: working with
   alpha-equated terms means, for example, that the two type-schemes
 
@@ -279,7 +279,7 @@
   Our insistence on reasoning with alpha-equated terms comes from the
   wealth of experience we gained with the older version of Nominal Isabelle:
   for non-trivial properties, reasoning with alpha-equated terms is much
-  easier than reasoning with raw terms. The fundamental reason for this is
+  easier than reasoning with `raw' terms. The fundamental reason for this is
   that the HOL-logic underlying Nominal Isabelle allows us to replace
   `equals-by-equals'. In contrast, replacing
   `alpha-equals-by-alpha-equals' in a representation based on `raw' terms
@@ -394,7 +394,7 @@
   including properties about support, freshness and equality conditions for
   alpha-equated terms. We are also able to automatically derive strong
   induction principles that have the variable convention already built in.
-  For this we simplify the earlier automated proofs by using the proof tools
+  For this we simplify the earlier automated proofs by using the proving tools
   from the function package~\cite{Krauss09} of Isabelle/HOL.  The method
   behind our specification of general binders is taken from the Ott-tool, but
   we introduce crucial restrictions, and also extensions, so that our
@@ -604,9 +604,9 @@
   also a similar notion for equivariant relations, say @{text R}, namely the property
   that
   
-  \begin{center}
+  \[
   @{text "x R y"} \;\;\textit{implies}\;\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}
-  \end{center}
+  \]\smallskip
   
   Using freshness, the nominal logic work provides us with general means for renaming 
   binders. 
@@ -696,7 +696,7 @@
   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}}^{\textit{R}, \textit{fa}}$ for both `raw' terms and 
+  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ 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"}.
@@ -767,7 +767,7 @@
   abstract a single atom.
 
   In the rest of this section we are going to show that the alpha-equivalences
-  really lead to abstractions where some atoms are bound (more precisely
+  really lead to abstractions where some atoms are bound (or more precisely
   removed from the support).  For this we will consider three abstraction
   types that are quotients of the relations
 
@@ -843,7 +843,7 @@
 
   \noindent
   In effect, this theorem states that the atoms @{text "as"} are bound in the
-  abstraction. As stated earlier, this can be seen as litmus test that our
+  abstraction. As stated earlier, this can be seen as a litmus test that our
   Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
   idea of alpha-equivalence relations. Below we will give the proof for the
   first equation of Theorem \ref{suppabs}. The others follow by similar
@@ -875,11 +875,12 @@
   \end{lem}
   
   \begin{proof}
-  If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
+  If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b)"} is then
+  the identity permutation.
   Also in the other case the lemma is straightforward using \eqref{abseqiff}
   and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
-  (supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"}. as
-  the permutation fpr the proof obligation.
+  (supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"} as
+  the permutation for the proof obligation.
   \end{proof}
   
   \noindent
@@ -922,10 +923,10 @@
   This is because for every finite sets of atoms, say @{text "bs"}, we have 
   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
-  the first equation of Theorem~\ref{suppabs}. 
+  the first equation of Theorem~\ref{suppabs}. The others are similar.
 
   Recall the definition of support given in \eqref{suppdef}, and note the difference between 
-  the support of a `raw' pair and an abstraction
+  the support of a raw pair and an abstraction
 
   \[
   @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
@@ -1278,15 +1279,15 @@
 
 
   The `raw' datatype definition can be obtained by stripping off the 
-  binding clauses and the labels from the types. We also have to invent
-  new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-  given by the user. In our implementation we just use the affix `@{text "_raw"}'.
+  binding clauses and the labels from the types given by the user. We also have to invent
+  new names for the  types @{text "ty\<^sup>\<alpha>"} and the term-constructors @{text "C\<^sup>\<alpha>"}. 
+  In our implementation we just use the affix ``@{text "_raw"}''.
   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is given for alpha-equivalence classes and leave it out 
-  for the corresponding notion given on the `raw' level. So for example 
+  for the corresponding notion given on the raw level. So for example 
   we have @{text "ty\<^sup>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"}
   where @{term ty} is the type used in the quotient construction for 
-  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the `raw' type @{text "ty"},
+  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the raw type @{text "ty"},
   respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. 
 
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
@@ -1295,7 +1296,7 @@
   in Isabelle/HOL). 
   We subsequently define each of the user-specified binding 
   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
-  `raw' datatype. We also define permutation operations by 
+  raw datatype. We also define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
   
   \begin{equation}\label{ceqvt}
@@ -1335,7 +1336,7 @@
   While the idea behind these free-atom functions is simple (they just
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given
-  a `raw' term-constructor @{text "C"} of type @{text ty} and some associated
+  a raw 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
   "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 will define below what @{text "fa"} for a binding
@@ -1759,7 +1760,7 @@
   The function package of Isabelle/HOL allows us to prove the first part by
   mutual induction over the definitions of the functions.\footnote{We have
   that the free-atom functions are terminating. From this the function
-  package derives an induction principle \cite{Krauss09}.} The second is by a
+  package derives an induction principle~\cite{Krauss09}.} The second is by a
   straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and
   @{text "\<approx>bn"}$_{1..m}$ using the first part.
   \end{proof}
@@ -1785,7 +1786,7 @@
   We can feed the last lemma into our quotient package and obtain new types
   @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
   @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
-  @{text "C"}$^\alpha_{1..k}$ from the `raw' term-constructors @{text
+  @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
   binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
@@ -1811,9 +1812,9 @@
   \end{equation}\smallskip
 
   \noindent
-  holds for the corresponding `raw' term-constructors.
+  holds for the corresponding raw term-constructors.
   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
-  package needs to know that the `raw' term-constructors @{text "C"} and @{text "D"} 
+  package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 
   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
   Given, for example, @{text "C"} is of type @{text "ty"} with argument types
   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
@@ -1849,7 +1850,7 @@
   "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
   implication is \emph{not} true. A result is that in general the lifting of the
   corresponding binding functions in Ott to alpha-equated terms is impossible.
-  Having established respectfulness for the `raw' term-constructors, the 
+  Having established respectfulness for the raw term-constructors, the 
   quotient package is able to automatically deduce \eqref{distinctalpha} from 
   \eqref{distinctraw}.
 
@@ -1869,10 +1870,10 @@
   of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
   @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
   "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
-  The latter are defined automatically for the `raw' types @{text "ty"}$_{1..n}$
+  The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
   by the datatype package of Isabelle/HOL.
 
-  We also need to lift the properties that characterise when two `raw' terms of the form
+  We also need to lift the properties that characterise when two raw terms of the form
   
   \[
   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
@@ -1909,7 +1910,7 @@
   We can also add to our infrastructure cases lemmas and a (mutual)
   induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
   lemmas allow the user to deduce a property @{text "P"} by exhaustively
-  analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be
+  analysing how an element of a type, say @{text "ty\<AL>"}$_i$, can be
   constructed (that means one case for each of the term-constructors in @{text
   "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
   "ty\<AL>"}$_i\,$ looks as follows
@@ -1956,8 +1957,7 @@
   Recall the lambda-calculus with @{text "Let"}-patterns shown in
   \eqref{letpat}. The cases lemmas and the induction principle shown in
   \eqref{cases} and \eqref{induct} boil down in that example to the following three inference
-  rules (the cases lemmas are on the left-hand side; the induction principle
-  on the right):
+  rules:
 
   \begin{equation}\label{inductex}\mbox{
   \begin{tabular}{c}
@@ -2111,7 +2111,8 @@
   hypothesis requires us to establish (under some assumptions) a property
   @{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
   "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
-  any assumptions about the atoms that are bound. One obvious way around this
+  any assumptions about the atoms that are bound---for example assuming the variable convention. 
+  One obvious way around this
   problem is to rename them. Unfortunately, this leads to very clunky proofs
   and makes formalisations grievous experiences (especially in the context of 
   multiple bound atoms).
@@ -2156,10 +2157,14 @@
   "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
   for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
   all bound atoms from an assignment are fresh for @{text "c"} (fourth
-  line). If @{text "c"} is instantiated appropriately in the strong induction
-  principle, then the user can mimic the usual `pencil-and-paper' reasoning
-  employing the variable convention about bound and free variables being
-  distinct \cite{Urban08}.
+  line). In order to see how an instantiation for @{text "c"} in the
+  conclusion `controls' the premises, you have to take into account that
+  Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
+  with a pair, for example, then this type-constraint will be propagated to
+  the premises. The main point is that if @{text "c"} is instantiated
+  appropriately, then the user can mimic the usual `pencil-and-paper'
+  reasoning employing the variable convention about bound and free variables
+  being distinct \cite{Urban08}.
 
   In what follows we will show that the weak induction principle in
   \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
@@ -2172,7 +2177,7 @@
   each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
   step and the other is that we have covered all cases in the induction
   principle. Once these two proof obligations are discharged, the reasoning
-  infrastructure in the function package will automatically derive the
+  infrastructure of the function package will automatically derive the
   stronger induction principle. This way of establishing the stronger induction
   principle is considerably simpler than the earlier work presented \cite{Urban08}.
 
@@ -2229,7 +2234,7 @@
   \end{equation}\smallskip
 
   \noindent
-  which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
+  which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
   use this implication directly, because we have no information whether or not @{text
   "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
   \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
@@ -2274,7 +2279,7 @@
   \]\smallskip
 
   \noindent
-  where @{text x} and @{text y} are bound in the term, but they are also free
+  where @{text x} and @{text y} are bound in the term, but are also free
   in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say
   @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
   x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
@@ -2303,16 +2308,17 @@
 
   The remaining difficulty is when a deep binder contains some atoms that are
   bound and some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
-  the example \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
+  \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
   \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
   that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
-  does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+  does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
+  under the binder). However, the problem is that the
   permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all attoms in @{text "x\<^isub>1"}. To avoid this
   we introduce an auxiliary permutation operations, written @{text "_
   \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
   more precisely the atoms specified by the @{text "bn"}-functions) and leaves
   the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
-  can define these operations over raw terms analysing how the functions @{text
+  can define these permutation operations over raw terms analysing how the functions @{text
   "bn"}$_{1..m}$ are defined. Assuming the user specified a clause
 
   \[  
@@ -2331,7 +2337,8 @@
   \]\smallskip
 
   \noindent
-  Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} functions to 
+  Using again the quotient package  we can lift the auxiliary permutation operations
+  @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
   alpha-equated terms. Moreover we can prove the following two properties
 
   \begin{lem}\label{permutebn} 
@@ -2349,7 +2356,7 @@
   \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
-  atoms. The second states that @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} preserves
+  atoms. The second states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
   @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
   permutation functions is that they allow us to rename just the binders in a
   term, without changing anything else.
@@ -2366,8 +2373,8 @@
   \noindent
   hold. Using the first part of Lemma \ref{permutebn}, we can simplify this
   to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and 
-  @{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
-  @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by teh second part,
+  \mbox{@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since
+  @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by the second part,
   we can infer that
 
   \[
@@ -2376,7 +2383,7 @@
 
   \noindent
   holds. This allows us to use the implication from the strong cases
-  lemma.
+  lemma, and we are done.
 
   Conseqently,  we can discharge all proof-obligations about having covered all
   cases. This completes the proof establishing that the weak induction principles imply 
@@ -2449,7 +2456,7 @@
   any nominal techniques.  To our knowledge there is no concrete mathematical
   result concerning this notion of alpha-equivalence and free variables. We
   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
+  is as expected (that means bound atoms are removed from the support). We
   also showed that our specifications lift from `raw' types to types of
   alpha-equivalence classes. For this we had to establish (automatically) that every
   term-constructor and function defined for `raw' types 
@@ -2512,7 +2519,7 @@
   binder) that are not present in Ott. Our expectation is that we can still
   cover many interesting term-calculi from programming language research, for
   example the Core-Haskell language from the Introduction. With the work
-  presented in this paper we can define formally this language as shown in 
+  presented in this paper we can define it formally as shown in 
   Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
   a corresponding reasoning infrastructure.
 
@@ -2565,7 +2572,7 @@
   \end{boxedminipage}
   \caption{A definition for Core-Haskell in Nominal Isabelle. For the moment we
   do not support nested types; therefore we explicitly have to unfold the 
-  lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the 
+  lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that limitation, the 
   definition follows closely the original shown in Figure~\ref{corehas}. The
   point of our work is that having made such a definition in Nominal Isabelle,
   one obtains automatically a reasoning infrastructure for Core-Haskell.




