
diff -r aa1ba91ed1ff -r 95ff21cda33c LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Fri Apr 20 15:28:35 2012 +0200
+++ b/LMCS-Paper/Paper.thy	Fri Apr 20 15:29:40 2012 +0200
@@ -129,10 +129,10 @@
   address the following problem:
   Given a type-scheme, say @{text S}, how does one get access to the bound type-variables 
   and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though 
-  in general it will only provide some list of type-variables together with a type that are  
+  in general it will only provide \emph{a} list of type-variables together with \emph{a} type that are  
   ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
-  for alpha-equated type-schemes. With this 
-  definition in place we can formally define when a type is an instance of a type-scheme as follows:
+  for alpha-equated type-schemes. With the unbinding relation  
+  in place, we can define when a type @{text T} is an instance of a type-scheme @{text S} as follows:
 
   \[
   @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
@@ -144,15 +144,15 @@
   @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
   The problem with this definition is that we cannot follow the usual proofs 
   that are by induction on the type-part of the type-scheme (since it is under
-  an existential quantifier and only an alpha-variant). The representation of 
+  an existential quantifier and only an alpha-variant). The implementation of 
   type-schemes using iterations of single binders 
   prevents us from directly ``unbinding'' the bound type-variables and the type-part. 
-  Clearly, some more dignified approach to formalising algorithm W is desirable. 
+  Clearly, a more dignified approach for formalising algorithm W is desirable. 
   The purpose of this paper is to introduce general binders, which 
   allow us to represent type-schemes so that they can bind multiple variables at once
   and as a result solve this problem more straightforwardly.
   The need of iterating single binders is also one reason
-  why Nominal Isabelle and similar theorem provers that only provide
+  why the existing Nominal Isabelle and similar theorem provers that only provide
   mechanisms for binding single variables have so far not fared very well with
   the more advanced tasks in the POPLmark challenge \cite{challenge05},
   because also there one would like to bind multiple variables at once.
@@ -1290,7 +1290,7 @@
   
   To sum up this section, we introduced nominal datatype
   specifications, which are like standard datatype specifications in
-  Isabelle/HOL extended with specifications for binding
+  Isabelle/HOL but extended with binding clauses and specifications for binding
   functions. Each constructor argument in our specification can also
   have an optional label. These labels are used in the binding clauses
   of a constructor; there can be several binding clauses for each
@@ -1303,13 +1303,15 @@
   can also occur in more than one binding clause, unless they are
   recursive in which case they can only occur once. Each of the deep
   binders can only have a single binding function.  Binding functions
-  are defined by recursion over a nominal datatype.  They can only
+  are defined by recursion over a nominal datatype.  They can
   return the empty set, singleton atoms and unions of sets of atoms
   (for binding modes \isacommand{binds (set)} and \isacommand{binds
   (set+)}), and the empty list, singleton atoms and appended lists of
   atoms (for mode \isacommand{bind}). However, they can only return
-  atoms that are not mentioned in any binding clause.  In order to
-  simplify our definitions of free atoms and alpha-equivalence, we
+  atoms that are not mentioned in any binding clause.  
+
+  In order to
+  simplify our definitions of free atoms and alpha-equivalence we define next, we
   shall assume specifications of term-calculi are implicitly
   \emph{completed}. By this we mean that for every argument of a
   term-constructor that is \emph{not} already part of a binding clause
@@ -1413,7 +1415,7 @@
   "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
   clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). 
-  Suppose the binding clause @{text bc\<^isub>i} is of the form 
+  Suppose a binding clause @{text bc\<^isub>i} is of the form 
   
   \[
   \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
@@ -1614,10 +1616,10 @@
   term-constructor @{text C} is of type @{text ty} and has the binding clauses
   @{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form
   
-  \[
+  \begin{equation}\label{gform}
   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
   {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} 
-  \]\smallskip
+  \end{equation}\smallskip
 
   \noindent
   The task below is to specify what the premises corresponding to a binding
@@ -1634,8 +1636,8 @@
   the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>,
   d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
   whereby the labels @{text "d"}$_{1..q}$ refer to some of the arguments @{text
-  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of @{text
-  "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such
+  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of the @{text
+  "z\<PRIME>"}$_{1..n}$ in \eqref{gform}. In order to relate two such
   tuples we define the compound alpha-equivalence relation @{text "R"} as
   follows
 
@@ -1648,7 +1650,7 @@
   labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a
   recursive argument of @{text C} and have type @{text "ty\<^isub>i"}; otherwise
   we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the
-  latter is because @{text "ty\<^isub>i"} is not part of the specified types
+  latter is because @{text "ty\<^isub>i"} is then not part of the specified types
   and alpha-equivalence of any previously defined type is supposed to coincide
   with equality.  This lets us now define the premise for an empty binding
   clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be
@@ -1984,7 +1986,7 @@
   lemmas allow the user to deduce a property @{text "P"} by exhaustively
   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\,$). The lifted cases lemma for a type @{text
   "ty\<AL>"}$_i\,$ looks as follows
 
   \begin{equation}\label{cases}
@@ -2231,7 +2233,7 @@
   Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
   with, for example, a pair, 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'
+  appropriately, then the user can mimic the usual convenient `pencil-and-paper'
   reasoning employing the variable convention about bound and free variables
   being distinct \cite{Urban08}.
 
@@ -2453,8 +2455,8 @@
   holds. This allows us to use the implication from the strong cases
   lemma, and we are done.
 
-  Consequently,  we can discharge all proof-obligations about having covered all
-  cases. This completes the proof establishing that the weak induction principles imply 
+  Consequently,  we can discharge all proof-obligations about having `covered all
+  cases'. This completes the proof establishing that the weak induction principles imply 
   the strong induction principles. These strong induction principles have already proved 
   being very useful in practice, particularly for proving properties about 
   capture-avoiding substitution \cite{Urban08}. 
@@ -2507,11 +2509,11 @@
   \cite{BengtsonParow09,UrbanNipkow09}).  Both
   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 described in this paper, but needs a cumbersome
-  iteration with single binders. The resulting formal reasoning turned out to
-  be rather unpleasant. 
- 
+  the need to `unbind' bound variables and the resulting formal reasoning turned out to
+  be rather unpleasant. In contrast, the unbinding can be 
+  done in one step with our
+  general binders described in this paper.
+
   The most closely related work to the one presented here is the Ott-tool by
   Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
   \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
@@ -2525,9 +2527,9 @@
   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 atoms are removed from the support). We
-  also showed that our specifications lift from `raw' types to types of
+  also showed that our specifications lift from `raw' terms to 
   alpha-equivalence classes. For this we have established (automatically) that every
-  term-constructor and function defined for `raw' types 
+  term-constructor and function defined for `raw' terms 
   is respectful w.r.t.~alpha-equivalence.
 
   Although we were heavily inspired by the syntax of Ott, its definition of
@@ -2582,21 +2584,23 @@
   \]\smallskip
   
   \noindent
-  and therefore need the extra generality to be able to distinguish between
-  both specifications.  Because of how we set up our definitions, we also had
-  to impose some restrictions (like a single binding function for a deep
-  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 it formally as shown in 
-  Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
-  a corresponding reasoning infrastructure. However we have found out that 
-  telescopes seem to not easily representable in our framework. The reason is that
-  we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms.
-  This requires restrictions, which class with the `global' scope of binders in
-  telescopes. They can
-  be represented in the framework described in \cite{WeirichYorgeySheard11} using an extension of
-  the usual locally-nameless representation. 
+  and therefore need the extra generality to be able to distinguish
+  between both specifications.  Because of how we set up our
+  definitions, we also had to impose some restrictions (like a single
+  binding function for a deep 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 it formally as shown in
+  Figure~\ref{nominalcorehas} and then Nominal Isabelle derives
+  automatically a corresponding reasoning infrastructure. However we
+  have found out that telescopes seem to not easily be representable
+  in our framework.  The reason is that we need to be able to lift our
+  @{text bn}-functions to alpha-equated lambda-terms and therefore
+  need to restrict what these @{text bn}-functions can return.
+  Telescopes can be represented in the framework described in
+  \cite{WeirichYorgeySheard11} using an extension of the usual
+  locally-nameless representation. 
 
   \begin{figure}[p]
   \begin{boxedminipage}{\linewidth}
@@ -2631,10 +2635,10 @@
   \isacommand{and}~@{text "tvtk_lst ="}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
   \isacommand{and}~@{text "tvck_lst ="}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
   \isacommand{binder}\\
-  @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
-  @{text "bv\<^isub>1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  @{text "bv\<^isub>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  @{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
+  \;@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
+  \;@{text "bv\<^isub>1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+  \;@{text "bv\<^isub>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+  \;@{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
   \isacommand{where}\\
   \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv\<^isub>3 tvts) @ (bv\<^isub>2 tvcs) @ (bv\<^isub>1 vs)"}\\
   $|$~@{text "bv\<^isub>1 VTNil = []"}\\
@@ -2706,11 +2710,12 @@
   definitions to equivariant functions (for them we can provide more
   automation).
 
-  There are some restrictions we imposed in this paper that can be lifted using 
+  There are some restrictions we had
+  to impose in this paper that can be lifted using 
   a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which
-  is however not yet part of the stable distribution.
+  however is not yet part of the stable distribution.
   This reimplementation allows nested
-  datatype definitions would allow one to specify, for instance, the function kinds
+  datatype definitions and would allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). We can 
   also use it to represent the @{text "Let"}-terms from the Introduction where
@@ -2723,10 +2728,10 @@
   \]\smallskip
 
   \noindent
-  For this we have to represent the @{text "let"}-assignments as finite sets
+  For this we have to represent the @{text "Let"}-assignments as finite sets
   of pair and a binding function that picks out the left components to be bound in @{text s}.
 
-  One line of investigation is whether we can go beyond the 
+  One line of future investigation is whether we can go beyond the 
   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 




