
diff -r 06a8f782b2c1 -r c86b98642013 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Oct 07 14:23:32 2010 +0900
+++ b/Paper/Paper.thy	Fri Oct 08 13:41:54 2010 +0100
@@ -87,13 +87,14 @@
   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, this leads to a rather clumsy
-  formalisation of W. The need of iterating single binders is also one reason
-  why Nominal Isabelle 
+  formalisation of W. 
+  %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 
-  has not fared extremely well with the
-  more advanced tasks in the POPLmark challenge \cite{challenge05}, because
-  also there one would like to bind multiple variables at once. 
+  %has not fared extremely well with the
+  %more advanced tasks in the POPLmark challenge \cite{challenge05}, because
+  %also there one would like to bind multiple variables at once. 
 
   Binding multiple variables has interesting properties that cannot be captured
   easily by iterating single binders. For example in the case of type-schemes we do not
@@ -274,7 +275,7 @@
   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   terms is nearly always taken for granted, establishing it automatically in
   the Isabelle/HOL is a rather non-trivial task. For every
-  specification we will need to construct a type containing as elements the
+  specification we will need to construct type(s) containing as 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.  The
   construction we perform in Isabelle/HOL can be illustrated by the following picture:
@@ -309,8 +310,8 @@
   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 property that our relation for $\alpha$-equivalence is
-  indeed an equivalence relation).
+  in Isabelle/HOL and our relation for $\alpha$-equivalence is
+  an equivalence relation).
 
   %The fact that we obtain an isomorphism between the new type and the
   %non-empty subset shows that the new type is a faithful representation of
@@ -379,9 +380,9 @@
   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
   that our specifications make sense for reasoning about $\alpha$-equated terms.  
   The main improvement over Ott is that we introduce three binding modes
-  (only one is present in Ott), provide definitions for $\alpha$-equivalence and 
+  (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and 
   for free variables of our terms, and also derive a reasoning infrastructure
-  for our specifications inside Isabelle/HOL.
+  for our specifications inside Isabelle/HOL from ``first principles''.
 
 
   %\begin{figure}
@@ -459,20 +460,37 @@
   for example permutations acting on products, lists, sets, functions and booleans is
   given by:
   %
-  \begin{equation}\label{permute}
-  \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  %\begin{equation}\label{permute}
+  %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  %\begin{tabular}{@ {}l@ {}}
+  %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+  %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
+  %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+  %\end{tabular} &
+  %\begin{tabular}{@ {}l@ {}}
+  %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
+  %@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
+  %@{thm permute_bool_def[no_vars, THEN eq_reflection]}
+  %\end{tabular}
+  %\end{tabular}}
+  %\end{equation}
+  %
+  \begin{center}
+  \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
   \begin{tabular}{@ {}l@ {}}
-  @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
+  @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
+  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
+  \end{tabular} &
+  \begin{tabular}{@ {}l@ {}}
   @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
   @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
   @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
   \end{tabular}
   \end{tabular}}
-  \end{equation}
+  \end{center}
 
   \noindent
   Concrete permutations in Nominal Isabelle are built up from swappings, 
@@ -504,11 +522,12 @@
   A striking consequence of these definitions is that we can prove
   without knowing anything about the structure of @{term x} that
   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
-  @{text x} unchanged:
+  @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
+  then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.
 
-  \begin{myproperty}\label{swapfreshfresh}
-  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
-  \end{myproperty}
+  %\begin{myproperty}\label{swapfreshfresh}
+  %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+  %\end{myproperty}
 
   %While often the support of an object can be relatively easily 
   %described, for example for atoms, products, lists, function applications, 
@@ -629,8 +648,9 @@
 
   In order to keep our work with deriving the reasoning infrastructure
   manageable, we will wherever possible state definitions and perform proofs
-  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
-  generates them anew for each specification. To that end, we will consider
+  on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that
+  %generates them anew for each specification. 
+  To that end, we will consider
   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
   are intended to represent the abstraction, or binding, of the set of atoms @{text
   "as"} in the body @{text "x"}.
@@ -657,7 +677,7 @@
        \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\ 
   \end{array}
   \end{equation}
-
+  %
   \noindent
   Note that this relation depends on the permutation @{text
   "p"}; $\alpha$-equivalence between two pairs is then the relation where we
@@ -682,7 +702,7 @@
          \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
   \end{array}
   \end{equation}
-  
+  %
   \noindent
   where @{term set} is the function that coerces a list of atoms into a set of atoms.
   Now the last clause ensures that the order of the binders matters (since @{text as}
@@ -701,12 +721,12 @@
   \end{array}
   \end{equation}
 
-  It might be useful to consider first some examples about how these definitions
+  It might be useful to consider first some examples how these definitions
   of $\alpha$-equivalence pan out in practice.  For this consider the case of
   abstracting a set of atoms over types (as in type-schemes). We set
   @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
   define
-
+  %
   \begin{center}
   @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
   \end{center}
@@ -1049,7 +1069,7 @@
   \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 
   \end{tabular}}
   \end{equation}
-  
+  %
   \noindent
   In this specification the function @{text "bn"} determines which atoms of
   the pattern @{text p} are bound in the argument @{text "t"}. Note that in the
@@ -1059,14 +1079,14 @@
 
   As said above, for deep binders we allow binding clauses such as
   %
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "Bar p::pat t::trm"} &  
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
+  %\begin{center}
+  %\begin{tabular}{ll}
+  @{text "Bar p::pat t::trm"} %%%&  
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\
+  %\end{tabular}
+  %\end{center}
+  %
+  %\noindent
   where the argument of the deep binder also occurs in the body. We call such
   binders \emph{recursive}.  To see the purpose of such recursive binders,
   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
@@ -1088,7 +1108,7 @@
   \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
   \end{tabular}}
   \end{equation}
-
+  %
   \noindent
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
@@ -1098,7 +1118,7 @@
   To make sure that atoms bound by deep binders cannot be free at the
   same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
-
+  %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Baz\<^isub>1 p::pat t::trm"} & 
@@ -1244,20 +1264,20 @@
   @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the 
   set of binding atoms in the binders and @{text "B'"} for the set of free atoms in 
   non-recursive deep binders,
-  then the free atoms of the binding clause @{text bc\<^isub>i} are
+  then the free atoms of the binding clause @{text bc\<^isub>i} are\\[-2mm]
   %
   \begin{equation}\label{fadef}
   \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
   \end{equation}
-
+  %
   \noindent
   The set @{text D} is formally defined as
   %
-  \begin{center}
+  %\begin{center}
   @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
-  \end{center} 
-
-  \noindent
+  %\end{center} 
+  %
+  %\noindent
   where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the 
   specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function 
   we are defining by recursion; 
@@ -1265,7 +1285,7 @@
   otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
   
   In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
-  for atom types to which shallow binders may refer
+  for atom types to which shallow binders may refer\\[-4mm]
   %
   %\begin{center}
   %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -1276,21 +1296,21 @@
   %\end{center}
   %
   \begin{center}
-  @{text "bn_atom a \<equiv> {atom a}"}\hspace{17mm}
-  @{text "bn_atom_set as \<equiv> atoms as"}\\
-  @{text "bn_atom_list as \<equiv> atoms (set as)"}
+  @{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
+  @{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
+  @{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
   \end{center}
-
+  %
   \noindent 
   Like the function @{text atom}, the function @{text "atoms"} coerces 
   a set of atoms to a set of the generic atom type. 
   %It is defined as  @{text "atoms as \<equiv> {atom a | a \<in> as}"}. 
-  The set @{text B} is then formally defined as
+  The set @{text B} is then formally defined as\\[-4mm]
   %
   \begin{center}
   @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
   \end{center} 
-
+  %
   \noindent 
   where we use the auxiliary binding functions for shallow binders. 
   The set @{text "B'"} collects all free atoms in non-recursive deep
@@ -1303,12 +1323,12 @@
   %\noindent
   with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the 
   @{text "l"}$_{1..r}$ being among the bodies @{text
-  "d"}$_{1..q}$. The set @{text "B'"} is defined as
+  "d"}$_{1..q}$. The set @{text "B'"} is defined as\\[-5mm]
   %
   \begin{center}
-  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
-  \end{center} 
-
+  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
+  \end{center}
+  %
   \noindent
   This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
 
@@ -1365,7 +1385,7 @@
   Recall that @{text ANil} and @{text "ACons"} have no
   binding clause in the specification. The corresponding free-atom
   function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
-  occurring in an assignment (in case of @{text "ACons"}, they are given in
+  of an assignment (in case of @{text "ACons"}, they are given in
   terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). 
   The binding only takes place in @{text Let} and
   @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
@@ -1988,20 +2008,26 @@
   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
   %
   \begin{center}
-  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
+  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} \;\; with
+  $\begin{cases}
+  \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
+  \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
+  \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}  
+  \end{cases}$
   \end{center}
   %
+  %\noindent
+  %with @{text "y\<^isub>i"} determined as follows:
+  %
+  %\begin{center}
+  %\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+  %\end{tabular}
+  %\end{center}
+  %
   \noindent
-  with @{text "y\<^isub>i"} determined as follows:
-  %
-  \begin{center}
-  \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-  $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
-  $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
-  $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
-  \end{tabular}
-  \end{center}
-  %
   Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
   @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
   is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
@@ -2186,17 +2212,19 @@
   %unwanted terms. Our guess is that such predicates result in rather
   %intricate formal reasoning.
 
-  Another representation technique for binding is higher-order abstract syntax
-  (HOAS), which for example is implemented in the Twelf system. This representation
+  Another technique for representing binding is higher-order abstract syntax
+  (HOAS). %, which for example is implemented in the Twelf system. 
+  This %%representation
   technique supports very elegantly many aspects of \emph{single} binding, and
   impressive work has been done that uses HOAS for mechanising the metatheory
   of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
   binders of SML are represented in this work. Judging from the submitted
   Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
-  binding constructs where the number of bound variables is not fixed. For
-  example in the second part of this challenge, @{text "Let"}s involve
+  binding constructs where the number of bound variables is not fixed. %For
+  example 
+  In the second part of this challenge, @{text "Let"}s involve
   patterns that bind multiple variables at once. In such situations, HOAS
-  representations have to resort to the iterated-single-binders-approach with
+  seems to have to resort to the iterated-single-binders-approach with
   all the unwanted consequences when reasoning about the resulting terms.
 
   %Two formalisations involving general binders have been 
@@ -2224,7 +2252,7 @@
   notion of $\alpha$-equivalence.  A definition for the notion of free variables
   is work in progress in Ott.
 
-  Although we were heavily inspired by the syntax in Ott,
+  Although we were heavily inspired by the syntax of Ott,
   its definition of $\alpha$-equivalence is unsuitable for our extension of
   Nominal Isabelle. First, it is far too complicated to be a basis for
   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
@@ -2294,7 +2322,7 @@
   has a more operational flavour and calculates a partial (renaming) map. 
   In this way, the definition can deal with vacuous binders. However, to our
   best knowledge, no concrete mathematical result concerning this
-  definition of $\alpha$-equivalence has been proved.    
+  definition of $\alpha$-equivalence has been proved.\\[-7mm]    
 *}
 
 section {* Conclusion *}
@@ -2321,7 +2349,7 @@
   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We
   hope to do better this time by using the function package that has recently
   been implemented in Isabelle/HOL and also by restricting function
-  definitions to equivariant functions (for such functions it is possible to
+  definitions to equivariant functions (for such functions we can
   provide more automation).
 
   %There are some restrictions we imposed in this paper that we would like to lift in
@@ -2349,8 +2377,8 @@
   %where instead of lists, we abstract lists of distinct elements.
   %Once we feel confident about such binding modes, our implementation 
   %can be easily extended to accommodate them.
-
-  \medskip
+  %
+  \smallskip
   \noindent
   {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for  
   %many discussions about Nominal Isabelle. 
@@ -2358,7 +2386,7 @@
   making the informal notes \cite{SewellBestiary} available to us and 
   also for patiently explaining some of the finer points of the work on the Ott-tool.
   %Stephanie Weirich suggested to separate the subgrammars
-  %of kinds and types in our Core-Haskell example.  
+  %of kinds and types in our Core-Haskell example. \\[-6mm] 
 
 *}
 




