diff -r 9f55d7927e5b -r 9a894c42e80e Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Apr 02 03:23:25 2010 +0200
+++ b/Paper/Paper.thy	Fri Apr 02 05:09:47 2010 +0200
@@ -869,29 +869,28 @@
 
 text {*
   Our choice of syntax for specifications is influenced by the existing
-  datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool
-  \cite{ott-jfp}. For us a specification of a term-calculus 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
-  roughly as follows:
+  datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
+  Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
+  collection of (possibly mutual recursive) type declarations, say @{text
+  "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
+  binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
+  syntax in Nominal Isabelle for such specifications is roughly 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} @{text ty}$^\alpha_1 = \ldots$\\
-  \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\
+  \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
+  \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
   $\ldots$\\ 
-  \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ 
+  \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 
   \end{tabular}}
   \end{cases}$\\
   binding \mbox{function part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
-  \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\
+  \isacommand{with} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
   \isacommand{where}\\
   $\ldots$\\
   \end{tabular}}
@@ -901,9 +900,9 @@
 
   \noindent
   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 
-  term-constructors, each of which comes with a list of labelled 
+  term-constructors, each of which come with a list of labelled 
   types that stand for the types of the arguments of the term-constructor.
-  For example a term-constructor @{text "C\<^sup>\<alpha>"} might have
+  For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
 
   \begin{center}
   @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 
@@ -913,8 +912,9 @@
   whereby some of the @{text ty}$'_{1..l}$ (or their components) might be 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} of @{text "C\<^sup>\<alpha>"}. The types of such recursive 
+  In this case we will call the corresponding argument a
+  \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. 
+  %The types of such recursive 
   %arguments need to satisfy a  ``positivity''
   %restriction, which ensures that the type has a set-theoretic semantics 
   %\cite{Berghofer99}.  
@@ -936,8 +936,8 @@
   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). The ``\isacommand{in}-part'' of a binding
-  clause will be called the \emph{body}; the
-  ``\isacommand{bind}-part'' will be the \emph{binder}.
+  clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
+  be called the \emph{binder}.
 
   In addition we distinguish between \emph{shallow} and \emph{deep}
   binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
@@ -1154,7 +1154,7 @@
   we need to define 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"}
+  @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
   \end{center}
 
   \noindent
@@ -1163,7 +1163,7 @@
   @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
   %
   \begin{center}
-  @{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+  @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
   \end{center}
 
   \noindent
@@ -1252,7 +1252,7 @@
    $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
     recursive call @{text "bn x\<^isub>i"}\medskip\\
   $\bullet$ & @{term "{}"} provided @{text "rhs"} contains
-    @{term "x\<^isub>i"} without a recursive call.
+    @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
   \end{tabular}
   \end{center}
 
@@ -1296,13 +1296,13 @@
   that has also been pointed out in \cite{ott-jfp}. We can also see that
   %
   \begin{equation}\label{bnprop}
-  @{text "fv_ty x = bn x \<union> fv_bn x"}.
+  @{text "fv_ty x  =  bn x \<union> fv_bn x"}.
   \end{equation}
 
   \noindent
-  holds for any @{text "bn"}-function of type @{text "ty"}.
+  holds for any @{text "bn"}-function defined for the type @{text "ty"}.
 
-  Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+  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. 
   Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
@@ -1327,7 +1327,7 @@
   \noindent
   For what follows, let us assume 
   @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.
-  The task now is to specify what the premises of these clauses are. For this we
+  The task is to specify what the premises of these clauses are. For this we
   consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will 
   be easier to analyse these pairs according to  ``clusters'' of the binding clauses. 
   Therefore we distinguish the following cases:
@@ -1347,7 +1347,7 @@
 (*>*)
 text {*
   \begin{itemize}
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the 
+  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder with type @{text "ty"}. We assume the 
   \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
   \isacommand{bind\_set} we generate the premise
   \begin{center}
@@ -1357,8 +1357,8 @@
   For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for
   binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead. 
 
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
-  and @{text bn} being the auxiliary binding function. We assume 
+  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}
+  and @{text bn} is corresponding the binding function. We assume 
   @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 
   For the binding mode \isacommand{bind\_set} we generate two premises
   %
@@ -1371,8 +1371,8 @@
   where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
   @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
 
-  \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}
-  and with @{text bn} being the auxiliary binding function. We assume 
+  \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}
+  and  @{text bn} is the corresponding binding function. We assume 
   @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 
   For the binding mode \isacommand{bind\_set} we generate the premise
   %
@@ -1386,9 +1386,9 @@
   \end{itemize}
 
   \noindent
-  From these definition it is clear why we can only support one binding mode per binder
+  From this definition it is clear why we can only support one binding mode per binder
   and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
-  and $\approx_{\textit{res}}$. It is also clear why we had to impose the restriction
+  and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction
   of excluding overlapping binders, as these would need to be translated into separate
   abstractions.
 
@@ -1397,10 +1397,10 @@
   neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided
   the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are 
   recursive arguments of the term-constructor. If they are non-recursive arguments,
-  then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
+  then we generate the premise @{text "x\<^isub>i = y\<^isub>i"}.
 
 
-  The definitions of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions 
+  The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions 
   are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
   and need to generate appropriate premises. We generate first premises according to the first three
   rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 
@@ -1421,7 +1421,7 @@
   \end{tabular}
   \end{center}
 
-  Again lets take a look at an example for these definitions. For \eqref{letrecs}
+  Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
   we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$, with the clauses as follows:
 
@@ -1456,15 +1456,15 @@
   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 
   a non-recursive binder). The reason is that the terms inside an assignment are not meant 
-  to be under the binder. Such a premise is not needed in @{text "Let_rec"}, 
+  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. 
 *}
 
 section {* Establishing the Reasoning Infrastructure *}
 
 text {*
-  Having made all crucial definitions for raw terms, we can start introducing
-  the resoning infrastructure for the types the user specified. For this we first
+  Having made all necessary definitions for raw terms, we can start introducing
+  the reasoning infrastructure for the types the user specified. For this we first
   have to show that the alpha-equivalence relations defined in the previous
   section are indeed equivalence relations. 
 
@@ -1502,28 +1502,64 @@
   \end{equation}
   
   \noindent
-  By definition of alpha-equivalence on raw terms we can show that
+  By definition of alpha-equivalence we can show that
   for the raw term-constructors
-
-  \begin{center}
-  @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}$\;\not\approx@{text ty}\;$@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
-  \end{center}
+  %
+  \begin{equation}\label{distinctraw}
+  @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;\not\approx@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
+  \end{equation}
 
   \noindent
   In order to generate \eqref{distinctalpha} from this fact, the quotient
   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 
   are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}.
+  This means, given @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
+  @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, we have to show that
   
-  Given a term-constructor @{text C} of type @{text ty} and argument
-  types @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, respectfullness means that
-  %
+  \begin{center}
+  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+  \end{center}  
+
+  \noindent
+  under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
+  and  @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by 
+  analysing the definition of @{text "\<approx>ty"}. For this to succed we have to establish an
+  auxiliary fact: given a binding function @{text bn} defined for the type @{text ty}
+  we have that
+
   \begin{center}
-  aa
+  @{text "x \<approx>ty y"} implies @{text "x \<approx>bn y"}
   \end{center}
+
+  \noindent
+  This can be established by induction on the definition of @{text "\<approx>ty"}. 
    
+  Having established respectfullness for every raw term-constructor, the 
+  quotient package will automaticaly deduce \eqref{distinctalpha} from \eqref{distinctraw}.
+  In fact we can lift any fact from the raw level to the alpha-equated level that
+  apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The 
+  induction principles derived by the datatype package of Isabelle/HOL for @{text
+  "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
+  induction principles that establish
 
-  \mbox{}\bigskip\bigskip
-  then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
+  \begin{center}
+  @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
+  \end{center} 
+
+  \noindent
+  for every @{text "y\<^isub>i"} under the assumption we specified the types
+  @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of these induction principles look
+  as follows
+
+  \begin{center}
+  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 
+  \end{center}
+
+  \noindent
+  where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 
+
+
+To lift
   the raw definitions to the quotient type, we need to prove that they
   \emph{respect} the relation. We follow the definition of respectfullness given
   by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
@@ -1700,11 +1736,21 @@
   Instead of establishing the implication 
 
   \begin{center}
-  a
+  @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
   \end{center}
 
   \noindent
-  from the weak induction principle. 
+  from the weak induction principle, we will show that it is sufficient
+  to establish
+  
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+  \hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\
+  \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+  \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
+  \end{tabular}
+  \end{center}
 
 
   With the help of @{text "\<bullet>bn"} functions defined in the previous section