diff -r 8f142ae324e2 -r 46f753eeb0b8 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Jul 13 23:39:39 2010 +0100
+++ b/Paper/Paper.thy	Wed Jul 14 21:30:52 2010 +0100
@@ -37,6 +37,21 @@
   Cons ("_::_" [78,77] 73) and
   supp_gen ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
+
+consts alpha_trm ::'a
+consts fa_trm :: 'a
+consts alpha_trm2 ::'a
+consts fa_trm2 :: 'a
+consts ast :: 'a
+consts ast' :: 'a
+notation (latex output) 
+  alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+  fa_trm ("fa\<^bsub>trm\<^esub>") and
+  alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
+  fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
+  ast ("'(as, t')") and
+  ast' ("'(as', t\<PRIME> ')")
+
 (*>*)
 
 
@@ -923,7 +938,7 @@
   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 the
   cardinality does) and the last is for sets of binders (with vacuous binders
-  preserving $\alpha$-equivalence). As indicated, the ``\isacommand{in}-part'' of a binding
+  preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
   clause will be called \emph{bodies}; the
   ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
   Ott, we allow multiple labels in binders and bodies. For example we allow
@@ -1088,8 +1103,8 @@
   \noindent
   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"}.
-  (Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit 
-  such specifications.)
+  (Since the Ott-tool does not derive a reasoning infrastructure for 
+  $\alpha$-equated terms, it can permit such specifications.)
   
   We also need to restrict the form of the binding functions in order 
   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
@@ -1100,7 +1115,7 @@
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
   may have a binding clause involving the argument @{text t} (the only one that
   is \emph{not} used in the definition of the binding function). This restriction
-  is sufficient for defining the binding function over $\alpha$-equated terms.
+  is sufficient for having the binding function over $\alpha$-equated terms.
 
   In the version of
   Nominal Isabelle described here, we also adopted the restriction from the
@@ -1453,7 +1468,8 @@
   involving multiple binders. As above, we first build the tuples @{text "D"} and
   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
   compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 
-  For $\approx_{\,\textit{set}}$ we also need
+  For $\approx_{\,\textit{set}}$ (respectively $\approx_{\,\textit{list}}$ and 
+  $\approx_{\,\textit{res}}$)  we also need
   a compound free-atom function for the bodies defined as
   %
   \begin{center}
@@ -1479,12 +1495,12 @@
 
   \noindent
   This premise accounts for $\alpha$-equivalence of the bodies of the binding
-  clause. Similarly for the other binding modes.
+  clause. 
   However, in case the binders have non-recursive deep binders, this premise
   is not enough:
   we also have to ``propagate'' $\alpha$-equivalence inside the structure of
   these binders. An example is @{text "Let"} where we have to make sure the
-  right-hand sides of assignments are $\alpha$-equivalent. For this we use the
+  right-hand sides of assignments are $\alpha$-equivalent. For this we use 
   relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
   Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
   %
@@ -1493,15 +1509,17 @@
   \end{center}
 
   \noindent
+  The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
+  and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}. 
   All premises for @{text "bc\<^isub>i"} are then given by
   %
   \begin{center}
-  @{text "prems(bc\<^isub>i) \<equiv> P  \<and>  l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1  \<and> ... \<and>  l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
+  @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}
   \end{center} 
 
   \noindent 
-  where the auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ 
-  are defined as follows: assuming a @{text bn}-clause is of the form
+  The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ 
+  in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
   %
   \begin{center}
   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
@@ -1509,7 +1527,7 @@
 
   \noindent
   where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
-  then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+  then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
   %
   \begin{center}
   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
@@ -1537,26 +1555,8 @@
   that the premises of empty binding clauses are a special case of the clauses for 
   non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
   for the existentially quantified permutation).
-*}
-(*<*)
-consts alpha_ty ::'a
-consts alpha_trm ::'a
-consts fa_trm :: 'a
-consts alpha_trm2 ::'a
-consts fa_trm2 :: 'a
-consts ast :: 'a
-consts ast' :: 'a
-notation (latex output) 
-  alpha_ty ("\<approx>ty") and
-  alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
-  fa_trm ("fa\<^bsub>trm\<^esub>") and
-  alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
-  fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
-  ast ("'(as, t')") and
-  ast' ("'(as', t\<PRIME> ')")
-(*>*)
-text {*
-  Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
+
+  Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$ with the following clauses:
 
@@ -1564,14 +1564,14 @@
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
   {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
-  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
+  \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
   \end{tabular}
   \end{center}
 
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+  \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
   {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
   \end{tabular}
@@ -1579,7 +1579,7 @@
 
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+  \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
   {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
   \end{tabular}
@@ -1588,8 +1588,8 @@
   \noindent
   Note the difference between  $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of 
-  the components in an assignment that are \emph{not} bound. Therefore we have
-  a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 
+  the components in an assignment that are \emph{not} bound. This is needed in the 
+  in the clause for @{text "Let"} (which is has
   a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 
   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 
   because there everything from the assignment is under the binder. 
@@ -1602,7 +1602,7 @@
   introducing the reasoning infrastructure for the $\alpha$-equated types the
   user originally specified. We sketch in this section the facts we need for establishing
   this reasoning infrastructure. First we have to show that the
-  $\alpha$-equivalence relations defined in the previous section are indeed
+  $\alpha$-equivalence relations defined in the previous section are 
   equivalence relations.
 
   \begin{lemma}\label{equiv} 
@@ -1620,8 +1620,8 @@
 
   \noindent 
   We can feed this lemma into our quotient package and obtain new types @{text
-  "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain 
-  definitions for the term-constructors @{text
+  "ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$. 
+  We also obtain definitions for the term-constructors @{text
   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
   "C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
   "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
@@ -1652,7 +1652,7 @@
   are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
   @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
-  
+  %
   \begin{center}
   @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
   \end{center}  
@@ -1676,7 +1676,7 @@
   In fact we can from now on lift facts from the raw level to the $\alpha$-equated level
   as long as they contain raw term-constructors only. The 
   induction principles derived by the datatype package in Isabelle/HOL for the types @{text
-  "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+  "ty"}$_{1..n}$ fall into this category. So we can also add to our infrastructure
   induction principles that establish
 
   \begin{center}