21   supp ("supp _" [78] 73) and

    21   supp ("supp _" [78] 73) and

    22   uminus ("-_" [78] 73) and

    22   uminus ("-_" [78] 73) and

    23   If  ("if _ then _ else _" 10) and

    23   If  ("if _ then _ else _" 10) and

    24   alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and

    24   alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and

    25   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and

    25   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and

    27   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and

    27   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and

    28   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and

    28   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and

    29   fv ("fa'(_')" [100] 100) and

    29   fv ("fa'(_')" [100] 100) and

    30   equal ("=") and

    30   equal ("=") and

    31   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 

    31   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 

    32   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and

    32   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and

    33   Abs_lst ("[_]\<^bsub>list\<^esub>._") and

    33   Abs_lst ("[_]\<^bsub>list\<^esub>._") and

    34   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and

    34   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and

    36   Abs_print ("_\<^bsub>set\<^esub>._") and

    36   Abs_print ("_\<^bsub>set\<^esub>._") and

    37   Cons ("_::_" [78,77] 73) and

    37   Cons ("_::_" [78,77] 73) and

    38   supp_set ("aux _" [1000] 10) and

    38   supp_set ("aux _" [1000] 10) and

    39   alpha_bn ("_ \<approx>bn _")

    39   alpha_bn ("_ \<approx>bn _")

    40 

    40 

   102   we would like to regard the first pair of type-schemes as $\alpha$-equivalent,

   102   we would like to regard the first pair of type-schemes as $\alpha$-equivalent,

   103   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,

   103   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,

   104   the second pair should \emph{not} be $\alpha$-equivalent:

   104   the second pair should \emph{not} be $\alpha$-equivalent:

   105   %

   105   %

   106   \begin{equation}\label{ex1}

   106   \begin{equation}\label{ex1}

   108   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}

   108   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}

   109   \end{equation}

   109   \end{equation}

   110   %

   110   %

   111   \noindent

   111   \noindent

   112   Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ

   112   Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ

   136   we might not care in which order the assignments @{text "x = 3"} and

   136   we might not care in which order the assignments @{text "x = 3"} and

   137   \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard

   137   \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard

   138   \eqref{one} as $\alpha$-equivalent with

   138   \eqref{one} as $\alpha$-equivalent with

   139   %

   139   %

   140   \begin{center}

   140   \begin{center}

   142   \end{center}

   142   \end{center}

   143   %

   143   %

   144   \noindent

   144   \noindent

   145   Therefore we will also provide a separate binding mechanism for cases in

   145   Therefore we will also provide a separate binding mechanism for cases in

   146   which the order of binders does not matter, but the ``cardinality'' of the

   146   which the order of binders does not matter, but the ``cardinality'' of the

   316   %reasoning about a well-formedness predicate.

   316   %reasoning about a well-formedness predicate.

   317 

   317 

   318   The problem with introducing a new type in Isabelle/HOL is that in order to

   318   The problem with introducing a new type in Isabelle/HOL is that in order to

   319   be useful, a reasoning infrastructure needs to be ``lifted'' from the

   319   be useful, a reasoning infrastructure needs to be ``lifted'' from the

   320   underlying subset to the new type. This is usually a tricky and arduous

   320   underlying subset to the new type. This is usually a tricky and arduous

   322   described by Homeier \cite{Homeier05} for the HOL4 system. This package

   322   described by Homeier \cite{Homeier05} for the HOL4 system. This package

   323   allows us to lift definitions and theorems involving raw terms to

   323   allows us to lift definitions and theorems involving raw terms to

   324   definitions and theorems involving $\alpha$-equated terms. For example if we

   324   definitions and theorems involving $\alpha$-equated terms. For example if we

   325   define the free-variable function over raw lambda-terms

   325   define the free-variable function over raw lambda-terms

   326 

   326 

   727 

   727 

   728   \noindent

   728   \noindent

   729   Now recall the examples shown in \eqref{ex1} and

   729   Now recall the examples shown in \eqref{ex1} and

   730   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and

   730   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and

   731   @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to

   731   @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to

   733   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text

   733   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text

   734   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}

   734   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}

   735   since there is no permutation that makes the lists @{text "[x, y]"} and

   735   since there is no permutation that makes the lists @{text "[x, y]"} and

   736   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}

   736   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}

   738   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity

   738   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity

   739   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}

   739   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}

   740   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no

   740   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no

   741   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal

   741   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal

   742   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be

   742   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be

   749   \begin{equation}

   749   \begin{equation}

   750   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}

   750   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}

   751   \end{equation}

   751   \end{equation}

   752   

   752   

   753   \noindent

   753   \noindent

   755   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 

   755   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 

   756   relations. %% and equivariant.

   756   relations. %% and equivariant.

   757 

   757 

   758   \begin{lemma}\label{alphaeq} 

   758   \begin{lemma}\label{alphaeq} 

   759   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$

   759   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$

   761   %@{term "abs_set (as, x) (bs, y)"} then also 

   761   %@{term "abs_set (as, x) (bs, y)"} then also 

   762   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).

   762   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).

   763   \end{lemma}

   763   \end{lemma}

   764 

   764 

   765   \begin{proof}

   765   \begin{proof}

   770   calculations. 

   770   calculations. 

   771   \end{proof}

   771   \end{proof}

   772 

   772 

   773   \noindent

   773   \noindent

   774   This lemma allows us to use our quotient package for introducing 

   774   This lemma allows us to use our quotient package for introducing 

   776   representing $\alpha$-equivalence classes of pairs of type 

   776   representing $\alpha$-equivalence classes of pairs of type 

   777   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}

   777   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}

   778   (in the third case). 

   778   (in the third case). 

   779   The elements in these types will be, respectively, written as

   779   The elements in these types will be, respectively, written as

   780   %

   780   %

   795 

   795 

   796   \begin{center}

   796   \begin{center}

   797   \begin{tabular}{l}

   797   \begin{tabular}{l}

   798   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$

   798   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$

   799   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\

   799   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\

   802   \end{tabular}

   802   \end{tabular}

   803   \end{center}

   803   \end{center}

   804   \end{theorem}

   804   \end{theorem}

   805 

   805 

   806   \noindent

   806   \noindent

   948   (possibly empty) list of \emph{binding clauses}, which indicate the binders

   948   (possibly empty) list of \emph{binding clauses}, which indicate the binders

   949   and their scope in a term-constructor.  They come in three \emph{modes}:

   949   and their scope in a term-constructor.  They come in three \emph{modes}:

   950   %

   950   %

   951   \begin{center}

   951   \begin{center}

   952   \begin{tabular}{@ {}l@ {}}

   952   \begin{tabular}{@ {}l@ {}}

   956   \end{tabular}

   956   \end{tabular}

   957   \end{center}

   957   \end{center}

   958   %

   958   %

   959   \noindent

   959   \noindent

   960   The first mode is for binding lists of atoms (the order of binders matters);

   960   The first mode is for binding lists of atoms (the order of binders matters);

   979   %\end{center}

   979   %\end{center}

   980 

   980 

   981   \noindent

   981   \noindent

   982   %Similarly for the other binding modes. 

   982   %Similarly for the other binding modes. 

   983   %Interestingly, in case of \isacommand{bind (set)}

   983   %Interestingly, in case of \isacommand{bind (set)}

   985   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 

   985   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 

   986   %show this later with an example.

   986   %show this later with an example.

   987   

   987   

   988   There are also some restrictions we need to impose on our binding clauses in comparison to

   988   There are also some restrictions we need to impose on our binding clauses in comparison to

   989   the ones of Ott. The

   989   the ones of Ott. The

   996   alternative binder for the same body). 

   996   alternative binder for the same body). 

   997 

   997 

   998   For binders we distinguish between

   998   For binders we distinguish between

   999   \emph{shallow} and \emph{deep} binders.  Shallow binders are just

   999   \emph{shallow} and \emph{deep} binders.  Shallow binders are just

  1000   labels. The restriction we need to impose on them is that in case of

  1000   labels. The restriction we need to impose on them is that in case of

  1002   refer to atom types or to sets of atom types; in case of \isacommand{bind}

  1002   refer to atom types or to sets of atom types; in case of \isacommand{bind}

  1003   the labels must refer to atom types or lists of atom types. Two examples for

  1003   the labels must refer to atom types or lists of atom types. Two examples for

  1004   the use of shallow binders are the specification of lambda-terms, where a

  1004   the use of shallow binders are the specification of lambda-terms, where a

  1005   single name is bound, and type-schemes, where a finite set of names is

  1005   single name is bound, and type-schemes, where a finite set of names is

  1006   bound:

  1006   bound:

  1016   \begin{tabular}{@ {}l@ {}}

  1016   \begin{tabular}{@ {}l@ {}}

  1017   \isacommand{nominal\_datatype}~@{text ty} $=$\\

  1017   \isacommand{nominal\_datatype}~@{text ty} $=$\\

  1018   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\

  1018   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\

  1019   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\

  1019   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\

  1020   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%

  1020   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%

  1022   \end{tabular}

  1022   \end{tabular}

  1023   \end{tabular}

  1023   \end{tabular}

  1024   \end{center}

  1024   \end{center}

  1025 

  1025 

  1026   \noindent

  1026   \noindent

  1035   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

  1035   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

  1036   the atoms in one argument of the term-constructor, which can be bound in

  1036   the atoms in one argument of the term-constructor, which can be bound in

  1037   other arguments and also in the same argument (we will call such binders

  1037   other arguments and also in the same argument (we will call such binders

  1038   \emph{recursive}, see below). The binding functions are

  1038   \emph{recursive}, see below). The binding functions are

  1039   expected to return either a set of atoms (for \isacommand{bind (set)} and

  1039   expected to return either a set of atoms (for \isacommand{bind (set)} and

  1041   be defined by recursion over the corresponding type; the equations

  1041   be defined by recursion over the corresponding type; the equations

  1042   must be given in the binding function part of the scheme shown in

  1042   must be given in the binding function part of the scheme shown in

  1043   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

  1043   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

  1044   tuple patterns might be specified as:

  1044   tuple patterns might be specified as:

  1045   %

  1045   %

  1485   \end{equation}

  1485   \end{equation}

  1486 

  1486 

  1487   \noindent

  1487   \noindent

  1488   In this case we define a premise @{text P} using the relation

  1488   In this case we define a premise @{text P} using the relation

  1489   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly

  1489   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly

  1491   binding modes). This premise defines $\alpha$-equivalence of two abstractions

  1491   binding modes). This premise defines $\alpha$-equivalence of two abstractions

  1492   involving multiple binders. As above, we first build the tuples @{text "D"} and

  1492   involving multiple binders. As above, we first build the tuples @{text "D"} and

  1493   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding

  1493   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding

  1494   compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 

  1494   compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}). 

  1495   For $\approx_{\,\textit{set}}$  we also need

  1495   For $\approx_{\,\textit{set}}$  we also need

  1639   \end{lemma}

  1639   \end{lemma}

  1640 

  1640 

  1641   \begin{proof} 

  1641   \begin{proof} 

  1642   The proof is by mutual induction over the definitions. The non-trivial

  1642   The proof is by mutual induction over the definitions. The non-trivial

  1643   cases involve premises built up by $\approx_{\textit{set}}$, 

  1643   cases involve premises built up by $\approx_{\textit{set}}$, 

  1645   can be dealt with as in Lemma~\ref{alphaeq}.

  1645   can be dealt with as in Lemma~\ref{alphaeq}.

  1646   \end{proof}

  1646   \end{proof}

  1647 

  1647 

  1648   \noindent 

  1648   \noindent 

  1649   We can feed this lemma into our quotient package and obtain new types @{text

  1649   We can feed this lemma into our quotient package and obtain new types @{text

  1759   The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$

  1759   The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$

  1760   by the datatype package of Isabelle/HOL.

  1760   by the datatype package of Isabelle/HOL.

  1761 

  1761 

  1762   Finally we can add to our infrastructure a cases lemma (explained in the next section)

  1762   Finally we can add to our infrastructure a cases lemma (explained in the next section)

  1763   and a structural induction principle 

  1763   and a structural induction principle 

  1765   of the form

  1765   of the form

  1766   %

  1766   %

  1767   %\begin{equation}\label{weakinduct}

  1767   %\begin{equation}\label{weakinduct}

  1768   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}

  1768   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}

  1769   %\end{equation} 

  1769   %\end{equation} 

  1792   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\

  1792   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\

  1793   \end{tabular}

  1793   \end{tabular}

  1794   \end{center}

  1794   \end{center}

  1795   %

  1795   %

  1796   \noindent

  1796   \noindent

  1798   %%in \eqref{weakinduct}.

  1798   %%in \eqref{weakinduct}.

  1799   Having these equivariant properties established, we can

  1799   Having these equivariant properties established, we can

  1800   show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in

  1800   show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in

  1801   the support of its arguments, that means 

  1801   the support of its arguments, that means 

  1802 

  1802 

  1952   @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 

  1952   @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 

  1953   all well-founded. %It is straightforward to establish that these measures decrease 

  1953   all well-founded. %It is straightforward to establish that these measures decrease 

  1954   %in every induction step.

  1954   %in every induction step.

  1955   

  1955   

  1956   What is left to show is that we covered all cases. To do so, we use 

  1956   What is left to show is that we covered all cases. To do so, we use 

  1958   this lemma is of the form

  1958   this lemma is of the form

  1959   %

  1959   %

  1960   \begin{equation}\label{weakcases}

  1960   \begin{equation}\label{weakcases}

  1961   \infer{@{text "P\<^bsub>trm\<^esub>"}}

  1961   \infer{@{text "P\<^bsub>trm\<^esub>"}}

  1962   {\begin{array}{l@ {\hspace{9mm}}l}

  1962   {\begin{array}{l@ {\hspace{9mm}}l}

  1972   

  1972   

  1973   The only remaining difficulty is that in order to derive the stronger induction

  1973   The only remaining difficulty is that in order to derive the stronger induction

  1974   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that

  1974   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that

  1975   in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 

  1975   in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 

  1976   \emph{all} @{text Let}-terms. 

  1976   \emph{all} @{text Let}-terms. 

  1978   binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications

  1978   binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications

  1979   %

  1979   %

  1980   \begin{center}

  1980   \begin{center}

  1981   \begin{tabular}{l}

  1981   \begin{tabular}{l}

  1982   @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\

  1982   @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\

  2255   sense for our $\alpha$-equated terms. Third, it allows empty types that have no

  2255   sense for our $\alpha$-equated terms. Third, it allows empty types that have no

  2256   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2256   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2257   binding clauses. In Ott you specify binding clauses with a single body; we 

  2257   binding clauses. In Ott you specify binding clauses with a single body; we 

  2258   allow more than one. We have to do this, because this makes a difference 

  2258   allow more than one. We have to do this, because this makes a difference 

  2259   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 

  2259   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 

  2261   %

  2261   %

  2262   %Consider the examples

  2262   %Consider the examples

  2263   %

  2263   %

  2264   %\begin{center}

  2264   %\begin{center}

  2265   %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  2265   %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  2310   reasoning infrastructure is well beyond the purposes of his language. 

  2310   reasoning infrastructure is well beyond the purposes of his language. 

  2311   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.

  2311   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.

  2312   

  2312   

  2313   In a slightly different domain (programming with dependent types), the 

  2313   In a slightly different domain (programming with dependent types), the 

  2314   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2314   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2316   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it

  2316   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it

  2317   has a more operational flavour and calculates a partial (renaming) map. 

  2317   has a more operational flavour and calculates a partial (renaming) map. 

  2318   In this way, the definition can deal with vacuous binders. However, to our

  2318   In this way, the definition can deal with vacuous binders. However, to our

  2319   best knowledge, no concrete mathematical result concerning this

  2319   best knowledge, no concrete mathematical result concerning this

  2320   definition of $\alpha$-equivalence has been proved.\\[-7mm]    

  2320   definition of $\alpha$-equivalence has been proved.\\[-7mm]    

  2328   variables. For this extension we introduced new definitions of 

  2328   variables. For this extension we introduced new definitions of 

  2329   $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.

  2329   $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.

  2330   To specify general binders we used the specifications from Ott, but extended them 

  2330   To specify general binders we used the specifications from Ott, but extended them 

  2331   in some places and restricted

  2331   in some places and restricted

  2332   them in others so that they make sense in the context of $\alpha$-equated terms. 

  2332   them in others so that they make sense in the context of $\alpha$-equated terms. 

  2334   exist in Ott. 

  2334   exist in Ott. 

  2335   We have tried out the extension with calculi such as Core-Haskell, type-schemes 

  2335   We have tried out the extension with calculi such as Core-Haskell, type-schemes 

  2336   and approximately a  dozen of other typical examples from programming 

  2336   and approximately a  dozen of other typical examples from programming 

  2337   language research~\cite{SewellBestiary}. 

  2337   language research~\cite{SewellBestiary}. 

  2338   %The code

  2338   %The code