--- 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.
 
 
 *}