
diff -r 89f9d7e85e88 -r 8bda1d947df3 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Apr 10 16:02:30 2012 +0100
+++ b/LMCS-Paper/Paper.thy	Thu Apr 12 01:39:54 2012 +0100
@@ -114,9 +114,9 @@
   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
   type-variables.  While it is possible to implement this kind of more general
   binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
-  formalisation of W. For example, the usual definition when a 
-  type is an instance of a type-scheme requires in the iterated version 
-  the following auxiliary \emph{unbinding relation}
+  formalisation of W. For example, the usual definition for a
+  type being an instance of a type-scheme requires in the iterated version 
+  the following auxiliary \emph{unbinding relation}:
 
   \[
   \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
@@ -127,14 +127,12 @@
   \noindent
   Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
   address the following problem:
-  Given a type-scheme @{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, though in general 
-  we will only get access to some type-variables and some type that are  
+  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  
   ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
-  for alpha-equated type-schemes. 
-  Still, 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 this 
+  definition in place we can formally define when a type is an instance of a type-scheme as follows:
 
   \[
   @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
@@ -142,16 +140,17 @@
   
   \noindent
   This means there exists a list of type-variables @{text xs} and a type @{text T'} to which
-  the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
+  the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} whose domain is
   @{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 
   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. 
   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.
+  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
   mechanisms for binding single variables have so far not fared very well with
@@ -509,7 +508,8 @@
   where the generic type @{text "\<beta>"} is the type of the object 
   over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
-  the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}, 
+  the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}} 
+  (even if this operation is non-commutative), 
   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 atoms, products, lists, permutations, sets, 
@@ -1232,20 +1232,17 @@
   \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Baz\<^isub>1 p::pat t::trm"} & 
-     \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
+     \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text "p t"}\\
   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 
-     \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
-     \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
+     \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "p t\<^isub>1"},
+     \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "p t\<^isub>2"}\\
   \end{tabular}}
   \]\smallskip
 
   \noindent
   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
   out different atoms to become bound, respectively be free, 
-  in @{text "p"}.\footnote{Although harmless, in our implementation 
-  we exlude such specifications even 
-  if @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} are the same binding 
-  functions.}$^,$\footnote{Since the Ott-tool does not derive a reasoning 
+  in @{text "p"}.\footnote{Since the Ott-tool does not derive a reasoning 
   infrastructure for 
   alpha-equated terms with deep binders, it can permit such specifications.}
   
@@ -1291,13 +1288,35 @@
   unions of atom sets or appended atom lists (case @{text ACons'}). This
   restriction will simplify some automatic definitions and proofs later on.
   
-  In order to simplify our definitions of free atoms and alpha-equivalence, 
-  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 given by the user, we add implicitly a special \emph{empty} binding
-  clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
-  of the lambda-terms, the completion produces
+  To sum up this section, we introduced nominal datatype
+  specifications, which are like standard datatype specifications in
+  Isabelle/HOL extended with 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
+  constructor, but bodies of binding clauses can only occur in a
+  single one. Binding clauses come in three modes: \isacommand{binds},
+  \isacommand{binds (set)} and \isacommand{binds (set+)}.  Binders
+  fall into two categories: shallow binders and deep binders. Shallow
+  binders can occur in more than one binding clause and only have to
+  respect the binding mode (i.e.~be of the right type). Deep binders
+  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
+  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
+  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
+  given by the user, we add implicitly a special \emph{empty} binding
+  clause, written \isacommand{binds}~@{term
+  "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms,
+  the completion produces
 
   \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}




