--- a/Paper/Paper.thy	Thu Mar 18 23:38:01 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 23:39:26 2010 +0100
@@ -23,6 +23,7 @@
   \end{center}
 
   \noindent
+  where bound variables have a name.
   For such terms it derives automatically a reasoning
   infrastructure, which has been used in formalisations of an equivalence
   checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
@@ -148,19 +149,79 @@
   \end{center}
 
   \noindent
-  where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound
-  in $s$. In this representation we need additional predicates to ensure 
+  where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes 
+  bound in $s$. In this representation we need additional predicates to ensure 
   that the two lists are of equal length. This can result into very 
   unintelligible reasoning (see for example~\cite{BengtsonParow09}). 
+  To avoid this, we will allow for example specifications of $\mathtt{let}$s 
+  as follows
+
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
+  $trm$ & $::=$  & \ldots\\ 
+        & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;t\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN t$\\[1mm]
+  $assn$ & $::=$  & $\mathtt{anil}$\\
+         & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  where $assn$ is an auxiliary type representing a list of assignments
+  and $bn$ an auxilary function identifying the variables to be bound by 
+  the $\mathtt{let}$, given by 
+
+  \begin{center}
+  $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ 
+  \end{center}
   
+  \noindent
+  This style of specifications for term-calculi with multiple binders is heavily 
+  inspired by the Ott-tool \cite{ott-jfp}.
+
+  We will not be able to deal with all specifications that are allowed by
+  Ott. One reason is that we establish the reasoning infrastructure for
+  alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its
+  specifiactions a reasoning infrastructure involving concrete,
+  \emph{non}-alpha-equated terms. To see the difference, note that working
+  with alpha-equated terms means that the two type-schemes with $x$, $y$ and
+  $z$ being distinct
+
+  \begin{center}
+  $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$ 
+  \end{center}
+  
+  \noindent
+  are not just alpha-equal, but actually equal---we are working with 
+  alpha-equivalence classes, but still have that bound variables 
+  carry a name.
+  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 about alpha-equated terms is much easier than reasoning 
+  with concrete terms. The fundamental reason is that the HOL-logic 
+  underlying Nominal Isabelle allows us to replace ``equals-by-equals''. 
+  Replacing ``alpha-equals-by-alpha-equals'' requires a lot of work.
+  
+  Although a reasoning infrastructure for alpha-equated terms with names 
+  is in informal reasoning nearly always taken for granted, establishing 
+  it automatically in a theorem prover is a rather non-trivial task. 
+  For every specification we will construct a type that contains 
+  exactly the corresponding alpha-equated terms. For this we use the 
+  standard HOL-technique of defining a new type that has been 
+  identified as a non-empty subset of an existing type. In our 
+  context we take as the starting point the type of sets of concrete
+  terms (the latter being defined as datatypes). Then quotient these
+  sets according to our alpha-equivalence relation and then identifying
+  the new type as these alpha-equivalence classes.  The construction we 
+  can perform in HOL is illustrated by the following picture:
+
   
 
-  
-  
   Contributions:  We provide definitions for when terms
   involving general bindings are alpha-equivelent.
 
-  %\begin{center}
+  \begin{center}
+  figure
   %\begin{pspicture}(0.5,0.0)(8,2.5)
   %%\showgrid
   %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
@@ -180,9 +241,24 @@
   %\rput[c](1.7,1.5){$\lama$}
   %\rput(3.7,1.75){isomorphism}
   %\end{pspicture}
-  %\end{center}
+  \end{center}
+
+  \noindent
+  To ``lift'' the reasoning from the underlying type to the new type
+  is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL
+  the quotient package described by Homeier in \cite{Homeier05}. This
+  re-implementation will automate the proofs we require for our
+  reasoning infrastructure over alpha-equated terms.\medskip
 
-  quotient package \cite{Homeier05}
+  \noindent
+  {\bf Contributions:}  We provide new definitions for when terms
+  involving multiple binders are alpha-equivalent. These definitions are
+  inspired by earlier work of Pitts \cite{}. By means of automatic
+  proofs, we establish a reasoning infrastructure for alpha-equated
+  terms, including properties about support, freshness and equality
+  conditions for alpha-equated terms. We will also derive for these
+  terms a strong induction principle that has the variable convention
+  already built in.
 *}
 
 section {* A Short Review of the Nominal Logic Work *}
@@ -291,10 +367,11 @@
   \medskip
 
   \noindent
-  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the 
+  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
-  also for explaining some of the finer points of the OTT-tool.
+  also for explaining some of the finer points about the abstract 
+  definitions and about the implmentation of the Ott-tool.
 
 
 *}

--- a/Paper/document/root.bib	Thu Mar 18 23:38:01 2010 +0100
+++ b/Paper/document/root.bib	Thu Mar 18 23:39:26 2010 +0100
@@ -9,6 +9,22 @@
   series = 	 {LNCS}
 }
 
+@article{ott-jfp,
+ author     = {P.~Sewell and 
+               F.~Z.~Nardelli and 
+               S.~Owens and 
+               G.~Peskine and 
+               T.~Ridge and 
+               S.~Sarkar and 
+               R.~Strni\v{s}a},
+ title      = {{Ott}: {E}ffective {T}ool {S}upport for the {W}orking {S}emanticist},
+ journal    = {Journal of Functional Programming},
+ year       = {2010},
+ volume     = {20},
+ number     = {1},
+ pages      = {70--122}
+}
+
 @INPROCEEDINGS{Pottier06,
   author = {F.~Pottier},
   title = {{A}n {O}verview of {C$\alpha$ml}},

--- a/Paper/document/root.tex	Thu Mar 18 23:38:01 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 23:39:26 2010 +0100
@@ -47,14 +47,15 @@
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
-programming language calculi. In this paper we present an extension of Nominal
-Isabelle in order to deal with general binding structures. Such binding structures
-are ubiquitous in programming language research and only very poorly supported
-with single binders, as for example found in the lambda-calculus. For our
-extension we introduce novel definitions of alpha-equivalence and establish
-automatically the reasoning infrastructure for alpha-equated terms. This
-includes a strong induction principle which has the variable convention
-already built in.
+programming language calculi involving bound variables that have names (as
+opposed to de-Bruijn indices). In this paper we present an extension of
+Nominal Isabelle in order to deal with general binding structures. Such
+binding structures are ubiquitous in programming language research and only
+very poorly supported with single binders, as for example found in the
+lambda-calculus. For our extension we introduce novel definitions of
+alpha-equivalence and establish automatically the reasoning infrastructure for
+alpha-equated terms. This includes strong induction principles that have the
+variable convention already built in.
 \end{abstract}