
diff -r 36aeb97fabb0 -r e90f6a26d74b Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jul 01 14:18:36 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 02 01:54:19 2010 +0100
@@ -946,13 +946,14 @@
   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
   %show this later with an example.
   
-  There are also some restrictions we need to impose on binding clauses: the
+  There are also some restrictions we need to impose on binding clauses. The
   main idea behind these restrictions is that we obtain a sensible notion of
   $\alpha$-equivalence where it is ensured that within a given scope a 
-  variable occurence cannot be bound and free at the same time.  First, a body can only occur in
+  variable occurence cannot be both bound and free at the same time.  The first
+  restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor (this ensures that the bound
   variables of a body cannot be free at the same time by specifying an
-  alternative binder for the body). For binders we distinguish between
+  alternative binder for the same body). For binders we distinguish between
   \emph{shallow} and \emph{deep} binders.  Shallow binders are just
   labels. The restriction we need to impose on them is that in case of
   \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
@@ -1040,7 +1041,7 @@
   \end{center}
 
   \noindent
-  where the argument of the deep binder is also in the body. We call such
+  where the argument of the deep binder also occurs in the body. We call such
   binders \emph{recursive}.  To see the purpose of such recursive binders,
   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
   specification:
@@ -1070,8 +1071,8 @@
   function and $\alpha$-equivalence relation, which we are going to define later.
   
   To make sure that variables bound by deep binders cannot be free at the
-  same time, we have to impose some further restrictions. First,
-  we cannot have more than one binding function for one binder. So we exclude:
+  same time, we cannot have more than one binding function for one binder. 
+  Consequently we exclude specifications such as
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@@ -1084,12 +1085,12 @@
   \end{center}
 
   \noindent
-  Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
-  out different atoms to become bound in @{text "p"}.
+  Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
+  out different atoms to become bound, respectively be free, in @{text "p"}.
   
-
-  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
+  We also need to restrict the form of the binding functions in order 
+  to ensure the @{text "bn"}-functions can be lifted defined for $\alpha$-equated 
+  terms. As a result 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"}).
@@ -1168,22 +1169,18 @@
   non-empty and the types in the constructors only occur in positive 
   position (see \cite{Berghofer99} for an indepth description of the datatype package
   in Isabelle/HOL). We then define the user-specified binding 
-  functions, called @{term "bn"}, by recursion over the corresponding 
+  functions @{term "bn"} by recursion over the corresponding 
   raw datatype. We can also easily define permutation operations by 
-  recursion so that for each term constructor @{text "C"} with the 
-  argument types @{text "ty"}$_{1..n}$ we have that
+  recursion so that for each term constructor @{text "C"} with  
+  arguments @{text "z"}$_{1..n}$ we have that
   %
   \begin{equation}\label{ceqvt}
   @{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}
 
-  \noindent
-  where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$.
-  
   The first non-trivial step we have to perform is the generation of
-  free-variable functions from the specifications. Given a raw term, these 
-  functions return sets of atoms. Assuming a nominal datatype
-  specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$, 
+  free-variable functions from the specifications. For the 
+  \emph{raw} types @{text "ty"}$_{1..n}$ of a specification,
   we define the free-variable functions
   %
   \begin{equation}\label{fvars}
@@ -1206,120 +1203,113 @@
 
   While the idea behind these free-variable functions is clear (they just
   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 "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
-  the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for 
-  each binding clause. Given a binding clause @{text bc} is of the form
+  binding mechanisms their definitions are somewhat involved. The functions
+  are defined by recursion defining a clause for each term-constructor.  Given
+  the term-constructor @{text "C"} of type @{text ty} and some associated
+  binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
+  "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
+  "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"}. Given the binding clause @{text
+  bc\<^isub>i} is of the form
   %
   \begin{equation}
-  \mbox{\isacommand{bind} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+  \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
   \end{equation}
 
   \noindent
-  where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders 
-  @{text b}$_{1..p}$
+  in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
+  and the binders @{text b}$_{1..p}$
   either refer to labels of atom types (in case of shallow binders) or to binding 
   functions taking a single label as argument (in case of deep binders). Assuming the
-  free variables of the bodies is the set @{text "D"}, the bound variables of the binders 
-  is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"}
-  then the free variables of the binding clause @{text bc} is
+  set @{text "D"} stands for the free atoms in the bodies, @{text B} for the 
+  binding atoms in the binders and @{text "B'"} for the free atoms in 
+  non-recursive deep binders,
+  then the free atoms of the binding clause @{text bc\<^isub>i} are given by
   %
   \begin{center}
-  @{text "fv(bc) = (D - B) \<union> B'"}
+  @{text "fv(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
   \end{center}
 
   \noindent
-  Formally the set @{text D} is the union of the free variables for the bodies
+  The set @{text D} is defined as
   %
   \begin{center}
-  @{text "D = fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+  @{text "D \<equiv> fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
   \end{center} 
 
   \noindent
-  whereby the free variable functions @{text "fv_ty\<^isub>i"} are the ones in \eqref{fvars}
-  provided the @{text "d\<^isub>i"} refers to one of the types @{text "ty"}$_{1..n}$; 
-  otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
-
-
-if @{text "d\<^isub>i"} is a label
-  for an atomic type we use the following auxiliary free variable functions
-
+  whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion 
+  (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the types 
+  @{text "ty"}$_{1..n}$; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  In order to define the set @{text B} we use the following auxiliary bn-functions
+  for atom types to which shallow binders have to refer
+  %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\
-  @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
-  @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+  @{text "bn_atom a"} & @{text "="} & @{text "{atom a}"}\\
+  @{text "bn_atom_set as"} & @{text "="} & @{text "atoms as"}\\
+  @{text "bn_atom_list as"} & @{text "="} & @{text "atoms (set as)"}
   \end{tabular}
   \end{center}
 
   \noindent 
   In these functions, @{text "atoms"}, like @{text "atom"}, 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}"}. Otherwise
-  
+  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}"}. 
+  The set @{text B} is then defined as
+  %
+  \begin{center}
+  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
+  \end{center} 
 
-
-the values, @{text v}, calculated by the rules for each bining clause:
+  \noindent 
+  The set @{text "B'"} collects all free atoms in non-recursive deep
+  binders. Lets assume these binders in @{text "bc\<^isub>i"} are
   %
-  \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> .. \<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> .. \<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 (that is 
-    @{text "x \<noteq> y"}$_{1..m}$), the second for a recursive deep binder
-  \end{tabular}}
-  \end{equation}
+  \begin{center}
+  @{text "bn\<^isub>1 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
+  \end{center}
+
+  \noindent
+  with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
+  "d"}$_{1..q}$. The set @{text "B'"} is then defined as
+  %
+  \begin{center}
+  @{text "B' \<equiv> fv_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fv_bn\<^isub>r a\<^isub>r"}
+  \end{center} 
 
   \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 define the function @{text "fv_bn"}. Assume
-  for the constructor @{text "C"} the binding function is of the form @{text
-  "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: 
+  Similarly for the other binding modes. 
+
+  Note that for non-recursive deep binders, we have to add all atoms that are left 
+  unbound by the binding function @{text "bn"}. This is the purpose of the functions 
+  @{text "fv_bn"}, also defined by recursion. Assume the user has specified 
+  a @{text bn}-clause of the form
   %
-  \begin{equation}\label{bnemptybinder}
-  \mbox{%
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{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}}
-  \end{equation}
+  \begin{center}
+  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>n) = rhs"}
+  \end{center}
 
   \noindent
-  The reason why we only have to treat the empty binding clauses specially in
-  the definition of @{text "fv_bn"} is that binding functions can only use arguments
-  that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
-  be lifted to $\alpha$-equated terms.
+  where the @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$. For each of
+  the arguments we calculate the free atoms as follows
+  %
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  $\bullet$ & @{term "fv_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\
+  $\bullet$ & @{term "fv_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
+  with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
+  $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
+  but without a recursive call
+  \end{tabular}
+  \end{center}
 
-
+  \noindent
+  For defining @{text "fv_bn (C z\<^isub>1 \<dots> z\<^isub>n)"}, we just union up all these values.
+ 
   To see how these definitions work in practice, let us reconsider the term-constructors 
   @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 
-  For this specification we need to define three free-variable functions, namely
-  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
+  For them we consider three free-variable functions, namely
+  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}:
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1363,6 +1353,8 @@
   \noindent
   holds for any @{text "bn"}-function defined for the type @{text "ty"}.
 
+  TBD below.
+
   Next we define $\alpha$-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 
   we also need to  define auxiliary $\alpha$-equivalence relations for the binding functions. 
@@ -1382,7 +1374,8 @@
   conclusions of the form  
   %
   \begin{center}
-  @{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"} 
+  \mbox{\infer{@{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"}}
+  {@{text "prems(bc\<^isub>1)"} & @{text "\<dots>"} & @{text "prems(bc\<^isub>p)"}}} 
   \end{center}
 
   \noindent
@@ -2060,24 +2053,6 @@
   \end{tabular}
   \end{center}
 
-  To see this, consider the following equations 
-
-  \begin{center}
-  \begin{tabular}{c}
-  @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\
-  @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\
-  \end{tabular}
-  \end{center}
-  
-  \noindent
-  The interesting point is that they do not imply
-
-   \begin{center}
-  \begin{tabular}{c}
-  @{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\
-  \end{tabular}
-  \end{center}
-
   Because of how we set up our definitions, we had to impose restrictions,
   like a single binding function for a deep binder, that are not present in Ott. Our
   expectation is that we can still cover many interesting term-calculi from




