
diff -r 13d905f1999a -r 3b89de6150ed Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 17:56:39 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 18:45:50 2010 +0200
@@ -7,6 +7,8 @@
   fv :: "'a \<Rightarrow> 'b"
   abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
   alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
+  alpha2 :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f" 
 
 definition
  "equal \<equiv> (op =)" 
@@ -22,6 +24,8 @@
   alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
+  abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
+  alpha2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{\#{}list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   fv ("fv'(_')" [100] 100) and
   equal ("=") and
   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
@@ -1040,7 +1044,6 @@
   @{text "Foo' x::name p::pat t::trm"} & 
      \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} 
-  
   \end{tabular}
   \end{center}
 
@@ -1882,7 +1885,7 @@
   variables at once. This extension can deal with term-calculi such as
   Core-Haskell. For such calculi, we can also derive strong induction
   principles that have the usual variable already built in. At the moment we
-  can do so only with some manual help, but future work will automate them
+  can do so only with manual help, but future work will automate them
   completely.  The code underlying this extension will become part of the
   Isabelle distribution, but for the moment it can be downloaded from the
   Mercurial repository linked at
@@ -1890,26 +1893,76 @@
   {http://isabelle.in.tum.de/nominal/download}.
 
   We have left out a discussion about how functions can be defined
-  over alpha-equated terms. In earlier work \cite{UrbanBerghofer06}
-  this turned out to be a thorny issue in the old Nominal Isabelle.
+  over alpha-equated terms with general binders. In earlier work \cite{UrbanBerghofer06}
+  this turned out to be a thorny issue for  Nominal Isabelle.
   We hope to do better this time by using the function package that
-  has recently been implemented in Isabelle/HOL and by restricting
+  has recently been implemented in Isabelle/HOL and also by restricting
   function definitions to equivariant functions (for such functions
   it is possible to provide more automation).
 
-  There are some restrictions we imposed, like absence of nested type
+  There are some restrictions we imposed, like the absence of nested type
   definitions that allow one to specify the function kinds as 
   @{text "TFun string (ty list)"} instead of the unfolded version
-  @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}, that 
-  can be easily lifted. They essentially amount only to a more
-  clever implementation. More interesting is lifting our restriction
-  about overlapping deep binders.
+  @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}; such
+  restrictions can be easily lifted. They essentially amount to a more
+  clever implementation than we have at the moment. More interesting is 
+  lifting our restriction about overlapping deep binders. Given our
+  current setup, we cannot deal with specifications such as
+ 
+  \begin{center}
+  \begin{tabular}{ll}
+  @{text "Foo r::pat s::pat t::trm"} & 
+     \isacommand{bind} @{text "bn(r)"} \isacommand{in} @{text t},\;
+     \isacommand{bind} @{text "bn(s)"} \isacommand{in} @{text t}
+  \end{tabular}
+  \end{center}
   
-  Complication when the single scopedness restriction is lifted (two 
-  overlapping permutations)
+  \noindent
+  where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap.. 
+  We would need to implement such bindings with alpha-equivalences like
+
+  \begin{center}
+  @{term "\<exists>p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \<and> abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"}
+  \end{center}
+
+  \noindent
+  or
+
+  \begin{center}
+  @{term "\<exists>p q. abs_set2 (bn r\<^isub>1 \<union> bn s\<^isub>1, t\<^isub>1) (p + q)  (bn r\<^isub>2 \<union> bn s\<^isub>2, t\<^isub>2)"}
+  \end{center}
 
-  Future work: distinct list abstraction
+  \noindent
+  Both versions require two permutations (for each binding). But unfortunately the 
+  first version cannot not work since it leaves unbound atoms that should be 
+  bound by the respective other binder. This problem is avoided in the second
+  version, but at the expense that the two permutations can interfere with each 
+  other. We have not yet been able to find a way to avoid such interferences. 
+  On the other hand, such bindings can be made sense of \cite{SewellBestiary}.
+  This clearly needs more investigation.
 
+  We have also not yet played with other binding modes. For example we can
+  imagine that the here is a mode \isacommand{bind\_\#list} with the associated
+  alpha-equivalence definition
+  %
+  \begin{center}
+  $\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
+  \multicolumn{2}{l}{@{term "alpha2 (as, x) R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+             & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
+  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\
+  \wedge     & @{text "(p \<bullet> x) R y"}\\
+  \wedge     & @{term "(p \<bullet> as) = bs"}\\
+  \wedge     & @{term "distinct as"} 
+  \end{array}$
+  \end{center}
+
+  \noindent
+  In this definition we added the requirement that all bound variables 
+  in a list are distinct. We can imagine applications for such a notion
+  of binding, but have not explored them yet. Our implementation can 
+  easily extended to accommodate further binding modes.
+
+  \medskip
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
@@ -1920,21 +1973,6 @@
   of kinds and types in our Core-Haskell example.  
 *}
 
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
-  Restrictions
-
-  \begin{itemize}
-  \item non-emptiness
-  \item positive datatype definitions
-  \item finitely supported abstractions
-  \item respectfulness of the bn-functions\bigskip
-  \item binders can only have a ``single scope''
-  \item in particular "bind a in b, bind b in c" is not allowed.
-  \item all bindings must have the same mode
-  \end{itemize}
-*}
-
 (*<*)
 end
 (*>*)




