311   datatype in Isabelle/HOL); identify then the $\alpha$-equivalence classes in

   311   datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in

  1602   introducing the reasoning infrastructure for the $\alpha$-equated types the

  1602   with establishing the reasoning infrastructure for the $\alpha$-equated types

  1603   user originally specified. We sketch in this section the facts we need for establishing

  1603   @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch

  1604   this reasoning infrastructure. First we have to show that the

  1604   in this section the proofs we need for establishing this infrastructure. One

  1605   main point of our work is that we have completely automated these proofs in Isabelle/HOL.

  1606 

  1607   First we establish that the

  1609   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions

  1612   Given the raw types @{text "ty"}$_{1..n}$ and binding functions

  1610   @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and 

  1613   @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 

  1611   @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.

  1614   @{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.

  1625   "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text

  1628   "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text

  1626   "C"}$_{1..m}$, and similar definitions for the free-atom functions @{text

  1629   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text

  1627   "fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text

  1630   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text

  1628   "bn"}$^\alpha_{1..k}$. However, these definitions are not really useful to the 

  1631   "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the 

  1633   The first useful property to the user is the fact that term-constructors are 

  1636   The first useful property for the user is the fact that distinct 

  1634   distinct, that is

  1637   term-constructors are not 

  1638   equal, that is

  1637   \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 

  1641   \mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~% 

  1638   @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} 

  1642   @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 

  1639   \end{equation}

  1643   \end{equation}

  1640   

  1644   

  1641   \noindent

  1645   \noindent

  1642   By definition of $\alpha$-equivalence we can show that

  1646   whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.

  1643   for the raw term-constructors

  1647   In order to derive this fact, we use the definition of $\alpha$-equivalence

  1648   and establish that

  1646   \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}

  1651   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}

  1647   \end{equation}

  1652   \end{equation}

  1648 

  1653 

  1649   \noindent

  1654   \noindent

  1650   In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient

  1655   holds for the corresponding raw term-constructors.

  1651   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 

  1656   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient

  1657   package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 

  1653   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types

  1659   Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types

  1654   @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that

  1660   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that

  1655   %

  1661   %

  1656   \begin{center}

  1662   \begin{center}

  1657   @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}

  1663   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1661   are $\alpha$-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments

  1667   holds under the assumptions that we have \mbox{@{text

  1662   and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by 

  1668   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}

  1663   analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish 

  1669   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and

  1664   the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 

  1670   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this

  1665   for the type @{text ty\<^isub>i}, we have that

  1671   implication by applying the corresponding rule in our $\alpha$-equivalence

  1666   %

  1672   definition and by establishing the following auxiliary facts 

  1667   \begin{center}

  1668   @{text "x \<approx>ty\<^isub>i y"} implies @{text "x \<approx>bn\<^isub>i y"}

  1669   \end{center}

  1670 

  1671   \noindent

  1672   This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. 

  1673    

  1674   Having established respectfulness for every raw term-constructor, the 

  1675   quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.

  1676   In fact we can from now on lift facts from the raw level to the $\alpha$-equated level

  1677   as long as they contain raw term-constructors only. The 

  1678   induction principles derived by the datatype package in Isabelle/HOL for the types @{text

  1679   "ty"}$_{1..n}$ fall into this category. So we can also add to our infrastructure

  1680   induction principles that establish

  1681 

  1682   \begin{center}

  1683   @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "}

  1684   \end{center} 

  1685 

  1686   \noindent

  1687   for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties

  1688   defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of 

  1689   these induction principles look

  1690   as follows

  1691 

  1692   \begin{center}

  1693   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^esub>\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^esub>\<^isub>j x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 

  1694   \end{center}

  1695 

  1696   \noindent

  1697   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 

  1698   Next we lift the permutation operations defined in \eqref{ceqvt} for

  1699   the raw term-constructors @{text "C"}. These facts contain, in addition 

  1700   to the term-constructors, also permutation operations. In order to make the 

  1701   lifting go through, 

  1702   we have to know that the permutation operations are respectful 

  1703   w.r.t.~$\alpha$-equivalence. This amounts to showing that the 

  1704   $\alpha$-equivalence relations are equivariant, which we already established 

  1705   in Lemma~\ref{equiv}. As a result we can establish the equations

  1706   

  1707   \begin{equation}\label{calphaeqvt}

  1708   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

  1709   \end{equation}

  1710 

  1711   \noindent

  1712   for our infrastructure. In a similar fashion we can lift the equations

  1713   characterising the free-atom functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fa_bn\<AL>\<^isub>k"}, and the 

  1714   binding functions @{text "bn\<AL>\<^isub>k"}. The necessary respectfulness lemmas for these

  1715   lifting are the properties:

  1720   @{text "x \<approx>ty\<^isub>j y"} implies @{text "fa_ty\<^isub>j x = fa_ty\<^isub>j y"}\\

  1677   @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\

  1721   @{text "x \<approx>ty\<^isub>k y"} implies @{text "fa_bn\<^isub>k x = fa_bn\<^isub>k y"}\\

  1678   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\

  1722   @{text "x \<approx>ty\<^isub>k y"} implies @{text "bn\<^isub>k x = bn\<^isub>k y"}

  1679   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\

  1680   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\

  1727   which can be established by induction on @{text "\<approx>ty"}. Whereas the first

  1685   They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,

  1728   property is always true by the way we defined the free-atom

  1686   second and last implication are true by how we stated our definitions, the 

  1729   functions for types, the second and third do \emph{not} hold in general. There is, in principle, 

  1687   third \emph{only} holds because of our restriction

  1730   the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound

  1688   imposed on the form of the binding functions---namely \emph{not} returning 

  1731   atom. Then the third property is just not true. However, our 

  1689   any bound atoms. In Ott, in contrast, the user may 

  1732   restrictions imposed on the binding functions

  1690   define @{text "bn"}$_{1..m}$ so that they return bound

  1733   exclude this possibility.

  1691   atoms and in this case the third implication is \emph{not} true. A 

  1734 

  1692   result is that the lifing of the corresponding binding functions to $\alpha$-equated

  1735   Having the facts \eqref{fnresp} at our disposal, we can lift the

  1693   terms is impossible.

  1736   definitions that characterise when two terms of the form

  1694 

  1737 

  1695   Having established respectfulness for the raw term-constructors, the 

  1738   \begin{center}

  1696   quotient package is able to automatically deduce \eqref{distinctalpha} from 

  1739   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}

  1697   \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 

  1698   also lift properties that characterise when two raw terms of the form

  1699   %

  1700   \begin{center}

  1701   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1745 

  1707   %

  1746   \begin{center}

  1708   \begin{center}

  1747   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}

  1709   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1748   \end{center}

  1710   \end{center}

  1749 

  1711 

  1750   \noindent

  1712   \noindent

  1751   We call these conditions as \emph{quasi-injectivity}. Except for one function, which

  1713   We call these conditions as \emph{quasi-injectivity}. They correspond to

  1752   we have to lift in the next section, we completed

  1714   the premises in our $\alpha$-equivalence relations.

  1753   the lifting part of establishing the reasoning infrastructure. 

  1715 

  1754 

  1716   Next we can lift the permutation 

  1755   By working now completely on the $\alpha$-equated level, we can first show that 

  1717   operations defined in \eqref{ceqvt}. In order to make this 

  1756   the free-atom functions and binding functions

  1718   lifting to go through, we have to show that the permutation operations are respectful. 

  1757   are equivariant, namely

  1719   This amounts to showing that the 

  1758 

  1720   $\alpha$-equivalence relations are equivariant, which we already established 

  1721   in Lemma~\ref{equiv}. As a result we can add the equations

  1722   %

  1723   \begin{equation}\label{calphaeqvt}

  1724   @{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)"}

  1725   \end{equation}

  1726 

  1727   \noindent

  1728   to our infrastructure. In a similar fashion we can lift the defining equations

  1729   of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and

  1730   @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text

  1731   "bn\<AL>"}$_{1..m}$ and of the size functions @{text "size_ty\<AL>"}$_{1..n}$.

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

  1733   by the datatype package of Isabelle/HOL.

  1734 

  1735   Finally we can add to our infrastructure a structural induction principle 

  1736   for the types @{text "ty\<AL>"}$_{i..n}$ whose 

  1737   conclusion of the form

  1738   %

  1739   \begin{equation}\label{weakinduct}

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

  1741   \end{equation} 

  1742 

  1743   \noindent

  1744   whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 

  1745   have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each

  1746   term constructor @{text "C"}$^\alpha$ a premise of the form

  1747   %

  1748   \begin{equation}\label{weakprem}

  1749   \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)"}} 

  1750   \end{equation}

  1751 

  1752   \noindent 

  1753   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 

  1754   the recursive arguments of @{text "C\<AL>"}. 

  1755 

  1756   By working now completely on the $\alpha$-equated level, we

  1757   can first show that the free-atom functions and binding functions are

  1758   equivariant, namely

  1759   %

  1761   @{text "p \<bullet> (fa_ty\<^sup>\<alpha> x)"} & $=$ & @{text "fa_ty\<^sup>\<alpha> (p \<bullet> x)"}\\

  1762   @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\

  1762   @{text "p \<bullet> (fa_bn\<^sup>\<alpha> x)"} & $=$ & @{text "fa_bn\<^sup>\<alpha> (p \<bullet> x)"}\\

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

  1763   @{text "p \<bullet> (bn\<^sup>\<alpha> x)"}    & $=$ & @{text "bn\<^sup>\<alpha> (p \<bullet> x)"}

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

  1764   \end{tabular}

  1765   \end{tabular}

  1765   \end{center}

  1766   \end{center}

  1766 

  1767 

  1767   \noindent

  1768   \noindent

  1768   These properties can be established by structural induction over the @{text x}

  1769   These properties can be established using the induction principle

  1769   (using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).

  1770   in \eqref{weakinduct}.

  1770 

  1771   Having these equivariant properties established, we can

  1771   Until now we have not yet derived anything about the support of the 

  1772   $\alpha$-equated terms. This however will be necessary in order to derive

  1773   the strong induction principles in the next section.

  1774   Using the equivariance properties in \eqref{ceqvt} we can

  1778   @{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>n) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}

  1775   @{text "(supp x\<^isub>1 \<union> \<dots> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}

  1783  

  1780   for every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, 

  1784   \begin{center}

  1781   namely @{text "finite (supp x)"}. This can be again shown by induction 

  1785   @{text "finite (supp x\<^isub>i)"}

  1782   over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of 

  1786   \end{center}

  1783   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.

  1787 

  1784   This important fact provides evidence that our notions of free-atoms and 

  1788   \noindent

  1785   $\alpha$-equivalence are correct.

  1789   by a structural induction over @{text "x\<^isub>1, \<dots>, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types 

  1790   @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}). Lastly, we can show that the support of elements in 

  1791   @{text "ty\<AL>\<^bsub>1..n\<^esub>"} coincides with @{text "fa_ty\<AL>\<^bsub>1..n\<^esub>"}.

  1794   For every @{text "x\<^isub>i"} of type @{text "ty\<AL>\<^bsub>1..n\<^esub>"}, we have that 

  1788   For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have

  1795   @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"} holds.

  1789   @{text "supp x = fa_ty\<AL>\<^isub>i x"}.

  1799   The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case

  1793   The proof is by induction. In each case

  1801   term-constructors and the use then quasi-injectivity lemmas in order to complete the

  1795   term-constructors and then use the quasi-injectivity lemmas in order to complete the

  1807   for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"} 

  1801   for the types @{text "ty\<AL>"}$_{1..n}$ 

  1809   then establish facts about these lifted definitions. All necessary proofs

  1803   then by establishing facts about these lifted definitions. All necessary proofs

  1817   \isacommand{atom\_decl}~@{text "var"}\\

  1811   \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]

  1818   \isacommand{atom\_decl}~@{text "cvar"}\\

  1819   \isacommand{atom\_decl}~@{text "tvar"}\\[1mm]

  1891   We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},

  1883   We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},

  1892   the induction hypothesis requires us to establish the implication

  1884   the induction hypothesis requires us to establish the implications \eqref{weakprem}.

  1893   %

  1885   The problem with these implications is that in general they are not easy to establish.

  1894   \begin{equation}\label{weakprem}

  1895   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. 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>n)"} 

  1896   \end{equation}

  1897 

  1898   \noindent

  1899   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 

  1900   The problem with this implication is that in general it is not easy to establish it.

  1917   we define  %

  1902   we define @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"} with @{text "y\<^isub>i"} determined as follows:

  1918   \begin{center}

  1919   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}

  1920   \end{center}

  1921 

  1922   \noindent

  1923   with @{text "y\<^isub>i"} determined as follows:

  1970 

  1949   %

  2016 

  1995   %

  2026   establish

  2005   establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.

  2027 

  2028   \begin{center}

  2029   @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}

  2030   \end{center}

  2031 

  2032   \noindent

  2036 

  2009   %

  2066   algorithm W. This formalisation implements binding in type schemes using a

  2039   algorithm W. This formalisation implements binding in type-schemes using a

  2067   de-Bruijn indices representation. Since type schemes in W contain only a single

  2040   de-Bruijn indices representation. Since type-schemes in W contain only a single

  2216   extension will become part of the Isabelle distribution, but for the moment

  2176   extension will become part of the Isabelle distribution.\footnote{For the moment

  2219   {http://isabelle.in.tum.de/nominal/download}.

  2179   {http://isabelle.in.tum.de/nominal/download}.}

  2240   properties like \eqref{bnprop} provide us with means to support more interesting

  2200   properties like

  2201   %

  2202   \begin{center}

  2203   @{text "fa_ty x  =  bn x \<union> fa_bn x"}.

  2204   \end{center}

  2205   

  2206   \noindent

  2207   provide us with means to support more interesting

  2245   imagine that there is need for a binding mode \isacommand{bind\_\#list} with

  2212   imagine that there is need for a binding mode 

  2246   an associated abstraction of the form

  2247   %

  2248   \begin{center}

  2249   @{term "Abs_dist as x"}

  2250   \end{center}

  2251 

  2252   \noindent

  2257   \medskip

  2217   %\medskip

  2258   \noindent

  2218   %\noindent

  2259   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  

  2219   %{\bf Acknowledgements:} We are very grateful to Andrew Pitts for  

  2260   many discussions about Nominal Isabelle. We also thank Peter Sewell for 

  2220   %many discussions about Nominal Isabelle. We also thank Peter Sewell for 

  2261   making the informal notes \cite{SewellBestiary} available to us and 

  2221   %making the informal notes \cite{SewellBestiary} available to us and 

  2262   also for patiently explaining some of the finer points of the work on the Ott-tool.

  2222   %also for patiently explaining some of the finer points of the work on the Ott-tool.

  2263   Stephanie Weirich suggested to separate the subgrammars

  2223   %Stephanie Weirich suggested to separate the subgrammars

  2264   of kinds and types in our Core-Haskell example.  

  2224   %of kinds and types in our Core-Haskell example.