
diff -r ae860c95bf9f -r 69780ae147f5 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Oct 06 08:13:09 2010 +0100
+++ b/Paper/Paper.thy	Wed Oct 06 21:32:44 2010 +0100
@@ -124,9 +124,10 @@
   where @{text z} does not occur freely in the type.  In this paper we will
   give a general binding mechanism and associated notion of $\alpha$-equivalence
   that can be used to faithfully represent this kind of binding in Nominal
-  Isabelle.  The difficulty of finding the right notion for $\alpha$-equivalence
-  can be appreciated in this case by considering that the definition given by
-  Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
+  Isabelle.  
+  %The difficulty of finding the right notion for $\alpha$-equivalence
+  %can be appreciated in this case by considering that the definition given by
+  %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
 
   However, the notion of $\alpha$-equivalence that is preserved by vacuous
   binders is not always wanted. For example in terms like
@@ -240,7 +241,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 \cite{Berghofer99}.
+  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 
@@ -261,14 +262,14 @@
   to a variable bound somewhere else, are not excluded by Ott, but we have
   to).  
 
-  Our insistence on reasoning with $\alpha$-equated terms comes from the
-  wealth of experience we gained with the older version of Nominal Isabelle:
-  for non-trivial properties, reasoning with $\alpha$-equated terms is much
-  easier than reasoning with raw terms. The fundamental reason for this is
-  that the HOL-logic underlying Nominal Isabelle allows us to replace
-  ``equals-by-equals''. In contrast, replacing
-  ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
-  requires a lot of extra reasoning work.
+  %Our insistence on reasoning with $\alpha$-equated terms comes from the
+  %wealth of experience we gained with the older version of Nominal Isabelle:
+  %for non-trivial properties, reasoning with $\alpha$-equated terms is much
+  %easier than reasoning with raw terms. The fundamental reason for this is
+  %that the HOL-logic underlying Nominal Isabelle allows us to replace
+  %``equals-by-equals''. In contrast, replacing
+  %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
+  %requires a lot of extra reasoning work.
 
   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   terms is nearly always taken for granted, establishing it automatically in
@@ -349,9 +350,10 @@
   and lambda are lifted to the quotient level.)  This construction, of course,
   only works if $\alpha$-equivalence is indeed an equivalence relation, and the
   ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
-  For example, we will not be able to lift a bound-variable function. Although
-  this function can be defined for raw terms, it does not respect
-  $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
+  %For example, we will not be able to lift a bound-variable function. Although
+  %this function can be defined for raw terms, it does not respect
+  %$\alpha$-equivalence and therefore cannot be lifted. 
+  To sum up, every lifting
   of theorems to the quotient level needs proofs of some respectfulness
   properties (see \cite{Homeier05}). In the paper we show that we are able to
   automate these proofs and as a result can automatically establish a reasoning 
@@ -379,7 +381,7 @@
   The main improvement over Ott is that we introduce three binding modes
   (only one is present in Ott), provide definitions for $\alpha$-equivalence and 
   for free variables of our terms, and also derive a reasoning infrastructure
-  about our specifications inside Isabelle/HOL.
+  for our specifications inside Isabelle/HOL.
 
 
   %\begin{figure}
@@ -448,7 +450,7 @@
   the identity everywhere except on a finite number of atoms. There is a 
   two-place permutation operation written
   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-  where the generic type @{text "\<beta>"} stands for the type of the object 
+  where the generic type @{text "\<beta>"} is the type of the object 
   over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
@@ -504,9 +506,9 @@
   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
   @{text x} unchanged:
 
-  \begin{property}\label{swapfreshfresh}
+  \begin{myproperty}\label{swapfreshfresh}
   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
-  \end{property}
+  \end{myproperty}
 
   %While often the support of an object can be relatively easily 
   %described, for example for atoms, products, lists, function applications, 
@@ -546,11 +548,11 @@
   %The main point of @{text supports} is that we can establish the following 
   %two properties.
   %
-  %\begin{property}\label{supportsprop}
+  %\begin{myproperty}\label{supportsprop}
   %Given a set @{text "as"} of atoms.
   %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
   %{\it (ii)} @{thm supp_supports[no_vars]}.
-  %\end{property}
+  %\end{myproperty}
   %
   %Another important notion in the nominal logic work is \emph{equivariance}.
   %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
@@ -589,16 +591,16 @@
   proved too unwieldy for dealing with multiple binders. For such binders the 
   following generalisations turned out to be easier to use.
 
-  \begin{property}\label{supppermeq}
+  \begin{myproperty}\label{supppermeq}
   @{thm[mode=IfThen] supp_perm_eq[no_vars]}
-  \end{property}
+  \end{myproperty}
 
-  \begin{property}\label{avoiding}
+  \begin{myproperty}\label{avoiding}
   For a finite set @{text as} and a finitely supported @{text x} with
   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
   @{term "supp x \<sharp>* p"}.
-  \end{property}
+  \end{myproperty}
 
   \noindent
   The idea behind the second property is that given a finite set @{text as}
@@ -760,15 +762,15 @@
   representing $\alpha$-equivalence classes of pairs of type 
   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
   (in the third case). 
-  The elements in these types will be, respectively, written as:
-
-  \begin{center}
-  @{term "Abs_set as x"} \hspace{5mm} 
-  @{term "Abs_res as x"} \hspace{5mm}
-  @{term "Abs_lst as x"} 
-  \end{center}
-
-  \noindent
+  The elements in these types will be, respectively, written as
+  %
+  %\begin{center}
+  @{term "Abs_set as x"}, %\hspace{5mm} 
+  @{term "Abs_res as x"} and %\hspace{5mm}
+  @{term "Abs_lst as x"}, 
+  %\end{center}
+  %
+  %\noindent
   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
   call the types \emph{abstraction types} and their elements
   \emph{abstractions}. The important property we need to derive is the support of 
@@ -875,7 +877,8 @@
 
 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
+  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
@@ -975,7 +978,9 @@
   restriction is that a body can only occur in
   \emph{one} binding clause of a term constructor (this ensures that the bound
   atoms of a body cannot be free at the same time by specifying an
-  alternative binder for the same 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
@@ -1108,7 +1113,7 @@
   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 infrastructure for 
-  $\alpha$-equated terms, it can permit such specifications.)
+  $\alpha$-equated terms with deep binders, 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 
@@ -1181,10 +1186,11 @@
   where @{term ty} is the type used in the quotient construction for 
   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
 
-  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{Berghofer99} for an in-depth description of the datatype package
-  in Isabelle/HOL). We subsequently define each of the user-specified binding 
+  %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{Berghofer99} for an in-depth description of the datatype package
+  %in Isabelle/HOL). 
+  We subsequently define each of the user-specified binding 
   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
   raw datatype. We can also easily define permutation operations by 
   recursion so that for each term constructor @{text "C"} we have that
@@ -1674,15 +1680,16 @@
   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
   implication by applying the corresponding rule in our $\alpha$-equivalence
-  definition and by establishing the following auxiliary facts 
+  definition and by establishing the following auxiliary implications %facts 
   %
   \begin{equation}\label{fnresp}
   \mbox{%
-  \begin{tabular}{l}
-  @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\
-  @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\
-  @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
-  @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
+  \begin{tabular}{ll@ {\hspace{7mm}}ll}
+  \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
+  \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+
+  \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
+  \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
   \end{tabular}}
   \end{equation}
 
@@ -1710,11 +1717,11 @@
   are $\alpha$-equivalent. This gives us conditions when the corresponding
   $\alpha$-equated terms are \emph{equal}, namely
   %
-  \begin{center}
-  @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  \end{center}
-
-  \noindent
+  %\begin{center}
+  @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
+  %\end{center}
+  %
+  %\noindent
   We call these conditions as \emph{quasi-injectivity}. They correspond to
   the premises in our $\alpha$-equivalence relations.
 
@@ -1744,11 +1751,11 @@
   for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
   of the form
   %
-  \begin{equation}\label{weakinduct}
+  %\begin{equation}\label{weakinduct}
   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
-  \end{equation} 
-
-  \noindent
+  %\end{equation} 
+  %
+  %\noindent
   whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
   have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
   term constructor @{text "C"}$^\alpha$ a premise of the form
@@ -1766,36 +1773,38 @@
   equivariant, namely
   %
   \begin{center}
-  \begin{tabular}{rcl}
-  @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\
+  \begin{tabular}{rcl@ {\hspace{10mm}}rcl}
+  @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &
+  @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\
   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
-  @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}
   \end{tabular}
   \end{center}
-
+  %
   \noindent
-  These properties can be established using the induction principle
-  in \eqref{weakinduct}.
+  These properties can be established using the induction principle.
+  %%in \eqref{weakinduct}.
   Having these equivariant properties established, we can
-  show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
+  show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
+  the support of its arguments, that means 
 
   \begin{center}
-  @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
+  @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
   \end{center}
  
   \noindent
-  holds. This together with Property~\ref{supportsprop} allows us to prove
-  that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, 
-  namely @{text "finite (supp x)"}. This can be again shown by induction 
-  over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of 
+  holds. This allows us to prove by induction that
+  every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported. 
+  %This can be again shown by induction 
+  %over @{text "ty\<AL>"}$_{1..n}$. 
+  Lastly, we can show that the support of 
   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
   This fact is important in a nominal setting, but also provides evidence 
   that our notions of free-atoms and $\alpha$-equivalence are correct.
 
-  \begin{lemma} 
-  For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
-  @{text "supp x = fa_ty\<AL>\<^isub>i x"}.
-  \end{lemma}
+  \begin{theorem} 
+  For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
+  @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
+  \end{theorem}
 
   \begin{proof}
   The proof is by induction. In each case
@@ -1888,170 +1897,270 @@
 section {* Strong Induction Principles *}
 
 text {*
-  In the previous section we were able to provide induction principles that 
-  allow us to perform structural inductions over $\alpha$-equated terms. 
-  We call such induction principles \emph{weak}, because in case of the 
-  term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+  In the previous section we derived induction principles for $\alpha$-equated terms. 
+  We call such induction principles \emph{weak}, because for a 
+  term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
   the induction hypothesis requires us to establish the implications \eqref{weakprem}.
   The problem with these implications is that in general they are difficult to establish.
-  The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} 
-  (for example we cannot assume the variable convention for them).
+  The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}. 
+  %%(for example we cannot assume the variable convention for them).
 
   In \cite{UrbanTasson05} we introduced a method for automatically
   strengthening weak induction principles for terms containing single
   binders. These stronger induction principles allow the user to make additional
   assumptions about binders. 
-  These additional assumptions amount to a formal
-  version of the informal variable convention for binders. A natural question is
-  whether we can also strengthen the weak induction principles involving
-  the general binders presented here. We will indeed be able to so, but for this we need an 
-  additional notion for permuting deep binders. 
-
-  Given a binding function @{text "bn"} we define an auxiliary permutation 
-  operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
-  Assuming a clause of @{text bn} is given as 
+  %These additional assumptions amount to a formal
+  %version of the informal variable convention for binders. 
+  To sketch how this strengthening extends to the case of multiple binders, we use as
+  running example the term-constructors @{text "Lam"} and @{text "Let"}
+  from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
+  the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
+  where the additional parameter @{text c} controls
+  which freshness assumptions the binders should satisfy. For the two term constructors 
+  this means that the user has to establish in inductions the implications
   %
   \begin{center}
-  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
+  \begin{tabular}{l}
+  @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
+  @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+  \end{tabular}
   \end{center}
 
-  \noindent 
-  then we define 
+  In \cite{UrbanTasson05} we showed how the weaker induction principles imply
+  the stronger ones. This was done by some quite complicated, nevertheless automated,
+  induction proofs. In this paper we simplify this work by leveraging the automated proof
+  methods from the function package of Isabelle/HOL generates. 
+
+  The reasoning principle we employ here is well-founded induction. For this we have to discharge
+  two proof obligations: one is that we have
+  well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 
+  every induction step and the other is that we have covered all cases. 
+  As measures we use are the size functions 
+  @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 
+  all well-founded. It is straightforward to establish that these measures decrease 
+  in every induction step.
+  
+  What is left to show is that we covered all cases. To do so, we use 
+  a cases lemma derived for each type, which for the terms in \eqref{letpat} 
+  is of the form
+  %
+  \begin{equation}\label{weakcases}
+  \infer{@{text "P\<^bsub>trm\<^esub>"}}
+  {\begin{array}{l@ {\hspace{9mm}}l}
+  @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+  @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+  \end{array}}
+  \end{equation}
+  %
+  These cases lemmas have a premise for auch term-constructor.
+  The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
+  provided we can show that this property holds if we substitute for @{text "t"} all 
+  possible term-constructors. 
+  
+  The only remaining difficulty is that in order to derive the stronger induction
+  principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
+  in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 
+  \emph{all} @{text Let}-terms. 
+  What we need instead is a cases rule where we only have to consider terms that have 
+  binders being fresh w.r.t.~a context @{text "c"}, namely
+  %
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+  @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}
+  \end{tabular}
+  \end{center}
+  %
+  However, this can be relatively easily be derived from the implications in \eqref{weakcases} 
+  by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
+  that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with 
+  a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and 
+  @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
+  By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
+  and we are done with this case.
+
+  The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
+  The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+  because @{text p} might contain names that are bound (by @{text bn}) and that are 
+  free. To solve this problem we have to introduce a permutation functions that only
+  permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
+  by lifting. Assuming a
+  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
   %
   \begin{center}
   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
   \end{center}
-  
+  %
   \noindent
   with @{text "y\<^isub>i"} determined as follows:
   %
   \begin{center}
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
   \end{tabular}
   \end{center}
+  %
+  Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
+  @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
+  is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
+  these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+  completes the interesting cases in \eqref{letpat} for stregthening the induction
+  principles.
   
-  \noindent
-  Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
-  $\alpha$-equated terms. We can then prove the following two facts
+
 
-  \begin{lemma}\label{permutebn} 
-  Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
-  {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
-    @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
-  \end{lemma}
+  %A natural question is
+  %whether we can also strengthen the weak induction principles involving
+  %the general binders presented here. We will indeed be able to so, but for this we need an 
+  %additional notion for permuting deep binders. 
 
-  \begin{proof} 
-  By induction on @{text x}. The equations follow by simple unfolding 
-  of the definitions. 
-  \end{proof}
+  %Given a binding function @{text "bn"} we define an auxiliary permutation 
+  %operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
+  %Assuming a clause of @{text bn} is given as 
+  %
+  %\begin{center}
+  %@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
+  %\end{center}
 
-  \noindent
-  The first property states that a permutation applied to a binding function is
-  equivalent to first permuting the binders and then calculating the bound
-  atoms. The second amounts to the fact that permuting the binders has no 
-  effect on the free-atom function. The main point of this permutation
-  function, however, is that if we have a permutation that is fresh 
-  for the support of an object @{text x}, then we can use this permutation 
-  to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
-  @{text "Let"} term-constructor from the example shown 
-  in \eqref{letpat} this means for a permutation @{text "r"}
+  %\noindent 
+  %then we define 
+  %
+  %\begin{center}
+  %@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
+  %\end{center}
+  
+  %\noindent
+  %with @{text "y\<^isub>i"} determined as follows:
   %
-  \begin{equation}\label{renaming}
-  \begin{array}{l}
-  \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
-  \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
-  \end{array}
-  \end{equation}
+  %\begin{center}
+  %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+  %\end{tabular}
+  %\end{center}
+  
+  %\noindent
+  %Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
+  %$\alpha$-equated terms. We can then prove the following two facts
+
+  %\begin{lemma}\label{permutebn} 
+  %Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
+  %{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
+  %  @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
+  %\end{lemma}
 
-  \noindent
-  This fact will be crucial when establishing the strong induction principles below.
+  %\begin{proof} 
+  %By induction on @{text x}. The equations follow by simple unfolding 
+  %of the definitions. 
+  %\end{proof}
+
+  %\noindent
+  %The first property states that a permutation applied to a binding function is
+  %equivalent to first permuting the binders and then calculating the bound
+  %atoms. The second amounts to the fact that permuting the binders has no 
+  %effect on the free-atom function. The main point of this permutation
+  %function, however, is that if we have a permutation that is fresh 
+  %for the support of an object @{text x}, then we can use this permutation 
+  %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
+  %@{text "Let"} term-constructor from the example shown 
+  %in \eqref{letpat} this means for a permutation @{text "r"}
+  %%
+  %\begin{equation}\label{renaming}
+  %\begin{array}{l}
+  %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
+  %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+  %\end{array}
+  %\end{equation}
+
+  %\noindent
+  %This fact will be crucial when establishing the strong induction principles below.
 
  
-  In our running example about @{text "Let"}, the strong induction
-  principle means that instead 
-  of establishing the implication 
+  %In our running example about @{text "Let"}, the strong induction
+  %principle means that instead 
+  %of establishing the implication 
   %
-  \begin{center}
-  @{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
-  it is sufficient to establish the following implication
+  %\begin{center}
+  %@{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
+  %it is sufficient to establish the following implication
   %
-  \begin{equation}\label{strong}
-  \mbox{\begin{tabular}{l}
-  @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
-  \hspace{5mm}@{text "set (bn 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{equation}
-
-  \noindent 
-  While this implication contains an additional argument, namely @{text c}, and 
-  also additional universal quantifications, it is usually easier to establish.
-  The reason is that we have the freshness 
-  assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
-  chosen by the user as long as it has finite support.
-
-  Let us now show how we derive the strong induction principles from the
-  weak ones. In case of the @{text "Let"}-example we derive by the weak 
-  induction the following two properties
+  %\begin{equation}\label{strong}
+  %\mbox{\begin{tabular}{l}
+  %@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+  %\hspace{5mm}@{text "set (bn 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{equation}
+  %
+  %\noindent 
+  %While this implication contains an additional argument, namely @{text c}, and 
+  %also additional universal quantifications, it is usually easier to establish.
+  %The reason is that we have the freshness 
+  %assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
+  %chosen by the user as long as it has finite support.
+  %
+  %Let us now show how we derive the strong induction principles from the
+  %weak ones. In case of the @{text "Let"}-example we derive by the weak 
+  %induction the following two properties
+  %
+  %\begin{equation}\label{hyps}
+  %@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
+  %@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+  %\end{equation} 
   %
-  \begin{equation}\label{hyps}
-  @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
-  @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
-  \end{equation} 
-
-  \noindent
-  For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
-  assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
-  By Property~\ref{avoiding} we
-  obtain a permutation @{text "r"} such that 
+  %\noindent
+  %For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
+  %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
+  %By Property~\ref{avoiding} we
+  %obtain a permutation @{text "r"} such that 
   %
-  \begin{equation}\label{rprops}
-  @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
-  @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
-  \end{equation}
-
-  \noindent
-  hold. The latter fact and \eqref{renaming} give us
+  %\begin{equation}\label{rprops}
+  %@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
+  %@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
+  %\end{equation}
+  %
+  %\noindent
+  %hold. The latter fact and \eqref{renaming} give us
+  %%
+  %\begin{center}
+  %\begin{tabular}{l}
+  %@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
+  %\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+  %\end{tabular}
+  %\end{center}
   %
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-  \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-  establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
-  To do so, we will use the implication \eqref{strong} of the strong induction
-  principle, which requires us to discharge
-  the following four proof obligations:
+  %\noindent
+  %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
+  %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
+  %To do so, we will use the implication \eqref{strong} of the strong induction
+  %principle, which requires us to discharge
+  %the following four proof obligations:
+  %%
+  %\begin{center}
+  %\begin{tabular}{rl}
+  %{\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+  %{\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+  %{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+  %{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
+  %\end{tabular}
+  %\end{center}
   %
-  \begin{center}
-  \begin{tabular}{rl}
-  {\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-  {\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-  {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-  {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
-  others from the induction hypotheses in \eqref{hyps} (in the fourth case
-  we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
-
-  Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
-  we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
-  This completes the proof showing that the weak induction principles imply 
-  the strong induction principles. 
+  %\noindent
+  %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
+  %others from the induction hypotheses in \eqref{hyps} (in the fourth case
+  %we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
+  %
+  %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
+  %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
+  %This completes the proof showing that the weak induction principles imply 
+  %the strong induction principles. 
 *}
 
 
@@ -2073,9 +2182,9 @@
   datatypes.  However, in both approaches it seems difficult to achieve our
   fine-grained control over the ``semantics'' of bindings (i.e.~whether the
   order of binders should matter, or vacuous binders should be taken into
-  account). To do so, one would require additional predicates that filter out
-  unwanted terms. Our guess is that such predicates result in rather
-  intricate formal reasoning.
+  account). %To do so, one would require additional predicates that filter out
+  %unwanted terms. Our guess is that such predicates result in rather
+  %intricate formal reasoning.
 
   Another representation technique for binding is higher-order abstract syntax
   (HOAS), which for example is implemented in the Twelf system. This representation
@@ -2158,9 +2267,10 @@
   %and therefore need the extra generality to be able to distinguish between 
   %both specifications.
   Because of how we set up our definitions, we also had to impose some 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
-  programming language research, for example Core-Haskell. 
+  (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
+  %programming language research, for example Core-Haskell. 
 
   Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
   representing terms with general binders inside OCaml. This language is
@@ -2175,6 +2285,7 @@
   Still, this definition is rather different from ours and he only proves that
   it defines an equivalence relation. A complete
   reasoning infrastructure is well beyond the purposes of his language. 
+  Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.
   
   In a slightly different domain (programming with dependent types), the 
   paper \cite{Altenkirch10} presents a calculus with a notion of 




