1719   infrastructure. One main point of our work is that we have completely

  1719   infrastructure. One point of our work is that we have completely

  1723   alpha-equivalences are equivariant.

  1723   alpha-equi\-va\-lences are equivariant.

  1733   The function package of Isabelle/HOL allows us to prove the first part is by mutual 

  1733   The function package of Isabelle/HOL allows us to prove the first part is by

  1734   induction over the definitions of the functions. The second is by a straightforward

  1734   mutual induction over the definitions of the functions (we know that they

  1735   induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 

  1735   are terminating functions, from which an induction principle can be

  1736   the first part.

  1736   derived). The second is by a straightforward induction over the rules of

  1737   @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using the first part.

  1741   previous section are equivalence relations.

  1742   previous section are indeed equivalence relations.

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

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

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

  1758   We can feed the last lemma into our quotient package and obtain new types

  1758   "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$. 

  1759   @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types

  1759   

  1760   @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors

  1760   We also obtain definitions for the term-constructors @{text

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

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

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

  1762   and similar definitions for the free-atom functions @{text

  1764   binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show

  1764   binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions

  1765   by induction over the definitions of alpha-equivalences that the ``raw'' 

  1765   are not really useful to the user, since they are given in terms of the

  1766   functions are respectful. This means we need to establish that

  1766   isomorphisms we obtained by creating new types in Isabelle/HOL (recall the

  1767 

  1767   picture shown in the Introduction).

  1768 

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

  1770   term-constructors are not equal, that is the property

  1771   

  1772   \begin{equation}\label{distinctalpha}

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

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

  1775   \end{equation}\smallskip

  1776   

  1777   \noindent

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

  1779   In order to derive this property, we use the definition of alpha-equivalence

  1780   and establish that

  1781   

  1782   \begin{equation}\label{distinctraw}

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

  1784   \end{equation}\smallskip

  1785 

  1786   \noindent

  1787   holds for the corresponding raw term-constructors.

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

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

  1790   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).

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

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

  1793   

  1785   }\]\smallskip

  1814   }\end{equation}\smallskip

  1786 

  1815   

  1787   \noindent

  1816   \noindent

  1788   The respectfulness properties are crucial, ... ???

  1817   whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}

  1789   However, these definitions are not really useful to the 

  1818   is defined. These implications can be established by induction on @{text

  1790   user, since they are given in terms of the isomorphisms we obtained by 

  1819   "\<approx>ty"}$_{1..n}$. Whereas the first, second and last implication are true by

  1791   creating new types in Isabelle/HOL (recall the picture shown in the 

  1820   how we stated our definitions, the third \emph{only} holds because of our

  1792   Introduction).

  1821   restriction imposed on the form of the binding functions---namely \emph{not}

  1793 

  1822   returning any bound atoms. In Ott, in contrast, the user may define @{text

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

  1823   "bn"}$_{1..m}$ so that they return bound atoms and in this case the third

  1795   term-constructors are not 

  1824   implication is \emph{not} true. A result is that the lifting of the

  1796   equal, that is

  1825   corresponding binding functions in Ott to alpha-equated terms is impossible.

  1797   

  1798   \[\label{distinctalpha}

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

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

  1801   \]\smallskip

  1802   

  1803   \noindent

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

  1805   In order to derive this fact, we use the definition of alpha-equivalence

  1806   and establish that

  1807   

  1808   \[\label{distinctraw}

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

  1810   \]\smallskip

  1811 

  1812   \noindent

  1813   holds for the corresponding raw term-constructors.

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

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

  1816   are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).

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

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

  1819   

  1820   \begin{center}

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

  1822   \end{center}  

  1823 

  1824   \noindent

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

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

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

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

  1829   implication by applying the corresponding rule in our alpha-equivalence

  1830   definition and by establishing the following auxiliary implications %facts 

  1831   %

  1832   \begin{equation}\label{fnresp}

  1833   \mbox{%

  1834   \begin{tabular}{ll@ {\hspace{7mm}}ll}

  1835   \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>"} &

  1836   \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\

  1837 

  1838   \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>"} &

  1839   \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\

  1840   \end{tabular}}

  1841   \end{equation}

  1842 

  1843   \noindent

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

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

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

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

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

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

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

  1851   result is that the lifting of the corresponding binding functions in Ott to alpha-equated

  1852   terms is impossible.

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

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

  1873   the premises in our alpha-equivalence relations.

  1846   the premises in our alpha-equiva\-lence relations.

  1874 

  1847 

  1875   Next we can lift the permutation 

  1848   Next we can lift the permutation operations defined in \eqref{ceqvt}. In

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

  1849   order to make this lifting to go through, we have to show that the

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

  1850   permutation operations are respectful. This amounts to showing that the

  1878   This amounts to showing that the 

  1851   alpha-equivalence relations are equivariant, which

  1879   alpha-equivalence relations are equivariant \cite{HuffmanUrban10}.

  1852   we already established in Lemma~\ref{equiv}. As a result we can add the

  1880   , which we already established 

  1853   equations

  1881   in Lemma~\ref{equiv}. 

  1882   As a result we can add the equations

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

  1867   Finally we can add to our infrastructure cases lemmas and a structural

  1897   and a structural induction principle 

  1868   induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases

  1898   for the types @{text "ty\<AL>"}$_{1..n}$. The conclusion of the induction principle is

  1869   lemmas allow the user to deduce a property @{text "P"} by exhaustively 

  1899   of the form

  1870   analysing all cases how the elements in a type @{text "ty\<AL>"}$_i$ can

  1900   

  1871   be constructed (that means one case for each of term-constructors @{text "C\<AL>"}$_{1..m}$

  1901   \begin{equation}\label{weakinduct}

  1872   of type @{text "ty\<AL>"}$_i\,$). These are lifted versions of the cases

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

  1873   lemma over the raw type  @{text "ty"}$_i$ and schematically look as

  1903   \end{equation} \smallskip

  1874   follows

  1904   

  1875 

  1905   \noindent

  1876   \[

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

  1877   \infer{P}

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

  1878   {\begin{array}{l}

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

  1879   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\

  1880   \hspace{5mm}\ldots\\

  1881   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\

  1882   \end{array}}

  1883   \]\smallskip

  1884 

  1885   \noindent

  1886   where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the 

  1887   property that is established by the case analysis. Similarly, we have an induction

  1888   principle for the types @{text "ty\<AL>"}$_{1..n}$, which is

  1889 

  1890    \[

  1891   \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}

  1892   {\begin{array}{l}

  1893   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\

  1894   \hspace{5mm}\ldots\\

  1895   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\

  1896   \end{array}}

  1897   \]\smallskip

  1898 

  1899   \noindent

  1900   whereby the @{text P}$_{1..n}$ are the properties established by induction 

  1901   and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. 

  1902   This induction principle has for all term constructors @{text "C"}$^\alpha$ 

  1903   a premise of the form

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

  1911   the recursive arguments of the term constructor. In case of the lambda-calculus,

  1912   the cases lemma and the induction principle boil down to the following:

  1913 

  1914   \[\mbox{

  1915   \begin{tabular}{c@ {\hspace{10mm}}c}

  1916   \infer{@{text "P"}}

  1917   {\begin{array}{l}

  1918    @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P"}\\

  1919    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}\\

  1920    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}

  1921    \end{array}} &

  1922 

  1923   \infer{@{text "P y"}}

  1924   {\begin{array}{l}

  1925    @{text "\<forall>x. P (Var\<^sup>\<alpha> x)"}\\

  1926    @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>1 \<and> P x\<^isub>2 \<Rightarrow> P (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  1927    @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}

  1928    \end{array}}

  1929   \end{tabular}}

  1930   \]\smallskip

  1928   \]

  1942   \]\smallskip

  1933   types @{text "ty\<AL>"}$_{1..n}$.  in \eqref{weakinduct}.  Having these

  1947   types @{text "ty\<AL>"}$_{1..n}$.  Having these

  1943   holds. This allows us to prove by induction that

  1957   holds. This allows us to prove by induction that every @{text x} of type

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

  1958   @{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by

  1945   This can be again shown by induction 

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

  1946   over @{text "ty\<AL>"}$_{1..n}$. 

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

  1947   Lastly, we can show that the support of 

  1961   "fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting, but

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

  1962   also provides evidence that our notions of free-atoms and alpha-equivalence

  1949   This fact is important in a nominal setting, but also provides evidence 

  1963   are sensible.

  1950   that our notions of free-atoms and alpha-equivalence are correct.