
diff -r a5da7b6aff8f -r 6f38e357b337 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 16 21:14:43 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2393 +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"
-  Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-  Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-
-definition
- "equal \<equiv> (op =)" 
-
-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 ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_res ("_ \<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 
-  Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
-  Abs_lst ("[_]\<^bsub>list\<^esub>._") and
-  Abs_dist ("[_]\<^bsub>#list\<^esub>._") 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 alpha_trm2 ::'a
-consts fa_trm2 :: 'a
-consts ast :: 'a
-consts ast' :: 'a
-notation (latex output) 
-  alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
-  fa_trm ("fa\<^bsub>trm\<^esub>") and
-  alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
-  fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
-  ast ("'(as, t')") and
-  ast' ("'(as', t\<PRIME> ')")
-
-(*>*)
-
-
-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"},
-  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{9mm}
-  @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
-  \end{array}
-  \end{equation}
-  %
-  \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, this leads to a rather clumsy
-  formalisation of W. 
-  %The need of iterating single binders is also one reason
-  %why Nominal Isabelle 
-  % and similar theorem provers that only provide
-  %mechanisms for binding single variables 
-  %has not fared extremely 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 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>{y, x}. y \<rightarrow> x"}\hspace{10mm}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
-  \end{equation}
-  %
-  \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}
-  %
-  \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 by
-  %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
-
-  However, the notion of $\alpha$-equivalence that is preserved by vacuous
-  binders is not always wanted. For example in terms like
-  %
-  \begin{equation}\label{one}
-  @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}
-  \end{equation}
-
-  \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 to regard
-  \eqref{one} as $\alpha$-equivalent with
-  %
-  \begin{center}
-  @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
-  \end{center}
-  %
-  \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}
-  %
-  \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
-  %
-  \begin{center}
-  @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
-  \end{center}
-  %
-  \noindent
-  As a result, we provide three general binding mechanisms each of which binds
-  multiple variables at once, and let the user chose which one is intended
-  in a formalisation.
-  %%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
-  %
-  \begin{center}
-  @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
-  \end{center}
-  %
-  \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
-  %
-  \begin{center}
-  @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}
-  \end{center}
-  %
-  \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
-  %
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
-  @{text trm} & @{text "::="}  & @{text "\<dots>"} 
-              & @{text "|"}  @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 
-                                 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm]
-  @{text assn} & @{text "::="} & @{text "\<ANIL>"}
-               &  @{text "|"}  @{text "\<ACONS>  name  trm  assn"}
-  \end{tabular}
-  \end{center}
-  %
-  \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
-  %
-  \begin{center}
-  @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} 
-  @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 
-  \end{center}
-  %
-  \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{bind} @{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}. 
-
-  %Though, Ott
-  %has only one binding mode, namely the one where the order of
-  %binders matters. Consequently, type-schemes with binding sets
-  %of names cannot be modelled in Ott.
-
-  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 @{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
-
-  \begin{center}
-  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 
-  \end{center}
-  
-  \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{center}
-  \begin{tikzpicture}[scale=0.89]
-  %\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.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
-  \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
-  \draw (1.8, 0.48) node[right=-0.1mm]
-    {\footnotesize\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 {\footnotesize\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{center}
-  %
-  \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
-  (non-emptiness is 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
-
-  \begin{center}
-  @{text "fv(x) = {x}"}\hspace{8mm}
-  @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
-  @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
-  \end{center}
-  
-  \noindent
-  then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
-  operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This
-  lifted function is characterised by the equations
-
-  \begin{center}
-  @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}
-  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}
-  @{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
-  \end{center}
-
-  \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 includes the term language of Core-Haskell. 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 specification of SML, which includes
-  %includes bindings as 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 automatic
-  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 derive strong 
-  induction principles that have the variable convention already built in.
-  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''.
-
-
-  %\begin{figure}
-  %\begin{boxedminipage}{\linewidth}
-  %%\begin{center}
-  %\begin{tabular}{r@ {\hspace{1mm}}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> "}\\
-  %& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
-  %& @{text "|"} & @{text "\<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>"}\\
-  %& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
-  %& @{text "|"} & @{text "\<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.\label{corehas}}
-  %\end{figure}
-*}
-
-section {* A Short Review of the Nominal Logic Work *}
-
-text {*
-  At its core, Nominal Isabelle is an adaption 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 "p, q, \<dots>"} to stand for
-  permutations. 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> _  ::  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 p} and @{term q} as \mbox{@{term "p + q"}}, 
-  and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-  operation is defined over the type-hierarchy \cite{HuffmanUrban10};
-  for example permutations acting on products, lists, sets, functions and booleans are
-  given by:
-  %
-  %\begin{equation}\label{permute}
-  %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
-  %\begin{tabular}{@ {}l@ {}}
-  %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
-  %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
-  %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
-  %\end{tabular} &
-  %\begin{tabular}{@ {}l@ {}}
-  %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-  %@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  %@{thm permute_bool_def[no_vars, THEN eq_reflection]}
-  %\end{tabular}
-  %\end{tabular}}
-  %\end{equation}
-  %
-  \begin{center}
-  \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
-  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
-  @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
-  @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  \end{tabular}
-  \end{tabular}}
-  \end{center}
-
-  \noindent
-  Concrete permutations in Nominal Isabelle are built up from swappings, 
-  written as \mbox{@{text "(a b)"}}, which are permutations that behave 
-  as follows:
-  %
-  \begin{center}
-  @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
-  \end{center}
-
-  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. The 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}
-
-  \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]}.
-  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 if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
-  then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
-  %
-  %\begin{myproperty}\label{swapfreshfresh}
-  %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
-  %\end{myproperty}
-  %
-  %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{center}
-  %\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 p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
-  %\end{tabular}
-  %\end{tabular}
-  %\end{center}
-  %
-  %\noindent 
-  %in some cases it can be difficult to characterise the support precisely, and
-  %only an approximation can be established (as for functions above). 
-  %
-  %Reasoning about
-  %such approximations can be simplified with the notion \emph{supports}, defined 
-  %as follows:
-  %
-  %\begin{definition}
-  %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{definition}
-  %
-  %\noindent
-  %The main point of @{text supports} is that we can establish the following 
-  %two properties.
-  %
-  %\begin{myproperty}\label{supportsprop}
-  %Given a set @{text "as"} of atoms.
-  %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
-  %{\it (ii)} @{thm supp_supports[no_vars]}.
-  %\end{myproperty}
-  %
-  %Another important notion in the nominal logic work is \emph{equivariance}.
-  %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
-  %it is required that every permutation leaves @{text f} unchanged, that is
-  %%
-  %\begin{equation}\label{equivariancedef}
-  %@{term "\<forall>p. p \<bullet> f = f"}
-  %\end{equation}
-  %
-  %\noindent or equivalently that a permutation applied to the application
-  %@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-  %functions @{text f}, we have for all permutations @{text p}:
-  %%
-  %\begin{equation}\label{equivariance}
-  %@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
-  %@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
-  %\end{equation}
-  % 
-  %\noindent
-  %From property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  %can easily deduce that equivariant functions have empty support. There is
-  %also a similar notion for equivariant relations, say @{text R}, namely the property
-  %that
-  %%
-  %\begin{center}
-  %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
-  %\end{center}
-  %
-  %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 
-  %Property~\ref{swapfreshfresh}
-  this property to rename single binders, it %%this property 
-  proved too unwieldy for dealing with multiple binders. For such binders the 
-  following generalisations turned out to be easier to use.
-
-  \begin{myproperty}\label{supppermeq}
-  @{thm[mode=IfThen] supp_perm_eq[no_vars]}
-  \end{myproperty}
-
-  \begin{myproperty}\label{avoiding}
-  For a finite set @{text as} and a finitely supported @{text x} with
-  @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
-  exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
-  @{term "supp x \<sharp>* p"}.
-  \end{myproperty}
-
-  \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 p} such that
-  the renamed binders @{term "p \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
-  as long as it is finitely supported) and also @{text "p"} does not affect anything
-  in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last 
-  fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
-  @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
-
-  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 
-  extensive use of these properties in order to define $\alpha$-equivalence in 
-  the presence of multiple binders.
-*}
-
-
-section {* General Bindings\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 write 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 x} and @{text y} need to have the same set of free
-  atoms; moreover there must be a permutation @{text p} such that {\it
-  (ii)} @{text p} leaves the free atoms of @{text x} and @{text 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 p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
-  requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
-  %
-  \begin{equation}\label{alphaset}
-  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-       \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
-       \mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
-       \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} & 
-       \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\ 
-  \end{array}
-  \end{equation}
-  %
-  \noindent
-  Note that this relation depends on the permutation @{text
-  "p"}; $\alpha$-equivalence between two pairs is then the relation where we
-  existentially quantify over this @{text "p"}. Also 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}}$ 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"}.
-
-  The definition in \eqref{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{equation}\label{alphalist}
-  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-         \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & 
-         \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-         \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
-         \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
-  \end{array}
-  \end{equation}
-  %
-  \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 \emph{restrict} names, then we keep sets of binders, but drop 
-  condition {\it (iv)} in \eqref{alphaset}:
-  %
-  \begin{equation}\label{alphares}
-  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} & 
-             \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
-             \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
-  \end{array}
-  \end{equation}
-
-  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
-  %
-  \begin{center}
-  @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
-  \end{center}
-
-  \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 "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
-  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} 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 p} 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 the rest of this section we are going to introduce three abstraction 
-  types. For this we define 
-  %
-  \begin{equation}
-  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
-  \end{equation}
-  
-  \noindent
-  (similarly for $\approx_{\,\textit{abs\_set+}}$ 
-  and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
-  relations. %% and equivariant.
-
-  \begin{lemma}\label{alphaeq} 
-  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
-  and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 
-  %@{term "abs_set (as, x) (bs, y)"} then also 
-  %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
-  \end{lemma}
-
-  \begin{proof}
-  Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
-  a permutation @{text p} and for the proof obligation take @{term "-p"}. In case 
-  of transitivity, we have two permutations @{text p} and @{text q}, and for the
-  proof obligation use @{text "q + p"}. All conditions are then by simple
-  calculations. 
-  \end{proof}
-
-  \noindent
-  This lemma allows us to use our quotient package for introducing 
-  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
-  representing $\alpha$-equivalence classes of pairs of type 
-  @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
-  (in the third case). 
-  The elements in these types will be, respectively, written as
-  %
-  %\begin{center}
-  @{term "Abs_set as x"}, %\hspace{5mm} 
-  @{term "Abs_res as x"} and %\hspace{5mm}
-  @{term "Abs_lst as x"}, 
-  %\end{center}
-  %
-  %\noindent
-  indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
-  call the types \emph{abstraction types} and their elements
-  \emph{abstractions}. The important property we need to derive is the support of 
-  abstractions, namely:
-
-  \begin{theorem}[Support of Abstractions]\label{suppabs} 
-  Assuming @{text x} has finite support, then
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$
-  @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\
-  @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$
-  @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}
-  \end{tabular}
-  \end{center}
-  \end{theorem}
-
-  \noindent
-  This theorem states that the bound names do not appear in the support.
-  For brevity we omit the proof and again refer the reader to
-  our formalisation in Isabelle/HOL.
-
-  %\noindent
-  %Below we will show the first equation. The others 
-  %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
-  %we have 
-  %%
-  %\begin{equation}\label{abseqiff}
-  %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
-  %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
-  %\end{equation}
-  %
-  %\noindent
-  %and also
-  %
-  %\begin{equation}\label{absperm}
-  %%@%{%thm %permute_Abs[no_vars]}%
-  %\end{equation}
-
-  %\noindent
-  %The second fact derives from the definition of permutations acting on pairs 
-  %\eqref{permute} and $\alpha$-equivalence being equivariant 
-  %(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
-  %the following lemma about swapping two atoms in an abstraction.
-  %
-  %\begin{lemma}
-  %@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
-  %\end{lemma}
-  %
-  %\begin{proof}
-  %This lemma is straightforward using \eqref{abseqiff} and observing that
-  %the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-  %Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
-  %\end{proof}
-  %
-  %\noindent
-  %Assuming that @{text "x"} has finite support, this lemma together 
-  %with \eqref{absperm} allows us to show
-  %
-  %\begin{equation}\label{halfone}
-  %@{thm Abs_supports(1)[no_vars]}
-  %\end{equation}
-  %
-  %\noindent
-  %which by Property~\ref{supportsprop} gives us ``one half'' of
-  %Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
-  %it, 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]}.
-  %
-  %Using the second equation in \eqref{equivariance}, we can show that 
-  %@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"}) 
-  %and therefore has empty support. 
-  %This in turn means
-  %
-  %\begin{center}
-  %@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
-  %\end{center}
-  %
-  %\noindent
-  %using \eqref{suppfun}. 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}
-  %
-  %\noindent
-  %since for finite sets of atoms, @{text "bs"}, we have 
-  %@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
-  %Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
-  %Theorem~\ref{suppabs}. 
-
-  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
-  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 mutual recursive) type declarations, say @{text
-  "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
-  binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
-  syntax in Nominal Isabelle for such specifications is roughly as follows:
-  %
-  \begin{equation}\label{scheme}
-  \mbox{\begin{tabular}{@ {}p{2.5cm}l}
-  type \mbox{declaration part} &
-  $\begin{cases}
-  \mbox{\small\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}$\\
-  binding \mbox{function part} &
-  $\begin{cases}
-  \mbox{\small\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}
-
-  \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
-
-  \begin{center}
-  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 
-  \end{center}
-  
-  \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 
-  %\cite{Berghofer99}.  
-  The labels
-  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}:
-  %
-  \begin{center}
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
-  \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
-  \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}
-  \end{tabular}
-  \end{center}
-  %
-  \noindent
-  The first mode is for binding lists of atoms (the order of binders matters);
-  the second is for sets of binders (the order does not matter, but the
-  cardinality does) and the last is for sets of binders (with vacuous binders
-  preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
-  clause will be called \emph{bodies}; the
-  ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
-  Ott, we allow multiple labels in binders and bodies. 
-
-  %For example we allow
-  %binding clauses of the form:
-  %
-  %\begin{center}
-  %\begin{tabular}{@ {}ll@ {}}
-  %@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &  
-  %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
-  %@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &  
-  %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 
-  %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
-  %\end{tabular}
-  %\end{center}
-
-  \noindent
-  %Similarly for the other binding modes. 
-  %Interestingly, in case of \isacommand{bind (set)}
-  %and \isacommand{bind (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
-  the ones of Ott. The
-  main idea behind these restrictions is that we obtain a sensible 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 (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{bind (set)} and \isacommand{bind (set+)} the labels must either
-  refer to atom types or to sets of atom types; in case of \isacommand{bind}
-  the labels must refer to atom types or 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:
-
-  \begin{center}\small
-  \begin{tabular}{@ {}c@ {\hspace{7mm}}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"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
-  \end{tabular} &
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text ty} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
-  \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
-  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
-  \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\
-  \end{tabular}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  In these specifications @{text "name"} refers to an 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}. However, having
-  \isacommand{bind (set)} or \isacommand{bind} 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{bind (set)} and
-  \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can
-  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 might be specified as:
-  %
-  \begin{equation}\label{letpat}
-  \mbox{\small%
-  \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{bind} @{text x} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 
-     \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
-  \isacommand{and} @{text pat} $=$
-  @{text PNil}
-  $\mid$~@{text "PVar name"}
-  $\mid$~@{text "PTup pat pat"}\\ 
-  \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{text "bn(PNil) = []"}\\
-  \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
-  \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 
-  \end{tabular}}
-  \end{equation}
-  %
-  \noindent
-  In this specification the function @{text "bn"} determines which atoms of
-  the pattern @{text p} 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.
-
-  As said above, for deep binders we allow binding clauses such as
-  %
-  %\begin{center}
-  %\begin{tabular}{ll}
-  @{text "Bar p::pat t::trm"} %%%&  
-     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\
-  %\end{tabular}
-  %\end{center}
-  %
-  %\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{\small%
-  \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
-  \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
-     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
-  \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-  \isacommand{and} @{text "assn"} $=$
-  @{text "ANil"}
-  $\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}
-  %
-  \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
-  %
-  \begin{center}\small
-  \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-  @{text "Baz\<^isub>1 p::pat t::trm"} & 
-     \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
-  @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 
-     \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
-     \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
-  out different atoms to become bound, respectively be free, in @{text "p"}.
-  (Since the Ott-tool does not derive a reasoning 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. That means in \eqref{letpat} 
-  that the term-constructors @{text PVar} and @{text PTup} may
-  not have a binding clause (all arguments are used to define @{text "bn"}).
-  In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
-  may have a binding clause involving the argument @{text trm} (the only one that
-  is \emph{not} used in the definition of the binding function). This restriction
-  is sufficient for lifting the binding function to $\alpha$-equated 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 PNil}), a singleton set or singleton list containing an
-  atom (case @{text PVar}), or unions of atom sets or appended atom lists
-  (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
-  later on.
-  
-  In order to simplify our definitions of free atoms and $\alpha$-equivalence, 
-  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{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
-  of the lambda-terms, the completion produces
-
-  \begin{center}\small
-  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
-  \isacommand{nominal\_datatype} @{text lam} =\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
-    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
-  \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
-    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
-  \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
-    \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
-  \end{tabular}
-  \end{center}
-
-  \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{Pottier06,Cheney05}, 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 @{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. We also have to invent
-  new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
-  given by the user. 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> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
-  where @{term ty} is the type used in the quotient construction for 
-  @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
-
-  %The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
-  %non-empty and the types in the constructors only occur in positive 
-  %position (see \cite{Berghofer99} for an in-depth description of the datatype package
-  %in Isabelle/HOL). 
-  We subsequently define each of the user-specified binding 
-  functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
-  raw datatype. We can also easily define permutation operations by 
-  recursion so that for each term constructor @{text "C"} we have that
-  %
-  \begin{equation}\label{ceqvt}
-  @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
-  \end{equation}
-
-  The first non-trivial step we have to perform is the generation of
-  free-atom functions from the specification. For the 
-  \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
-  %
-  %\begin{equation}\label{fvars}
-  @{text "fa_ty\<^isub>"}$_{1..n}$
-  %\end{equation}
-  %
-  %\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
-  %
-  %\begin{center}
-  @{text "fa_bn\<^isub>"}$_{1..m}$.
-  %\end{center}
-  %
-  %\noindent
-  The reason for this setup is that in a deep binder not all atoms have to be
-  bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
-  that calculates those free atoms in a deep binder.
-
-  While the idea behind these free-atom functions is clear (they just
-  collect all atoms that are not bound), because of our rather complicated
-  binding mechanisms their definitions are somewhat involved.  Given
-  a 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{bind (set)} (the other modes are similar). 
-  Suppose the binding clause @{text bc\<^isub>i} is of the form 
-  %
-  %\begin{center}
-  \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
-  %\end{center}
-  %
-  %\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\\[-2mm]
-  %
-  \begin{equation}\label{fadef}
-  \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
-  \end{equation}
-  %
-  \noindent
-  The set @{text D} is formally defined as
-  %
-  %\begin{center}
-  @{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
-  %\end{center} 
-  %
-  %\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; 
-  %(see \eqref{fvars}); 
-  otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
-  
-  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{center}
-  %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  %@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
-  %@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
-  %@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
-  %\end{tabular}
-  %\end{center}
-  %
-  \begin{center}
-  @{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
-  @{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
-  @{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
-  \end{center}
-  %
-  \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} is then formally defined as\\[-4mm]
-  %
-  \begin{center}
-  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
-  \end{center} 
-  %
-  \noindent 
-  where we use the auxiliary binding functions for shallow binders. 
-  The set @{text "B'"} collects all free atoms in non-recursive deep
-  binders. Let us assume these binders in @{text "bc\<^isub>i"} are
-  %
-  %\begin{center}
-  \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
-  %\end{center}
-  %
-  %\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\\[-5mm]
-  %
-  \begin{center}
-  @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
-  \end{center}
-  %
-  \noindent
-  This completes the definition of 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}$, which are also defined by mutual
-  recursion. Assume the user specified a @{text bn}-clause of the form
-  %
-  %\begin{center}
-  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  %\end{center}
-  %
-  %\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:
-  %
-  \begin{center}
-  \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),\\
-  $\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"}, and\\
-  $\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in  @{text "rhs"},
-  but without a recursive call.
-  \end{tabular}
-  \end{center}
-  %
-  \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:
-  %
-  \begin{center}\small
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{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 "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
-
-  @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
-
-  @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
-  \end{tabular}
-  \end{center}
-
-  \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.
-
-  Next we define the $\alpha$-equivalence relations for the raw types @{text
-  "ty"}$_{1..n}$ from the specification. We write them as
-  %
-  %\begin{center}
-  @{text "\<approx>ty"}$_{1..n}$.
-  %\end{center}
-  %
-  %\noindent
-  Like with the free-atom functions, we also need to
-  define auxiliary $\alpha$-equivalence relations 
-  %
-  %\begin{center}
-  @{text "\<approx>bn\<^isub>"}$_{1..m}$
-  %\end{center}
-  %
-  %\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.
-  %
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
-  @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^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}
-  \end{center}
-
-
-  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{center}
-  \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{center}
-
-  \noindent
-  The task below is to specify what the premises of a binding clause are. As a
-  special instance, we first treat the case where @{text "bc\<^isub>i"} is the
-  empty binding clause of the form
-  %
-  \begin{center}
-  \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \end{center}
-
-  \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 arguments @{text "z"}$_{1..n}$ and
-  respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. 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}
-
-  \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} with type @{text "ty\<^isub>i"}; otherwise
-  we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us 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
-  %
-  %\begin{center}
-  @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1  \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}.
-  %\end{center}
-  %
-  %\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{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
-  \end{equation}
-
-  \noindent
-  In this case we define a premise @{text P} using the relation
-  $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
-  $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other
-  binding modes). This premise defines $\alpha$-equivalence of two abstractions
-  involving multiple binders. As above, we first build the tuples @{text "D"} and
-  @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
-  compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 
-  For $\approx_{\,\textit{set}}$  we also need
-  a compound free-atom function for the bodies defined as
-  %
-  \begin{center}
-  \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
-  \end{center}
-
-  \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
-
-  \begin{center}
-  @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
-  \end{center}
-
-  \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:
-  %
-  \begin{center}
-  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
-  \end{center}
-
-  \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 formally define shortly).
-  Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
-  %
-  %\begin{center}
-  @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
-  %\end{center}
-  %
-  %\noindent
-  The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
-  and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}. 
-  All premises for @{text "bc\<^isub>i"} are then given by
-  %
-  \begin{center}
-  @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}
-  \end{center} 
-
-  \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
-  %
-  %\begin{center}
-  @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
-  %\end{center}
-  %
-  %\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
-  %
-  \begin{center}
-  \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
-  {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
-  \end{center}
-  
-  \noindent
-  In this clause the relations @{text "R"}$_{1..s}$ are given by 
-
-  \begin{center}
-  \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},\\
-  $\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},\\
-  $\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\\
-  $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
-  recursive call.
-  \end{tabular}
-  \end{center}
-
-  \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}}$ and take @{text "0"}
-  for the existentially quantified permutation).
-
-  Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
-  we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$ with the following clauses:
-
-  \begin{center}\small
-  \begin{tabular}{@ {}c @ {}}
-  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
-  \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
-  \end{tabular}
-  \end{center}
-
-  \begin{center}\small
-  \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'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
-  \end{tabular}
-  \end{center}
-
-  \begin{center}\small
-  \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'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  Note the difference between  $\approx_{\textit{assn}}$ and
-  $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of 
-  the components in an assignment that are \emph{not} bound. 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. 
-*}
-
-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 sketch
-  in this section the proofs we need for establishing this infrastructure. One
-  main point of our work is that we have completely automated these proofs in Isabelle/HOL.
-
-  First we establish that the
-  $\alpha$-equivalence relations defined in the previous section are 
-  equivalence relations.
-
-  \begin{lemma}\label{equiv} 
-  Given the raw types @{text "ty"}$_{1..n}$ and binding functions
-  @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 
-  @{text "\<approx>bn"}$_{1..m}$ are equivalence relations.%% and equivariant.
-  \end{lemma}
-
-  \begin{proof} 
-  The proof is by mutual induction over the definitions. 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}.
-  \end{proof}
-
-  \noindent 
-  We can feed this 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
-  %
-  \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}
-  
-  \noindent
-  whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
-  In order to derive this fact, 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}
-
-  \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}).
-  Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
-  @{text "ty"}$_{1..r}$, respectfulness amounts to showing that
-  %
-  \begin{center}
-  @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  \end{center}  
-
-  \noindent
-  holds under the assumptions that we have \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. We can prove this
-  implication by applying the corresponding rule in our $\alpha$-equivalence
-  definition and by establishing the following auxiliary implications %facts 
-  %
-  \begin{equation}\label{fnresp}
-  \mbox{%
-  \begin{tabular}{ll@ {\hspace{7mm}}ll}
-  \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
-  \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
-
-  \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
-  \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
-  \end{tabular}}
-  \end{equation}
-
-  \noindent
-  They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. 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} returning 
-  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 the lifing 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}. Having the facts \eqref{fnresp} at our disposal, we can 
-  also lift properties that characterise when two raw terms of the form
-  %
-  \begin{center}
-  @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
-  \end{center}
-
-  \noindent
-  are $\alpha$-equivalent. This gives us conditions when the corresponding
-  $\alpha$-equated terms are \emph{equal}, namely
-  %
-  %\begin{center}
-  @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
-  %\end{center}
-  %
-  %\noindent
-  We call these conditions as \emph{quasi-injectivity}. They correspond to
-  the premises in our $\alpha$-equivalence relations.
-
-  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 \cite{HuffmanUrban10}.
-  %, which we already established 
-  %in Lemma~\ref{equiv}. 
-  As a result we can add the equations
-  %
-  \begin{equation}\label{calphaeqvt}
-  @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
-  \end{equation}
-
-  \noindent
-  to our infrastructure. In a similar fashion we can lift the defining equations
-  of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
-  @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
-  "bn\<AL>"}$_{1..m}$ and the 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.
-
-  Finally we can add to our infrastructure a cases lemma (explained in the next section)
-  and a structural induction principle 
-  for the types @{text "ty\<AL>"}$_{1..n}$. The conclusion of the induction principle is
-  of the form
-  %
-  %\begin{equation}\label{weakinduct}
-  \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
-  %\end{equation} 
-  %
-  %\noindent
-  whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
-  have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
-  term constructor @{text "C"}$^\alpha$ a premise of the form
-  %
-  \begin{equation}\label{weakprem}
-  \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}} 
-  \end{equation}
-
-  \noindent 
-  in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 
-  the recursive arguments of @{text "C\<AL>"}. 
-
-  By working now completely on the $\alpha$-equated level, we
-  can first show that the free-atom functions and binding functions are
-  equivariant, namely
-  %
-  \begin{center}
-  \begin{tabular}{rcl@ {\hspace{10mm}}rcl}
-  @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &
-  @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\
-  @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
-  \end{tabular}
-  \end{center}
-  %
-  \noindent
-  These properties can be established using the induction principle for the types @{text "ty\<AL>"}$_{1..n}$.
-  %%in \eqref{weakinduct}.
-  Having these equivariant properties established, we can
-  show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
-  the support of its arguments, that means 
-
-  \begin{center}
-  @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
-  \end{center}
- 
-  \noindent
-  holds. This allows us to prove by induction that
-  every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported. 
-  %This can be again shown by induction 
-  %over @{text "ty\<AL>"}$_{1..n}$. 
-  Lastly, we can show that the support of 
-  elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
-  This fact is important in a nominal setting, but also provides evidence 
-  that our notions of free-atoms and $\alpha$-equivalence are correct.
-
-  \begin{theorem} 
-  For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
-  @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
-  \end{theorem}
-
-  \begin{proof}
-  The proof is by induction. In each case
-  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 the facts derived in Theorem~\ref{suppabs}.
-  \end{proof}
-
-  \noindent
-  To sum up this section, we can establish automatically 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 establishing facts about these lifted definitions. All necessary proofs
-  are generated automatically by custom ML-code. 
-
-  %This code can deal with 
-  %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
-
-  %\begin{figure}[t!]
-  %\begin{boxedminipage}{\linewidth}
-  %\small
-  %\begin{tabular}{l}
-  %\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
-  %\isacommand{nominal\_datatype}~@{text "tkind ="}\\
-  %\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ 
-  %\isacommand{and}~@{text "ckind ="}\\
-  %\phantom{$|$}~@{text "CKSim ty ty"}\\
-  %\isacommand{and}~@{text "ty ="}\\
-  %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
-  %$|$~@{text "TFun string ty_list"}~%
-  %$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
-  %$|$~@{text "TArr ckind ty"}\\
-  %\isacommand{and}~@{text "ty_lst ="}\\
-  %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
-  %\isacommand{and}~@{text "cty ="}\\
-  %\phantom{$|$}~@{text "CVar cvar"}~%
-  %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-  %$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{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 ="}\\
-  %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
-  %\isacommand{and}~@{text "trm ="}\\
-  %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
-  %$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
-  %$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{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"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
-  %$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
-  %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
-  %\isacommand{and}~@{text "assoc_lst ="}\\
-  %\phantom{$|$}~@{text ANil}~%
-  %$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
-  %\isacommand{and}~@{text "pat ="}\\
-  %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
-  %\isacommand{and}~@{text "vt_lst ="}\\
-  %\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
-  %\isacommand{and}~@{text "tvtk_lst ="}\\
-  %\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
-  %\isacommand{and}~@{text "tvck_lst ="}\\ 
-  %\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
-  %\isacommand{binder}\\
-  %@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
-  %@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  %@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
-  %@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
-  %\isacommand{where}\\
-  %\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
-  %$|$~@{text "bv1 VTNil = []"}\\
-  %$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
-  %$|$~@{text "bv2 TVTKNil = []"}\\
-  %$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
-  %$|$~@{text "bv3 TVCKNil = []"}\\
-  %$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
-  %\end{tabular}
-  %\end{boxedminipage}
-  %\caption{The nominal datatype declaration for Core-Haskell. 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. This will be improved
-  %in a future version of Nominal Isabelle. Apart from that, the 
-  %declaration follows closely the original in Figure~\ref{corehas}. The
-  %point of our work is that having made such a declaration in Nominal Isabelle,
-  %one obtains automatically a reasoning infrastructure for Core-Haskell.
-  %\label{nominalcorehas}}
-  %\end{figure}
-*}
-
-
-section {* Strong Induction Principles *}
-
-text {*
-  In the previous section we derived induction principles for $\alpha$-equated terms. 
-  We call such induction principles \emph{weak}, because for a 
-  term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
-  the induction hypothesis requires us to establish the implications \eqref{weakprem}.
-  The problem with these implications is that in general they are difficult to establish.
-  The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 
-  %%(for example we cannot assume the variable convention for them).
-
-  In \cite{UrbanTasson05} we introduced a method for automatically
-  strengthening weak induction principles for terms containing single
-  binders. These stronger induction principles allow the user to make additional
-  assumptions about bound atoms. 
-  %These additional assumptions amount to a formal
-  %version of the informal variable convention for binders. 
-  To sketch how this strengthening extends to the case of multiple binders, we use as
-  running example the term-constructors @{text "Lam"} and @{text "Let"}
-  from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
-  the stronger induction principle for \eqref{letpat} establishes properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
-  where the additional parameter @{text c} controls
-  which freshness assumptions the binders should satisfy. For the two term constructors 
-  this means that the user has to establish in inductions the implications
-  %
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
-  @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}\\%[-0mm]
-  \end{tabular}
-  \end{center}
-
-  In \cite{UrbanTasson05} we showed how the weaker induction principles imply
-  the stronger ones. This was done by some quite complicated, nevertheless automated,
-  induction proof. In this paper we simplify this work by leveraging the automated proof
-  methods from the function package of Isabelle/HOL. 
-  The reasoning principle these methods employ 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 (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 
-  every induction step and the other is that we have covered all cases. 
-  As measures we use the size functions 
-  @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 
-  all well-founded. %It is straightforward to establish that these measures decrease 
-  %in every induction step.
-  
-  What is left to show is that we covered all cases. To do so, we use 
-  a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} 
-  this lemma is of the form
-  %
-  \begin{equation}\label{weakcases}
-  \infer{@{text "P\<^bsub>trm\<^esub>"}}
-  {\begin{array}{l@ {\hspace{9mm}}l}
-  @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  \end{array}}\\[-1mm]
-  \end{equation}
-  %
-  where we have a premise for each term-constructor.
-  The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
-  provided we can show that this property holds if we substitute for @{text "t"} all 
-  possible term-constructors. 
-  
-  The only remaining difficulty is that in order to derive the stronger induction
-  principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
-  in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 
-  \emph{all} @{text Let}-terms. 
-  What we need instead is a cases lemma where we only have to consider terms that have 
-  binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications
-  %
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
-  @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\%[-2mm]
-  \end{tabular}
-  \end{center}
-  %
-  \noindent
-  which however can be relatively easily be derived from the implications in \eqref{weakcases} 
-  by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
-  that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with 
-  a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and 
-  @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
-  By using Property \ref{supppermeq}, we can infer from the latter 
-  that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
-  and we are done with this case.
-
-  The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
-  The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
-  because @{text p} might contain names that are bound (by @{text bn}) and so are 
-  free. To solve this problem we have to introduce a permutation function that only
-  permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
-  by lifting. For a
-  clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
-  %
-  \begin{center}
-  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}  with
-  $\begin{cases}
-  \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
-  \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
-  \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}  
-  \end{cases}$
-  \end{center}
-  %
-  %\noindent
-  %with @{text "y\<^isub>i"} determined as follows:
-  %
-  %\begin{center}
-  %\begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
-  %\end{tabular}
-  %\end{center}
-  %
-  \noindent
-  Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
-  @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
-  is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. 
-  These facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
-  completes the non-trivial cases in \eqref{letpat} for strengthening the corresponding induction
-  principle.
-  
-
-
-  %A natural question is
-  %whether we can also strengthen the weak induction principles involving
-  %the general binders presented here. We will indeed be able to so, but for this we need an 
-  %additional notion for permuting deep binders. 
-
-  %Given a binding function @{text "bn"} we define an auxiliary permutation 
-  %operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
-  %Assuming a clause of @{text bn} is given as 
-  %
-  %\begin{center}
-  %@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
-  %\end{center}
-
-  %\noindent 
-  %then we define 
-  %
-  %\begin{center}
-  %@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
-  %\end{center}
-  
-  %\noindent
-  %with @{text "y\<^isub>i"} determined as follows:
-  %
-  %\begin{center}
-  %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
-  %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
-  %\end{tabular}
-  %\end{center}
-  
-  %\noindent
-  %Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
-  %$\alpha$-equated terms. We can then prove the following two facts
-
-  %\begin{lemma}\label{permutebn} 
-  %Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
-  %{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
-  %  @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
-  %\end{lemma}
-
-  %\begin{proof} 
-  %By induction on @{text x}. The equations follow by simple unfolding 
-  %of the definitions. 
-  %\end{proof}
-
-  %\noindent
-  %The first property states that a permutation applied to a binding function is
-  %equivalent to first permuting the binders and then calculating the bound
-  %atoms. The second amounts to the fact that permuting the binders has no 
-  %effect on the free-atom function. The main point of this permutation
-  %function, however, is that if we have a permutation that is fresh 
-  %for the support of an object @{text x}, then we can use this permutation 
-  %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
-  %@{text "Let"} term-constructor from the example shown 
-  %in \eqref{letpat} this means for a permutation @{text "r"}
-  %%
-  %\begin{equation}\label{renaming}
-  %\begin{array}{l}
-  %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
-  %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
-  %\end{array}
-  %\end{equation}
-
-  %\noindent
-  %This fact will be crucial when establishing the strong induction principles below.
-
- 
-  %In our running example about @{text "Let"}, the strong induction
-  %principle means that instead 
-  %of establishing the implication 
-  %
-  %\begin{center}
-  %@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
-  %\end{center}
-  %
-  %\noindent
-  %it is sufficient to establish the following implication
-  %
-  %\begin{equation}\label{strong}
-  %\mbox{\begin{tabular}{l}
-  %@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
-  %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
-  %\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
-  %\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
-  %\end{tabular}}
-  %\end{equation}
-  %
-  %\noindent 
-  %While this implication contains an additional argument, namely @{text c}, and 
-  %also additional universal quantifications, it is usually easier to establish.
-  %The reason is that we have the freshness 
-  %assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
-  %chosen by the user as long as it has finite support.
-  %
-  %Let us now show how we derive the strong induction principles from the
-  %weak ones. In case of the @{text "Let"}-example we derive by the weak 
-  %induction the following two properties
-  %
-  %\begin{equation}\label{hyps}
-  %@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
-  %@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
-  %\end{equation} 
-  %
-  %\noindent
-  %For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
-  %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
-  %By Property~\ref{avoiding} we
-  %obtain a permutation @{text "r"} such that 
-  %
-  %\begin{equation}\label{rprops}
-  %@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
-  %@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
-  %\end{equation}
-  %
-  %\noindent
-  %hold. The latter fact and \eqref{renaming} give us
-  %%
-  %\begin{center}
-  %\begin{tabular}{l}
-  %@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
-  %\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
-  %\end{tabular}
-  %\end{center}
-  %
-  %\noindent
-  %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
-  %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
-  %To do so, we will use the implication \eqref{strong} of the strong induction
-  %principle, which requires us to discharge
-  %the following four proof obligations:
-  %%
-  %\begin{center}
-  %\begin{tabular}{rl}
-  %{\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
-  %{\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
-  %{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
-  %{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
-  %\end{tabular}
-  %\end{center}
-  %
-  %\noindent
-  %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
-  %others from the induction hypotheses in \eqref{hyps} (in the fourth case
-  %we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
-  %
-  %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
-  %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
-  %This completes the proof showing that the weak induction principles imply 
-  %the strong induction principles. 
-*}
-
-
-section {* Related Work\label{related} *}
-
-text {*
-  To our knowledge the earliest usage of general binders in a theorem prover
-  is described in \cite{NaraschewskiNipkow99} about 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 in the locally nameless
-  approach to binding \cite{chargueraud09}.  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 or
-  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.
-
-  Another technique for representing binding is higher-order abstract syntax
-  (HOAS). %, which for example is implemented in the Twelf system. 
-  This %%representation
-  technique supports very elegantly many aspects of \emph{single} binding, and
-  impressive work has been done that uses HOAS for mechanising the metatheory
-  of SML~\cite{LeeCraryHarper07}. 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'' variables. This can be done in one step with our
-  %general binders described in this paper, but needs a cumbersome
-  %iteration with single binders. The resulting formal reasoning turned out to
-  %be rather unpleasant. The hope is that the extension presented in this paper
-  %is a substantial improvement.
- 
-  The most closely related work to the one presented here is the Ott-tool
-  \cite{ott-jfp} and the C$\alpha$ml language \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 of 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.  Also the definition for the 
-  notion of free variables
-  is work in progress.
-
-  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. 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 you specify 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{bind (set)} and 
-  \isacommand{bind (set+)}. 
-  %
-  %Consider the examples
-  %
-  %\begin{center}
-  %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-  %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
-  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
-  %@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
-  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
-  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
-  %\end{tabular}
-  %\end{center}
-  %
-  %\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
-  % 
-  %\begin{center}
-  %\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)"}\\
-  %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
-  %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
-  %\end{tabular}
-  %\end{center}
-  %
-  %\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 Core-Haskell. 
-
-  Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
-  representing terms with general binders inside OCaml. 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{bind} 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}.
-  
-  In a slightly different domain (programming with dependent types), the 
-  paper \cite{Altenkirch10} presents a calculus with a notion of 
-  $\alpha$-equivalence related to our binding mode \isacommand{bind (set+)}.
-  The definition in \cite{Altenkirch10} 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.\\[-7mm]    
-*}
-
-section {* Conclusion *}
-
-text {*
-  We have presented an extension of Nominal Isabelle for dealing with
-  general binders, that is term-constructors having multiple bound 
-  variables. 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 specifications from Ott, but extended them 
-  in some places and restricted
-  them in others so that they 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 next Isabelle distribution.\footnote{For the moment
-  %it can be downloaded from the Mercurial repository linked at
-  %\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 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 imposed in this paper that we would like to lift in
-  %future work. One is the exclusion of nested datatype definitions. Nested
-  %datatype definitions 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}). To
-  %achieve this, we need a slightly more clever implementation than we have at the moment. 
-
-  %A more interesting line of 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
-  %%
-  %\begin{center}
-  %@{text "fa_ty x  =  bn x \<union> fa_bn x"}.
-  %\end{center}
-  %
-  %\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 lists, we abstract lists of distinct elements.
-  %Once we feel confident about such binding modes, our implementation 
-  %can be easily extended to accommodate them.
-  %
-  \smallskip
-  \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.\\[-7mm]    
-  %Stephanie Weirich suggested to separate the subgrammars
-  %of kinds and types in our Core-Haskell example. \\[-6mm] 
-*}
-
-
-(*<*)
-end
-(*>*)




