# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1278697802 -3600
# Node ID eaf5209669ded639102f206cb06bac03cd3d0281
# Parent  09b476c20fe19e8ea9e484bd8704d55c132c8656
before examples

diff -r 09b476c20fe1 -r eaf5209669de Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jul 09 10:00:37 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 09 18:50:02 2010 +0100
@@ -1275,7 +1275,8 @@
   \end{center}
 
   \noindent
-  with none of the @{text "l"}$_{1..r}$ being among the bodies @{text
+  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
   %
   \begin{center}
@@ -1287,7 +1288,7 @@
 
   Note that for non-recursive deep binders, we have to add in \eqref{fadef}
   the set of atoms that are left unbound by the binding functions @{text
-  "bn"}$_{1..m}$. We use for the definition of
+  "bn"}$_{1..m}$. We used for the definition of
   this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
   recursion. Assume the user specified a @{text bn}-clause of the form
   %
@@ -1335,7 +1336,7 @@
   \end{center}
 
   \noindent
-  For these definitions, recall that @{text ANil} and @{text "ACons"} have no
+  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 by 
@@ -1351,7 +1352,7 @@
   "set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
   @{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. 
   Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the 
-  list of assignments, but instead returns the free atoms, that means in this 
+  list of assignments, but instead returns the free atoms, which means in this 
   example the free atoms in the argument @{text "t"}.  
 
   An interesting point in this
@@ -1449,7 +1450,7 @@
   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
   $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
   binding modes). This premise defines $\alpha$-equivalence of two abstractions
-  involving multiple binders. We first define as above the tuples @{text "D"} and
+  involving multiple binders. As above, we first build the tuples @{text "D"} and
   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
   compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 
   For $\approx_{\,\textit{set}}$ we also need
@@ -1472,13 +1473,15 @@
   Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   %
-  \begin{equation}\label{pprem}
+  \begin{center}
   \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
-  \end{equation}
+  \end{center}
 
   \noindent
   This premise accounts for $\alpha$-equivalence of the bodies of the binding
-  clause. However, in case the binders have non-recursive deep binders, then
+  clause. Similarly for the other binding modes.
+  However, in case the binders have non-recursive deep binders, this premise
+  is not enough:
   we also have to ``propagate'' $\alpha$-equivalence inside the structure of
   these binders. An example is @{text "Let"} where we have to make sure the
   right-hand sides of assignments are $\alpha$-equivalent. For this we use the
@@ -1490,17 +1493,15 @@
   \end{center}
 
   \noindent
-  The premises for @{text "bc\<^isub>i"} are then defined as
+  All premises for @{text "bc\<^isub>i"} are then given by
   %
   \begin{center}
   @{text "prems(bc\<^isub>i) \<equiv> P  \<and>  l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1  \<and> ... \<and>  l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
   \end{center} 
 
-  \noindent
-  where @{text "P"} is defined in \eqref{pprem}. 
- 
-  The $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ are defined as follows:
-  given a @{text bn}-clause of the form
+  \noindent 
+  where the auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ 
+  are defined as follows: assuming a @{text bn}-clause is of the form
   %
   \begin{center}
   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
@@ -1516,7 +1517,7 @@
   \end{center}
   
   \noindent
-  whereby the relations @{text "R"}$_{1..s}$ are given by 
+  In this clause the relations @{text "R"}$_{1..s}$ are given by 
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1535,19 +1536,27 @@
   This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
   that the premises of empty binding clauses are a special case of the clauses for 
   non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
-  as the permutation).
+  for the existentially quantified permutation).
 *}
-(*<*)consts alpha_ty ::'a
+(*<*)
+consts alpha_ty ::'a
 consts alpha_trm ::'a
 consts fa_trm :: 'a
 consts alpha_trm2 ::'a
 consts fa_trm2 :: 'a
+(*consts ast :: 'a
+consts ast' :: 'a*)
+(*
 notation (latex output) 
   alpha_ty ("\<approx>ty") and
   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
   fa_trm ("fa\<^bsub>trm\<^esub>") and
-  alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
-  fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")(*>*)
+  alpha_trm2 ("\<approx>\<^bsub>assn\<^esub>\<approx>\<^bsub>trm\<^esub>") and
+  fa_trm2 ("fa\<^bsub>assn\<^esub>fa\<^bsub>trm\<^esub>") and
+  ast ("'(as, t')") and
+  ast' ("'(as', t\<PRIME> ')")
+*)
+(*>*)
 text {*
   Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
@@ -1555,10 +1564,10 @@
 
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
-  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
+%  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+%  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+%  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+%  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
   \end{tabular}
   \end{center}