
diff -r d5b223b9c2bb -r a5501c9fad9b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 24 19:50:42 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 25 07:21:41 2010 +0100
@@ -528,30 +528,30 @@
 section {* Alpha-Equivalence and Free Variables *}
 
 text {*
-  Our specifications for term-calculi are heavily
-  inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
-  a collection of (possibly mutual recursive) type declarations, say
-  $ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an
-  associated collection of binding functions, say
-  $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle 
-  for such specifications is rougly as follows:
+  Our specifications for term-calculi are heavily inspired by the existing
+  datatype package of Isabelle/HOL and by the syntax of the Ott-tool
+  \cite{ott-jfp}. A specification is a collection of (possibly mutual
+  recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots, 
+  @{text ty}$^\alpha_n$, and an associated collection
+  of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
+  bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
+  rougly as follows:
   %
   \begin{equation}\label{scheme}
   \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\
-  \isacommand{and} $ty^\alpha_2 = \ldots$\\
+  \isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\
+  \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\
   $\ldots$\\ 
-  \isacommand{and} $ty^\alpha_n = \ldots$\\ 
+  \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ 
   \end{tabular}}
   \end{cases}$\\
   binding \mbox{function part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$
-  $\ldots$\\
+  \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\
   \isacommand{where}\\
   $\ldots$\\
   \end{tabular}}
@@ -560,22 +560,22 @@
   \end{equation}
 
   \noindent
-  Every type declaration $ty^\alpha_i$ consists of a collection of 
+  Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 
   term-constructors, each of which comes with a list of labelled 
   types that stand for the types of the arguments of the term-constructor.
-  For example a term-constructor $C^\alpha$ might have
+  For example a term-constructor @{text "C\<^sup>\<alpha>"} might have
 
   \begin{center}
-  $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ 
+  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 
   \end{center}
   
   \noindent
-  whereby some of the $ty'_k$ (or their components) are contained in the collection
-  of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the
+  whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection
+  of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the
   corresponding argument a \emph{recursive argument}.  The labels annotated on
   the types are optional and can be used in the (possibly empty) list of
-  \emph{binding clauses}.  These clauses indicate the binders and the scope of
-  the binders in a term-constructor.  They come in three \emph{modes}
+  \emph{binding clauses}.  These clauses indicate the binders and their scope of
+  in a term-constructor.  They come in three \emph{modes}:
 
 
   \begin{center}
@@ -588,17 +588,17 @@
 
   \noindent
   The first mode is for binding lists of atoms (the order of binders matters); the second is for sets
-  of binders (the order does not matter, but cardinality does) and the last is for  
+  of binders (the order does not matter, but the cardinality does) and the last is for  
   sets of binders (with vacuous binders preserving alpha-equivalence).
 
   In addition we distinguish between \emph{shallow} binders and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
-  \isacommand{in}\; {\it another\_label} (similar for the other two modes). The
+  \isacommand{in}\; {\it label'} (similar for the other two modes). The
   restriction we impose on shallow binders is that the {\it label} must either
   refer to a type that is an atom type or to a type that is a finite set or
-  list of an atom type. For example the specifications for lambda-terms, where
-  a single name is bound, and type-schemes, where a finite set of names is
-  bound, use shallow binders (the type \emph{name} is an atom type):
+  list of an atom type. Two examples for the use of shallow binders are the
+  specification of lambda-terms, where a single name is bound, and of
+  type-schemes, where a finite set of names is bound:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -620,12 +620,13 @@
   \end{center}
 
   \noindent
+  Note that in this specification \emph{name} refers to an atom type.
   If we have shallow binders that ``share'' a body, for instance $t$ in
-  the term-constructor Foo$_0$
+  the following term-constructor
 
   \begin{center}
   \begin{tabular}{ll}
-  \it {\rm Foo}$_0$ x::name y::name t::lam & \it 
+  \it {\rm Foo} x::name y::name t::lam & \it 
                               \isacommand{bind}\;x\;\isacommand{in}\;t,\;
                               \isacommand{bind}\;y\;\isacommand{in}\;t  
   \end{tabular}
@@ -633,19 +634,19 @@
 
   \noindent
   then we have to make sure the modes of the binders agree. We cannot
-  have in the first binding clause the mode \isacommand{bind} and in the second 
-  \isacommand{bind\_set}.
+  have, for instance, in the first binding clause the mode \isacommand{bind} 
+  and in the second \isacommand{bind\_set}.
 
   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
-  call such binders \emph{recursive}). 
+  call such binders \emph{recursive}, see below). 
   The binding functions are expected to return either a set of atoms
   (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
   (for \isacommand{bind}). They can be defined by primitive recursion over the
   corresponding type; the equations must be given in the binding function part of
   the scheme shown in \eqref{scheme}. For example for a calculus containing lets 
-  with tuple patterns, you might declare
+  with tuple patterns, you might specify
 
   \begin{center}
   \begin{tabular}{l}
@@ -657,52 +658,59 @@
   \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} 
      \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
   \isacommand{and} {\it pat} =\\
-  \hspace{5mm}\phantom{$\mid$} PNo\\
-  \hspace{5mm}$\mid$ PVr\;{\it name}\\
-  \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\ 
+  \hspace{5mm}\phantom{$\mid$} PNil\\
+  \hspace{5mm}$\mid$ PVar\;{\it name}\\
+  \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\ 
   \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
-  \isacommand{where} $bn(\textrm{PNil}) = []$\\
-  \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\
-  \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\ 
+  \isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\
+  \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\
+  \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\ 
   \end{tabular}
   \end{center}
   
   \noindent
-  In this specification the function $atom$ coerces a name into the generic
-  atom type of Nominal Isabelle. 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 also is bound in the term-constructor. In the present
-  version of Nominal Isabelle, we adopted the restriction the Ott-tool imposes
-  on the binding functions, namely a binding function can only return the
-  empty set (case PNil), a singleton set containing an atom (case PVar) or
-  unions of atom sets (case PPrd). Moreover, as with shallow binders, deep
-  binders with shared body need to have the same binding mode. Finally, 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:
+  In this specification the function @{text "bn"} determines which atoms of @{text  p} are
+  bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}
+  coerces a name into the generic atom type of Nominal Isabelle. 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 PVar and PTup must not have a
+  binding clause.  In the present version of Nominal Isabelle, we also adopted
+  the restriction from the Ott-tool that binding functions can only return:
+  the empty set or empty list (as in case PNil), a singleton set or singleton
+  list containing an atom (case PVar), or unions of atom sets or appended atom
+  lists (case PTup). This restriction will simplify proofs later on.
+  The 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:
 
   \begin{center}
   \begin{tabular}{ll}
-  \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+  \it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
                               \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\
-  \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
+  \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;
                               \isacommand{bind}\;bn(p)\;\isacommand{in}\;t 
   
   \end{tabular}
   \end{center}
 
   \noindent
-  In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms 
-  from $q$ in $t$. As a result we have no way to determine whether the binder came from the
-  binding function in $p$ or $q$. Similarly in the second case:
-  the binder $bn(p)$ overlaps with the shallow binder $x$. We must exclude such specifiactions, 
-  as we will not be able to represent them using the general binders described in 
-  Section \ref{sec:binders}. However the following two term-constructors are allowed:
+  In the first case we bind all atoms from the pattern @{text p} in @{text t}
+  and also all atoms from @{text q} in @{text t}. As a result 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. There the binder
+  @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
+  we must exclude such specifiactions is that they cannot be represent by
+  the general binders described in Section \ref{sec:binders}. However
+  the following two term-constructors are allowed
 
   \begin{center}
   \begin{tabular}{ll}
-  \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
+  \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
                                             \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\
-  \it {\rm Bar}$_2$ p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
+  \it {\rm Bar}$'$p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
                                       \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
   \end{tabular}
   \end{center}
@@ -710,15 +718,19 @@
   \noindent
   since there is no overlap of binders.
   
-  Let us come back one more time to the specification of simultaneous lets. 
-  A specification for them looks as follows:
+  Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
+  Whenver such a binding clause is present, we will call the binder \emph{recursive}.
+  To see the purpose for this, consider ``plain'' Lets and Let\_recs:
 
   \begin{center}
-  \begin{tabular}{l}
+  \begin{tabular}{@ {}l@ {}}
   \isacommand{nominal\_datatype} {\it trm} =\\
   \hspace{5mm}\phantom{$\mid$}\ldots\\
   \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} 
      \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
+  \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm} 
+     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
+         \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
   \isacommand{and} {\it assn} =\\
   \hspace{5mm}\phantom{$\mid$} ANil\\
   \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
@@ -729,65 +741,77 @@
   \end{center}
 
   \noindent
-  The intention with this specification is to bind all variables 
-  from the assignments inside the body @{text t}. However one might
-  like to consider the variant where the variables are not just
-  bound in @{term t}, but also in the assignments themselves. In
-  this case we need to specify
+  The difference is that with Let we only want to bind the atoms @{text
+  "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms
+  inside the assignment. This requires recursive binders and also has
+  consequences for the free variable function and alpha-equivalence relation,
+  which we are going to explain in the rest of this section.
+ 
+  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. Because of the problem
+  Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+  term-constructors so that binders and their bodies are next to each other, and
+  then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
+  @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
+  extract datatype definitions from the specification and then define an
+  alpha-equiavlence relation over them.
+
+
+  The datatype definition can be obtained by just stripping off the 
+  binding clauses and the labels on the types. We also have to invent
+  new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
+  given by user. In our implementation we just use an affix like
 
   \begin{center}
-  \begin{tabular}{l}
-  Let\_rec\;{\it a::assn}\; {\it t::trm} 
-     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
-         \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
-  \end{tabular}
+  @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
   \end{center}
   
   \noindent
-  where we bind also in @{text a} all the atoms @{text bn} returns. In this
-  case we will say the binder is a \emph{recursive binder}.
-
-  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. Because of the problem Pottier and Cheney pointed out, we cannot 
-  in general re-arrange arguments of term-constructors so that binders and 
-  their bodies next to each other, an then use the type constructors 
-  @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section 
-  \ref{sec:binders}. Therefore
-  we will first extract datatype definitions from the specification and
-  then define an alpha-equiavlence relation over them.
-
-  The datatype definition can be obtained by just stripping of the 
-  binding clauses and the labels on the types. We also have to invent
-  new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$
-  given by user. We just use an affix like
+  The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
+  non-empty and the types in the constructors only occur in positive 
+  position (see \cite{} for an indepth explanataion of the datatype package
+  in Isabelle/HOL). We then define the user-specified binding 
+  functions by primitive recursion over the raw datatypes. We can also
+  easily define a permutation operation by primitive recursion so that for each
+  term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
 
   \begin{center}
-  $ty^\alpha \mapsto ty\_raw  \qquad C^\alpha \mapsto C\_raw$
+  @{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{center}
   
   \noindent
-  The datatype definition can be made, provided the usual conditions hold: 
-  the datatypes must be non-empty and they must only occur in positive 
-  position (see \cite{}). We then consider the user-specified binding 
-  functions and define them by primitive recursion over the raw datatypes.
+  From this definition we can easily show that the raw datatypes are 
+  all permutation types (Def ??) by a simple structural induction over
+  the @{text "ty_raw"}s.
+
+  The first non-trivial step we have to perform is the generatation free-variable 
+  functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
+  we need to define the free-variable functions
+
+  \begin{center}
+  @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+  \end{center}
+
+  \noindent
+  and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define 
+  the free-variable functions
 
-  The first non-trivial step we have to generate free-variable 
-  functions from the specifications. The basic idea is to collect
-  all atoms that are not bound, but because of the rather complicated
-  binding mechanisms the details are somewhat involved.
-  There are two kinds of free-variable functions: one corresponds to types,
-  written $\fv\_ty$, and the other corresponds to binding functions,
-  written $\fv\_bn$. They have to be defined at the same time, since there can
-  be dependencies between them. 
+  \begin{center}
+  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+  \end{center}
 
-  Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with 
-  some  binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be 
-  the union of the values generated for each argument, say $x_i$ with type $ty_i$. 
-  By the binding clause we know whether the argument $x_i$ is a shallow or deep
-  binder and in the latter case also whether it is a recursive or non-recursive  
-  of a binder. In these cases we return as value: 
+  \noindent
+  The basic idea behind these free-variable functions is to collect all atoms
+  that are not bound in a term constructor, but because of the rather
+  complicated binding mechanisms the details are somewhat involved. 
+
+  Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with 
+  some  binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be 
+  the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}. 
+  From the binding clause of this term constructor, we can determine whether the 
+  argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also 
+  whether it is a recursive or non-recursive of a binder. In these cases the value is: 
 
   \begin{center}
   \begin{tabular}{cp{7cm}}
@@ -798,12 +822,13 @@
   \end{center}
 
   \noindent
-  The binding clause will also give us whether the argument @{term "x\<^isub>i"} is
-  a body of one or more abstractions. There are two cases: either the 
+  In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
+  one or more abstractions. There are two cases: either the 
   corresponding binders are all shallow or there is a single deep binder. 
   In the former case we build the union of all shallow binders; in the 
   later case we just take set or list of atoms the specified binding
-  function returns. Below use @{text "bnds"} to stand for them. 
+  function returns. Let @{text "bnds"} be an abbreviation of the bound
+  atoms. Then the value is given by:  
  
   \begin{center}
   \begin{tabular}{cp{7cm}}
@@ -816,13 +841,37 @@
   \end{center}
 
   \noindent
-  If the argument is neither a binder, nor a body, then it is defined as
-  the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms
+  If the argument is neither a binder, nor a body of an abstraction, then the 
+  value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms
   are abstracted.
 
+  TODO
+
+  Given a clause of a binding function of the form 
+
+  \begin{center}
+  @{text "bn_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}
+  \end{center}
+
+  \noindent
+  then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the
+  union of the values calculated for the @{text "x\<^isub>j"} as follows:
+
+  \begin{center}
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+  $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 
+    with the recursive call @{text "bn_ty x\<^isub>j"}\\
+  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+  $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
+  $\bullet$ & @{term "{}"} otherwise 
+  \end{tabular}
+  \end{center}
+
 *}
 
-
+section {* The Lifting of Definitions and Properties *} 
 
 text {*
   Restrictions




