
diff -r 47e2e91705f3 -r 774d631726ad Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Apr 27 19:01:22 2010 +0200
+++ b/Paper/Paper.thy	Tue Apr 27 19:51:35 2010 +0200
@@ -921,7 +921,7 @@
   ``\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:
+  we have binding clauses of the form:
 
   \begin{center}
   \begin{tabular}{ll}
@@ -931,18 +931,20 @@
   \end{center}
 
   \noindent
+  Similarly for the other binding modes.
   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.
+  \emph{one} binding clause of a term constructor. 
 
-  In addition we distinguish between \emph{shallow} and \emph{deep}
-  binders.  Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
+  For binders we distinguish between \emph{shallow} and \emph{deep} binders.
+  Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
   \isacommand{in}\; {\it labels'} (similar for the other two modes). The
-  restriction we impose on shallow binders is that the {\it labels} must either
-  refer to atom types or to finite sets or
-  lists of atom types. Two examples for the use of shallow binders are the
-  specification of lambda-terms, where a single name is bound, and 
-  type-schemes, where a finite set of names is bound:
+  restriction we impose on shallow binders is that in case of
+  \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
+  either refer to atom types or to sets of atom types; in case of
+  \isacommand{bind} we allow labels to atom types or lists of atom types. Two
+  examples for the use of shallow binders are the specification of
+  lambda-terms, where a single name is bound, and type-schemes, where a finite
+  set of names is bound:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -965,7 +967,8 @@
 
   \noindent
   Note that in this specification @{text "name"} refers to an atom type, and
-  @{text "fset"} to the type of finite sets.
+  @{text "fset"} to the type of finite sets. Shallow binders can occur in the 
+  binding part of several binding clauses. 
  
   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  
@@ -1005,16 +1008,6 @@
   coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
   us to treat binders of different atom type uniformly. 
 
-  As will shortly become clear, we cannot return an atom in a binding function
-  that is also bound in the corresponding term-constructor. That means in the
-  example above that the term-constructors @{text PVar} and @{text PTup} may not have a
-  binding clause.  In the version of Nominal Isabelle described here, we also adopted
-  the restriction from the Ott-tool that binding functions can only return:
-  the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
-  list containing an atom (case @{text PVar}), or unions of atom sets or appended atom
-  lists (case @{text PTup}). This restriction will simplify definitions and 
-  proofs later on.
-  
   The most drastic restriction we have to impose on deep binders is that 
   we cannot have ``overlapping'' deep binders. Consider for example the 
   term-constructors:
@@ -1047,11 +1040,22 @@
   \end{center}
 
   \noindent
-  since there is no overlap of binders.
+  since there is no overlap of binders. Unlike shallow binders, we restrict deep
+  binders to occur in only one binding clause. Therefore @{text "Bar\<^isub>2"} cannot 
+  be reformulated as
+
+  \begin{center}
+  \begin{tabular}{ll}
+  @{text "Bar\<^isub>3 p::pat t::trm"} &  
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p"}, 
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t"}\\
+  \end{tabular}
+  \end{center}
   
-  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
+  Note that in the @{text "Bar\<^isub>2"}, we wrote \isacommand{bind}~@{text
+  "bn(p)"}~\isacommand{in}~@{text "p.."}.  Whenever such a binding clause 
+  is present, where the argument in the binder also occurs in the body, 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:
   %
@@ -1079,8 +1083,23 @@
   inside the assignment. This difference has consequences for the free-variable 
   function and alpha-equivalence relation, which we are going to describe in the 
   rest of this section.
- 
-  In order to simplify some definitions, we shall assume specifications 
+
+  We also need to restrict the form of the binding functions. As will shortly
+  become clear, we cannot return an atom in a binding function that is also
+  bound in the corresponding term-constructor. That means in the example
+  \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
+  not have a binding clause (all arguments are used to define @{text "bn"}).
+  In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
+  may have binding clause involving the argument @{text t} (the only one that
+  is \emph{not} used in the definition of the binding function).  In the version of
+  Nominal Isabelle described here, we also adopted the restriction from the
+  Ott-tool that binding functions can only return: the empty set or empty list
+  (as in case @{text PNil}), a singleton set or singleton list containing an
+  atom (case @{text PVar}), or unions of atom sets or appended atom lists
+  (case @{text PTup}). This restriction will simplify some automatic proofs
+  later on.
+  
+  In order to simplify some later 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
@@ -1102,7 +1121,7 @@
 
   \noindent 
   The point of completion is that we can make definitions over the binding
-  clauses and be sure to capture all arguments of a term constructor. 
+  clauses and be sure to have captured 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
@@ -1142,7 +1161,7 @@
   we have that
   %
   \begin{equation}\label{ceqvt}
-  @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
+  @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
   \end{equation}
   
   The first non-trivial step we have to perform is the generation free-variable 
@@ -1187,28 +1206,32 @@
   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 @{text bcs}, the result of the @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be
+  clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^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}
+  \begin{equation}\label{deepbinderA}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
   \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}{\isacommand{bind}~@{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> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ 
-  & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ 
+  & \hspace{15mm}@{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\\
-  
+  \end{tabular}}
+  \end{equation}
+  \begin{equation}\label{deepbinderB}
+  \mbox{%
+  \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
   \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - set (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) - set (bn x)"}\\
      & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first 
-    clause applies for @{text x} being a non-recursive deep binder, the 
-    second for a recursive deep binder
+    clause applies for @{text x} being a non-recursive deep binder (that is 
+    @{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder
   \end{tabular}}
   \end{equation}
 
@@ -1217,8 +1240,8 @@
   binder, we have to add all atoms that are left unbound by the binding
   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
+  "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}. We again define a value
+  @{text v} which is exactly as in \eqref{deepbinderA}/\eqref{deepbinderB} for shallow and deep
   binding clauses, except for empty binding clauses are defined as follows: 
   %
   \begin{equation}\label{bnemptybinder}




