
diff -r 1dbc4f33549c -r 5b0bdd64956e Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Mar 22 16:22:28 2010 +0100
+++ b/Paper/Paper.thy	Mon Mar 22 18:19:13 2010 +0100
@@ -385,36 +385,34 @@
 section {* General Binders *}
 
 text {*
-  In order to keep our work manageable we give need to give definitions  
-  and perform proofs inside Isabelle wherever possible, as opposed to write
-  custom ML-code that generates them  for each 
-  instance of a term-calculus. To this end we will first consider pairs
+  In Nominal Isabelle the user is expected to write down a specification of a
+  term-calculus and a reasoning infrastructure is then automatically derived
+  from this specifcation (remember that Nominal Isabelle is a definitional
+  extension of Isabelle/HOL and cannot introduce new axioms).
+
 
-  \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. These pairs
-  are intended to represent the abstraction or binding of the set $as$ 
-  in the body $x$ (similarly to type-schemes given in \eqref{tysch}). 
+  In order to keep our work manageable, we will wherever possible state
+  definitions and perform proofs inside Isabelle, as opposed to write custom
+  ML-code that generates them for each instance of a term-calculus. To that
+  end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
+  These pairs are intended to represent the abstraction, or binding, of the set $as$ 
+  in the body $x$.
 
-  The first question we have to answer is when we should consider pairs such as
-  $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
+  The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
+  alpha-equivalent? (At the moment we are interested in
   the notion of alpha-equivalence that is \emph{not} preserved by adding 
-  vacuous binders.) To answer this we identify four conditions: {\it i)} given 
-  a free-variable function of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
+  vacuous binders.) To answer this, we identify four conditions: {\it i)} given 
+  a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 
   need to have the same set of free variables; moreover there must be a permutation,
-  $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, 
-  but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, 
+  $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, 
+  but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, 
   say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes 
-  the abstracted sets $as$ and $bs$ equal (since at the moment we do not want 
-  that the sets $as$ and $bs$ differ on vacuous binders). These requirements can 
-  be stated formally as follows
+  the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can 
+  be stated formally as follows:
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
              & @{text "fv(x) - as = fv(y) - bs"}\\
   \wedge     & @{text "fv(x) - as #* p"}\\
   \wedge     & @{text "(p \<bullet> x) R y"}\\
@@ -423,20 +421,23 @@
   \end{equation}
 
   \noindent
-  Alpha equivalence between such pairs is then the relation with the additional 
-  existential quantification over $p$. Note that this relation is additionally 
-  dependent on the free-variable function $\fv$ and the relation $R$. The reason 
-  for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms
-  and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and
-  we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.
+  Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where 
+  we existentially quantify over this $p$. 
+  Also note that the relation is dependent on a free-variable function $\fv$ and a relation 
+  $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both 
+  ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by 
+  equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support 
+  of $x$ and $y$. To have these parameters means, however, we can derive properties about 
+  them generically.
 
   The definition in \eqref{alphaset} does not make any distinction between the
-  order of abstracted variables. If we do want this then we can define alpha-equivalence 
-  for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by
+  order of abstracted variables. If we want this, then we can define alpha-equivalence 
+  for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 
+  as follows
   %
   \begin{equation}\label{alphalist}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
              & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
   \wedge     & @{text "fv(x) - (set as) #* p"}\\
   \wedge     & @{text "(p \<bullet> x) R y"}\\
@@ -448,34 +449,65 @@
   where $set$ is just the function that coerces a list of atoms into a set of atoms.
 
   If we do not want to make any difference between the order of binders and
-  allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}
-  and define
+  also allow vacuous binders, then we keep sets of binders, but drop the fourth 
+  condition in \eqref{alphaset}:
   %
-  \begin{equation}\label{alphaset}
+  \begin{equation}\label{alphares}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
              & @{text "fv(x) - as = fv(y) - bs"}\\
   \wedge     & @{text "fv(x) - as #* p"}\\
   \wedge     & @{text "(p \<bullet> x) R y"}\\
   \end{array}
   \end{equation}
 
-  To get a feeling how these definitions pan out in practise consider the case of 
-  abstracting names over types (like in type-schemes). For this we set $R$ to be 
-  the equality and for $\fv(T)$ we define
+  \begin{exmple}\rm
+  It might be useful to consider some examples for how these definitions pan out in practise.
+  For this consider the case of abstracting a set of variables over types (as in type-schemes). 
+  We set $R$ to be the equality and for $\fv(T)$ we define
 
   \begin{center}
   $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
   \end{center}
 
   \noindent
-  Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily 
-  checked that @{text "({x,y}, x \<rightarrow> y)"} and
-  @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to
-  be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance 
-  $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 
-  makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}
-  unchanged.
+  Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily 
+  checked that @{text "({x, y}, x \<rightarrow> y)"} and
+  @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
+  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then 
+  $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 
+  makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the 
+  type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
+   $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
+  However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
+  the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
+  \end{exmple}
+
+  \noindent
+  Let $\star$ range over $\{set, res, list\}$. We prove next under which 
+  conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence 
+  relations and equivariant:
+
+  \begin{lemma}
+  {\it i)} Given the fact that $x\;R\;x$ holds, then 
+  $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
+  that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
+  $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
+  $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
+  that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies 
+  @{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
+  and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
+  $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
+  @{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
+  @{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
+  $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
+  $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star 
+  (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
+  \end{lemma}
+  
+  \begin{proof}
+  All properties are by unfolding the definitions and simple calculations. 
+  \end{proof}
 *}
 
 section {* Alpha-Equivalence and Free Variables *}




