1 (*<*)

     2 theory Paper

     3 imports "../Nominal/Nominal2" 

     4         "~~/src/HOL/Library/LaTeXsugar"

     5 begin

     6 

     7 consts

     8   fv :: "'a \<Rightarrow> 'b"

     9   abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"

    10   alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    11   abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"

    12   equ2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    13   Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 

    14   Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 

    15 

    16 definition

    17  "equal \<equiv> (op =)" 

    18 

    19 fun alpha_set_ex where

    20   "alpha_set_ex (bs, x) R f (cs, y) = (\<exists>pi. alpha_set (bs, x) R f pi (cs, y))"

    21  

    22 fun alpha_res_ex where

    23   "alpha_res_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_res (bs, x) R f pi (cs, y))"

    24 

    25 fun alpha_lst_ex where

    26   "alpha_lst_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_lst (bs, x) R f pi (cs, y))"

    27 

    28 

    29 

    30 notation (latex output)

    31   swap ("'(_ _')" [1000, 1000] 1000) and

    32   fresh ("_ # _" [51, 51] 50) and

    33   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and

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

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

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

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

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

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

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

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

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

    43   equal ("=") and

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

    45   alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and 

    46   alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and 

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

    48   Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and

    49   Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) and

    50   Abs_res ("[_]\<^bsub>set+\<^esub>._") and

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

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

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

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

    55 

    56 consts alpha_trm ::'a

    57 consts fa_trm :: 'a

    58 consts fa_trm_al :: 'a

    59 consts alpha_trm2 ::'a

    60 consts fa_trm2 :: 'a

    61 consts fa_trm2_al :: 'a

    62 consts supp2 :: 'a

    63 consts ast :: 'a

    64 consts ast' :: 'a

    65 consts bn_al :: "'b \<Rightarrow> 'a"

    66 notation (latex output) 

    67   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and

    68   fa_trm ("fa\<^bsub>trm\<^esub>") and

    69   fa_trm_al ("fa\<AL>\<^bsub>trm\<^esub>") and

    70   alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and

    71   fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and

    72   fa_trm2_al ("'(fa\<AL>\<^bsub>assn\<^esub>, fa\<AL>\<^bsub>trm\<^esub>')") and

    73   ast ("'(as, t')") and

    74   ast' ("'(as', t\<PRIME> ')") and

    75   equ2 ("'(=, =')") and

    76   supp2 ("'(supp, supp')") and

    77   bn_al ("bn\<^sup>\<alpha> _" [100] 100)

    78 (*>*)

    79 

    80 

    81 section {* Introduction *}

    82 

    83 text {*

    84   So far, Nominal Isabelle provided a mechanism for constructing alpha-equated

    85   terms, for example lambda-terms

    86 

    87   \[

    88   @{text "t ::= x | t t | \<lambda>x. t"}

    89   \]\smallskip

    90 

    91   \noindent

    92   where free and bound variables have names.  For such alpha-equated terms,

    93   Nominal Isabelle derives automatically a reasoning infrastructure that has

    94   been used successfully in formalisations of an equivalence checking

    95   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

    96   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

    97   \cite{BengtsonParow09} and a strong normalisation result for cut-elimination

    98   in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for

    99   formalisations in the locally-nameless approach to binding

   100   \cite{SatoPollack10}.

   101 

   102   However, Nominal Isabelle has fared less well in a formalisation of the

   103   algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,

   104   respectively, of the form

   105 

   106   \begin{equation}\label{tysch}

   107   \begin{array}{l}

   108   @{text "T ::= x | T \<rightarrow> T"}\hspace{15mm}

   109   @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}

   110   \end{array}

   111   \end{equation}\smallskip

   112 

   113   \noindent

   114   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of

   115   type-variables.  While it is possible to implement this kind of more general

   116   binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy

   117   formalisation of W. For example, the usual definition for a

   118   type being an instance of a type-scheme requires in the iterated version 

   119   the following auxiliary \emph{unbinding relation}:

   120 

   121   \[

   122   \infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad

   123   \infer{\forall @{text x.S} \hookrightarrow (@{text x}\!::\!@{text xs}, @{text T})}

   124    {@{text S} \hookrightarrow (@{text xs}, @{text T})}

   125   \]\smallskip

   126 

   127   \noindent

   128   Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to

   129   address the following problem:

   130   Given a type-scheme, say @{text S}, how does one get access to the bound type-variables 

   131   and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though 

   132   in general it will only provide \emph{a} list of type-variables together with \emph{a} type that are  

   133   ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function

   134   for alpha-equated type-schemes. With the unbinding relation  

   135   in place, we can define when a type @{text T} is an instance of a type-scheme @{text S} as follows:

   136 

   137   \[

   138   @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}

   139   \]\smallskip

   140   

   141   \noindent

   142   This means there exists a list of type-variables @{text xs} and a type @{text T'} to which

   143   the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} whose domain is

   144   @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.

   145   The problem with this definition is that we cannot follow the usual proofs 

   146   that are by induction on the type-part of the type-scheme (since it is under

   147   an existential quantifier and only an alpha-variant). The implementation of 

   148   type-schemes using iterations of single binders 

   149   prevents us from directly ``unbinding'' the bound type-variables and the type-part. 

   150   Clearly, a more dignified approach for formalising algorithm W is desirable. 

   151   The purpose of this paper is to introduce general binders, which 

   152   allow us to represent type-schemes so that they can bind multiple variables at once

   153   and as a result solve this problem more straightforwardly.

   154   The need of iterating single binders is also one reason

   155   why the existing Nominal Isabelle and similar theorem provers that only provide

   156   mechanisms for binding single variables have so far not fared very well with

   157   the more advanced tasks in the POPLmark challenge \cite{challenge05},

   158   because also there one would like to bind multiple variables at once.

   159 

   160   Binding multiple variables has interesting properties that cannot be captured

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

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

   163   we would like to regard in \eqref{ex1} below  the first pair of type-schemes as alpha-equivalent,

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

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

   166 

   167   \begin{equation}\label{ex1}

   168   @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, y}. y \<rightarrow> x"}\hspace{10mm}

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

   170   \end{equation}\smallskip

   171 

   172   \noindent

   173   Moreover, we like to regard type-schemes as alpha-equivalent, if they differ

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

   175 

   176   \begin{equation}\label{ex3}

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

   178   \end{equation}\smallskip

   179 

   180   \noindent

   181   where @{text z} does not occur freely in the type.  In this paper we will

   182   give a general binding mechanism and associated notion of alpha-equivalence

   183   that can be used to faithfully represent this kind of binding in Nominal

   184   Isabelle.  The difficulty of finding the right notion for alpha-equivalence

   185   can be appreciated in this case by considering that the definition given for

   186   type-schemes by Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).

   187 

   188   However, the notion of alpha-equivalence that is preserved by vacuous

   189   binders is not always wanted. For example in terms like

   190 

   191   \begin{equation}\label{one}

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

   193   \end{equation}\smallskip

   194 

   195   \noindent

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

   197   \mbox{@{text "y = 2"}} are given, but it would be often unusual (particularly

   198   in strict languages) to regard \eqref{one} as alpha-equivalent with

   199 

   200   \[

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

   202   \]\smallskip

   203 

   204   \noindent

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

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

   207   binders has to agree.

   208 

   209   However, we found that this is still not sufficient for dealing with

   210   language constructs frequently occurring in programming language

   211   research. For example in @{text "\<LET>"}s containing patterns like

   212 

   213   \begin{equation}\label{two}

   214   @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}

   215   \end{equation}\smallskip

   216 

   217   \noindent

   218   we want to bind all variables from the pattern inside the body of the

   219   $\mathtt{let}$, but we also care about the order of these variables, since

   220   we do not want to regard \eqref{two} as alpha-equivalent with

   221 

   222   \[

   223   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}

   224   \]\smallskip

   225 

   226   \noindent

   227   As a result, we provide three general binding mechanisms each of which binds

   228   multiple variables at once, and let the user choose which one is intended

   229   when formalising a term-calculus.

   230 

   231   By providing these general binding mechanisms, however, we have to work

   232   around a problem that has been pointed out by Pottier \cite{Pottier06} and

   233   Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form

   234 

   235   \[

   236   @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}

   237   \]\smallskip

   238 

   239   \noindent

   240   we care about the information that there are as many bound variables @{text

   241   "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if

   242   we represent the @{text "\<LET>"}-constructor by something like

   243 

   244   \[

   245   @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}

   246   \]\smallskip

   247 

   248   \noindent

   249   where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text

   250   "x\<^isub>i"} becomes bound in @{text s}. In this representation the term

   251   \mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly

   252   legal instance, but the lengths of the two lists do not agree. To exclude

   253   such terms, additional predicates about well-formed terms are needed in

   254   order to ensure that the two lists are of equal length. This can result in

   255   very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid

   256   this, we will allow type specifications for @{text "\<LET>"}s as follows

   257 

   258   \[

   259   \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll}

   260   @{text trm} & @{text "::="}  & @{text "\<dots>"} \\

   261               & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 

   262                                  \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]

   263   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\

   264                &  @{text "|"}  & @{text "\<ACONS>  name  trm  assn"}

   265   \end{tabular}}

   266   \]\smallskip

   267 

   268   \noindent

   269   where @{text assn} is an auxiliary type representing a list of assignments

   270   and @{text bn} an auxiliary function identifying the variables to be bound

   271   by the @{text "\<LET>"}. This function can be defined by recursion over @{text

   272   assn} as follows

   273 

   274   \[

   275   @{text "bn(\<ANIL>) ="}~@{term "{}"} \hspace{10mm} 

   276   @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 

   277   \]\smallskip

   278 

   279   \noindent

   280   The scope of the binding is indicated by labels given to the types, for

   281   example @{text "s::trm"}, and a binding clause, in this case

   282   \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding

   283   clause states that all the names the function @{text "bn(as)"} returns

   284   should be bound in @{text s}.  This style of specifying terms and bindings

   285   is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work

   286   extends Ott in several aspects: one is that we support three binding

   287   modes---Ott has only one, namely the one where the order of binders matters.

   288   Another is that our reasoning infrastructure, like strong induction principles

   289   and the notion of free variables, is derived from first principles within 

   290   the Isabelle/HOL theorem prover.

   291 

   292   However, we will not be able to cope with all specifications that are

   293   allowed by Ott. One reason is that Ott lets the user specify `empty' types

   294   like \mbox{@{text "t ::= t t | \<lambda>x. t"}} where no clause for variables is

   295   given. Arguably, such specifications make some sense in the context of Coq's

   296   type theory (which Ott supports), but not at all in a HOL-based environment

   297   where every datatype must have a non-empty set-theoretic model

   298   \cite{Berghofer99}.  Another reason is that we establish the reasoning

   299   infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a

   300   reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or

   301   `raw', terms. While our alpha-equated terms and the `raw' terms produced by

   302   Ott use names for bound variables, there is a key difference: working with

   303   alpha-equated terms means, for example, that the two type-schemes

   304 

   305   \[

   306   @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 

   307   \]\smallskip

   308   

   309   \noindent

   310   are not just alpha-equal, but actually \emph{equal}! As a result, we can

   311   only support specifications that make sense on the level of alpha-equated

   312   terms (offending specifications, which for example bind a variable according

   313   to a variable bound somewhere else, are not excluded by Ott, but we have

   314   to).  

   315 

   316   Our insistence on reasoning with alpha-equated terms comes from the

   317   wealth of experience we gained with the older version of Nominal Isabelle:

   318   for non-trivial properties, reasoning with alpha-equated terms is much

   319   easier than reasoning with `raw' terms. The fundamental reason for this is

   320   that the HOL-logic underlying Nominal Isabelle allows us to replace

   321   `equals-by-equals'. In contrast, replacing

   322   `alpha-equals-by-alpha-equals' in a representation based on `raw' terms

   323   requires a lot of extra reasoning work.

   324 

   325   Although in informal settings a reasoning infrastructure for alpha-equated

   326   terms is nearly always taken for granted, establishing it automatically in

   327   Isabelle/HOL is a rather non-trivial task. For every

   328   specification we will need to construct type(s) containing as elements the

   329   alpha-equated terms. To do so, we use the standard HOL-technique of defining

   330   a new type by identifying a non-empty subset of an existing type.  The

   331   construction we perform in Isabelle/HOL can be illustrated by the following picture:

   332 

   333   \begin{equation}\label{picture}

   334   \mbox{\begin{tikzpicture}[scale=1.1]

   335   %\draw[step=2mm] (-4,-1) grid (4,1);

   336   

   337   \draw[very thick] (0.7,0.4) circle (4.25mm);

   338   \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);

   339   \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);

   340   

   341   \draw (-2.0, 0.845) --  (0.7,0.845);

   342   \draw (-2.0,-0.045)  -- (0.7,-0.045);

   343 

   344   \draw ( 0.7, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};

   345   \draw (-2.4, 0.5) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};

   346   \draw (1.8, 0.48) node[right=-0.1mm]

   347     {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};

   348   \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};

   349   \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};

   350   

   351   \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);

   352   \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};

   353 

   354   \end{tikzpicture}}

   355   \end{equation}\smallskip

   356 

   357   \noindent

   358   We take as the starting point a definition of raw terms (defined as a

   359   datatype in Isabelle/HOL); then identify the alpha-equivalence classes in

   360   the type of sets of raw terms according to our alpha-equivalence relation,

   361   and finally define the new type as these alpha-equivalence classes (the

   362   non-emptiness requirement is always satisfied whenever the raw terms are

   363   definable as datatype in Isabelle/HOL and our relation for alpha-equivalence

   364   is an equivalence relation).

   365 

   366   The fact that we obtain an isomorphism between the new type and the

   367   non-empty subset shows that the new type is a faithful representation of

   368   alpha-equated terms. That is not the case for example for terms using the

   369   locally nameless representation of binders \cite{McKinnaPollack99}: in this

   370   representation there are `junk' terms that need to be excluded by

   371   reasoning about a well-formedness predicate.

   372 

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

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

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

   376   task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}

   377   the quotient package described by Homeier \cite{Homeier05} for the HOL4

   378   system. This package allows us to lift definitions and theorems involving

   379   raw terms to definitions and theorems involving alpha-equated terms. For

   380   example if we define the free-variable function over raw lambda-terms

   381   as follows

   382 

   383   \[

   384   \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}

   385   @{text "fv(x)"}     & @{text "\<equiv>"} & @{text "{x}"}\\

   386   @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\<equiv>"} & @{text "fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\

   387   @{text "fv(\<lambda>x.t)"}  & @{text "\<equiv>"} & @{text "fv(t) - {x}"}

   388   \end{tabular}}

   389   \]\smallskip

   390   

   391   \noindent

   392   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}

   393   operating on quotients, that is alpha-equivalence classes of lambda-terms. This

   394   lifted function is characterised by the equations

   395 

   396   \[

   397   \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}

   398   @{text "fv\<^sup>\<alpha>(x)"}     & @{text "="} & @{text "{x}"}\\

   399   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\

   400   @{text "fv\<^sup>\<alpha>(\<lambda>x.t)"}  & @{text "="} & @{text "fv\<^sup>\<alpha>(t) - {x}"}

   401   \end{tabular}}

   402   \]\smallskip

   403 

   404   \noindent

   405   (Note that this means also the term-constructors for variables, applications

   406   and lambda are lifted to the quotient level.)  This construction, of course,

   407   only works if alpha-equivalence is indeed an equivalence relation, and the

   408   `raw' definitions and theorems are respectful w.r.t.~alpha-equivalence.

   409   For example, we will not be able to lift a bound-variable function. Although

   410   this function can be defined for raw terms, it does not respect

   411   alpha-equivalence and therefore cannot be lifted. 

   412   To sum up, every lifting

   413   of theorems to the quotient level needs proofs of some respectfulness

   414   properties (see \cite{Homeier05}). In the paper we show that we are able to

   415   automate these proofs and as a result can automatically establish a reasoning 

   416   infrastructure for alpha-equated terms.\smallskip

   417 

   418   The examples we have in mind where our reasoning infrastructure will be

   419   helpful include the term language of Core-Haskell (see

   420   Figure~\ref{corehas}). This term language involves patterns that have lists

   421   of type-, coercion- and term-variables, all of which are bound in @{text

   422   "\<CASE>"}-expressions. In these patterns we do not know in advance how many

   423   variables need to be bound. Another example is the algorithm W,

   424   which includes multiple binders in type-schemes.\medskip

   425 

   426   \noindent

   427   {\bf Contributions:} We provide three new definitions for when terms

   428   involving general binders are alpha-equivalent. These definitions are

   429   inspired by earlier work of Pitts \cite{Pitts04}. By means of automati\-cally-generated

   430   proofs, we establish a reasoning infrastructure for alpha-equated terms,

   431   including properties about support, freshness and equality conditions for

   432   alpha-equated terms. We are also able to automatically derive strong

   433   induction principles that have the variable convention already built in.

   434   For this we simplify the earlier automated proofs by using the proving tools

   435   from the function package~\cite{Krauss09} of Isabelle/HOL.  The method

   436   behind our specification of general binders is taken from the Ott-tool, but

   437   we introduce crucial restrictions, and also extensions, so that our

   438   specifications make sense for reasoning about alpha-equated terms.  The main

   439   improvement over Ott is that we introduce three binding modes (only one is

   440   present in Ott), provide formalised definitions for alpha-equivalence and

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

   442   for our specifications from `first principles' inside a theorem prover.

   443 

   444 

   445   \begin{figure}[t]

   446   \begin{boxedminipage}{\linewidth}

   447   \begin{center}

   448   \begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}

   449   \multicolumn{3}{@ {}l}{Type Kinds}\\

   450   @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\

   451   \multicolumn{3}{@ {}l}{Coercion Kinds}\\

   452   @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\

   453   \multicolumn{3}{@ {}l}{Types}\\

   454   @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 

   455   @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\

   456   \multicolumn{3}{@ {}l}{Coercion Types}\\

   457   @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}

   458   @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> | refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2"}\\

   459   & @{text "|"} & @{text "\<gamma> @ \<sigma> | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\

   460   \multicolumn{3}{@ {}l}{Terms}\\

   461   @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> | \<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2"}\\

   462   & @{text "|"} & @{text "\<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 | \<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\

   463   \multicolumn{3}{@ {}l}{Patterns}\\

   464   @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\

   465   \multicolumn{3}{@ {}l}{Constants}\\

   466   & @{text C} & coercion constants\\

   467   & @{text T} & value type constructors\\

   468   & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\

   469   & @{text K} & data constructors\smallskip\\

   470   \multicolumn{3}{@ {}l}{Variables}\\

   471   & @{text a} & type variables\\

   472   & @{text c} & coercion variables\\

   473   & @{text x} & term variables\\

   474   \end{tabular}

   475   \end{center}

   476   \end{boxedminipage}

   477   \caption{The System @{text "F\<^isub>C"}

   478   \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this

   479   version of @{text "F\<^isub>C"} we made a modification by separating the

   480   grammars for type kinds and coercion kinds, as well as for types and coercion

   481   types. For this paper the interesting term-constructor is @{text "\<CASE>"},

   482   which binds multiple type-, coercion- and term-variables (the overlines stand for lists).\label{corehas}}

   483   \end{figure}

   484 *}

   485 

   486 section {* A Short Review of the Nominal Logic Work *}

   487 

   488 text {*

   489   At its core, Nominal Isabelle is an adaptation of the nominal logic work by

   490   Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in

   491   \cite{HuffmanUrban10} (including proofs). We shall briefly review this work

   492   to aid the description of what follows. 

   493 

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

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

   496   c, \<dots>"} to stand for atoms and @{text "\<pi>, \<pi>\<^isub>1, \<dots>"} to stand for permutations,

   497   which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to

   498   represent variables, be they bound or free. The sorts of atoms can be used

   499   to represent different kinds of variables, such as the term-, coercion- and

   500   type-variables in Core-Haskell.  It is assumed that there is an infinite

   501   supply of atoms for each sort. In the interest of brevity, we shall restrict

   502   ourselves in what follows to only one sort of atoms.

   503 

   504   Permutations are bijective functions from atoms to atoms that are 

   505   the identity everywhere except on a finite number of atoms. There is a 

   506   two-place permutation operation written

   507   @{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   508   where the generic type @{text "\<beta>"} is the type of the object 

   509   over which the permutation 

   510   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},

   511   the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}} 

   512   (even if this operation is non-commutative), 

   513   and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation

   514   operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};

   515   for example permutations acting on atoms, products, lists, permutations, sets, 

   516   functions and booleans are given by:

   517   

   518   \begin{equation}\label{permute}

   519   \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}

   520   \begin{tabular}{@ {}l@ {}}

   521   @{text "\<pi> \<bullet> a \<equiv> \<pi> a"}\\

   522   @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]

   523   @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   524   @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   525   \end{tabular} &

   526   \begin{tabular}{@ {}l@ {}}

   527   @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", no_vars, THEN eq_reflection]}\\

   528   @{thm permute_set_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   529   @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\

   530   @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}

   531   \end{tabular}

   532   \end{tabular}}

   533   \end{equation}\smallskip

   534   

   535   \noindent

   536   Concrete permutations in Nominal Isabelle are built up from swappings, 

   537   written as \mbox{@{text "(a b)"}}, which are permutations that behave 

   538   as follows:

   539   

   540   \[

   541   @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}

   542   \]\smallskip

   543 

   544   The most original aspect of the nominal logic work of Pitts is a general

   545   definition for the notion of the `set of free variables of an object @{text

   546   "x"}'.  This notion, written @{term "supp x"}, is general in the sense that

   547   it applies not only to lambda-terms (alpha-equated or not), but also to lists,

   548   products, sets and even functions. Its definition depends only on the

   549   permutation operation and on the notion of equality defined for the type of

   550   @{text x}, namely:

   551   

   552   \begin{equation}\label{suppdef}

   553   @{thm supp_def[no_vars, THEN eq_reflection]}

   554   \end{equation}\smallskip

   555 

   556   \noindent

   557   There is also the derived notion for when an atom @{text a} is \emph{fresh}

   558   for an @{text x}, defined as 

   559 

   560   \[

   561   @{thm fresh_def[no_vars]}

   562   \]\smallskip

   563 

   564   \noindent

   565   We use for sets of atoms the abbreviation 

   566   @{thm (lhs) fresh_star_def[no_vars]}, defined as 

   567   @{thm (rhs) fresh_star_def[no_vars]}.

   568   A striking consequence of these definitions is that we can prove

   569   without knowing anything about the structure of @{term x} that

   570   swapping two fresh atoms, say @{text a} and @{text b}, leaves 

   571   @{text x} unchanged, namely 

   572   

   573   \begin{prop}\label{swapfreshfresh}

   574   If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}

   575   then @{thm (concl) swap_fresh_fresh[no_vars]}.

   576   \end{prop}

   577   

   578   While often the support of an object can be relatively easily 

   579   described, for example for atoms, products, lists, function applications, 

   580   booleans and permutations as follows

   581   

   582   \begin{equation}\label{supps}\mbox{

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

   584   \begin{tabular}{rcl}

   585   @{term "supp a"} & $=$ & @{term "{a}"}\\

   586   @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\

   587   @{term "supp []"} & $=$ & @{term "{}"}\\

   588   @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\

   589   \end{tabular}

   590   &

   591   \begin{tabular}{rcl}

   592   @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\

   593   @{term "supp b"} & $=$ & @{term "{}"}\\

   594   @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}

   595   \end{tabular}

   596   \end{tabular}}

   597   \end{equation}\smallskip

   598   

   599   \noindent 

   600   in some cases it can be difficult to characterise the support precisely, and

   601   only an approximation can be established (as for function applications

   602   above). Reasoning about such approximations can be simplified with the

   603   notion \emph{supports}, defined as follows:

   604   

   605   \begin{defi}

   606   A set @{text S} \emph{supports} @{text x}, if for all atoms @{text a} and @{text b}

   607   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   608   \end{defi}

   609   

   610   \noindent

   611   The main point of @{text supports} is that we can establish the following 

   612   two properties.

   613   

   614   \begin{prop}\label{supportsprop}

   615   Given a set @{text "bs"} of atoms.\\

   616   {\it (i)} If @{thm (prem 1) supp_is_subset[where S="bs", no_vars]}

   617   and @{thm (prem 2) supp_is_subset[where S="bs", no_vars]} then 

   618   @{thm (concl) supp_is_subset[where S="bs", no_vars]}.\\

   619   {\it (ii)} @{thm supp_supports[no_vars]}.

   620   \end{prop}

   621   

   622   Another important notion in the nominal logic work is \emph{equivariance}.

   623   For a function @{text f} to be equivariant 

   624   it is required that every permutation leaves @{text f} unchanged, that is

   625   

   626   \begin{equation}\label{equivariancedef}

   627   @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}\;.

   628   \end{equation}\smallskip

   629   

   630   \noindent

   631   If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, say, this definition is equivalent to 

   632   the fact that a permutation applied to the application

   633   @{text "f x"} can be moved to the argument @{text x}. That means for 

   634   such functions, we have for all permutations @{text "\<pi>"}:

   635   

   636   \begin{equation}\label{equivariance}

   637   @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;

   638   @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}\;.

   639   \end{equation}\smallskip

   640    

   641   \noindent

   642   There is

   643   also a similar property for relations, which are in HOL functions of type @{text "\<alpha> \<Rightarrow> \<beta> \<Rightarrow> bool"}.

   644   Suppose a relation @{text R}, then for all permutations @{text \<pi>}:

   645   

   646   \[

   647   @{text "\<pi> \<bullet> R = R"} \;\;\;\;\textit{if and only if}\;\;\;\;

   648   @{text "\<forall>x y."}~~@{text "x R y"} \;\textit{implies}\; @{text "(\<pi> \<bullet> x) R (\<pi> \<bullet> y)"}\;.

   649   \]\smallskip

   650 

   651   \noindent

   652   Note that from property \eqref{equivariancedef} and the definition of @{text supp}, we 

   653   can easily deduce that for a function being equivariant is equivalent to having empty support.

   654 

   655   Using freshness, the nominal logic work provides us with general means for renaming 

   656   binders. 

   657   

   658   \noindent

   659   While in the older version of Nominal Isabelle, we used extensively 

   660   Proposition~\ref{swapfreshfresh} to rename single binders, this property 

   661   proved too unwieldy for dealing with multiple binders. For such binders the 

   662   following generalisations turned out to be easier to use.

   663 

   664   \begin{prop}\label{supppermeq}

   665   @{thm[mode=IfThen] supp_perm_eq[where p="\<pi>", no_vars]}

   666   \end{prop}

   667 

   668   \begin{prop}\label{avoiding}

   669   For a finite set @{text as} and a finitely supported @{text x} with

   670   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there

   671   exists a permutation @{text "\<pi>"} such that @{term "(\<pi> \<bullet> as) \<sharp>* c"} and

   672   @{term "supp x \<sharp>* \<pi>"}.

   673   \end{prop}

   674 

   675   \noindent

   676   The idea behind the second property is that given a finite set @{text as}

   677   of binders (being bound, or fresh, in @{text x} is ensured by the

   678   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that

   679   the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen

   680   as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything

   681   in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 

   682   fact and Property~\ref{supppermeq} allow us to `rename' just the binders 

   683   @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. 

   684 

   685   Note that @{term "supp x \<sharp>* \<pi>"}

   686   is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate 

   687   Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the 

   688   reasoning infrastructure of Nominal Isabelle is set up so that it provides more

   689   automation for the formulation given above.

   690 

   691   Most properties given in this section are described in detail in \cite{HuffmanUrban10}

   692   and all are formalised in Isabelle/HOL. In the next sections we will make 

   693   use of these properties in order to define alpha-equivalence in 

   694   the presence of multiple binders.

   695 *}

   696 

   697 

   698 section {* Abstractions\label{sec:binders} *}

   699 

   700 text {*

   701   In Nominal Isabelle, the user is expected to write down a specification of a

   702   term-calculus and then a reasoning infrastructure is automatically derived

   703   from this specification (remember that Nominal Isabelle is a definitional

   704   extension of Isabelle/HOL, which does not introduce any new axioms).

   705 

   706   In order to keep our work with deriving the reasoning infrastructure

   707   manageable, we will wherever possible state definitions and perform proofs

   708   on the `user-level' of Isabelle/HOL, as opposed to writing custom ML-code that

   709   generates them anew for each specification. 

   710   To that end, we will consider

   711   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs

   712   are intended to represent the abstraction, or binding, of the set of atoms @{text

   713   "as"} in the body @{text "x"}.

   714 

   715   The first question we have to answer is when two pairs @{text "(as, x)"} and

   716   @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in

   717   the notion of alpha-equivalence that is \emph{not} preserved by adding

   718   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}

   719   given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

   720   set"}}, then @{text "(as, x)"} and @{text "(bs, y)"} need to have the same set of free

   721   atoms; moreover there must be a permutation @{text \<pi>} such that {\it

   722   (ii)} @{text \<pi>} leaves the free atoms of @{text "(as, x)"} and @{text "(bs, y)"} unchanged, but

   723   {\it (iii)} `moves' their bound names so that we obtain modulo a relation,

   724   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}

   725   @{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The

   726   requirements {\it (i)} to {\it (iv)} can be stated formally as:

   727 

   728   \begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\

   729   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  

   730   @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} & 

   731     \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 

   732        & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\

   733        & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\

   734        & \mbox{\it (iii)} &  @{text "(\<pi> \<bullet> x) R y"} \\

   735        & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"} \\ 

   736   \end{tabular}

   737   \end{defi}

   738  

   739   \noindent

   740   Note that the relation is

   741   dependent on a free-atom function @{text "fa"} and a relation @{text

   742   "R"}. The reason for this extra generality is that we will use

   743   $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both raw terms and 

   744   alpha-equated terms. In

   745   the latter case, @{text R} will be replaced by equality @{text "="} and we

   746   will prove that @{text "fa"} is equal to @{text "supp"}.

   747 

   748   Definition \ref{alphaset} does not make any distinction between the

   749   order of abstracted atoms. If we want this, then we can define alpha-equivalence 

   750   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 

   751   as follows

   752   

   753   \begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\

   754   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  

   755   @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &

   756   \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 

   757          & \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\ 

   758          & \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\

   759          & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\

   760          & \mbox{\it (iv)}  & @{term "(\<pi> \<bullet> as) = bs"}\\

   761   \end{tabular}

   762   \end{defi}

   763   

   764   \noindent

   765   where @{term set} is the function that coerces a list of atoms into a set of atoms.

   766   Now the last clause ensures that the order of the binders matters (since @{text as}

   767   and @{text bs} are lists of atoms).

   768 

   769   If we do not want to make any difference between the order of binders \emph{and}

   770   also allow vacuous binders, that means according to Pitts~\cite{Pitts04} 

   771   \emph{restrict} atoms, then we keep sets of binders, but drop 

   772   condition {\it (iv)} in Definition~\ref{alphaset}:

   773 

   774   \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\

   775   \begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}  

   776   @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &

   777   \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\ 

   778              & \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"}\\

   779              & \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\

   780              & \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\

   781   \end{tabular}

   782   \end{defi}

   783 

   784 

   785   It might be useful to consider first some examples how these definitions

   786   of alpha-equivalence pan out in practice.  For this consider the case of

   787   abstracting a set of atoms over types (as in type-schemes). We set

   788   @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we

   789   define

   790   

   791   \[

   792   @{text "fa(x) \<equiv> {x}"}  \hspace{10mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}

   793   \]\smallskip

   794 

   795   \noindent

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

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

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

   799   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text "\<pi>"} to

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

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

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

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

   804   unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$

   805   @{text "({x, y}, x)"} which holds by taking @{text "\<pi>"} to be the identity

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

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

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

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

   810   shown that all three notions of alpha-equivalence coincide, if we only

   811   abstract a single atom. In this case they also agree with the alpha-equivalence

   812   used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a

   813   proof of this fact since the details are hairy and not really important for the

   814   purpose of this paper.}

   815 

   816   In the rest of this section we are going to show that the alpha-equivalences

   817   really lead to abstractions where some atoms are bound (or more precisely

   818   removed from the support).  For this we will consider three abstraction

   819   types that are quotients of the relations

   820 

   821   \begin{equation}

   822   \begin{array}{r}

   823   @{term "alpha_set_ex (as, x) equal supp (bs, y)"}\smallskip\\

   824   @{term "alpha_res_ex (as, x) equal supp (bs, y)"}\smallskip\\

   825   @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\

   826   \end{array}

   827   \end{equation}\smallskip

   828   

   829   \noindent

   830   Note that in these relations we replaced the free-atom function @{text "fa"}

   831   with @{term "supp"} and the relation @{text R} with equality. We can show

   832   the following two properties:

   833 

   834   \begin{lem}\label{alphaeq} 

   835   The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, 

   836   $\approx_{\,\textit{set+}}^{=, \textit{supp}}$

   837   and $\approx_{\,\textit{list}}^{=, \textit{supp}}$ are 

   838   equivalence relations and equivariant. 

   839   \end{lem}

   840 

   841   \begin{proof}

   842   Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have

   843   a permutation @{text "\<pi>"} and for the proof obligation take @{term "-

   844   \<pi>"}. In case of transitivity, we have two permutations @{text "\<pi>\<^isub>1"}

   845   and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text

   846   "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,

   847   \<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term

   848   "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we

   849   have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>

   850   \<pi>'"}. To show equivariance, we need to `pull out' the permutations,

   851   which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,

   852   set"} and @{text "supp"}, are equivariant (see

   853   \cite{HuffmanUrban10}). Finally, we apply the permutation operation on

   854   booleans.

   855   \end{proof}

   856 

   857   \noindent

   858   Recall the picture shown in \eqref{picture} about new types in HOL.

   859   The lemma above allows us to use our quotient package for introducing 

   860   new types @{text "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}

   861   representing alpha-equivalence classes of pairs of type 

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

   863   (in the third case). 

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

   865   

   866   \[

   867   @{term "Abs_set as x"} \hspace{10mm} 

   868   @{term "Abs_res as x"} \hspace{10mm}

   869   @{term "Abs_lst as x"} 

   870   \]\smallskip

   871   

   872   \noindent

   873   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will

   874   call the types \emph{abstraction types} and their elements

   875   \emph{abstractions}. The important property we need to derive is the support of 

   876   abstractions, namely:

   877 

   878   \begin{thm}[Support of Abstractions]\label{suppabs} 

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

   880 

   881   \[

   882   \begin{array}{l@ {\;=\;}l}

   883   @{thm (lhs) supp_Abs(1)[no_vars]} & @{thm (rhs) supp_Abs(1)[no_vars]}\\

   884   @{thm (lhs) supp_Abs(2)[no_vars]} & @{thm (rhs) supp_Abs(2)[no_vars]}\\

   885   @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} &

   886   @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\

   887   \end{array}

   888   \]\smallskip

   889   \end{thm}

   890 

   891   \noindent

   892   In effect, this theorem states that the atoms @{text "as"} are bound in the

   893   abstraction. As stated earlier, this can be seen as a litmus test that our

   894   Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the

   895   idea of alpha-equivalence relations. Below we will give the proof for the

   896   first equation of Theorem \ref{suppabs}. The others follow by similar

   897   arguments. By definition of the abstraction type @{text

   898   "abs\<^bsub>set\<^esub>"} we have

   899 

   900   \begin{equation}\label{abseqiff}

   901   @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; 

   902   @{term "alpha_set_ex (as, x) equal supp (bs, y)"}

   903   \end{equation}\smallskip

   904   

   905   \noindent

   906   and also set

   907   

   908   \begin{equation}\label{absperm}

   909   @{thm permute_Abs(1)[where p="\<pi>", no_vars, THEN eq_reflection]}

   910   \end{equation}\smallskip

   911 

   912   \noindent

   913   With this at our disposal, we can show 

   914   the following lemma about swapping two atoms in an abstraction.

   915   

   916   \begin{lem}

   917   If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and

   918   @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then 

   919   @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]}

   920   \end{lem}

   921   

   922   \begin{proof}

   923   If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b)"} is then

   924   the identity permutation.

   925   Also in the other case the lemma is straightforward using \eqref{abseqiff}

   926   and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =

   927   (supp x - as)"}.  We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"} as

   928   the permutation for the proof obligation.

   929   \end{proof}

   930   

   931   \noindent

   932   This lemma together 

   933   with \eqref{absperm} allows us to show

   934   

   935   \begin{equation}\label{halfone}

   936   @{thm Abs_supports(1)[no_vars]}

   937   \end{equation}\smallskip

   938   

   939   \noindent

   940   which by Property~\ref{supportsprop} gives us `one half' of

   941   Theorem~\ref{suppabs}. To establish the `other half', we 

   942   use a trick from \cite{Pitts04} and first define an auxiliary 

   943   function @{text aux}, taking an abstraction as argument

   944 

   945   \[

   946   @{thm supp_set.simps[THEN eq_reflection, no_vars]}

   947   \]\smallskip 

   948 

   949   \noindent

   950   Using the second equation in \eqref{equivariance}, we can show that 

   951   @{text "aux"} is equivariant (since @{term "\<pi> \<bullet> (supp x - as) = (supp (\<pi> \<bullet> x)) - (\<pi> \<bullet> as)"}) 

   952   and therefore has empty support. 

   953   This in turn means

   954   

   955   \[

   956   @{term "supp (supp_set (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}

   957   \]\smallskip

   958   

   959   \noindent

   960   using the fact about the support of function applications in \eqref{supps}. Assuming 

   961   @{term "supp x - as"} is a finite set, we further obtain

   962   

   963   \begin{equation}\label{halftwo}

   964   @{thm (concl) Abs_supp_subset1(1)[no_vars]}

   965   \end{equation}\smallskip

   966   

   967   \noindent

   968   This is because for every finite set of atoms, say @{text "bs"}, we have 

   969   @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not 

   970   the case for infinite sets.}

   971   Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 

   972   the first equation of Theorem~\ref{suppabs}. The others are similar.

   973 

   974   Recall the definition of support given in \eqref{suppdef}, and note the difference between 

   975   the support of a raw pair and an abstraction

   976 

   977   \[

   978   @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}

   979   @{term "supp (Abs_set as x) = supp x - as"}

   980   \]\smallskip

   981 

   982   \noindent

   983   While the permutation operations behave in both cases the same (a permutation

   984   is just moved to the arguments), the notion of equality is different for pairs and

   985   abstractions. Therefore we have different supports. In case of abstractions,

   986   we have established in Theorem~\ref{suppabs} that bound atoms are removed from 

   987   the support of the abstractions' bodies.

   988 

   989   The method of first considering abstractions of the form @{term "Abs_set as

   990   x"} etc is motivated by the fact that we can conveniently establish at the

   991   Isabelle/HOL level properties about them.  It would be extremely laborious

   992   to write custom ML-code that derives automatically such properties for every

   993   term-constructor that binds some atoms. Also the generality of the

   994   definitions for alpha-equivalence will help us in the next sections.

   995 *}

   996 

   997 section {* Specifying General Bindings\label{sec:spec} *}

   998 

   999 text {*

  1000   Our choice of syntax for specifications is influenced by the existing

  1001   datatype package of Isabelle/HOL \cite{Berghofer99} 

  1002   and by the syntax of the

  1003   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a

  1004   collection of (possibly mutually recursive) type declarations, say @{text

  1005   "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of

  1006   binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The

  1007   syntax in Nominal Isabelle for such specifications is schematically as follows:

  1008   

  1009   \begin{equation}\label{scheme}

  1010   \mbox{\begin{tabular}{@ {}p{2.5cm}l}

  1011   type \mbox{declaration part} &

  1012   $\begin{cases}

  1013   \mbox{\begin{tabular}{l}

  1014   \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\

  1015   \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\

  1016   \raisebox{2mm}{$\ldots$}\\[-2mm] 

  1017   \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 

  1018   \end{tabular}}

  1019   \end{cases}$\\[2mm]

  1020   binding \mbox{function part} &

  1021   $\begin{cases}

  1022   \mbox{\begin{tabular}{l}

  1023   \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\

  1024   \isacommand{where}\\

  1025   \raisebox{2mm}{$\ldots$}\\[-2mm]

  1026   \end{tabular}}

  1027   \end{cases}$\\

  1028   \end{tabular}}

  1029   \end{equation}\smallskip

  1030 

  1031   \noindent

  1032   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection

  1033   of term-constructors, each of which comes with a list of labelled types that

  1034   stand for the types of the arguments of the term-constructor.  For example a

  1035   term-constructor @{text "C\<^sup>\<alpha>"} might be specified with

  1036 

  1037   \[

  1038   @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}\mbox{$'_1$} @{text "\<dots> label\<^isub>l::ty"}\mbox{$'_l\;\;\;\;\;$}  

  1039   @{text "binding_clauses"} 

  1040   \]\smallskip

  1041   

  1042   \noindent

  1043   whereby some of the @{text ty}$'_{1..l}$ (or their components) can be

  1044   contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in

  1045   \eqref{scheme}. In this case we will call the corresponding argument a

  1046   \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such

  1047   recursive arguments need to satisfy a `positivity' restriction, which

  1048   ensures that the type has a set-theoretic semantics (see

  1049   \cite{Berghofer99}). If the types are polymorphic, we require the

  1050   type variables to stand for types that are finitely supported and over which 

  1051   a permutation operation is defined.

  1052   The labels @{text "label"}$_{1..l}$ annotated on the types are optional. Their

  1053   purpose is to be used in the (possibly empty) list of \emph{binding

  1054   clauses}, which indicate the binders and their scope in a term-constructor.

  1055   They come in three \emph{modes}:

  1056 

  1057 

  1058   \[\mbox{

  1059   \begin{tabular}{@ {}l@ {}}

  1060   \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\

  1061   \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\

  1062   \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies}

  1063   \end{tabular}}

  1064   \]\smallskip

  1065   

  1066   \noindent

  1067   The first mode is for binding lists of atoms (the order of bound atoms

  1068   matters); the second is for sets of binders (the order does not matter, but

  1069   the cardinality does) and the last is for sets of binders (with vacuous

  1070   binders preserving alpha-equivalence). As indicated, the labels in the

  1071   `\isacommand{in}-part' of a binding clause will be called \emph{bodies};

  1072   the `\isacommand{binds}-part' will be called \emph{binders}. In contrast to

  1073   Ott, we allow multiple labels in binders and bodies.  For example we allow

  1074   binding clauses of the form:

  1075  

  1076   \[\mbox{

  1077   \begin{tabular}{@ {}ll@ {}}

  1078   @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &  

  1079       \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\

  1080   @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &  

  1081       \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"}, 

  1082       \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\

  1083   \end{tabular}}

  1084   \]\smallskip

  1085 

  1086   \noindent

  1087   Similarly for the other binding modes. Interestingly, in case of

  1088   \isacommand{binds (set)} and \isacommand{binds (set+)} the binding clauses

  1089   above will make a difference to the semantics of the specifications (the

  1090   corresponding alpha-equivalence will differ). We will show this later with

  1091   an example.

  1092 

  1093   

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

  1095   comparison to Ott. The main idea behind these restrictions is

  1096   that we obtain a notion of alpha-equivalence where it is ensured

  1097   that within a given scope an atom occurrence cannot be both bound and free

  1098   at the same time.  The first restriction is that a body can only occur in

  1099   \emph{one} binding clause of a term constructor. So for example

  1100 

  1101   \[\mbox{

  1102   @{text "Foo x::name y::name t::trm"}\hspace{3mm}  

  1103   \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"},

  1104   \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}}

  1105   \]\smallskip

  1106 

  1107   \noindent

  1108   is not allowed. This ensures that the bound atoms of a body cannot be free

  1109   at the same time by specifying an alternative binder for the same body.

  1110 

  1111   For binders we distinguish between \emph{shallow} and \emph{deep} binders.

  1112   Shallow binders are just labels. The restriction we need to impose on them

  1113   is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the

  1114   labels must either refer to atom types or to sets of atom types; in case of

  1115   \isacommand{binds} the labels must refer to atom types or to lists of atom

  1116   types. Two examples for the use of shallow binders are the specification of

  1117   lambda-terms, where a single name is bound, and type-schemes, where a finite

  1118   set of names is bound:

  1119 

  1120   \[\mbox{

  1121   \begin{tabular}{@ {}c@ {\hspace{8mm}}c@ {}}

  1122   \begin{tabular}{@ {}l}

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

  1124   \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\

  1125   \hspace{2mm}$\mid$~@{text "App lam lam"}\\

  1126   \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}%

  1127   \isacommand{binds} @{text x} \isacommand{in} @{text t}\\

  1128   \\

  1129   \end{tabular} &

  1130   \begin{tabular}{@ {}l@ {}}

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

  1132   \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\

  1133   \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\

  1134   \isacommand{and}~@{text "tsc ="}\\