--- a/Paper/Paper.thy	Tue Mar 30 17:55:46 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 21:15:13 2010 +0200
@@ -1091,29 +1091,32 @@
   independently an alpha-equivalence relation over them.
 
 
-  The datatype definition can be obtained by just stripping off the 
+  The datatype definition can be obtained by stripping off the 
   binding clauses and the labels on 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 user. In our implementation we just use an affix @{text "_raw"}.
-  For the purpose of the paper we just use superscripts to indicate a
-  notion defined over alpha-equivalence classes and leave out the superscript
-  for the corresponding notion on the ``raw'' level. So for example we have
-
+  For the purpose of the paper we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
+  that a notion is defined over alpha-equivalence classes and leave it out 
+  for the corresponding notion defined on the ``raw'' level. So for example 
+  we have
+  
   \begin{center}
   @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
   \end{center}
   
   \noindent
+  
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   non-empty and the types in the constructors only occur in positive 
-  position (see \cite{Berghofer99} for an indepth explanation of the datatype package
+  position (see \cite{Berghofer99} for an indepth description of the datatype package
   in Isabelle/HOL). We then define the user-specified binding 
-  functions by primitive recursion over the raw datatypes. We can also
-  easily define a permutation operation by primitive recursion so that for each
-  term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
+  functions, called @{term "bn_ty"}, by primitive recursion over the corresponding 
+  raw datatype @{text ty}. We can also easily define permutation operations by 
+  primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} 
+  we have that
 
   \begin{center}
-  @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+  @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{center}
   
   % TODO: we did not define permutation types
@@ -1131,30 +1134,33 @@
   \end{center}
 
   \noindent
-  We define them together with the auxiliary free variable functions for
-  binding functions. Given binding functions for raw types
+  We define them together with auxiliary free variable functions for
+  the binding functions. Given binding functions 
   @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
-
+  %
   \begin{center}
-  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
   \end{center}
 
   \noindent
-  The basic idea behind these free-variable functions is to collect all atoms
-  that are not bound in a term constructor, but because of the rather
-  complicated binding mechanisms the details are somewhat involved. 
+  The reason for this setup is that in a deep binder not all atoms have to be
+  bound. While the idea behind these free variable functions is just to
+  collect all atoms that are not bound, because of the rather complicated
+  binding mechanisms their definitions are somewhat involved.
 
   Given a term-constructor @{text "C"} of type @{text ty} with argument types
-  @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} and some binding clauses, the function
+  \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}} and given some binding clauses associated with 
+  this constructor, the function
   @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
-  defined below for each argument. From the binding clause of this term
-  constructor, we can determine whether the argument is a shallow or deep
+  calculated below for each argument. 
+
+  First we deal with the case @{text "x\<^isub>i"} is a binder. From the binding clauses, 
+  we can determine whether the argument is a shallow or deep
   binder, and in the latter case also whether it is a recursive or
-  non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with
-  type @{text "ty\<^isub>i"}, is a binder, the value is:
+  non-recursive binder. 
 
   \begin{center}
-  \begin{tabular}{cp{7cm}}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
   $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
       non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\
@@ -1164,23 +1170,29 @@
   \end{center}
 
   \noindent
-  In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
-  one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated
-  as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.
-  Otherwise there are two cases: either the
-  corresponding binders are all shallow or there is a single deep binder.
-  In the former case we build the union of all shallow binders; in the
-  later case we just take the set of atoms specified binding
-  function returns. With @{text "bnds"} computed as above the value of
-  for @{text "x\<^isub>i"} is given by:
+  The first clause states that shallow binders do not contribute to the
+  free variables; in the second clause, we have to look up all
+  the free variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this
+  is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the 
+  binder is recursive, we need to bind all variables specified by 
+  @{text "bn_ty\<^isub>i"}---therefore we subtract @{text "bn_ty\<^isub>i x\<^isub>i"} from the free
+  variables of @{text "x\<^isub>i"}.
+
+  In case the argument is \emph{not} a binder, we need to consider 
+  whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. 
+  In this case we first calculate the set @{text "bnds"} as follows: 
+  either the binders are all shallow or there is a single deep binder.
+  In the former case we take @{text bnds} to be the union of all shallow 
+  binders; in the latter case, we just take the set of atoms specified by the 
+  binding function. The value for @{text "x\<^isub>i"} is then given by:
 
   \begin{center}
-  \begin{tabular}{cp{7cm}}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
   $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
   $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
-     we are defining with the free variable function @{text "fv_ty\<^isub>i"}\\
+  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
+     corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
 %     with a free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
@@ -1188,28 +1200,37 @@
   \end{center}
 
   \noindent 
-  Next, for each binding function @{text "bn_ty"} we define a
-  free variable function @{text "fv_bn_ty"}. The basic idea behind this
-  function is to compute all the free atoms that are not bound by the binding
-  function. So given that @{text "bn"} is a binding function for type
-  @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
-  omission of the arguments present in @{text "bn"}.
+  Like the function @{text atom}, @{text "atoms"} coerces a set of atoms to the generic atom type.
+  It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.
 
-  For a binding function clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
-  we define @{text "fv_bn"} to be the union of the values calculated
-  for @{text "x\<^isub>j"} as follows:
+  The last case we need to consider is when @{text "x\<^isub>i"} is neither
+  a binder nor a body of an abstraction. In this case it is defined 
+  as above, except that we do not subtract the set @{text bnds}.
+  
+  Next, we need to define a free variable function @{text "fv_bn_ty\<^isub>i"} for 
+  each binding function @{text "bn_ty\<^isub>i"}. The idea behind this
+  function is to compute the set of free atoms that are not bound by 
+  the binding function. Because of the restrictions we imposed on the 
+  form of binding functions, this can be done automatically by recursively 
+  building up the the set of free variables from the arguments that are 
+  not bound. Let us assume one clause of the binding function is 
+  @{text "bn_ty\<^isub>i (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the 
+  union of the values calculated for @{text "x\<^isub>j"} of type @{text "ty\<^isub>j"}
+  as follows:
 
   \begin{center}
-  \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom,
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\ 
+  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is an atom,
      atom list or atom set\\
-  $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 
-    with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\
-  $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\
-  $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\
-  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is 
-     one of the datatypes
-     we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+  $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the 
+  recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]
+  %
+  \multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\ 
+  $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\
+  $\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\
+  $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw
+     types corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
 %     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise

--- a/Paper/document/root.bib	Tue Mar 30 17:55:46 2010 +0200
+++ b/Paper/document/root.bib	Tue Mar 30 21:15:13 2010 +0200
@@ -2,19 +2,18 @@
   author = 	 {S.~Berghofer and M.~Wenzel},
   title = 	 {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in 
                   {F}ormal-{L}ogic {E}ngineering},
-  booktitle = 	 {Proc.~of the 12th International Conference Theorem Proving in 
-                  Higher Order Logics (TPHOLs)},
+  booktitle = 	 {Proc.~of the 12th TPHOLs conference},
   pages = 	 {19--36},
   year = 	 1999,
-  number = 	 1690,
+  volume = 	 1690,
   series = 	 {LNCS}
 }
 
 @InProceedings{CoreHaskell,
   author = 	 {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},
   title = 	 {{S}ystem {F} with {T}ype {E}quality {C}oercions},
-  booktitle = 	 {Proc of TLDI},
-  pages = 	 {??},
+  booktitle = 	 {Proc of the TLDI Workshop},
+  pages = 	 {53-66},
   year = 	 {2007}
 }
 
@@ -83,8 +82,8 @@
 @Unpublished{HuffmanUrban10,
   author = 	 {B.~Huffman and C.~Urban},
   title = 	 {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
-  note = 	 {To appear at {\it ITP'10 Conference}},
-  annote =       {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
+  note = 	 {To appear at {\it ITP'10 Conference}, 
+                  http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
   year = 	 {2010}
 }