97   %also there one would like to bind multiple variables at once. 

    97   %also there one would like to bind multiple variables at once. 

    98 

    98 

    99   Binding multiple variables has interesting properties that cannot be captured

    99   Binding multiple variables has interesting properties that cannot be captured

   100   easily by iterating single binders. For example in the case of type-schemes we do not

   100   easily by iterating single binders. For example in the case of type-schemes we do not

   101   want to make a distinction about the order of the bound variables. Therefore

   101   want to make a distinction about the order of the bound variables. Therefore

   103   %

   105   %

   104   \begin{equation}\label{ex1}

   106   \begin{equation}\label{ex1}

   114   \end{equation}

   109   \end{equation}

   115   %

   110   %

   116   \noindent

   111   \noindent

   117   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

   118   only on \emph{vacuous} binders, such as

   113   only on \emph{vacuous} binders, such as

   137   @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}

   132   @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}

   138   \end{equation}

   133   \end{equation}

   139 

   134 

   140   \noindent

   135   \noindent

   141   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

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

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

   144   %

   139   %

   145   \begin{center}

   140   \begin{center}

   146   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}

   141   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}

   147   \end{center}

   142   \end{center}

   380   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 

   375   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 

   381   that our specifications make sense for reasoning about $\alpha$-equated terms.  

   376   that our specifications make sense for reasoning about $\alpha$-equated terms.  

   382   The main improvement over Ott is that we introduce three binding modes

   377   The main improvement over Ott is that we introduce three binding modes

   383   (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and 

   378   (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and 

   384   for free variables of our terms, and also derive a reasoning infrastructure

   379   for free variables of our terms, and also derive a reasoning infrastructure

   386 

   381 

   387 

   382 

   388   %\begin{figure}

   383   %\begin{figure}

   389   %\begin{boxedminipage}{\linewidth}

   384   %\begin{boxedminipage}{\linewidth}

   390   %%\begin{center}

   385   %%\begin{center}

   438 

   433 

   439   Two central notions in the nominal logic work are sorted atoms and

   434   Two central notions in the nominal logic work are sorted atoms and

   440   sort-respecting permutations of atoms. We will use the letters @{text "a,

   435   sort-respecting permutations of atoms. We will use the letters @{text "a,

   441   b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for

   436   b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for

   442   permutations. The purpose of atoms is to represent variables, be they bound or free. 

   437   permutations. The purpose of atoms is to represent variables, be they bound or free. 

   445   It is assumed that there is an infinite supply of atoms for each

   440   It is assumed that there is an infinite supply of atoms for each

   446   sort. In the interest of brevity, we shall restrict ourselves 

   441   sort. In the interest of brevity, we shall restrict ourselves 

   447   in what follows to only one sort of atoms.

   442   in what follows to only one sort of atoms.

   448 

   443 

   449   Permutations are bijective functions from atoms to atoms that are 

   444   Permutations are bijective functions from atoms to atoms that are 

   729   \begin{center}

   724   \begin{center}

   730   @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}

   725   @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}

   731   \end{center}

   726   \end{center}

   732 

   727 

   733   \noindent

   728   \noindent

   735   \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

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

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

   737   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to

   732   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to

   738   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

   739   "([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)"}

   798   \begin{theorem}[Support of Abstractions]\label{suppabs} 

   793   \begin{theorem}[Support of Abstractions]\label{suppabs} 

   799   Assuming @{text x} has finite support, then

   794   Assuming @{text x} has finite support, then

   800 

   795 

   801   \begin{center}

   796   \begin{center}

   802   \begin{tabular}{l}

   797   \begin{tabular}{l}

   806   \end{tabular}

   802   \end{tabular}

   807   \end{center}

   803   \end{center}

   808   \end{theorem}

   804   \end{theorem}

   809 

   805 

   810   \noindent

   806   \noindent

   811   This theorem states that the bound names do not appear in the support.

   807   This theorem states that the bound names do not appear in the support.

   812   For brevity we omit the proof and again refer the reader to

   808   For brevity we omit the proof and again refer the reader to

   814 

   810 

   815   %\noindent

   811   %\noindent

   816   %Below we will show the first equation. The others 

   812   %Below we will show the first equation. The others 

   817   %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 

   813   %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 

   818   %we have 

   814   %we have 

  1008   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

  1009   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

  1010   bound:

  1006   bound:

  1011 

  1007 

  1012   \begin{center}\small

  1008   \begin{center}\small

  1014   \begin{tabular}{@ {}l}

  1010   \begin{tabular}{@ {}l}

  1015   \isacommand{nominal\_datatype} @{text lam} $=$\\

  1011   \isacommand{nominal\_datatype} @{text lam} $=$\\

  1020   \end{tabular} &

  1015   \end{tabular} &

  1021   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

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

  1027   \end{tabular}

  1022   \end{tabular}

  1028   \end{tabular}

  1023   \end{tabular}

  1029   \end{center}

  1024   \end{center}

  1030 

  1025 

  1031   \noindent

  1026   \noindent

  1116   

  1111   

  1117   To make sure that atoms bound by deep binders cannot be free at the

  1112   To make sure that atoms bound by deep binders cannot be free at the

  1118   same time, we cannot have more than one binding function for a deep binder. 

  1113   same time, we cannot have more than one binding function for a deep binder. 

  1119   Consequently we exclude specifications such as

  1114   Consequently we exclude specifications such as

  1120   %

  1115   %

  1122   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  1117   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  1123   @{text "Baz\<^isub>1 p::pat t::trm"} & 

  1118   @{text "Baz\<^isub>1 p::pat t::trm"} & 

  1124      \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\

  1119      \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\

  1125   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 

  1120   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 

  1126      \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},

  1121      \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},

  1919   In the previous section we derived induction principles for $\alpha$-equated terms. 

  1914   In the previous section we derived induction principles for $\alpha$-equated terms. 

  1920   We call such induction principles \emph{weak}, because for a 

  1915   We call such induction principles \emph{weak}, because for a 

  1921   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}

  1916   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}

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

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

  1923   The problem with these implications is that in general they are difficult to establish.

  1918   The problem with these implications is that in general they are difficult to establish.

  1925   %%(for example we cannot assume the variable convention for them).

  1920   %%(for example we cannot assume the variable convention for them).

  1926 

  1921 

  1927   In \cite{UrbanTasson05} we introduced a method for automatically

  1922   In \cite{UrbanTasson05} we introduced a method for automatically

  1928   strengthening weak induction principles for terms containing single

  1923   strengthening weak induction principles for terms containing single

  1929   binders. These stronger induction principles allow the user to make additional

  1924   binders. These stronger induction principles allow the user to make additional

  1931   %These additional assumptions amount to a formal

  1926   %These additional assumptions amount to a formal

  1932   %version of the informal variable convention for binders. 

  1927   %version of the informal variable convention for binders. 

  1933   To sketch how this strengthening extends to the case of multiple binders, we use as

  1928   To sketch how this strengthening extends to the case of multiple binders, we use as

  1934   running example the term-constructors @{text "Lam"} and @{text "Let"}

  1929   running example the term-constructors @{text "Lam"} and @{text "Let"}

  1935   from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},

  1930   from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},

  1945   \end{tabular}

  1940   \end{tabular}

  1946   \end{center}

  1941   \end{center}

  1947 

  1942 

  1948   In \cite{UrbanTasson05} we showed how the weaker induction principles imply

  1943   In \cite{UrbanTasson05} we showed how the weaker induction principles imply

  1949   the stronger ones. This was done by some quite complicated, nevertheless automated,

  1944   the stronger ones. This was done by some quite complicated, nevertheless automated,

  1951   methods from the function package of Isabelle/HOL. 

  1946   methods from the function package of Isabelle/HOL. 

  1952   The reasoning principle these methods employ is well-founded induction. 

  1947   The reasoning principle these methods employ is well-founded induction. 

  1953   To use them in our setting, we have to discharge

  1948   To use them in our setting, we have to discharge

  1954   two proof obligations: one is that we have

  1949   two proof obligations: one is that we have

  1955   well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 

  1950   well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 

  1956   every induction step and the other is that we have covered all cases. 

  1951   every induction step and the other is that we have covered all cases. 

  1957   As measures we use the size functions 

  1952   As measures we use the size functions 

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

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

  1961   

  1956   

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

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

  1963   a cases lemma derived for each type. For the terms in \eqref{letpat} 

  1958   a cases lemma derived for each type. For the terms in \eqref{letpat} 

  1964   this lemma is of the form

  1959   this lemma is of the form

  1965   %

  1960   %

  2007   permutes names bound by @{text bn} and leaves the other names unchanged. We do this again

  2002   permutes names bound by @{text bn} and leaves the other names unchanged. We do this again

  2008   by lifting. For a

  2003   by lifting. For a

  2009   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 

  2004   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 

  2010   %

  2005   %

  2011   \begin{center}

  2006   \begin{center}

  2013   $\begin{cases}

  2008   $\begin{cases}

  2014   \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\

  2009   \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\

  2015   \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\

  2010   \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\

  2016   \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}  

  2011   \text{@{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise}  

  2017   \end{cases}$

  2012   \end{cases}$

  2246   Ott can also generate theorem prover code using a raw representation of

  2241   Ott can also generate theorem prover code using a raw representation of

  2247   terms, and in Coq also a locally nameless representation. The developers of

  2242   terms, and in Coq also a locally nameless representation. The developers of

  2248   this tool have also put forward (on paper) a definition for

  2243   this tool have also put forward (on paper) a definition for

  2249   $\alpha$-equivalence of terms that can be specified in Ott.  This definition is

  2244   $\alpha$-equivalence of terms that can be specified in Ott.  This definition is

  2250   rather different from ours, not using any nominal techniques.  To our

  2245   rather different from ours, not using any nominal techniques.  To our

  2252   notion of $\alpha$-equivalence.  Also the definition for the 

  2247   notion of $\alpha$-equivalence.  Also the definition for the 

  2253   notion of free variables

  2248   notion of free variables

  2254   is work in progress.

  2249   is work in progress.

  2255 

  2250 

  2256   Although we were heavily inspired by the syntax of Ott,

  2251   Although we were heavily inspired by the syntax of Ott,

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

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

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

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

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

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

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

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

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

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

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

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

  2339   We also introduced two binding modes (set and res) that do not 

  2334   We also introduced two binding modes (set and res) that do not 

  2340   exist in Ott. 

  2335   exist in Ott. 

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

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

  2342   and approximately a  dozen of other typical examples from programming 

  2337   and approximately a  dozen of other typical examples from programming 

  2348 

  2344 

  2349   We have left out a discussion about how functions can be defined over

  2345   We have left out a discussion about how functions can be defined over

  2350   $\alpha$-equated terms involving general binders. In earlier versions of Nominal

  2346   $\alpha$-equated terms involving general binders. In earlier versions of Nominal

  2352   hope to do better this time by using the function package that has recently

  2348   hope to do better this time by using the function package that has recently

  2353   been implemented in Isabelle/HOL and also by restricting function

  2349   been implemented in Isabelle/HOL and also by restricting function

  2355   provide more automation).

  2351   provide more automation).

  2356 

  2352 

  2357   %There are some restrictions we imposed in this paper that we would like to lift in

  2353   %There are some restrictions we imposed in this paper that we would like to lift in

  2358   %future work. One is the exclusion of nested datatype definitions. Nested

  2354   %future work. One is the exclusion of nested datatype definitions. Nested

  2359   %datatype definitions allow one to specify, for instance, the function kinds

  2355   %datatype definitions allow one to specify, for instance, the function kinds

  2384   \noindent

  2380   \noindent

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

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

  2386   %many discussions about Nominal Isabelle. 

  2382   %many discussions about Nominal Isabelle. 

  2387   We thank Peter Sewell for 

  2383   We thank Peter Sewell for 

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

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

  2390   %Stephanie Weirich suggested to separate the subgrammars

  2386   %Stephanie Weirich suggested to separate the subgrammars

  2391   %of kinds and types in our Core-Haskell example. \\[-6mm] 

  2387   %of kinds and types in our Core-Haskell example. \\[-6mm] 

  2392 *}

  2388 *}

  2393 

  2389 

  2394 

  2390