
diff -r a3ef7fba983f -r 0c3c66f5c0e7 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 15:09:26 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 16:59:00 2010 +0200
@@ -222,7 +222,7 @@
   where no clause for variables is given. Arguably, such specifications make
   some sense in the context of Coq's type theory (which Ott supports), but not
   at all in a HOL-based environment where every datatype must have a non-empty
-  set-theoretic model.
+  set-theoretic model \cite{Berghofer99}.
 
   Another reason is that we establish the reasoning infrastructure
   for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning 
@@ -844,21 +844,20 @@
   \end{equation}
 
   \noindent
-  since for finite sets, @{text "S"}, we have 
-  @{thm (concl) supp_finite_atom_set[no_vars]}).
+  since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
 
-  Finally taking \eqref{halfone} and \eqref{halftwo} provides us with a proof
-  of Theorem~\ref{suppabs}. The point of these general lemmas about abstractions is that we 
-  can define and prove properties about them conveniently on the Isabelle/HOL level,
-  but also use them in what follows next when we deal with binding in specifications 
-  of term-calculi. 
+  Finally taking \eqref{halfone} and \eqref{halftwo} together provides us with a proof
+  of Theorem~\ref{suppabs}. The point of these properties of abstractions is that we 
+  can define and prove them aconveniently on the Isabelle/HOL level,
+  but also use them in what follows next when we deal with binding in 
+  specifications of term-calculi. 
 *}
 
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 
 text {*
   Our choice of syntax for specifications of term-calculi is influenced by the existing
-  datatype package of Isabelle/HOL and by the syntax of the Ott-tool
+  datatype package of Isabelle/HOL \cite{Berghofer99} 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
@@ -902,8 +901,8 @@
   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 their scope of
+  the types are optional. Their purpose is to be used in the (possibly empty) list of
+  \emph{binding clauses}, which indicate the binders and their scope
   in a term-constructor.  They come in three \emph{modes}:
 
 
@@ -920,7 +919,7 @@
   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}
+  In addition we distinguish between \emph{shallow} and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
   \isacommand{in}\; {\it label'} (similar for the other two modes). The
   restriction we impose on shallow binders is that the {\it label} must either
@@ -932,18 +931,18 @@
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
-  \isacommand{nominal\_datatype} {\it lam} =\\
-  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
-  \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
-  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
-  \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \isacommand{nominal\_datatype} @{text lam} =\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
+  \hspace{5mm}$\mid$~@{text "App lam lam"}\\
+  \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
+  \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype} {\it ty} =\\
-  \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
-  \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
-  \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
-  \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
+  \isacommand{nominal\_datatype}~@{text ty} =\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
+  \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
+  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
+  \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -955,9 +954,9 @@
 
   \begin{center}
   \begin{tabular}{ll}
-  \it {\rm Foo} x::name y::name t::lam & \it 
-                              \isacommand{bind}\;x\;\isacommand{in}\;t,\;
-                              \isacommand{bind}\;y\;\isacommand{in}\;t  
+  @{text "Foo x::name y::name t::lam"} &  
+                              \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+                              \isacommand{bind} @{text y} \isacommand{in} @{text t}  
   \end{tabular}
   \end{center}
 
@@ -979,27 +978,27 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \isacommand{nominal\_datatype} {\it trm} =\\
-  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
-  \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\
-  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} 
-     \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
-  \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$} 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} $\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)$\\ 
+  \isacommand{nominal\_datatype} @{text trm} =\\
+  \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
+  \hspace{5mm}$\mid$~@{term "App trm trm"}\\
+  \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 
+     \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+  \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 
+     \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
+  \isacommand{and} @{text pat} =\\
+  \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+  \hspace{5mm}$\mid$~@{text "PVar name"}\\
+  \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
+  \isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\
+  \isacommand{where}~@{text "bn(PNil) = []"}\\
+  \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
+  \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\ 
   \end{tabular}
   \end{center}
   
   \noindent
   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"}
+  bound in the argument @{text "t"}. Note that in 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. 
 
@@ -1011,16 +1010,19 @@
   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 
+  
+  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} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;
-                              \isacommand{bind}\;bn(q)\;\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 
+  @{text "Foo p::pat q::pat t::trm"} & 
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
+     \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\
+  @{text "Foo' x::name p::pat t::trm"} & 
+     \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} 
   
   \end{tabular}
   \end{center}
@@ -1037,10 +1039,12 @@
 
   \begin{center}
   \begin{tabular}{ll}
-  \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}$'$p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;
-                                      \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\
+  @{text "Bar p::pat t::trm s::trm"} & 
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\
+  @{text "Bar' 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}
 
@@ -1049,7 +1053,7 @@
   
   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
   Whenever 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:
+  To see the purpose for this, compare ``plain'' Lets and Let\_recs:
 
   \begin{center}
   \begin{tabular}{@ {}l@ {}}
@@ -1083,36 +1087,40 @@
   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-equivalence relation over them.
+  extract datatype definitions from the specification and then define 
+  independently an alpha-equivalence 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
+  given by user. In our implementation we just use an affix @{text "_raw"}.
+  For the purpose of the paper we just use superscripts to indicate a
+  notion defined over alpha-equivalence classes and leave out the superscript
+  for the corresponding notion on the ``raw'' level. So for example:
 
   \begin{center}
-  @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}
+  @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
   \end{center}
   
   \noindent
   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 explanation of the datatype package
+  position (see \cite{Berghofer99} for an indepth explanation 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
+  term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} we have that
 
   \begin{center}
-  @{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)"}
+  @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
   \end{center}
   
-  \noindent
-  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.
+  % TODO: we did not define permutation types
+  %\noindent
+  %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"}s.
 
   The first non-trivial step we have to perform is the generation free-variable 
   functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
@@ -1136,8 +1144,8 @@
   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 
+  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with 
+  some  binding clauses, the function @{text "fv_ty (C 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 
@@ -1184,7 +1192,7 @@
   @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
   omission of the arguments present in @{text "bn"}.
 
-  For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
+  For a binding function clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
   we define @{text "fv_bn"} to be the union of the values calculated
   for @{text "x\<^isub>j"} as follows:
 
@@ -1219,8 +1227,8 @@
   @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
   \end{center}
 
-  Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
-  of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there
+  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
   exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
   the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
@@ -1254,8 +1262,8 @@
   for their respective types, the difference is that they ommit checking the arguments that
   are bound. We assumed that there are no bindings in the type on which the binding function
   is defined so, there are no permutations involved. For a binding function clause 
-  @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
-  @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
+  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\




