1490   The first usefull property about term-constructors @{text

  1490   The first useful property about term-constructors 

  1491   "C"}$^\alpha_{1..m}$ is to know that they are distinct, that is

  1491   is to know that they are distinct, that is

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

  1492   %

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

  1493   \begin{equation}\label{distinctalpha}

  1494 

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

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

  1496   \end{equation}

  1497   

  1498   \noindent

  1499   By definition of alpha-equivalence on raw terms we can show that

  1500   for the raw term-constructors

  1501 

  1502   \begin{center}

  1503   @{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"}.

  1504   \end{center}

  1505 

  1506   \noindent

  1507   In order to generate \eqref{distinctalpha} from this fact, the quotient

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

  1509   are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}.

  1510   

  1511   Given a term-constructor @{text C} of type @{text ty} and argument

  1512   types @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, respectfullness means that

  1513   %

  1514   \begin{center}

  1515   aa

  1516   \end{center}

  1517    

  1518 

  1519   \mbox{}\bigskip\bigskip

  1775   setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation

  1800   is described in \cite{NaraschewskiNipkow99} about a formalisation of the

  1776   of the algorithm W. This formalisation implements binding in type schemes

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

  1777   using a de-Bruijn indices representation. Since type schemes contain only a

  1802   de-Bruijn indices representation. Since type schemes contain only a single

  1778   single binder, different indices do not refer to different binders (as in

  1803   binder, different indices do not refer to different binders (as in the usual

  1779   the usual de-Bruijn representation), but to different bound variables. Also

  1804   de-Bruijn representation), but to different bound variables. A similar idea

  1780   recently an extension for general binders has been proposed for the locally

  1805   has been recently explored for general binders in the locally nameless

  1781   nameless approach to binding \cite{chargueraud09}.  In this proposal, de-Bruijn 

  1806   approach to binding \cite{chargueraud09}.  There de-Bruijn indices consist

  1782   indices consist of two numbers, one referring to the place where a variable is bound

  1807   of two numbers, one referring to the place where a variable is bound and the

  1783   and the other to which variable is bound. The reasoning infrastructure for both

  1808   other to which variable is bound. The reasoning infrastructure for both

  1794   technique supports very elegantly some aspects of \emph{single} binding, and

  1823   technique supports very elegantly many aspects of \emph{single} binding, and

  1796   of SML \cite{LeeCraryHarper07}. We are not aware how multiple binders of SML

  1825   of SML \cite{LeeCraryHarper07}. We are, however, not aware how multiple binders of SML

  1797   are represented in this work, but the submitted Twelf-solution for the

  1826   are represented in this work. Judging from the submitted Twelf-solution for the

  1798   POPLmark challenge reveals that HOAS cannot easily deal with binding

  1827   POPLmark challenge, HOAS cannot easily deal with binding

  1800   the second part of this challenge, @{text "Let"}s involve patterns and bind

  1829   the second part of this challenge, @{text "Let"}s involve patterns that bind

  1801   multiple variables at once. In such situations, HOAS needs to use, essentially,

  1830   multiple variables at once. In such situations, HOAS representations have to 

  1802   iterated single binders for representing multiple binders.

  1831   resort, essentially, to the iterated-single-binders-approach with all the unwanted

  1832   consequences for reasoning about terms. 

  1806   use the approach based on iterated single binders. Our experience with the

  1836   use also the approach based on iterated single binders. Our experience with the

  1807   latter formalisation has been far from satisfying. The major pain arises

  1837   latter formalisation has been disappointing. The major pain arises

  1815   \cite{ott-jfp}. This tool is a nifty front end for creating \LaTeX{}

  1845   \cite{ott-jfp}. This tool is a nifty front-end for creating \LaTeX{}

  1818   representation and a locally nameless representation for terms. The

  1848   representation and in Coq also a locally nameless representation for

  1819   developers of this tool have also put forward a definition for the notion of

  1849   terms. The developers of this tool have also put forward (on paper) a

  1820   alpha-equivalence of the term-calculi that can be specified in Ott.  This

  1850   definition for the notion of alpha-equivalence of the term-calculi that can

  1821   definition is rather different from ours, not using any of the nominal

  1851   be specified in Ott.  This definition is rather different from ours, not

  1822   techniques; it also aims for maximum expressivity, covering as many binding

  1852   using any nominal techniques; it also aims for maximum expressivity,

  1823   structures from programming language research as possible.  Although we were

  1853   covering as many binding structures from programming language research as

  1824   heavily inspired by their syntax, their definition of alpha-equivalence was

  1854   possible.  Although we were heavily inspired by their syntax, their

  1825   no use at all for our extension of Nominal Isabelle. First, it is far too

  1855   definition of alpha-equivalence was no use at all for our extension of

  1826   complicated to be a basis for automated proofs implemented on the ML-level

  1856   Nominal Isabelle. First, it is far too complicated to be a basis for

  1827   of Isabelle/HOL. Second, it covers cases of binders depending on other

  1857   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  1828   binders, which just do not make sense for our alpha-equated terms, and it

  1858   covers cases of binders depending on other binders, which just do not make

  1829   also allows empty types that have no meaning in a HOL-based theorem

  1859   sense for our alpha-equated terms. It also allows empty types that have

  1830   prover. Because of how we set up our definitions, we had to impose some

  1860   no meaning in a HOL-based theorem prover. 

  1861 

  1862   Because of how we set up our definitions, we had to impose some

  1832   in Ott. Our motivation is that we can still cover interesting term-calculi

  1864   in Ott. Our expectation is that we can still cover many interesting term-calculi

  1835   unfortunately not yet powerful enough. On the other hand we are not aware

  1867   unfortunately not yet powerful enough to implement them. On the other hand 

  1836   that Ott can make any distinction between our three different binding

  1868   we are not aware that Ott can make any distinction between our three 

  1837   modes. Also, definitions for notions like free-variables are work in

  1869   different binding modes. Also, definitions for notions like free-variables 

  1838   progress in Ott.

  1870   are work in progress in Ott. Since Ott produces either raw representations

  1871   or locally nameless representations it can largely rely on the reasoning

  1872   infrastructure derived automatically by the theorem provers. In contrast,

  1873   have to make considerable effort to establish a reasoning infrastructure 

  1874   for alpha-equated terms.