
diff -r 6df6468f3c05 -r 028705c98304 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Apr 26 20:19:42 2010 +0200
+++ b/Paper/Paper.thy	Tue Apr 27 12:23:06 2010 +0200
@@ -706,34 +706,6 @@
   It can also relatively easily be shown that all tree notions of alpha-equivalence
   coincide, if we only abstract a single atom. 
 
-  % looks too ugly
-  %\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}
-
-
   In the rest of this section we are going to introduce three abstraction 
   types. For this we define 
   %
@@ -742,8 +714,8 @@
   \end{equation}
   
   \noindent
-  (similarly for $\approx_{\textit{abs\_list}}$ 
-  and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence 
+  (similarly for $\approx_{\textit{abs\_res}}$ 
+  and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence 
   relations and equivariant.
 
   \begin{lemma}\label{alphaeq} 
@@ -866,11 +838,12 @@
   Theorem~\ref{suppabs}. 
 
   The method of first considering abstractions of the
-  form @{term "Abs as x"} etc is motivated by the fact that properties about them
-  can be conveninetly established at the Isabelle/HOL level.  It would be
-  difficult to write custom ML-code that derives automatically such properties 
+  form @{term "Abs as x"} etc is motivated by the fact that 
+  we can conveniently establish  at the Isabelle/HOL level
+  properties about them.  It would be
+  laborious to write custom ML-code that derives automatically such properties 
   for every term-constructor that binds some atoms. Also the generality of
-  the definitions for alpha-equivalence will help us in definitions in the next section.
+  the definitions for alpha-equivalence will help us in the next section.
 *}
 
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -945,9 +918,22 @@
   cardinality does) and the last is for sets of binders (with vacuous binders
   preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
   clause will be called \emph{bodies} (there can be more than one); the 
-  ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur 
-  in \emph{one} binding clause. A binder, in contrast, may occur in several binding 
-  clauses, but cannot occur as a body.
+  ``\isacommand{bind}-part'' will be called \emph{binders}. 
+
+  In contrast to Ott, we allow multiple labels in binders and bodies. For example
+  we permit binding clauses as follows:
+
+  \begin{center}
+  \begin{tabular}{ll}
+  @{text "Foo x::name y::name t::lam s::lam"} &  
+      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  There are a few restrictions we need to impose: First, a body can only occur in
+  \emph{one} binding clause of a term constructor. A binder, in contrast, may
+  occur in several binding clauses, but cannot occur as a body.
 
   In addition we distinguish between \emph{shallow} and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
@@ -978,17 +964,9 @@
   \end{center}
 
   \noindent
-  Note that in this specification \emph{name} refers to an atom type.
-  Shallow binders may also ``share'' several bodies, for instance @{text t} 
-  and @{text s} in the following term-constructor
-
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "Foo x::name y::name t::lam s::lam"} &  
-      \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  
-  \end{tabular}
-  \end{center}
-
+  Note that in this specification @{text "name"} refers to an atom type, and
+  @{text "fset"} to the type of finite sets.
+ 
   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
   the atoms in one argument of the term-constructor, which can be bound in  
   other arguments and also in the same argument (we will
@@ -1055,7 +1033,7 @@
   and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way
   to determine whether the binder came from the binding function @{text
   "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. The reason why
-  we must exclude such specifications is that they cannot be represent by
+  we must exclude such specifications is that they cannot be represented by
   the general binders described in Section \ref{sec:binders}. However
   the following two term-constructors are allowed
 
@@ -1071,10 +1049,11 @@
   \noindent
   since there is no overlap of binders.
   
-  Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}.
-  Whenever such a binding clause is present, we will call the corresponding binder \emph{recursive}.
-  To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
-  in the following specification:
+  Note that in the last example we wrote \isacommand{bind}~@{text
+  "bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause is
+  present, we will call the corresponding binder \emph{recursive}.  To see the
+  purpose of such recursive binders, compare ``plain'' @{text "Let"}s and
+  @{text "Let_rec"}s in the following specification:
   %
   \begin{equation}\label{letrecs}
   \mbox{%
@@ -1101,12 +1080,12 @@
   function and alpha-equivalence relation, which we are going to describe in the 
   rest of this section.
  
-  In order to simplify matters below, we shall assume specifications 
+  In order to simplify some definitions, we shall assume specifications 
   of term-calculi are \emph{completed}. By this we mean that  
   for every argument of a term-constructor that is \emph{not} 
   already part of a binding clause, we add implicitly a special \emph{empty} binding
-  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "\<dots>"}. In case
-  of the lambda-calculus, the comletion is as follows:
+  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case
+  of the lambda-calculus, the completion produces
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
@@ -1123,17 +1102,15 @@
 
   \noindent 
   The point of completion is that we can make definitions over the binding
-  clauses, which defined purely over arguments, turned out to be unwieldy.
+  clauses and be sure to capture all arguments of a term constructor. 
 
   Having dealt with all syntax matters, the problem now is how we can turn
   specifications into actual type definitions in Isabelle/HOL and then
   establish a reasoning infrastructure for them. As
-  Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just 
+  Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
   re-arranging the arguments of
-  term-constructors so that binders and their bodies are next to each other, and
-  then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and
-  @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate
-  representatation. Therefore we will first
+  term-constructors so that binders and their bodies are next to each other will 
+  result in inadequate representations. Therefore we will first
   extract datatype definitions from the specification and then define 
   expicitly an alpha-equivalence relation over them.
 
@@ -1181,12 +1158,12 @@
   \end{center}
 
   \noindent 
-  Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces 
+  Like the coercion function @{text atom}, @{text "atoms"} coerces 
   the set of atoms to a set of the generic atom type.
   It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
 
-  Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
-  we define now free-variable functions
+  Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the
+  free-variable functions
 
   \begin{center}
   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
@@ -1210,24 +1187,25 @@
   collect all atoms that are not bound), because of our rather complicated
   binding mechanisms their definitions are somewhat involved.  Given a
   term-constructor @{text "C"} of type @{text ty} and some associated binding
-  clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
-  the union of the values, @{text v}, calculated below for each binding
-  clause. 
-
+  clauses @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+  the union of the values, @{text v}, calculated by the rules for empty, shallow and
+  deep binding clauses: 
+  %
   \begin{equation}\label{deepbinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
-  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
   $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
-  \multicolumn{2}{@ {}l}{Shallow binders of the form 
-  \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"} 
-     provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\
-  \multicolumn{2}{@ {}l}{Deep binders of the form 
-  \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
+  
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1..x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ 
+  & \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ 
+  & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the 
+  binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
+  
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
      & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first 
     clause applies for @{text x} being a non-recursive deep binder, the 
     second for a recursive deep binder
@@ -1237,22 +1215,20 @@
   \noindent
   Similarly for the other binding modes. Note that in a non-recursive deep
   binder, we have to add all atoms that are left unbound by the binding
-  function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume
-  for the constructor @{text "C"} the binding function equation is of the form @{text
+  function @{text "bn"}. For this we define the function @{text "fv_bn"}. Assume
+  for the constructor @{text "C"} the binding function is of the form @{text
   "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value
   @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep
-  binders. We only modify the clause for empty binding clauses as follows:
-
-
+  binding clauses, except for empty binding clauses are defined as follows: 
+  %
   \begin{equation}\label{bnemptybinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{@ {}l}{Empty binding clauses of the form 
-  \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
-  $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"}
-  and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\
-  $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in  @{text "rhs"}
-  with a recursive call @{text "bn\<^isub>i y"}\\
+  \multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
+  $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
+  and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\
+  $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in  @{text "rhs"}
+  with a recursive call @{text "bn y"}\\
   $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in  @{text "rhs"},
   but without a recursive call\\
   \end{tabular}}
@@ -1559,7 +1535,7 @@
   alpha-equivalence relations are equivariant, which we already established 
   in Lemma~\ref{equiv}. As a result we can establish the equations
   
-  \begin{equation}\label{ceqvt}
+  \begin{equation}\label{calphaeqvt}
   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{equation}
 




