
diff -r fb201e383f1b -r da575186d492 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2766 +0,0 @@
-(*<*)
-theory Paper
-imports "../Nominal/Nominal2" 
-        "~~/src/HOL/Library/LaTeXsugar"
-begin
-
-consts
-  fv :: "'a \<Rightarrow> 'b"
-  abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
-  alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
-  equ2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-  Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-
-definition
- "equal \<equiv> (op =)" 
-
-fun alpha_set_ex where
-  "alpha_set_ex (bs, x) R f (cs, y) = (\<exists>pi. alpha_set (bs, x) R f pi (cs, y))"
- 
-fun alpha_res_ex where
-  "alpha_res_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_res (bs, x) R f pi (cs, y))"
-
-fun alpha_lst_ex where
-  "alpha_lst_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_lst (bs, x) R f pi (cs, y))"
-
-
-
-notation (latex output)
-  swap ("'(_ _')" [1000, 1000] 1000) and
-  fresh ("_ # _" [51, 51] 50) and
-  fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
-  supp ("supp _" [78] 73) and
-  uminus ("-_" [78] 73) and
-  If  ("if _ then _ else _" 10) and
-  alpha_set_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and
-  alpha_lst_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and
-  alpha_res_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _\<^esup> _") and
-  abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
-  abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
-  fv ("fa'(_')" [100] 100) and
-  equal ("=") and
-  alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
-  alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and 
-  alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and 
-  Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
-  Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and
-  Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) and
-  Abs_res ("[_]\<^bsub>set+\<^esub>._") and
-  Abs_print ("_\<^bsub>set\<^esub>._") and
-  Cons ("_::_" [78,77] 73) and
-  supp_set ("aux _" [1000] 10) and
-  alpha_bn ("_ \<approx>bn _")
-
-consts alpha_trm ::'a
-consts fa_trm :: 'a
-consts fa_trm_al :: 'a
-consts alpha_trm2 ::'a
-consts fa_trm2 :: 'a
-consts fa_trm2_al :: 'a
-consts supp2 :: 'a
-consts ast :: 'a
-consts ast' :: 'a
-consts bn_al :: "'b \<Rightarrow> 'a"
-notation (latex output) 
-  alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
-  fa_trm ("fa\<^bsub>trm\<^esub>") and
-  fa_trm_al ("fa\<AL>\<^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
-  fa_trm2_al ("'(fa\<AL>\<^bsub>assn\<^esub>, fa\<AL>\<^bsub>trm\<^esub>')") and
-  ast ("'(as, t')") and
-  ast' ("'(as', t\<PRIME> ')") and
-  equ2 ("'(=, =')") and
-  supp2 ("'(supp, supp')") and
-  bn_al ("bn\<^sup>\<alpha> _" [100] 100)
-(*>*)
-
-
-section {* Introduction *}
-
-text {*
-  So far, Nominal Isabelle provided a mechanism for constructing alpha-equated
-  terms, for example lambda-terms
-
-  \[
-  @{text "t ::= x | t t | \<lambda>x. t"}
-  \]\smallskip
-
-  \noindent
-  where free and bound variables have names.  For such alpha-equated terms,
-  Nominal Isabelle derives automatically a reasoning infrastructure that has
-  been used successfully in formalisations of an equivalence checking
-  algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
-  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-  \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
-  in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for
-  formalisations in the locally-nameless approach to binding
-  \cite{SatoPollack10}.
-
-  However, Nominal Isabelle has fared less well in a formalisation of the
-  algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
-  respectively, of the form
-
-  \begin{equation}\label{tysch}
-  \begin{array}{l}
-  @{text "T ::= x | T \<rightarrow> T"}\hspace{15mm}
-  @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
-  \end{array}
-  \end{equation}\smallskip
-
-  \noindent
-  and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
-  type-variables.  While it is possible to implement this kind of more general
-  binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
-  formalisation of W. For example, the usual definition for a
-  type being an instance of a type-scheme requires in the iterated version 
-  the following auxiliary \emph{unbinding relation}:
-
-  \[
-  \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
-  \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})}
-   {@{text S} \hookrightarrow (@{text xs}, @{text T})}
-  \]\smallskip
-
-  \noindent
-  Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
-  address the following problem:
-  Given a type-scheme, say @{text S}, how does one get access to the bound type-variables 
-  and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though 
-  in general it will only provide \emph{a} list of type-variables together with \emph{a} type that are  
-  ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
-  for alpha-equated type-schemes. With the unbinding relation  
-  in place, we can define when a type @{text T} is an instance of a type-scheme @{text S} as follows:
-
-  \[
-  @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
-  \]\smallskip
-  
-  \noindent
-  This means there exists a list of type-variables @{text xs} and a type @{text T'} to which
-  the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} whose domain is
-  @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
-  The problem with this definition is that we cannot follow the usual proofs 
-  that are by induction on the type-part of the type-scheme (since it is under
-  an existential quantifier and only an alpha-variant). The implementation of 
-  type-schemes using iterations of single binders 
-  prevents us from directly ``unbinding'' the bound type-variables and the type-part. 
-  Clearly, a more dignified approach for formalising algorithm W is desirable. 
-  The purpose of this paper is to introduce general binders, which 
-  allow us to represent type-schemes so that they can bind multiple variables at once
-  and as a result solve this problem more straightforwardly.
-  The need of iterating single binders is also one reason
-  why the existing Nominal Isabelle and similar theorem provers that only provide
-  mechanisms for binding single variables have so far not fared very well with
-  the more advanced tasks in the POPLmark challenge \cite{challenge05},
-  because also there one would like to bind multiple variables at once.
-
-  Binding multiple variables has interesting properties that cannot be captured
-  easily by iterating single binders. For example in the case of type-schemes we do not
-  want to make a distinction about the order of the bound variables. Therefore
-  we would like to regard in \eqref{ex1} below  the first pair of type-schemes as alpha-equivalent,
-  but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
-  the second pair should \emph{not} be alpha-equivalent:
-
-  \begin{equation}\label{ex1}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, y}. y \<rightarrow> x"}\hspace{10mm}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
-  \end{equation}\smallskip
-
-  \noindent
-  Moreover, we like to regard type-schemes as alpha-equivalent, if they differ
-  only on \emph{vacuous} binders, such as
-
-  \begin{equation}\label{ex3}
-  @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, z}. x \<rightarrow> y"}
-  \end{equation}\smallskip
-
-  \noindent
-  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 for
-  type-schemes by Leroy in \cite[Page 18--19]{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
-
-  \begin{equation}\label{one}
-  @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}
-  \end{equation}\smallskip
-
-  \noindent
-  we might not care in which order the assignments @{text "x = 3"} and
-  \mbox{@{text "y = 2"}} are given, but it would be often unusual (particularly
-  in strict languages) to regard \eqref{one} as alpha-equivalent with
-
-  \[
-  @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
-  \]\smallskip
-
-  \noindent
-  Therefore we will also provide a separate binding mechanism for cases in
-  which the order of binders does not matter, but the `cardinality' of the
-  binders has to agree.
-
-  However, we found that this is still not sufficient for dealing with
-  language constructs frequently occurring in programming language
-  research. For example in @{text "\<LET>"}s containing patterns like
-
-  \begin{equation}\label{two}
-  @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
-  \end{equation}\smallskip
-
-  \noindent
-  we want to bind all variables from the pattern inside the body of the
-  $\mathtt{let}$, but we also care about the order of these variables, since
-  we do not want to regard \eqref{two} as alpha-equivalent with
-
-  \[
-  @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
-  \]\smallskip
-
-  \noindent
-  As a result, we provide three general binding mechanisms each of which binds
-  multiple variables at once, and let the user choose which one is intended
-  when formalising a term-calculus.
-
-  By providing these general binding mechanisms, however, we have to work
-  around a problem that has been pointed out by Pottier \cite{Pottier06} and
-  Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
-
-  \[
-  @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
-  \]\smallskip
-
-  \noindent
-  we care about the information that there are as many bound variables @{text
-  "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
-  we represent the @{text "\<LET>"}-constructor by something like
-
-  \[
-  @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}
-  \]\smallskip
-
-  \noindent
-  where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
-  "x\<^isub>i"} becomes bound in @{text s}. In this representation the term
-  \mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly
-  legal instance, but the lengths of the two lists do not agree. To exclude
-  such terms, additional predicates about well-formed terms are needed in
-  order to ensure that the two lists are of equal length. This can result in
-  very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid
-  this, we will allow type specifications for @{text "\<LET>"}s as follows
-
-  \[
-  \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll}
-  @{text trm} & @{text "::="}  & @{text "\<dots>"} \\
-              & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 
-                                 \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
-  @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
-               &  @{text "|"}  & @{text "\<ACONS>  name  trm  assn"}
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  where @{text assn} is an auxiliary type representing a list of assignments
-  and @{text bn} an auxiliary function identifying the variables to be bound
-  by the @{text "\<LET>"}. This function can be defined by recursion over @{text
-  assn} as follows
-
-  \[
-  @{text "bn(\<ANIL>) ="}~@{term "{}"} \hspace{10mm} 
-  @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 
-  \]\smallskip
-
-  \noindent
-  The scope of the binding is indicated by labels given to the types, for
-  example @{text "s::trm"}, and a binding clause, in this case
-  \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
-  clause states that all the names the function @{text "bn(as)"} returns
-  should be bound in @{text s}.  This style of specifying terms and bindings
-  is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
-  extends Ott in several aspects: one is that we support three binding
-  modes---Ott has only one, namely the one where the order of binders matters.
-  Another is that our reasoning infrastructure, like strong induction principles
-  and the notion of free variables, is derived from first principles within 
-  the Isabelle/HOL theorem prover.
-
-  However, we will not be able to cope with all specifications that are
-  allowed by Ott. One reason is that Ott lets the user specify `empty' types
-  like \mbox{@{text "t ::= t t | \<lambda>x. t"}} 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}.  Another reason is that we establish the reasoning
-  infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a
-  reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or
-  `raw', terms. While our alpha-equated terms and the `raw' terms produced by
-  Ott use names for bound variables, there is a key difference: working with
-  alpha-equated terms means, for example, that the two type-schemes
-
-  \[
-  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 
-  \]\smallskip
-  
-  \noindent
-  are not just alpha-equal, but actually \emph{equal}! As a result, we can
-  only support specifications that make sense on the level of alpha-equated
-  terms (offending specifications, which for example bind a variable according
-  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.
-
-  Although in informal settings a reasoning infrastructure for alpha-equated
-  terms is nearly always taken for granted, establishing it automatically in
-  Isabelle/HOL is a rather non-trivial task. For every
-  specification we will need to construct type(s) containing as elements the
-  alpha-equated terms. To do so, we use the standard HOL-technique of defining
-  a new type by identifying a non-empty subset of an existing type.  The
-  construction we perform in Isabelle/HOL can be illustrated by the following picture:
-
-  \begin{equation}\label{picture}
-  \mbox{\begin{tikzpicture}[scale=1.1]
-  %\draw[step=2mm] (-4,-1) grid (4,1);
-  
-  \draw[very thick] (0.7,0.4) circle (4.25mm);
-  \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
-  \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
-  
-  \draw (-2.0, 0.845) --  (0.7,0.845);
-  \draw (-2.0,-0.045)  -- (0.7,-0.045);
-
-  \draw ( 0.7, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};
-  \draw (-2.4, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
-  \draw (1.8, 0.48) node[right=-0.1mm]
-    {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
-  \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
-  \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
-  
-  \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
-  \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};
-
-  \end{tikzpicture}}
-  \end{equation}\smallskip
-
-  \noindent
-  We take as the starting point a definition of raw terms (defined as a
-  datatype in Isabelle/HOL); then identify the alpha-equivalence classes in
-  the type of sets of raw terms according to our alpha-equivalence relation,
-  and finally define the new type as these alpha-equivalence classes (the
-  non-emptiness requirement is always satisfied whenever the raw terms are
-  definable as datatype in Isabelle/HOL and our relation for alpha-equivalence
-  is an equivalence relation).
-
-  The fact that we obtain an isomorphism between the new type and the
-  non-empty subset shows that the new type is a faithful representation of
-  alpha-equated terms. That is not the case for example for terms using the
-  locally nameless representation of binders \cite{McKinnaPollack99}: in this
-  representation there are `junk' terms that need to be excluded by
-  reasoning about a well-formedness predicate.
-
-  The problem with introducing a new type in Isabelle/HOL is that in order to
-  be useful, a reasoning infrastructure needs to be `lifted' from the
-  underlying subset to the new type. This is usually a tricky and arduous
-  task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}
-  the quotient package described by Homeier \cite{Homeier05} for the HOL4
-  system. This package allows us to lift definitions and theorems involving
-  raw terms to definitions and theorems involving alpha-equated terms. For
-  example if we define the free-variable function over raw lambda-terms
-  as follows
-
-  \[
-  \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
-  @{text "fv(x)"}     & @{text "\<equiv>"} & @{text "{x}"}\\
-  @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\<equiv>"} & @{text "fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\
-  @{text "fv(\<lambda>x.t)"}  & @{text "\<equiv>"} & @{text "fv(t) - {x}"}
-  \end{tabular}}
-  \]\smallskip
-  
-  \noindent
-  then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
-  operating on quotients, that is alpha-equivalence classes of lambda-terms. This
-  lifted function is characterised by the equations
-
-  \[
-  \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
-  @{text "fv\<^sup>\<alpha>(x)"}     & @{text "="} & @{text "{x}"}\\
-  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\
-  @{text "fv\<^sup>\<alpha>(\<lambda>x.t)"}  & @{text "="} & @{text "fv\<^sup>\<alpha>(t) - {x}"}
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  (Note that this means also the term-constructors for variables, applications
-  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
-  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 
-  infrastructure for alpha-equated terms.\smallskip
-
-  The examples we have in mind where our reasoning infrastructure will be
-  helpful include the term language of Core-Haskell (see
-  Figure~\ref{corehas}). This term language involves patterns that have lists
-  of type-, coercion- and term-variables, all of which are bound in @{text
-  "\<CASE>"}-expressions. In these patterns we do not know in advance how many
-  variables need to be bound. Another example is the algorithm W,
-  which includes multiple binders in type-schemes.\medskip
-
-  \noindent
-  {\bf Contributions:} We provide three new definitions for when terms
-  involving general binders are alpha-equivalent. These definitions are
-  inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-generated
-  proofs, we establish a reasoning infrastructure for alpha-equated terms,
-  including properties about support, freshness and equality conditions for
-  alpha-equated terms. We are also able to automatically derive strong
-  induction principles that have the variable convention already built in.
-  For this we simplify the earlier automated proofs by using the proving tools
-  from the function package~\cite{Krauss09} of Isabelle/HOL.  The method
-  behind our specification of general binders is taken from the Ott-tool, but
-  we introduce crucial restrictions, and also extensions, so that our
-  specifications make sense for reasoning about alpha-equated terms.  The main
-  improvement over Ott is that we introduce three binding modes (only one is
-  present in Ott), provide formalised definitions for alpha-equivalence and
-  for free variables of our terms, and also derive a reasoning infrastructure
-  for our specifications from `first principles' inside a theorem prover.
-
-
-  \begin{figure}[t]
-  \begin{boxedminipage}{\linewidth}
-  \begin{center}
-  \begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{3}{@ {}l}{Type Kinds}\\
-  @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Coercion Kinds}\\
-  @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Types}\\
-  @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 
-  @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Coercion Types}\\
-  @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
-  @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> | refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2"}\\
-  & @{text "|"} & @{text "\<gamma> @ \<sigma> | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Terms}\\
-  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> | \<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2"}\\
-  & @{text "|"} & @{text "\<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 | \<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Patterns}\\
-  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
-  \multicolumn{3}{@ {}l}{Constants}\\
-  & @{text C} & coercion constants\\
-  & @{text T} & value type constructors\\
-  & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
-  & @{text K} & data constructors\smallskip\\
-  \multicolumn{3}{@ {}l}{Variables}\\
-  & @{text a} & type variables\\
-  & @{text c} & coercion variables\\
-  & @{text x} & term variables\\
-  \end{tabular}
-  \end{center}
-  \end{boxedminipage}
-  \caption{The System @{text "F\<^isub>C"}
-  \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
-  version of @{text "F\<^isub>C"} we made a modification by separating the
-  grammars for type kinds and coercion kinds, as well as for types and coercion
-  types. For this paper the interesting term-constructor is @{text "\<CASE>"},
-  which binds multiple type-, coercion- and term-variables (the overlines stand for lists).\label{corehas}}
-  \end{figure}
-*}
-
-section {* A Short Review of the Nominal Logic Work *}
-
-text {*
-  At its core, Nominal Isabelle is an adaptation of the nominal logic work by
-  Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
-  \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
-  to aid the description of what follows. 
-
-  Two central notions in the nominal logic work are sorted atoms and
-  sort-respecting permutations of atoms. We will use the letters @{text "a, b,
-  c, \<dots>"} to stand for atoms and @{text "\<pi>, \<pi>\<^isub>1, \<dots>"} to stand for permutations,
-  which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to
-  represent variables, be they bound or free. The sorts of atoms can be used
-  to represent different kinds of variables, such as the term-, coercion- and
-  type-variables in Core-Haskell.  It is assumed that there is an infinite
-  supply of atoms for each sort. In the interest of brevity, we shall restrict
-  ourselves in what follows to only one sort of atoms.
-
-  Permutations are bijective functions from atoms to atoms that are 
-  the identity everywhere except on a finite number of atoms. There is a 
-  two-place permutation operation written
-  @{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-  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 "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}} 
-  (even if this operation is non-commutative), 
-  and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
-  operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
-  for example permutations acting on atoms, products, lists, permutations, sets, 
-  functions and booleans are given by:
-  
-  \begin{equation}\label{permute}
-  \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
-  \begin{tabular}{@ {}l@ {}}
-  @{text "\<pi> \<bullet> a \<equiv> \<pi> a"}\\
-  @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
-  @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\
-  @{thm permute_set_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
-  @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
-  \end{tabular}
-  \end{tabular}}
-  \end{equation}\smallskip
-  
-  \noindent
-  Concrete permutations in Nominal Isabelle are built up from swappings, 
-  written as \mbox{@{text "(a b)"}}, which are permutations that behave 
-  as follows:
-  
-  \[
-  @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
-  \]\smallskip
-
-  The most original aspect of the nominal logic work of Pitts is a general
-  definition for the notion of the `set of free variables of an object @{text
-  "x"}'.  This notion, written @{term "supp x"}, is general in the sense that
-  it applies not only to lambda-terms (alpha-equated or not), but also to lists,
-  products, sets and even functions. Its definition depends only on the
-  permutation operation and on the notion of equality defined for the type of
-  @{text x}, namely:
-  
-  \begin{equation}\label{suppdef}
-  @{thm supp_def[no_vars, THEN eq_reflection]}
-  \end{equation}\smallskip
-
-  \noindent
-  There is also the derived notion for when an atom @{text a} is \emph{fresh}
-  for an @{text x}, defined as 
-
-  \[
-  @{thm fresh_def[no_vars]}
-  \]\smallskip
-
-  \noindent
-  We use for sets of atoms the abbreviation 
-  @{thm (lhs) fresh_star_def[no_vars]}, defined as 
-  @{thm (rhs) fresh_star_def[no_vars]}.
-  A striking consequence of these definitions is that we can prove
-  without knowing anything about the structure of @{term x} that
-  swapping two fresh atoms, say @{text a} and @{text b}, leaves 
-  @{text x} unchanged, namely 
-  
-  \begin{prop}\label{swapfreshfresh}
-  If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
-  then @{thm (concl) swap_fresh_fresh[no_vars]}.
-  \end{prop}
-  
-  While often the support of an object can be relatively easily 
-  described, for example for atoms, products, lists, function applications, 
-  booleans and permutations as follows
-  
-  \begin{equation}\label{supps}\mbox{
-  \begin{tabular}{c@ {\hspace{10mm}}c}
-  \begin{tabular}{rcl}
-  @{term "supp a"} & $=$ & @{term "{a}"}\\
-  @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
-  @{term "supp []"} & $=$ & @{term "{}"}\\
-  @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
-  \end{tabular}
-  &
-  \begin{tabular}{rcl}
-  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
-  @{term "supp b"} & $=$ & @{term "{}"}\\
-  @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
-  \end{tabular}
-  \end{tabular}}
-  \end{equation}\smallskip
-  
-  \noindent 
-  in some cases it can be difficult to characterise the support precisely, and
-  only an approximation can be established (as for function applications
-  above). Reasoning about such approximations can be simplified with the
-  notion \emph{supports}, defined as follows:
-  
-  \begin{defi}
-  A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b}
-  not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
-  \end{defi}
-  
-  \noindent
-  The main point of @{text supports} is that we can establish the following 
-  two properties.
-  
-  \begin{prop}\label{supportsprop}
-  Given a set @{text "bs"} of atoms.\\
-  {\it (i)} If @{thm (prem 1) supp_is_subset[where S="bs", no_vars]}
-  and @{thm (prem 2) supp_is_subset[where S="bs", no_vars]} then 
-  @{thm (concl) supp_is_subset[where S="bs", no_vars]}.\\
-  {\it (ii)} @{thm supp_supports[no_vars]}.
-  \end{prop}
-  
-  Another important notion in the nominal logic work is \emph{equivariance}.
-  For a function @{text f} to be equivariant 
-  it is required that every permutation leaves @{text f} unchanged, that is
-  
-  \begin{equation}\label{equivariancedef}
-  @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}\;.
-  \end{equation}\smallskip
-  
-  \noindent
-  If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, say, this definition is equivalent to 
-  the fact that a permutation applied to the application
-  @{text "f x"} can be moved to the argument @{text x}. That means for 
-  such functions, we have for all permutations @{text "\<pi>"}:
-  
-  \begin{equation}\label{equivariance}
-  @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}\;.
-  \end{equation}\smallskip
-   
-  \noindent
-  There is
-  also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.
-  Suppose a relation @{text R}, then for all permutations @{text \<pi>}:
-  
-  \[
-  @{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}\;.
-  \]\smallskip
-
-  \noindent
-  Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can easily deduce that for a function being equivariant is equivalent to having empty support.
-
-  Using freshness, the nominal logic work provides us with general means for renaming 
-  binders. 
-  
-  \noindent
-  While in the older version of Nominal Isabelle, we used extensively 
-  Proposition~\ref{swapfreshfresh} to rename single binders, this property 
-  proved too unwieldy for dealing with multiple binders. For such binders the 
-  following generalisations turned out to be easier to use.
-
-  \begin{prop}\label{supppermeq}
-  @{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}
-  \end{prop}
-
-  \begin{prop}\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 "\<pi>"} such that @{term "(\<pi> \<bullet> as) \<sharp>* c"} and
-  @{term "supp x \<sharp>* \<pi>"}.
-  \end{prop}
-
-  \noindent
-  The idea behind the second property is that given a finite set @{text as}
-  of binders (being bound, or fresh, in @{text x} is ensured by the
-  assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
-  the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-  as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
-  in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 
-  fact and Property~\ref{supppermeq} allow us to `rename' just the binders 
-  @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. 
-
-  Note that @{term "supp x \<sharp>* \<pi>"}
-  is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate 
-  Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the 
-  reasoning infrastructure of Nominal Isabelle is set up so that it provides more
-  automation for the formulation given above.
-
-  Most properties given in this section are described in detail in \cite{HuffmanUrban10}
-  and all are formalised in Isabelle/HOL. In the next sections we will make 
-  use of these properties in order to define alpha-equivalence in 
-  the presence of multiple binders.
-*}
-
-
-section {* Abstractions\label{sec:binders} *}
-
-text {*
-  In Nominal Isabelle, the user is expected to write down a specification of a
-  term-calculus and then a reasoning infrastructure is automatically derived
-  from this specification (remember that Nominal Isabelle is a definitional
-  extension of Isabelle/HOL, which does not introduce any new axioms).
-
-  In order to keep our work with deriving the reasoning infrastructure
-  manageable, we will wherever possible state definitions and perform proofs
-  on the `user-level' of Isabelle/HOL, as opposed to writing custom ML-code that
-  generates them anew for each specification. 
-  To that end, we will consider
-  first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs
-  are intended to represent the abstraction, or binding, of the set of atoms @{text
-  "as"} in the body @{text "x"}.
-
-  The first question we have to answer is when two pairs @{text "(as, x)"} and
-  @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
-  the notion of alpha-equivalence that is \emph{not} preserved by adding
-  vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
-  given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
-  set"}}, then @{text "(as, x)"} and @{text "(bs, y)"} need to have the same set of free
-  atoms; moreover there must be a permutation @{text \<pi>} such that {\it
-  (ii)} @{text \<pi>} leaves the free atoms of @{text "(as, x)"} and @{text "(bs, y)"} unchanged, but
-  {\it (iii)} `moves' their bound names so that we obtain modulo a relation,
-  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
-  @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
-  requirements {\it (i)} to {\it (iv)} can be stated formally as:
-
-  \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
-  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} & 
-    \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
-       & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
-       & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
-       & \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\
-       & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"} \\ 
-  \end{tabular}
-  \end{defi}
- 
-  \noindent
-  Note that the relation is
-  dependent on a free-atom function @{text "fa"} and a relation @{text
-  "R"}. The reason for this extra generality is that we will use
-  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both raw terms and 
-  alpha-equated terms. In
-  the latter case, @{text R} will be replaced by equality @{text "="} and we
-  will prove that @{text "fa"} is equal to @{text "supp"}.
-
-  Definition \ref{alphaset} does not make any distinction between the
-  order of abstracted atoms. If we want this, then we can define alpha-equivalence 
-  for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 
-  as follows
-  
-  \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
-  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
-  \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
-         & \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ 
-         & \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
-         & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
-         & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"}\\
-  \end{tabular}
-  \end{defi}
-  
-  \noindent
-  where @{term set} is the function that coerces a list of atoms into a set of atoms.
-  Now the last clause ensures that the order of the binders matters (since @{text as}
-  and @{text bs} are lists of atoms).
-
-  If we do not want to make any difference between the order of binders \emph{and}
-  also allow vacuous binders, that means according to Pitts~\cite{Pitts04} 
-  \emph{restrict} atoms, then we keep sets of binders, but drop 
-  condition {\it (iv)} in Definition~\ref{alphaset}:
-
-  \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
-  \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  
-  @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
-  \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 
-             & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\
-             & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
-             & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
-  \end{tabular}
-  \end{defi}
-
-
-  It might be useful to consider first some examples how these definitions
-  of alpha-equivalence pan out in practice.  For this consider the case of
-  abstracting a set of atoms over types (as in type-schemes). We set
-  @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
-  define
-  
-  \[
-  @{text "fa(x) \<equiv> {x}"}  \hspace{10mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
-  \]\smallskip
-
-  \noindent
-  Now recall the examples shown in \eqref{ex1} and
-  \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-  @{text "({x, y}, y \<rightarrow> x)"} are alpha-equivalent according to
-  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to
-  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
-  "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
-  since there is no permutation that makes the lists @{text "[x, y]"} and
-  @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
-  unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$
-  @{text "({x, y}, x)"} which holds by taking @{text "\<pi>"} to be the identity
-  permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-  $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
-  permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
-  (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
-  shown that all three notions of alpha-equivalence coincide, if we only
-  abstract a single atom. In this case they also agree with the alpha-equivalence
-  used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a
-  proof of this fact since the details are hairy and not really important for the
-  purpose of this paper.}
-
-  In the rest of this section we are going to show that the alpha-equivalences
-  really lead to abstractions where some atoms are bound (or more precisely
-  removed from the support).  For this we will consider three abstraction
-  types that are quotients of the relations
-
-  \begin{equation}
-  \begin{array}{r}
-  @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\
-  @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\
-  @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
-  \end{array}
-  \end{equation}\smallskip
-  
-  \noindent
-  Note that in these relations we replaced the free-atom function @{text "fa"}
-  with @{term "supp"} and the relation @{text R} with equality. We can show
-  the following two properties:
-
-  \begin{lem}\label{alphaeq} 
-  The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, 
-  $\approx_{\,\textit{set+}}^{=, \textit{supp}}$
-  and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are 
-  equivalence relations and equivariant. 
-  \end{lem}
-
-  \begin{proof}
-  Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
-  a permutation @{text "\<pi>"} and for the proof obligation take @{term "-
-  \<pi>"}. In case of transitivity, we have two permutations @{text "\<pi>\<^isub>1"}
-  and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text
-  "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
-  \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
-  "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we
-  have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>
-  \<pi>'"}. To show equivariance, we need to `pull out' the permutations,
-  which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,
-  set"} and @{text "supp"}, are equivariant (see
-  \cite{HuffmanUrban10}). Finally, we apply the permutation operation on
-  booleans.
-  \end{proof}
-
-  \noindent
-  Recall the picture shown in \eqref{picture} about new types in HOL.
-  The lemma above allows us to use our quotient package for introducing 
-  new types @{text "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}
-  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
-  
-  \[
-  @{term "Abs_set as x"} \hspace{10mm} 
-  @{term "Abs_res as x"} \hspace{10mm}
-  @{term "Abs_lst as x"} 
-  \]\smallskip
-  
-  \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 
-  abstractions, namely:
-
-  \begin{thm}[Support of Abstractions]\label{suppabs} 
-  Assuming @{text x} has finite support, then
-
-  \[
-  \begin{array}{l@ {\;=\;}l}
-  @{thm (lhs) supp_Abs(1)[no_vars]} & @{thm (rhs) supp_Abs(1)[no_vars]}\\
-  @{thm (lhs) supp_Abs(2)[no_vars]} & @{thm (rhs) supp_Abs(2)[no_vars]}\\
-  @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} &
-  @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\
-  \end{array}
-  \]\smallskip
-  \end{thm}
-
-  \noindent
-  In effect, this theorem states that the atoms @{text "as"} are bound in the
-  abstraction. As stated earlier, this can be seen as a litmus test that our
-  Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
-  idea of alpha-equivalence relations. Below we will give the proof for the
-  first equation of Theorem \ref{suppabs}. The others follow by similar
-  arguments. By definition of the abstraction type @{text
-  "abs\<^bsub>set\<^esub>"} we have
-
-  \begin{equation}\label{abseqiff}
-  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 
-  @{term "alpha_set_ex (as, x) equal supp (bs, y)"}
-  \end{equation}\smallskip
-  
-  \noindent
-  and also set
-  
-  \begin{equation}\label{absperm}
-  @{thm permute_Abs(1)[where p="\<pi>", no_vars, THEN eq_reflection]}
-  \end{equation}\smallskip
-
-  \noindent
-  With this at our disposal, we can show 
-  the following lemma about swapping two atoms in an abstraction.
-  
-  \begin{lem}
-  If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and
-  @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then 
-  @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}
-  \end{lem}
-  
-  \begin{proof}
-  If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b)"} is then
-  the identity permutation.
-  Also in the other case the lemma is straightforward using \eqref{abseqiff}
-  and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
-  (supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"} as
-  the permutation for the proof obligation.
-  \end{proof}
-  
-  \noindent
-  This lemma together 
-  with \eqref{absperm} allows us to show
-  
-  \begin{equation}\label{halfone}
-  @{thm Abs_supports(1)[no_vars]}
-  \end{equation}\smallskip
-  
-  \noindent
-  which by Property~\ref{supportsprop} gives us `one half' of
-  Theorem~\ref{suppabs}. To establish the `other half', we 
-  use a trick from \cite{Pitts04} and first define an auxiliary 
-  function @{text aux}, taking an abstraction as argument
-
-  \[
-  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
-  \]\smallskip 
-
-  \noindent
-  Using the second equation in \eqref{equivariance}, we can show that 
-  @{text "aux"} is equivariant (since @{term "\<pi> \<bullet> (supp x - as) = (supp (\<pi> \<bullet> x)) - (\<pi> \<bullet> as)"}) 
-  and therefore has empty support. 
-  This in turn means
-  
-  \[
-  @{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
-  \]\smallskip
-  
-  \noindent
-  using the fact about the support of function applications in \eqref{supps}. Assuming 
-  @{term "supp x - as"} is a finite set, we further obtain
-  
-  \begin{equation}\label{halftwo}
-  @{thm (concl) Abs_supp_subset1(1)[no_vars]}
-  \end{equation}\smallskip
-  
-  \noindent
-  This is because for every finite set of atoms, say @{text "bs"}, we have 
-  @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not 
-  the case for infinite sets.}
-  Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
-  the first equation of Theorem~\ref{suppabs}. The others are similar.
-
-  Recall the definition of support given in \eqref{suppdef}, and note the difference between 
-  the support of a raw pair and an abstraction
-
-  \[
-  @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
-  @{term "supp (Abs_set as x) = supp x - as"}
-  \]\smallskip
-
-  \noindent
-  While the permutation operations behave in both cases the same (a permutation
-  is just moved to the arguments), the notion of equality is different for pairs and
-  abstractions. Therefore we have different supports. In case of abstractions,
-  we have established in Theorem~\ref{suppabs} that bound atoms are removed from 
-  the support of the abstractions' bodies.
-
-  The method of first considering abstractions of the form @{term "Abs_set as
-  x"} etc is motivated by the fact that we can conveniently establish at the
-  Isabelle/HOL level properties about them.  It would be extremely laborious
-  to write custom ML-code that derives automatically such properties for every
-  term-constructor that binds some atoms. Also the generality of the
-  definitions for alpha-equivalence will help us in the next sections.
-*}
-
-section {* Specifying General Bindings\label{sec:spec} *}
-
-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 mutually 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 schematically as follows:
-  
-  \begin{equation}\label{scheme}
-  \mbox{\begin{tabular}{@ {}p{2.5cm}l}
-  type \mbox{declaration part} &
-  $\begin{cases}
-  \mbox{\begin{tabular}{l}
-  \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
-  \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
-  \raisebox{2mm}{$\ldots$}\\[-2mm] 
-  \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 
-  \end{tabular}}
-  \end{cases}$\\[2mm]
-  binding \mbox{function part} &
-  $\begin{cases}
-  \mbox{\begin{tabular}{l}
-  \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
-  \isacommand{where}\\
-  \raisebox{2mm}{$\ldots$}\\[-2mm]
-  \end{tabular}}
-  \end{cases}$\\
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  \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 types that
-  stand for the types of the arguments of the term-constructor.  For example a
-  term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
-
-  \[
-  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;\;\;\;$}  
-  @{text "binding_clauses"} 
-  \]\smallskip
-  
-  \noindent
-  whereby some of the @{text ty}$'_{1..l}$ (or their components) can 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 arguments need to satisfy a `positivity' restriction, which
-  ensures that the type has a set-theoretic semantics (see
-  \cite{Berghofer99}). If the types are polymorphic, we require the
-  type variables to stand for types that are finitely supported and over which 
-  a permutation operation is defined.
-  The labels @{text "label"}$_{1..l}$ annotated on 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}:
-
-
-  \[\mbox{
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\
-  \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\
-  \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies}
-  \end{tabular}}
-  \]\smallskip
-  
-  \noindent
-  The first mode is for binding lists of atoms (the order of bound atoms
-  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 labels in the
-  `\isacommand{in}-part' of a binding clause will be called \emph{bodies};
-  the `\isacommand{binds}-part' will be called \emph{binders}. In contrast to
-  Ott, we allow multiple labels in binders and bodies.  For example we allow
-  binding clauses of the form:
- 
-  \[\mbox{
-  \begin{tabular}{@ {}ll@ {}}
-  @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &  
-      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\
-  @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &  
-      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"}, 
-      \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  Similarly for the other binding modes. Interestingly, in case of
-  \isacommand{binds (set)} and \isacommand{binds (set+)} the binding clauses
-  above will make a difference to the semantics of the specifications (the
-  corresponding alpha-equivalence will differ). We will show this later with
-  an example.
-
-  
-  There are also some restrictions we need to impose on our binding clauses in
-  comparison to Ott. The main idea behind these restrictions is
-  that we obtain a notion of alpha-equivalence where it is ensured
-  that within a given scope an atom occurrence cannot be both bound and free
-  at the same time.  The first restriction is that a body can only occur in
-  \emph{one} binding clause of a term constructor. So for example
-
-  \[\mbox{
-  @{text "Foo x::name y::name t::trm"}\hspace{3mm}  
-  \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"},
-  \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}}
-  \]\smallskip
-
-  \noindent
-  is not allowed. 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 \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{binds (set)} and \isacommand{binds (set+)} the
-  labels must either refer to atom types or to sets of atom types; in case of
-  \isacommand{binds} the labels must refer to atom types or to lists of atom
-  types. Two examples for the use of shallow binders are the specification of
-  lambda-terms, where a single name is bound, and type-schemes, where a finite
-  set of names is bound:
-
-  \[\mbox{
-  \begin{tabular}{@ {}c@ {\hspace{8mm}}c@ {}}
-  \begin{tabular}{@ {}l}
-  \isacommand{nominal\_datatype} @{text lam} $=$\\
-  \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
-  \hspace{2mm}$\mid$~@{text "App lam lam"}\\
-  \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}%
-  \isacommand{binds} @{text x} \isacommand{in} @{text t}\\
-  \\
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text ty} $=$\\
-  \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\
-  \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\
-  \isacommand{and}~@{text "tsc ="}\\
-  \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}%
-  \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
-  \end{tabular}
-  \end{tabular}}
-  \]\smallskip
-
-
-  \noindent
-  In these specifications @{text "name"} refers to a (concrete) atom type, and @{text
-  "fset"} to the type of finite sets.  Note that for @{text Lam} it does not
-  matter which binding mode we use. The reason is that we bind only a single
-  @{text name}, in which case all three binding modes coincide. However, having 
-  \isacommand{binds (set)} or just \isacommand{binds}
-  in the second case makes a difference to the semantics of the specification
-  (which we will define in the next section).
-
-  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}, see below). The binding functions are
-  expected to return either a set of atoms (for \isacommand{binds (set)} and
-  \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need
-  to be defined by recursion over the corresponding type; the equations
-  must be given in the binding function part of the scheme shown in
-  \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
-  tuple patterns may be specified as:
-
-  \begin{equation}\label{letpat}
-  \mbox{%
-  \begin{tabular}{l}
-  \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{binds} @{text x} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} 
-     \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
-  \isacommand{and} @{text pat} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "PVar name"}\\
-  \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
-  \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{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)"}\smallskip\\ 
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  \noindent
-  In this specification the function @{text "bn"} determines which atoms of
-  the pattern @{text p} (fifth line) are bound in the argument @{text "t"}. Note that in the
-  second-last @{text bn}-clause the function @{text "atom"} coerces a name
-  into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This
-  allows us to treat binders of different atom type uniformly.
-
-  For deep binders we allow binding clauses such as
-  
-  \[\mbox{
-  \begin{tabular}{ll}
-  @{text "Bar p::pat t::trm"} &  
-     \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\
-  \end{tabular}}
-  \]\smallskip
-
-  
-  \noindent
-  where the argument of the deep binder also occurs in the body. We call such
-  binders \emph{recursive}.  To see the purpose of such recursive binders,
-  compare `plain' @{text "Let"}s and @{text "Let_rec"}s in the following
-  specification:
- 
-  \begin{equation}\label{letrecs}
-  \mbox{%
-  \begin{tabular}{@ {}l@ {}l}
-  \isacommand{nominal\_datatype}~@{text "trm ="}\\
-  \hspace{5mm}\phantom{$\mid$}~\ldots\\
-  \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
-     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-  \isacommand{and} @{text "assn"} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
-  \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
-  \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{text "bn(ANil) = []"}\\
-  \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
-  \end{tabular}}
-  \end{equation}\smallskip
-  
-  \noindent
-  The difference is that with @{text Let} we only want to bind the atoms @{text
-  "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
-  inside the assignment. This difference has consequences for the associated
-  notions of free-atoms and alpha-equivalence.
-  
-  To make sure that atoms bound by deep binders cannot be free at the
-  same time, we cannot have more than one binding function for a deep binder. 
-  Consequently we exclude specifications such as
-
-  \[\mbox{
-  \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-  @{text "Baz\<^isub>1 p::pat t::trm"} & 
-     \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text "p t"}\\
-  @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 
-     \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "p t\<^isub>1"},
-     \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "p t\<^isub>2"}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \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"}.\footnote{Since the Ott-tool does not derive a reasoning 
-  infrastructure for 
-  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
-  terms. The main restriction is that we cannot return an atom in a binding
-  function that is also bound in the corresponding term-constructor.
-  Consider again the specification for @{text "trm"} and a contrived
-  version for assignments @{text "assn"}:
-
-  \begin{equation}\label{bnexp}
-  \mbox{%
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
-  \isacommand{and} @{text "assn"} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "ANil'"}\\
-  \hspace{5mm}$\mid$~@{text "ACons' x::name y::name t::trm assn"}
-     \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\
-  \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{text "bn(ANil') = []"}\\
-  \hspace{5mm}$\mid$~@{text "bn(ACons' x y t as) = [atom x] @ bn(as)"}\\
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  \noindent
-  In this example the term constructor @{text "ACons'"} has four arguments with
-  a binding clause involving two of them. This constructor is also used in the definition
-  of the binding function. The restriction we have to impose is that the
-  binding function can only return free atoms, that is the ones that are \emph{not}
-  mentioned in a binding clause.  Therefore @{text "y"} cannot be used in the
-  binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the
-  binding clause), but @{text x} can (since it is a free atom). This
-  restriction is sufficient for lifting the binding function to alpha-equated
-  terms. If we would permit @{text "bn"} to return @{text "y"},
-  then it would not be respectful and therefore cannot be lifted to
-  alpha-equated lambda-terms.
-
-  In the version of Nominal Isabelle described here, we also adopted the
-  restriction from the Ott-tool that binding functions can only return: the
-  empty set or empty list (as in case @{text ANil'}), a singleton set or
-  singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
-  unions of atom sets or appended atom lists (case @{text ACons'}). This
-  restriction will simplify some automatic definitions and proofs later on.
-  
-  To sum up this section, we introduced nominal datatype
-  specifications, which are like standard datatype specifications in
-  Isabelle/HOL but extended with binding clauses and specifications for binding
-  functions. Each constructor argument in our specification can also
-  have an optional label. These labels are used in the binding clauses
-  of a constructor; there can be several binding clauses for each
-  constructor, but bodies of binding clauses can only occur in a
-  single one. Binding clauses come in three modes: \isacommand{binds},
-  \isacommand{binds (set)} and \isacommand{binds (set+)}.  Binders
-  fall into two categories: shallow binders and deep binders. Shallow
-  binders can occur in more than one binding clause and only have to
-  respect the binding mode (i.e.~be of the right type). Deep binders
-  can also occur in more than one binding clause, unless they are
-  recursive in which case they can only occur once. Each of the deep
-  binders can only have a single binding function.  Binding functions
-  are defined by recursion over a nominal datatype.  They can
-  return the empty set, singleton atoms and unions of sets of atoms
-  (for binding modes \isacommand{binds (set)} and \isacommand{binds
-  (set+)}), and the empty list, singleton atoms and appended lists of
-  atoms (for mode \isacommand{bind}). However, they can only return
-  atoms that are not mentioned in any binding clause.  
-
-  In order to
-  simplify our definitions of free atoms and alpha-equivalence we define next, we
-  shall assume specifications of term-calculi are implicitly
-  \emph{completed}. By this we mean that for every argument of a
-  term-constructor that is \emph{not} already part of a binding clause
-  given by the user, we add implicitly a special \emph{empty} binding
-  clause, written \isacommand{binds}~@{term
-  "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms,
-  the completion produces
-
-  \[\mbox{
-  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
-  \isacommand{nominal\_datatype} @{text lam} =\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
-    \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
-  \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
-    \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
-  \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
-    \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent 
-  The point of completion is that we can make definitions over the binding
-  clauses and be sure to have captured all arguments of a term constructor. 
-*}
-
-section {* Alpha-Equivalence and Free Atoms\label{sec:alpha} *}
-
-text {*
-  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. As Pottier and Cheney pointed
-  out \cite{Cheney05,Pottier06}, just re-arranging the arguments of
-  term-constructors so that binders and their bodies are next to each other
-  will result in inadequate representations in cases like \mbox{@{text "Let
-  x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}}. Therefore we will
-  first extract `raw' datatype definitions from the specification and then
-  define explicitly an alpha-equivalence relation over them. We subsequently
-  construct the quotient of the datatypes according to our alpha-equivalence.
-
-
-  The `raw' datatype definition can be obtained by stripping off the 
-  binding clauses and the labels from the types given by the user. We also have to invent
-  new names for the  types @{text "ty\<^sup>\<alpha>"} and the term-constructors @{text "C\<^sup>\<alpha>"}. 
-  In our implementation we just use the affix ``@{text "_raw"}''.
-  But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
-  that a notion is given for alpha-equivalence classes and leave it out 
-  for the corresponding notion given on the raw level. So for example 
-  we have @{text "ty\<^sup>\<alpha> / ty"} and @{text "C\<^sup>\<alpha> / C"}
-  where @{term ty} is the type used in the quotient construction for 
-  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the raw type @{text "ty"},
-  respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}. 
-
-  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 also define permutation operations by 
-  recursion so that for each term constructor @{text "C"} we have that
-  
-  \begin{equation}\label{ceqvt}
-  @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
-  \end{equation}\smallskip
-
-  \noindent
-  We will need this operation later when we define the notion of alpha-equivalence.
-
-  The first non-trivial step we have to perform is the generation of
-  \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
-  details of our definitions will be somewhat involved. However they are still
-  conceptually simple in comparison with the `positional' approach taken in
-  Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and
-  \emph{partial equivalence relations} over sets of occurrences.} For the
-  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
-
-  \begin{equation}\label{fvars}
-  \mbox{@{text "fa_ty"}$_{1..n}$}
-  \end{equation}\smallskip
-  
-  \noindent
-  by recursion.
-  We define these functions together with auxiliary free-atom functions for
-  the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
-  we define
-  
-  \[
-  @{text "fa_bn"}\mbox{$_{1..m}$}.
-  \]\smallskip
-  
-  \noindent
-  The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we saw in \eqref{letrecs} with the example of `plain' @{text Let}s. We need
-  therefore functions that calculate those free atoms in deep binders.
-
-  While the idea behind these free-atom functions is simple (they just
-  collect all atoms that are not bound), because of our rather complicated
-  binding mechanisms their definitions are somewhat involved.  Given
-  a raw term-constructor @{text "C"} of type @{text ty} and some associated
-  binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
-  "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
-  "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
-  clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). 
-  Suppose a binding clause @{text bc\<^isub>i} is of the form 
-  
-  \[
-  \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-  \]\smallskip
-  
-  \noindent
-  in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text
-  ty}$_{1..q}$, and the binders @{text b}$_{1..p}$ either refer to labels of
-  atom types (in case of shallow binders) or to binding functions taking a
-  single label as argument (in case of deep binders). Assuming @{text "D"}
-  stands for the set of free atoms of the bodies, @{text B} for the set of
-  binding atoms in the binders and @{text "B'"} for the set of free atoms in
-  non-recursive deep binders, then the free atoms of the binding clause @{text
-  bc\<^isub>i} are
-
-  \begin{equation}\label{fadef}
-  \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
-  \end{equation}\smallskip
-  
-  \noindent
-  The set @{text D} is formally defined as
-  
-  \[
-  @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
-  \]\smallskip
-  
-  \noindent
-  where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the 
-  specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function 
-  we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i \<equiv> supp"}}. The reason
-  for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and
-  we assume @{text supp} is the generic function that characterises the free variables of 
-  a type (in fact in the next section we will show that the free-variable functions we
-  define here, are equal to the support once lifted to alpha-equivalence classes).
-  
-  In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
-  for atom types to which shallow binders may refer\\[-4mm]
-  
-  \begin{equation}\label{bnaux}\mbox{
-  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-  @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-  @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
-  \end{tabular}}
-  \end{equation}\smallskip
-  
-  \noindent 
-  Like the function @{text atom}, the function @{text "atoms"} coerces 
-  a set of atoms to a set of the generic atom type. 
-  It is defined as  @{text "atoms as \<equiv> {atom a | a \<in> as}"}. 
-  The set @{text B} in \eqref{fadef} is then formally defined as
-  
-  \begin{equation}\label{bdef}
-  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
-  \end{equation}\smallskip
-
-  \noindent 
-  where we use the auxiliary binding functions from \eqref{bnaux} for shallow 
-  binders (that means when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
-  @{text "atom list"}). 
-
-  The set @{text "B'"} in \eqref{fadef} collects all free atoms in
-  non-recursive deep binders. Let us assume these binders in the binding 
-  clause @{text "bc\<^isub>i"} are
-
-  \[
-  \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
-  \]\smallskip
-  
-  \noindent
-  with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and 
-  none of the @{text "l"}$_{1..r}$ being among the bodies
-  @{text "d"}$_{1..q}$. The set @{text "B'"} is defined as
-  
-  \begin{equation}\label{bprimedef}
-  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
-  \end{equation}\smallskip
-  
-  \noindent
-  This completes all clauses for the free-atom functions @{text "fa_ty"}$_{1..n}$.
-
-  Note that for non-recursive deep binders, we have to add in \eqref{fadef}
-  the set of atoms that are left unbound by the binding functions @{text
-  "bn"}$_{1..m}$. We used for
-  the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The
-  definition for those functions needs to be extracted from the clauses the
-  user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text
-  bn}-clause of the form
-  
-  \[
-  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  \]\smallskip
-  
-  \noindent
-  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For 
-  each of the arguments we calculate the free atoms as follows:
-  
-  \[\mbox{
-  \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-  $\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}\\ 
-  & (that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\smallskip\\
-  $\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"}
-  with the recursive call @{text "bn\<^isub>i z\<^isub>i"}\\
-  & (that means whatever is `left over' from the @{text "bn"}-function is free)\smallskip\\
-  $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-  but without a recursive call\\
-  & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
-  \end{tabular}}
-  \]\smallskip
-  
-  \noindent
-  For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
- 
-  To see how these definitions work in practice, let us reconsider the
-  term-constructors @{text "Let"} and @{text "Let_rec"} shown in
-  \eqref{letrecs} together with the term-constructors for assignments @{text
-  "ANil"} and @{text "ACons"}. Since there is a binding function defined for
-  assignments, we have three free-atom functions, namely @{text
-  "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
-  "fa\<^bsub>bn\<^esub>"} as follows:
-  
-  \[\mbox{
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
-  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\
-
-  @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\
-  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
-
-  @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\
-  @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
-  \end{tabular}}
-  \]\smallskip
-
-
-  \noindent
-  Recall that @{text ANil} and @{text "ACons"} have no binding clause in the
-  specification. The corresponding free-atom function @{text
-  "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms of an assignment
-  (in case of @{text "ACons"}, they are given in terms of @{text supp}, @{text
-  "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). The binding
-  only takes place in @{text Let} and @{text "Let_rec"}. In case of @{text
-  "Let"}, the binding clause specifies that all atoms given by @{text "set (bn
-  as)"} have to be bound in @{text t}. Therefore we have to subtract @{text
-  "set (bn as)"} from @{text "fa\<^bsub>trm\<^esub> t"}. However, we also need
-  to add all atoms that are free in @{text "as"}. This is in contrast with
-  @{text "Let_rec"} where we have a recursive binder to bind all occurrences
-  of the atoms in @{text "set (bn as)"} also inside @{text "as"}. Therefore we
-  have to subtract @{text "set (bn as)"} from both @{text
-  "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}. Like the
-  function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses
-  the list of assignments, but instead returns the free atoms, which means in
-  this example the free atoms in the argument @{text "t"}.
-
-
-  An interesting point in this example is that a `naked' assignment (@{text
-  "ANil"} or @{text "ACons"}) does not bind any atoms, even if the binding
-  function is specified over assignments. Only in the context of a @{text Let}
-  or @{text "Let_rec"}, where the binding clauses are given, will some atoms
-  actually become bound.  This is a phenomenon that has also been pointed out
-  in \cite{ott-jfp}. For us this observation is crucial, because we would not
-  be able to lift the @{text "bn"}-functions to alpha-equated terms if they
-  act on atoms that are bound. In that case, these functions would \emph{not}
-  respect alpha-equivalence.
-
-  Having the free-atom functions at our disposal, we can next define the 
-  alpha-equivalence relations for the raw types @{text
-  "ty"}$_{1..n}$. We write them as
-  
-  \[
-  \mbox{@{text "\<approx>ty"}$_{1..n}$}.
-  \]\smallskip
-  
-  \noindent
-  Like with the free-atom functions, we also need to
-  define auxiliary alpha-equivalence relations 
-  
-  \[
-  \mbox{@{text "\<approx>bn\<^isub>"}$_{1..m}$}
-  \]\smallskip
-  
-  \noindent
-  for the binding functions @{text "bn"}$_{1..m}$, 
-  To simplify our definitions we will use the following abbreviations for
-  \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples.
-  
-  \[\mbox{
-  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (y\<^isub>1,\<dots>, y\<^isub>n)"} & @{text "\<equiv>"} &
-  @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n y\<^isub>n"}\\
-  @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
-  \end{tabular}}
-  \]\smallskip
-
-
-  The alpha-equivalence relations are defined as inductive predicates
-  having a single clause for each term-constructor. Assuming a
-  term-constructor @{text C} is of type @{text ty} and has the binding clauses
-  @{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form
-  
-  \begin{equation}\label{gform}
-  \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
-  {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} 
-  \end{equation}\smallskip
-
-  \noindent
-  The task below is to specify what the premises corresponding to a binding
-  clause are. To understand better what the general pattern is, let us first 
-  treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause 
-  of the form
-
-  \[
-  \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \]\smallskip
-
-  \noindent
-  In this binding clause no atom is bound and we only have to `alpha-relate'
-  the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>,
-  d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
-  whereby the labels @{text "d"}$_{1..q}$ refer to some of the arguments @{text
-  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of the @{text
-  "z\<PRIME>"}$_{1..n}$ in \eqref{gform}. In order to relate two such
-  tuples we define the compound alpha-equivalence relation @{text "R"} as
-  follows
-
-  \begin{equation}\label{rempty}
-  \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
-  \end{equation}\smallskip
-
-  \noindent
-  with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding
-  labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a
-  recursive argument of @{text C} and have type @{text "ty\<^isub>i"}; otherwise
-  we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the
-  latter is because @{text "ty\<^isub>i"} is then not part of the specified types
-  and alpha-equivalence of any previously defined type is supposed to coincide
-  with equality.  This lets us now define the premise for an empty binding
-  clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be
-  unfolded to the series of premises
-  
-  \[
-  @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}.
-  \]\smallskip
-  
-  \noindent
-  We will use the unfolded version in the examples below.
-
-  Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form 
-  
-  \begin{equation}\label{nonempty}
-  \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \end{equation}\smallskip
-
-  \noindent
-  In this case we define a premise @{text P} using the relation
-  $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly
-  $\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and 
-  $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other
-  binding modes). 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}}^{\textit{R}, \textit{fa}}$  we also need
-  a compound free-atom function for the bodies defined as
-  
-  \[
-  \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
-  \]\smallskip
-
-  \noindent
-  with the assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
-  The last ingredient we need are the sets of atoms bound in the bodies.
-  For this we take
-
-  \[
-  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
-  \]\smallskip
-
-  \noindent
-  Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This 
-  lets us formally define the premise @{text P} for a non-empty binding clause as:
-  
-  \[
-  \mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
-  \]\smallskip
-
-  \noindent
-  This premise accounts for alpha-equivalence of the bodies of the binding
-  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 relations @{text "\<approx>bn"}$_{1..m}$ (which we
-  will define shortly).  Let us assume the non-recursive deep binders
-  in @{text "bc\<^isub>i"} are
-  
-  \[
-  @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
-  \]\smallskip
-  
-  \noindent
-  The tuple @{text L} consists then of all these binders @{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
-  
-  \[
-  @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}
-  \]\smallskip
-
-  \noindent 
-  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
-  
-  \[
-  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  \]\smallskip
-  
-  \noindent
-  where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
-  then the corresponding alpha-equivalence clause for @{text "\<approx>bn"} has the form
-  
-  \[
-  \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
-  {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
-  \]\smallskip
-  
-  \noindent
-  In this clause the relations @{text "R"}$_{1..s}$ are given by 
-
-  \[\mbox{
-  \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-  $\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and 
-  is a recursive argument of @{text C},\smallskip\\
-  $\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
-  and is a non-recursive argument of @{text C},\smallskip\\
-  $\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
-  with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\smallskip\\
-  $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
-  recursive call.
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  This completes the definition of alpha-equivalence. As a sanity check, we can show
-  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}}^{\textit{R}, \textit{fa}}$ and take @{text "0"}
-  for the existentially quantified permutation).
-
-  Again let us take a look at a concrete example for these definitions. For 
-  the specification shown in \eqref{letrecs}
-  we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$ with the following rules:
-
-  \begin{equation}\label{rawalpha}\mbox{
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & 
-  \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\\
-  \\
-  \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\
-  \\
-
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
-  \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
-  {@{text "a = a'"} & \hspace{5mm}@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
-  \end{tabular}\\
-  \\
-
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
-  \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
-  {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
-  \end{tabular}
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  \noindent
-  Notice 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. This is needed in the 
-  clause for @{text "Let"} (which 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 all components of an assignment are `under' the binder. 
-  Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above)
-  we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
-  equivalence relation and a compound free-atom function. This is because the
-  corresponding binding clause specifies a binder with two bodies, namely
-  @{text "as"} and @{text "t"}.
-*}
-
-section {* Establishing the Reasoning Infrastructure *}
-
-text {*
-  Having made all necessary definitions for raw terms, we can start with
-  establishing the reasoning infrastructure for the alpha-equated types @{text
-  "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We
-  give in this section and the next the proofs we need for establishing this
-  infrastructure. One point of our work is that we have completely
-  automated these proofs in Isabelle/HOL.
-
-  First we establish that the free-variable functions, the binding functions and the
-  alpha-equi\-va\-lences are equivariant.
-
-  \begin{lem}\mbox{}\\
-  @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and
-  @{text "bn"}$_{1..m}$ are equivariant.\\
-  @{text "(ii)"} The relations @{text "\<approx>ty"}$_{1..n}$ and
-  @{text "\<approx>bn"}$_{1..m}$ are equivariant.
-  \end{lem}
-
-  \begin{proof}
-  The function package of Isabelle/HOL allows us to prove the first part by
-  mutual induction over the definitions of the functions.\footnote{We have
-  that the free-atom functions are terminating. From this the function
-  package derives an induction principle~\cite{Krauss09}.} The second is by a
-  straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and
-  @{text "\<approx>bn"}$_{1..m}$ using the first part.
-  \end{proof}
-
-  \noindent
-  Next we establish that the alpha-equivalence relations defined in the
-  previous section are indeed equivalence relations.
-
-  \begin{lem}\label{equiv} 
-  The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
-  equivalence relations.
-  \end{lem}
-
-  \begin{proof} 
-  The proofs are by induction. The non-trivial
-  cases involve premises built up by $\approx_{\textit{set}}$, 
-  $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 
-  can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
-  case needs in addition the fact that the relations are equivariant. 
-  \end{proof}
-
-  \noindent 
-  We can feed the last lemma into our quotient package and obtain new types
-  @{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..k}$ from the raw term-constructors @{text
-  "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
-  "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
-  binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
-  are not really useful to the user, since they are given in terms of the
-  isomorphisms we obtained by creating new types in Isabelle/HOL (recall the
-  picture shown in the Introduction).
-
-  The first useful property for the user is the fact that distinct 
-  term-constructors are not equal, that is the property
-  
-  \begin{equation}\label{distinctalpha}
-  \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~% 
-  @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 
-  \end{equation}\smallskip
-  
-  \noindent
-  whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
-  In order to derive this property, we use the definition of alpha-equivalence
-  and establish that
-  
-  \begin{equation}\label{distinctraw}
-  \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
-  \end{equation}\smallskip
-
-  \noindent
-  holds for the corresponding raw term-constructors.
-  In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
-  package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 
-  are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
-  Given, for example, @{text "C"} is of type @{text "ty"} with argument types
-  @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
-  
-  \[\mbox{
-  @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  }\]\smallskip
-
-  \noindent
-  holds under the assumptions \mbox{@{text
-  "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
-  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 
-  (similarly for @{text "D"}). For this we have to show
-  by induction over the definitions of alpha-equivalences the following 
-  auxiliary implications
-
-  \begin{equation}\label{fnresp}\mbox{
-  \begin{tabular}{lll}
-  @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
-  @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
-  \end{tabular}
-  }\end{equation}\smallskip
-  
-  \noindent
-  whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}
-  is defined. Whereas the first, second and last implication are true by
-  how we stated our definitions, the third \emph{only} holds because of our
-  restriction imposed on the form of the binding functions---namely \emph{not}
-  to return any bound atoms. In Ott, in contrast, the user may define @{text
-  "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
-  implication is \emph{not} true. A result is that in general the lifting of the
-  corresponding binding functions in Ott to alpha-equated terms is impossible.
-  Having established respectfulness for the raw term-constructors, the 
-  quotient package is able to automatically deduce \eqref{distinctalpha} from 
-  \eqref{distinctraw}.
-
-  Next we can lift the permutation operations defined in \eqref{ceqvt}. In
-  order to make this lifting to go through, we have to show that the
-  permutation operations are respectful. This amounts to showing that the
-  alpha-equivalence relations are equivariant, which
-  we already established in Lemma~\ref{equiv}. As a result we can add the
-  equations
-  
-  \begin{equation}\label{calphaeqvt}
-  @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
-  \end{equation}\smallskip
-
-  \noindent
-  to our infrastructure. In a similar fashion we can lift the defining equations
-  of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
-  @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-  "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
-  The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
-  by the datatype package of Isabelle/HOL.
-
-  We also need to lift the properties that characterise when two raw terms of the form
-  
-  \[
-  \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
-  \]\smallskip
-
-  \noindent
-  are alpha-equivalent. This gives us conditions when the corresponding
-  alpha-equated terms are \emph{equal}, namely
-  
-  \[
-  @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
-  \]\smallskip
-  
-  \noindent
-  We call these conditions \emph{quasi-injectivity}. They correspond to the
-  premises in our alpha-equiva\-lence relations, except that the
-  relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
-  the free-atom and binding functions are replaced by their lifted
-  counterparts). Recall the alpha-equivalence rules for @{text "Let"} and
-  @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and
-  @{text "Let_rec\<^sup>\<alpha>"} we have
-
-  \begin{equation}\label{alphalift}\mbox{
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
-  {@{term "alpha_lst_ex (bn_al as, t) equal fa_trm_al (bn as', t')"} & 
-  \hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
-  \\
-  \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
-  {@{term "alpha_lst_ex (bn_al as, ast) equ2 fa_trm2_al (bn_al as', ast')"}}}\\
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  We can also add to our infrastructure cases lemmas and a (mutual)
-  induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
-  lemmas allow the user to deduce a property @{text "P"} by exhaustively
-  analysing how an element of a type, say @{text "ty\<AL>"}$_i$, can be
-  constructed (that means one case for each of the term-constructors in @{text
-  "ty\<AL>"}$_i\,$). The lifted cases lemma for a type @{text
-  "ty\<AL>"}$_i\,$ looks as follows
-
-  \begin{equation}\label{cases}
-  \infer{P}
-  {\begin{array}{l}
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
-  \hspace{5mm}\vdots\\
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
-  \end{array}}
-  \end{equation}\smallskip
-
-  \noindent
-  where @{text "y"} is a variable of type @{text "ty\<AL>"}$_i$ and @{text "P"} is the 
-  property that is established by the case analysis. Similarly, we have a (mutual) 
-  induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the 
-  form
-
-   \begin{equation}\label{induct}
-  \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
-  {\begin{array}{l}
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
-  \hspace{5mm}\vdots\\
-  @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
-  \end{array}}
-  \end{equation}\smallskip
-
-  \noindent
-  whereby the @{text P}$_{1..n}$ are the properties established by the
-  induction, and the @{text y}$_{1..n}$ are of type @{text
-  "ty\<AL>"}$_{1..n}$. Note that for the term constructor @{text
-  "C"}$^\alpha_1$ the induction principle has a hypothesis of the form
-
-  \[
-  \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}} 
-  \]\smallskip
-
-  \noindent 
-  in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are the
-  recursive arguments of this term constructor (similarly for the other
-  term-constructors). 
-
-  Recall the lambda-calculus with @{text "Let"}-patterns shown in
-  \eqref{letpat}. The cases lemmas and the induction principle shown in
-  \eqref{cases} and \eqref{induct} boil down in that example to the following three inference
-  rules:
-
-  \begin{equation}\label{inductex}\mbox{
-  \begin{tabular}{c}
-  \multicolumn{1}{@ {\hspace{-5mm}}l}{cases lemmas:}\smallskip\\
-  \infer{@{text "P\<^bsub>trm\<^esub>"}}
-  {\begin{array}{@ {}l@ {}}
-   @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-   \end{array}}\hspace{10mm}
-
-  \infer{@{text "P\<^bsub>pat\<^esub>"}}
-  {\begin{array}{@ {}l@ {}}
-   @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
-  \end{array}}\medskip\\
-
-  \multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\
-  
-  \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
-  {\begin{array}{@ {}l@ {}}
-   @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
-  \end{array}}
-  \end{tabular}}
-  \end{equation}\smallskip
-
-  By working now completely on the alpha-equated level, we
-  can first show using \eqref{calphaeqvt} and Property~\ref{swapfreshfresh} that the support of each term
-  constructor is included in the support of its arguments, 
-  namely
-
-  \[
-  @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
-  \]\smallskip
-
-  \noindent
-  This allows us to prove using the induction principle for  @{text "ty\<AL>"}$_{1..n}$ 
-  that every element of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported 
-  (using Proposition~\ref{supportsprop}{\it (i)}). 
-  Similarly, we can establish by induction that the free-atom functions and binding 
-  functions are equivariant, namely
-  
-  \[\mbox{
-  \begin{tabular}{rcl}
-  @{text "\<pi> \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (\<pi> \<bullet> x)"}\\
-  @{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
-  @{text "\<pi> \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
-  \end{tabular}}
-  \]\smallskip
-
-  
-  \noindent
-  Lastly, we can show that the support of elements in @{text
-  "ty\<AL>"}$_{1..n}$ is the same as the free-atom functions @{text
-  "fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting where
-  the general theory is formulated in terms of support and freshness, but also
-  provides evidence that our notions of free-atoms and alpha-equivalence
-  `match up' correctly.
-
-  \begin{thm}\label{suppfa} 
-  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{thm}
-
-  \begin{proof}
-  The proof is by induction on @{text "x"}$_{1..n}$. In each case
-  we unfold the definition of @{text "supp"}, move the swapping inside the 
-  term-constructors and then use the quasi-injectivity lemmas in order to complete the
-  proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
-  for which we have to know that every body of an abstraction is finitely supported.
-  This, we have proved earlier.
-  \end{proof}
-
-  \noindent
-  Consequently, we can replace the free-atom functions by @{text "supp"} in  
-  our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance,
-  we obtain for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} 
-
-  \[\mbox{
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
-  {@{term "alpha_lst_ex (bn_al as, t) equal supp (bn_al as', t')"} & 
-  \hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
-  \\
-  \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
-  {@{term "alpha_lst_ex (bn_al as, ast) equ2 supp2 (bn_al as', ast')"}}}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  Taking into account that the compound equivalence relation @{term
-  "equ2"} and the compound free-atom function @{term "supp2"} are by
-  definition equal to @{term "equal"} and @{term "supp"}, respectively, the
-  above rules simplify further to
-
-  \[\mbox{
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let\<^sup>\<alpha> as t = Let\<^sup>\<alpha> as' t'"}}
-  {@{term "Abs_lst (bn_al as) t = Abs_lst (bn_al as') t'"} & 
-  \hspace{5mm}@{text "as \<approx>\<AL>\<^bsub>bn\<^esub> as'"}}\\
-  \\
-  \makebox[0mm]{\infer{@{text "Let_rec\<^sup>\<alpha> as t = Let_rec\<^sup>\<alpha> as' t'"}}
-  {@{term "Abs_lst (bn_al as) ast = Abs_lst (bn_al as') ast'"}}}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  which means we can characterise equality between term-constructors (on the
-  alpha-equated level) in terms of equality between the abstractions defined
-  in Section~\ref{sec:binders}. From this we can deduce the support for @{text
-  "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}, namely
-
-
-  \[\mbox{
-  \begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
-  @{text "supp (Let\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t - set (bn\<^sup>\<alpha> as)) \<union> fa\<AL>\<^bsub>bn\<^esub> as"}\\
-  @{text "supp (Let_rec\<^sup>\<alpha> as t)"} & @{text "="} & @{text "(supp t \<union> supp as) - set (bn\<^sup>\<alpha> as)"}\\
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  using the support of abstractions derived in Theorem~\ref{suppabs}.
-
-  To sum up this section, we have established a reasoning infrastructure for the
-  types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
-  `raw' level to the quotient level and then by proving facts about
-  these lifted definitions. All necessary proofs are generated automatically
-  by custom ML-code.
-*}
-
-
-section {* Strong Induction Principles *}
-
-text {*
-  In the previous section we derived induction principles for alpha-equated
-  terms (see \eqref{induct} for the general form and \eqref{inductex} for an
-  example). This was done by lifting the corresponding inductions principles
-  for `raw' terms.  We already employed these induction principles for
-  deriving several facts about alpha-equated terms, including the property that
-  the free-atom functions and the notion of support coincide. Still, we
-  call these induction principles \emph{weak}, because for a term-constructor,
-  say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
-  hypothesis requires us to establish (under some assumptions) a property
-  @{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
-  "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
-  any assumptions about the atoms that are bound---for example assuming the variable convention. 
-  One obvious way around this
-  problem is to rename bound atoms. Unfortunately, this leads to very clunky proofs
-  and makes formalisations grievous experiences (especially in the context of 
-  multiple bound atoms).
-
-  For the older versions of Nominal Isabelle we described in \cite{Urban08} a
-  method for automatically strengthening weak induction principles. These
-  stronger induction principles allow the user to make additional assumptions
-  about bound atoms. The advantage of these assumptions is that they make in
-  most cases any renaming of bound atoms unnecessary.  To explain how the
-  strengthening works, we use as running example the lambda-calculus with
-  @{text "Let"}-patterns shown in \eqref{letpat}. Its weak induction principle
-  is given in \eqref{inductex}.  The stronger induction principle is as
-  follows:
-
-  \begin{equation}\label{stronginduct}
-  \mbox{
-  \begin{tabular}{@ {}c@ {}}
-  \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"}}
-  {\begin{array}{l}
-   @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ 
-   \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
-  \end{array}}
-  \end{tabular}}
-  \end{equation}\smallskip
-
-
-  \noindent
-  Notice that instead of establishing two properties of the form @{text "
-  P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the
-  weak one does, the stronger induction principle establishes the properties
-  of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \<and>
-  P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text
-  c} is assumed to be of finite support. The purpose of @{text "c"} is to
-  `control' which freshness assumptions the binders should satisfy in the
-  @{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text
-  "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
-  for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
-  all bound atoms from an assignment are fresh for @{text "c"} (fourth
-  line). In order to see how an instantiation for @{text "c"} in the
-  conclusion `controls' the premises, one has to take into account that
-  Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
-  with, for example, a pair, then this type-constraint will be propagated to
-  the premises. The main point is that if @{text "c"} is instantiated
-  appropriately, then the user can mimic the usual convenient `pencil-and-paper'
-  reasoning employing the variable convention about bound and free variables
-  being distinct \cite{Urban08}.
-
-  In what follows we will show that the weak induction principle in
-  \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
-  single binders in \cite{Urban08} by some quite involved, nevertheless
-  automated, induction proof. In this paper we simplify the proof by
-  leveraging the automated proving tools from the function package of
-  Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these tools
-  is well-founded induction. To use them in our setting, we have to discharge
-  two proof obligations: one is that we have well-founded measures (one for
-  each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
-  step and the other is that we have covered all cases in the induction
-  principle. Once these two proof obligations are discharged, the reasoning
-  infrastructure of the function package will automatically derive the
-  stronger induction principle. This way of establishing the stronger induction
-  principle is considerably simpler than the earlier work presented in \cite{Urban08}.
-
-  As measures we can use 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 the sizes decrease in every
-  induction step. What is left to show is that we covered all cases. 
-  To do so, we have to derive stronger cases lemmas, which look in our
-  running example as follows:
-
-  \[\mbox{
-  \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
-  \infer{@{text "P\<^bsub>trm\<^esub>"}}
-  {\begin{array}{@ {}l@ {}}
-   @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-   \end{array}} &
-
-  \infer{@{text "P\<^bsub>pat\<^esub>"}}
-  {\begin{array}{@ {}l@ {}}
-   @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
-   @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
-  \end{array}}
-  \end{tabular}}
-  \]\smallskip 
-
-  \noindent
-  They are stronger in the sense that they allow us to assume in the @{text
-  "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
-  avoid, or are fresh for, a context @{text "c"} (which is assumed to be finitely supported).
-  
-  These stronger cases lemmas can be derived from the `weak' cases lemmas
-  given in \eqref{inductex}. This is trivial in case of patterns (the one on
-  the right-hand side) since the weak and strong cases lemma coincide (there
-  is no binding in patterns).  Interesting are only the cases for @{text
-  "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
-  therefore have an additional assumption about avoiding @{text "c"}.  Let us
-  first establish the case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
-  \eqref{inductex} we can assume that
-
-  \begin{equation}\label{assm}
-  @{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
-  \end{equation}\smallskip
-
-  \noindent
-  holds, and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the 
-  corresponding implication 
-
-  \begin{equation}\label{imp}
-  @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-  \end{equation}\smallskip
-
-  \noindent
-  which we must use in order to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
-  use this implication directly, because we have no information whether or not @{text
-  "x\<^isub>1"} is fresh for @{text "c"}.  However, we can use Properties
-  \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}. We know
-  by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
-  x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
-  {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
-  permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
-  c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
-  By using Property \ref{supppermeq}, we can infer from the latter that 
-
-  \[
-  @{text "Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"} 
-  \]\smallskip
-
-  \noindent
-  holds. We can use this equation in the assumption \eqref{assm}, and hence
-  use the implication \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
-  and @{text "\<pi> \<bullet> x\<^isub>2"} for concluding this case.
-
-  The @{text "Let_pat\<^sup>\<alpha>"}-case involving a deep binder is slightly more complicated.
-  We have the assumption
-
-  \begin{equation}\label{assmtwo}
-  @{text "y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
-  \end{equation}\smallskip
-
-  \noindent
-  and the implication from the stronger cases lemma
-
-  \begin{equation}\label{impletpat}
-  @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
-  \end{equation}\smallskip
-
-  \noindent
-  The reason that this case is more complicated is that we cannot directly apply Property 
-  \ref{avoiding} for obtaining a renaming permutation. Property \ref{avoiding} requires
-  that the binders are fresh for the term in which we want to perform the renaming. But
-  this is not true in terms such as (using an informal notation)
-
-  \[
-  @{text "Let (x, y) := (x, y) in (x, y)"}
-  \]\smallskip
-
-  \noindent
-  where @{text x} and @{text y} are bound in the term, but are also free
-  in the right-hand side of the assignment. We can, however, obtain such a renaming permutation, say
-  @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
-  x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
-  \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet> x\<^isub>3) =
-  Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text
-  "bn\<^sup>\<alpha>"} are equivariant).  Now the quasi-injective property for @{text
-  "Let_pat\<^sup>\<alpha>"} states that
-
-  \[
-  \infer{@{text "Let_pat\<^sup>\<alpha> p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\<alpha> p\<PRIME> t\<PRIME>\<^isub>1 t\<PRIME>\<^isub>2"}}
-  {@{text "[bn\<^sup>\<alpha> p]\<^bsub>list\<^esub>. t\<^isub>2 = [bn\<^sup>\<alpha> p']\<^bsub>list\<^esub>. t\<PRIME>\<^isub>2"}\;\; & 
-  @{text "p \<approx>\<AL>\<^bsub>bn\<^esub> p\<PRIME>"}\;\; & @{text "t\<^isub>1 = t\<PRIME>\<^isub>1"}}
-  \]\smallskip
-
-  \noindent
-  Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}, we can infer
-  that @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
-
-  \[
-  @{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}  
-  \]\smallskip
-  
-  \noindent
-  Taking the left-hand side in the assumption shown in \eqref{assmtwo}, we can use
-  the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
-
-  The remaining difficulty is when a deep binder contains some atoms that are
-  bound and some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
-  \eqref{letrecs}.  In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
-  \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea however is
-  that @{text "\<pi>"} only renames atoms that become bound. In this way @{text "\<pi>"}
-  does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} (which only tracks alpha-equivalence of terms that are not
-  under the binder). However, the problem is that the
-  permutation operation @{text "\<pi> \<bullet> x\<^isub>1"} applies to all atoms in @{text "x\<^isub>1"}. To avoid this
-  we introduce an auxiliary permutation operations, written @{text "_
-  \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
-  more precisely the atoms specified by the @{text "bn"}-functions) and leaves
-  the other atoms unchanged. Like the functions @{text "fa_bn"}$_{1..m}$, we
-  can define these permutation operations over raw terms analysing how the functions @{text
-  "bn"}$_{1..m}$ are defined. Assuming the user specified a clause
-
-  \[  
-  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
-  \]\smallskip
-
-  \noindent
-  we define @{text "\<pi> \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} with @{text "y\<^isub>i"} determined as follows:
-
-  \[\mbox{
-  \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> \<pi> \<bullet>\<^bsub>bn\<^esub> x\<^isub>i"} provided @{text "bn x\<^isub>i"} is in @{text "rhs"}\\
-  $\bullet$ & @{text "y\<^isub>i \<equiv> \<pi> \<bullet> x\<^isub>i"} otherwise
-  \end{tabular}}
-  \]\smallskip
-
-  \noindent
-  Using again the quotient package  we can lift the auxiliary permutation operations
-  @{text "_ \<bullet>\<^bsub>bn\<^esub> _"}
-  to alpha-equated terms. Moreover we can prove the following two properties:
-
-  \begin{lem}\label{permutebn} 
-  Given a binding function @{text "bn\<^sup>\<alpha>"} and auxiliary equivalence @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"} 
-  then for all @{text "\<pi>"}\smallskip\\
-  {\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\ 
-  {\it (ii)} @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.
-  \end{lem}
-
-  \begin{proof} 
-  By induction on @{text x}. The properties follow by 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 states that @{text "_ \<bullet>\<AL>\<^bsub>bn\<^esub> _"} preserves
-  @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}.  The main point of the auxiliary
-  permutation functions is that they allow us to rename just the bound atoms in a
-  term, without changing anything else.
-  
-  Having the auxiliary permutation function in place, we can now solve all remaining cases. 
-  For the @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding} 
-  obtain a @{text "\<pi>"} such that 
-
-  \[
-  @{text "(\<pi> \<bullet> (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c"} \hspace{10mm}
-  @{text "\<pi> \<bullet> [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2 = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"} 
-  \]\smallskip
-
-  \noindent
-  hold. Using the first part of Lemma \ref{permutebn}, we can simplify this
-  to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and 
-  \mbox{@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}}. Since
-  @{text "(\<pi>  \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by the second part,
-  we can infer that
-
-  \[
-  @{text "Let\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}  
-  \]\smallskip
-
-  \noindent
-  holds. This allows us to use the implication from the strong cases
-  lemma, and we are done.
-
-  Consequently,  we can discharge all proof-obligations about having `covered all
-  cases'. This completes the proof establishing that the weak induction principles imply 
-  the strong induction principles. These strong induction principles have already proved 
-  being very useful in practice, particularly for proving properties about 
-  capture-avoiding substitution \cite{Urban08}. 
-*}
-
-
-section {* Related Work\label{related} *}
-
-text {*
-  To our knowledge the earliest usage of general binders in a theorem prover
-  is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with a
-  formalisation of the algorithm W. This formalisation implements binding in
-  type-schemes using a de-Bruijn indices representation. Since type-schemes in
-  W contain only a single place where variables are bound, different indices
-  do not refer to different binders (as in the usual de-Bruijn
-  representation), but to different bound variables. A similar idea has been
-  recently explored for general binders by Chargu\'eraud \cite{chargueraud09}
-  in the locally nameless approach to
-  binding.  There, de-Bruijn indices consist of two
-  numbers, one referring to the place where a variable is bound, and the other
-  to which variable is bound. The reasoning infrastructure for both
-  representations of bindings comes for free in theorem provers like
-  Isabelle/HOL and Coq, since the corresponding term-calculi can be implemented
-  as `normal' 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. We are not aware of any formalisation of 
-  a non-trivial language that uses Chargu\'eraud's idea.
-
-  Another technique for representing binding is higher-order abstract syntax
-  (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. 
-  This representation technique supports very elegantly many aspects of
-  \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} 
-  has been done that uses HOAS for mechanising the metatheory of SML. We
-  are, however, not aware how multiple binders of SML are represented in this
-  work. Judging from the submitted Twelf-solution for the POPLmark challenge,
-  HOAS cannot easily deal with binding constructs where the number of bound
-  variables is not fixed. For example, in the second part of this challenge,
-  @{text "Let"}s involve patterns that bind multiple variables at once. In
-  such situations, HOAS seems to have to resort to the
-  iterated-single-binders-approach with all the unwanted consequences when
-  reasoning about the resulting terms.
-
-
-  Two formalisations involving general binders have been 
-  performed in older
-  versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
-  \cite{BengtsonParow09,UrbanNipkow09}).  Both
-  use the approach based on iterated single binders. Our experience with
-  the latter formalisation has been disappointing. The major pain arose from
-  the need to `unbind' bound variables and the resulting formal reasoning turned out to
-  be rather unpleasant. In contrast, the unbinding can be 
-  done in one step with our
-  general binders described in this paper.
-
-  The most closely related work to the one presented here is the Ott-tool by
-  Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
-  \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
-  from specifications of term-calculi involving general binders. For a subset
-  of the specifications Ott can also generate theorem prover code using a `raw'
-  representation of terms, and in Coq also a locally nameless
-  representation. The developers of this tool have also put forward (on paper)
-  a definition for alpha-equivalence and free variables for terms that can be
-  specified in Ott.  This definition is rather different from ours, not using
-  any nominal techniques.  To our knowledge there is no concrete mathematical
-  result concerning this notion of alpha-equivalence and free variables. We
-  have proved that our definitions lead to alpha-equated terms, whose support
-  is as expected (that means bound atoms are removed from the support). We
-  also showed that our specifications lift from `raw' terms to 
-  alpha-equivalence classes. For this we have established (automatically) that every
-  term-constructor and function defined for `raw' terms 
-  is respectful w.r.t.~alpha-equivalence.
-
-  Although we were heavily inspired by the syntax of Ott, its definition of
-  alpha-equi\-valence is unsuitable for our extension of Nominal
-  Isabelle. First, it is far too complicated to be a basis for automated
-  proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
-  of binders depending on other binders, which just do not make sense for our
-  alpha-equated terms (the corresponding @{text "fa"}-functions would not lift). 
-  Third, it allows empty types that have no meaning in a
-  HOL-based theorem prover. We also had to generalise slightly Ott's binding
-  clauses. In Ott one specifies binding clauses with a single body; we allow
-  more than one. We have to do this, because this makes a difference for our
-  notion of alpha-equivalence in case of \isacommand{binds (set)} and
-  \isacommand{binds (set+)}. Consider the examples
-  
-  \[\mbox{
-  \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-  @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
-      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
-  @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
-      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
-      \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
-  \end{tabular}}
-  \]\smallskip
-  
-  \noindent
-  In the first term-constructor we have a single body that happens to be
-  `spread' over two arguments; in the second term-constructor we have two
-  independent bodies in which the same variables are bound. As a result we
-  have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
-  make @{text "(a, b)"} equal with both @{text "(a, b)"} and @{text "(b, a)"}, but
-  there are two permutations so that we can make @{text "(a, b)"} and @{text
-  "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
-  a)"} with the other.}
-
-   
-  \[\mbox{
-  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
-  @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & 
-  @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}
-  \end{tabular}}
-  \]\smallskip
- 
-  \noindent
-  but 
-
-  \[\mbox{
-  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
-  @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
-  @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
-  \end{tabular}}
-  \]\smallskip
-  
-  \noindent
-  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 the Core-Haskell
-  language from the Introduction. With the work presented in this
-  paper we can define it formally as shown in
-  Figure~\ref{nominalcorehas} and then Nominal Isabelle derives
-  automatically a corresponding reasoning infrastructure. However we
-  have found out that telescopes seem to not easily be representable
-  in our framework.  The reason is that we need to be able to lift our
-  @{text bn}-functions to alpha-equated lambda-terms and therefore
-  need to restrict what these @{text bn}-functions can return.
-  Telescopes can be represented in the framework described in
-  \cite{WeirichYorgeySheard11} using an extension of the usual
-  locally-nameless representation. 
-
-  \begin{figure}[p]
-  \begin{boxedminipage}{\linewidth}
-  \small
-  \begin{tabular}{l}
-  \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
-  \isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ 
-  \isacommand{and}~@{text "ckind ="}~@{text "CKSim ty ty"}\\
-  \isacommand{and}~@{text "ty ="}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
-  $|$~@{text "TFun string ty_list"}~%
-  $|$~@{text "TAll tv::tvar tkind ty::ty"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
-  $|$~@{text "TArr ckind ty"}\\
-  \isacommand{and}~@{text "ty_lst ="}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
-  \isacommand{and}~@{text "cty ="}~@{text "CVar cvar"}~%
-  $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-  $|$~@{text "CAll cv::cvar ckind cty::cty"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
-  $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
-  $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
-  $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
-  \isacommand{and}~@{text "co_lst ="}~@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
-  \isacommand{and}~@{text "trm ="}~@{text "Var var"}~$|$~@{text "K string"}\\
-  $|$~@{text "LAM_ty tv::tvar tkind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "LAM_cty cv::cvar ckind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
-  $|$~@{text "Lam v::var ty t::trm"}\hspace{3mm}\isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "Let x::var ty trm t::trm"}\hspace{3mm}\isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
-  $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
-  \isacommand{and}~@{text "assoc_lst ="}~@{text ANil}~%
-  $|$~@{text "ACons p::pat t::trm assoc_lst"}\hspace{3mm}\isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
-  \isacommand{and}~@{text "pat ="}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
-  \isacommand{and}~@{text "vt_lst ="}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
-  \isacommand{and}~@{text "tvtk_lst ="}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
-  \isacommand{and}~@{text "tvck_lst ="}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
-  \isacommand{binder}\\
-  \;@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
-  \;@{text "bv\<^isub>1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  \;@{text "bv\<^isub>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  \;@{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
-  \isacommand{where}\\
-  \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv\<^isub>3 tvts) @ (bv\<^isub>2 tvcs) @ (bv\<^isub>1 vs)"}\\
-  $|$~@{text "bv\<^isub>1 VTNil = []"}\\
-  $|$~@{text "bv\<^isub>1 (VTCons x ty tl) = (atom x)::(bv\<^isub>1 tl)"}\\
-  $|$~@{text "bv\<^isub>2 TVTKNil = []"}\\
-  $|$~@{text "bv\<^isub>2 (TVTKCons a ty tl) = (atom a)::(bv\<^isub>2 tl)"}\\
-  $|$~@{text "bv\<^isub>3 TVCKNil = []"}\\
-  $|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
-  \end{tabular}
-  \end{boxedminipage}
-  \caption{A definition for Core-Haskell in Nominal Isabelle. For the moment we
-  do not support nested types; therefore we explicitly have to unfold the 
-  lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that limitation, the 
-  definition follows closely the original shown in Figure~\ref{corehas}. The
-  point of our work is that having made such a definition in Nominal Isabelle,
-  one obtains automatically a reasoning infrastructure for Core-Haskell.
-  \label{nominalcorehas}}
-  \end{figure}
-  \afterpage{\clearpage}
-
-  Pottier presents a programming language, called C$\alpha$ml, for
-  representing terms with general binders inside OCaml \cite{Pottier06}. This
-  language is implemented as a front-end that can be translated to OCaml with
-  the help of a library. He presents a type-system in which the scope of
-  general binders can be specified using special markers, written @{text
-  "inner"} and @{text "outer"}. It seems our and his specifications can be
-  inter-translated as long as ours use the binding mode \isacommand{binds}
-  only.  However, we have not proved this. Pottier gives a definition for
-  alpha-equivalence, which also uses a permutation operation (like ours).
-  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} and more recently 
-  by Weirich et al \cite{WeirichYorgeySheard11}.
-
-  In a slightly different domain (programming with dependent types),
-  Altenkirch et al \cite{Altenkirch10} present a calculus with a notion of
-  alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
-  Their definition is similar to the one by Pottier, except that it has a more
-  operational flavour and calculates a partial (renaming) map. In this way,
-  the definition can deal with vacuous binders. However, to our best
-  knowledge, no concrete mathematical result concerning this definition of
-  alpha-equivalence has been proved.
-*}
-
-section {* Conclusion *}
-
-text {*
-
-  We have presented an extension of Nominal Isabelle for dealing with general
-  binders, that is where term-constructors have multiple bound atoms. For this
-  extension we introduced new definitions of alpha-equivalence and automated
-  all necessary proofs in Isabelle/HOL.  To specify general binders we used
-  the syntax from Ott, but extended it in some places and restricted
-  it in others so that the definitions make sense in the context of alpha-equated
-  terms. We also introduced two binding modes (set and set+) that do not exist
-  in Ott. We have tried out the extension with calculi such as Core-Haskell,
-  type-schemes and approximately a dozen of other typical examples from
-  programming language research~\cite{SewellBestiary}. The code will
-  eventually become part of the Isabelle distribution.\footnote{It 
-  can be downloaded already from \href{http://isabelle.in.tum.de/nominal/download}
-  {http://isabelle.in.tum.de/nominal/download}.}
-
-  We have left out a discussion about how functions can be defined over
-  alpha-equated terms involving general binders. In earlier versions of
-  Nominal Isabelle this turned out to be a thorny issue.  We hope to do better
-  this time by using the function package \cite{Krauss09} that has recently
-  been implemented in Isabelle/HOL and also by restricting function
-  definitions to equivariant functions (for them we can provide more
-  automation).
-
-  There are some restrictions we had
-  to impose in this paper that can be lifted using 
-  a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which
-  however is not yet part of the stable distribution.
-  This reimplementation allows nested
-  datatype definitions and would allow one to specify, for instance, the function kinds
-  in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
-  version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). We can 
-  also use it to represent the @{text "Let"}-terms from the Introduction where
-  the order of @{text "let"}-assignments does not matter. This means we can represent @{text "Let"}s
-  such that the following two terms are equal
-
-  \[
-  @{text "Let x\<^isub>1 = t\<^isub>1 and x\<^isub>2 = t\<^isub>2 in s"} \;\;=\;\;
-  @{text "Let x\<^isub>2 = t\<^isub>2 and x\<^isub>1 = t\<^isub>1 in s"} 
-  \]\smallskip
-
-  \noindent
-  For this we have to represent the @{text "Let"}-assignments as finite sets
-  of pair and a binding function that picks out the left components to be bound in @{text s}.
-
-  One line of future investigation is whether we can go beyond the 
-  simple-minded form of binding functions that we adopted from Ott. At the moment, binding
-  functions can only return the empty set, a singleton atom set or unions
-  of atom sets (similarly for lists). It remains to be seen whether 
-  properties like
-  
-  \[
-  \mbox{@{text "fa_ty x  =  bn x \<union> fa_bn x"}}
-  \]\smallskip
-  
-  \noindent
-  allow us to support more interesting binding functions. 
-  
-  We have also not yet played with other binding modes. For example we can
-  imagine that there is need for a binding mode where instead of usual lists,
-  we abstract lists of distinct elements (the corresponding type @{text
-  "dlist"} already exists in the library of Isabelle/HOL). We expect the
-  presented work can be extended to accommodate such binding modes.\medskip
-  
-  \noindent
-  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for many
-  discussions about Nominal Isabelle. We thank Peter Sewell for making the
-  informal notes \cite{SewellBestiary} available to us and also for patiently
-  explaining some of the finer points of the Ott-tool.  Stephanie Weirich
-  suggested to separate the subgrammars of kinds and types in our Core-Haskell
-  example. Ramana Kumar and Andrei Popescu helped us with comments for
-  an earlier version of this paper.
-*}
-
-
-(*<*)
-end
-(*>*)




