
diff -r 73992021c8f0 -r a7072d498723 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 19 18:56:13 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 19 21:04:24 2010 +0100
@@ -54,7 +54,7 @@
   also there one would like to bind multiple variables at once.
 
   Binding multiple variables has interesting properties that are not captured
-  by iterating single binders. First, in the case of type-schemes, we do not
+  by iterating single binders. For example in the case of type-schemes we do not
   like to make a distinction about the order of the bound variables. Therefore
   we would like to regard the following two type-schemes as alpha-equivalent
 
@@ -152,14 +152,14 @@
   would be perfectly legal instance, and so one needs additional predicates about terms 
   to ensure that the two lists are of equal length. This can result into very 
   messy reasoning (see for example~\cite{BengtsonParow09}). 
-  To avoid this, we will allow for example to specify $\mathtt{let}$s 
+  To avoid this, we will allowto specify for example $\mathtt{let}$s 
   as follows
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-  $trm$ & $::=$  & \ldots\\ 
+  $trm$ & $=$  & \ldots\\ 
         & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]
-  $assn$ & $::=$  & $\mathtt{anil}$\\
+  $assn$ & $=$  & $\mathtt{anil}$\\
          & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$
   \end{tabular}
   \end{center}
@@ -167,7 +167,7 @@
   \noindent
   where $assn$ is an auxiliary type representing a list of assignments
   and $bn$ an auxiliary function identifying the variables to be bound by 
-  the $\mathtt{let}$. This function can be defined as 
+  the $\mathtt{let}$. This function can be defined by recursion over $assn$ as 
 
   \begin{center}
   $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ 
@@ -176,7 +176,7 @@
   \noindent
   The scope of the binding is indicated by labels given to the types, for
   example \mbox{$s\!::\!trm$}, and a binding clause, in this case
-  $\mathtt{bind}\;bn\,(a) \IN s$, that states bind all the names the function
+  $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind all the names the function
   $bn$ returns in $s$.  This style of specifying terms and bindings is heavily
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
@@ -185,7 +185,7 @@
   for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of
   its specifications a reasoning infrastructure in Isabelle/HOL for
   \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
-  and the raw terms produced by Ott use names for the bound variables,
+  and the raw terms produced by Ott use names for bound variables,
   there is a key difference: working with alpha-equated terms means that the
   two type-schemes with $x$, $y$ and $z$ being distinct
 
@@ -197,11 +197,12 @@
   are not just alpha-equal, but actually equal. As a
   result, we can only support specifications that make sense on the level of
   alpha-equated terms (offending specifications, which for example bind a variable
-  according to a variable bound somewhere else, are not excluded by Ott).  Our
+  according to a variable bound somewhere else, are not excluded by Ott, but we 
+  have to).  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 raw terms. The fundamental reason is that the
+  than reasoning with raw terms. The fundamental reason for this is that the
   HOL-logic underlying Nominal Isabelle allows us to replace
   ``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals''
   in a representation based on raw terms requires a lot of extra reasoning work.
@@ -210,14 +211,10 @@
   terms (that have names for bound variables) is nearly always taken for granted, establishing 
   it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. 
   For every specification we will need to construct a type containing as 
-  elements the alpha-equated terms. To do so we use 
+  elements the alpha-equated terms. To do so, we use 
   the standard HOL-technique of defining a new type by  
-  identifying a non-empty subset of an existing type. In our 
-  case  we take as the starting point the type of sets of raw
-  terms (the latter being defined as a datatype); identify the 
-  alpha-equivalence classes according to our alpha-equivalence relation and 
-  then define the new type as these alpha-equivalence classes.  The construction we 
-  can perform in HOL is illustrated by the following picture:
+  identifying a non-empty subset of an existing type.   The construction we 
+  perform in HOL is illustrated by the following picture:
  
   \begin{center}
   \begin{tikzpicture}
@@ -240,36 +237,37 @@
   \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
   \draw (-0.95, 0.3) node[above=0mm] {isomorphism};
 
-  %\rput(3.7,1.75){isomorphism}
   \end{tikzpicture}
-
-  %%\begin{pspicture}(0.5,0.0)(8,2.5)
-  %%\showgrid
-  %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
-  %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}
-  %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9)
-  
-  %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5)
-  
-  %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1)
-  %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9)
-
-  %\rput(7.3,2.2){$\mathtt{phi}$}
-  %\rput(6,1.5){$\lama$}
-  %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}}
-  %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}}
-  %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}}
-  %\rput[c](1.7,1.5){$\lama$}
-  %\rput(3.7,1.75){isomorphism}
-  %\end{pspicture}
   \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 \cite{Homeier05}. This
-  re-implementation will automate the proofs we require for our
-  reasoning infrastructure over alpha-equated terms.\medskip
+  We take as the starting point a definition of raw terms (being defined as a 
+  datatype in Isabelle/HOL); identify then the 
+  alpha-equivalence classes in the type of sets of raw terms, according to our 
+  alpha-equivalence relation and finally define the new type as these 
+  alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are 
+  definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an 
+  equivalence relation).\marginpar{\footnotesize Does Ott allow definitions of ``strange'' types?}
+
+  The fact that we obtain an isomorphism between between the new type and the non-empty 
+  subset shows that the new type is a faithful representation of alpha-equated terms. 
+  That is different for example in the representation of terms using the locally 
+  nameless representation of binders: there are non-well-formed terms that need to
+  be excluded by reasoning about a well-formedness predicate.
+
+  The problem with introducing a new type is that in order to be useful 
+  a resoning infrastructure needs to be ``lifted'' from the underlying type
+  and subset to the new type. This is usually a tricky task. To ease this task 
+  we reimplemented in Isabelle/HOL the quotient package described by Homeier 
+  \cite{Homeier05}. Gieven that alpha is an equivalence relation, this package 
+  allows us to automatically lift definitions and theorems involving raw terms
+  to definitions and theorems involving alpha-equated terms. This of course
+  only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
+  Hence we will be able to lift, for instance, the function for free
+  variables of raw terms to alpha-equated terms (since this function respects 
+  alpha-equivalence), but we will not be able to do this with a bound-variable
+  function (since it does not respect alpha-equivalence). As a result, each
+  lifting needs some respectulness proofs which we automated.\medskip
 
   \noindent
   {\bf Contributions:}  We provide new definitions for when terms
@@ -285,15 +283,16 @@
 section {* A Short Review of the Nominal Logic Work *}
 
 text {*
-  At its core, Nominal Isabelle is based on the nominal logic work by Pitts
-  \cite{Pitts03}. The implementation of this work are described in
+  At its core, Nominal Isabelle is an adaption of the nominal logic work by
+  Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
   \cite{HuffmanUrban10}, which we review here briefly to aid the description
-  of what follows in the next sections. Two central notions in the nominal
-  logic work are sorted atoms and permutations of atoms. The sorted atoms
-  represent different kinds of variables, such as term- and type-variables in
-  Core-Haskell, and it is assumed that there is an infinite supply of atoms
-  for each sort. However, in order to simplify the description, we
-  shall assume in what follows that there is only a single sort of atoms.
+  of what follows. Two central notions in the nominal logic work are sorted
+  atoms and permutations of atoms. The sorted atoms represent different kinds
+  of variables, such as term- and type-variables in Core-Haskell, and it is
+  assumed that there is an infinite supply of atoms for each sort. However, in
+  order to simplify the description, we shall assume in what follows that
+  there is only a single sort of atoms.
+
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 
@@ -348,9 +347,55 @@
 *}
 
 
-section {* Abstractions *}
+section {* General Binders *}
 
 text {*
+  In order to keep our work managable we like to state general definitions  
+  and perform proofs inside Isabelle as much as possible, as opposed to write
+  custom ML-code that generates appropriate definitions and proofs for each 
+  instance of a term-calculus. For this, we like to consider pairs
+
+  \begin{equation}\label{three}
+  \mbox{@{text "(as, x) :: atom set \<times> \<beta>"}}
+  \end{equation}
+ 
+  \noindent
+  consisting of a set of atoms and an object of generic type. The pairs
+  are intended to be used for representing binding such as found in 
+  type-schemes
+
+  \begin{center}
+  $\forall \{x_1,\ldots,x_n\}. T$
+  \end{center}
+  
+  \noindent
+  where the atoms $x_1,\ldots,x_n$ is intended to be in \eqref{three} the 
+  set @{text as} of atoms we want to bind, and $T$, an object-level type, is 
+  one instance for the generic $x$.
+
+  The first question we have to answer is when we should consider the pairs 
+  in \eqref{three} as alpha-equivelent? (At the moment we are interested in
+  the notion of alpha-equivalence that is \emph{not} preserved by adding 
+  vacuous binders.) Assuming we are given a free-variable function, say 
+  \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then we expect for two alpha-equivelent
+  pairs that their sets of free variables aggree. That is
+  %
+  \begin{equation}\label{four}
+  \mbox{@{text "(as, x) \<approx> (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}} 
+  \end{equation}
+
+  \noindent
+  Next we expect that there is a permutation, say $p$, that leaves the 
+  free variables unchanged, but ``moves'' the bound names in $x$ so that
+  we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two
+  elments of type $\beta$ are equivalent. We also expect that $p$ 
+  makes the binders equal. We can formulate these requirements as: there
+  exists a $p$ such that $i)$  @{term "(fv(x) - as) \<sharp>* p"}, $ii)$ @{text "(p \<bullet> x) R y"} and
+  $iii)$ @{text "(p \<bullet> as) = bs"}. 
+
+  We take now \eqref{four} and the three 
+ 
+
   General notion of alpha-equivalence (depends on a free-variable
   function and a relation).
 *}
@@ -391,7 +436,7 @@
   {\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 about the abstract 
+  also for patiently explaining some of the finer points about the abstract 
   definitions and about the implementation of the Ott-tool.
 
 




