1 

     2 (*<*)

     3 theory Paper

     4 imports "../Nominal/Nominal2" 

     5         "~~/src/HOL/Library/LaTeXsugar"

     6 begin

     7 

     8 consts

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

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

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

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

    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 notation (latex output)

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

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

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

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

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

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

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

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

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

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

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

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

    32   equal ("=") and

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

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

    35   Abs_lst ("[_]\<^bsub>list\<^esub>._") and

    36   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and

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

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

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

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

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

    42 

    43 consts alpha_trm ::'a

    44 consts fa_trm :: 'a

    45 consts alpha_trm2 ::'a

    46 consts fa_trm2 :: 'a

    47 consts ast :: 'a

    48 consts ast' :: 'a

    49 notation (latex output) 

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

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

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

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

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

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

    56 

    57 (*>*)

    58 

    59 

    60 section {* Introduction *}

    61 

    62 text {*

    63 

    64   So far, Nominal Isabelle provided a mechanism for constructing

    65   $\alpha$-equated terms, for example lambda-terms,

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

    67   where free and bound variables have names.  For such $\alpha$-equated terms,

    68   Nominal Isabelle derives automatically a reasoning infrastructure that has

    69   been used successfully in formalisations of an equivalence checking

    70   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

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

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

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

    74   formalisations in the locally-nameless approach to binding

    75   \cite{SatoPollack10}.

    76 

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

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

    79   respectively, of the form

    80   %

    81   \begin{equation}\label{tysch}

    82   \begin{array}{l}

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

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

    85   \end{array}

    86   \end{equation}

    87   %

    88   \noindent

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

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

    91   binders by iterating single binders, this leads to a rather clumsy

    92   formalisation of W. 

    93   %The need of iterating single binders is also one reason

    94   %why Nominal Isabelle 

    95   % and similar theorem provers that only provide

    96   %mechanisms for binding single variables 

    97   %has not fared extremely well with the

    98   %more advanced tasks in the POPLmark challenge \cite{challenge05}, because

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

   100 

   101   Binding multiple variables has interesting properties that cannot be captured

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

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

   104   we would like to regard the first pair of type-schemes as $\alpha$-equivalent,

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

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

   107   %

   108   \begin{equation}\label{ex1}

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

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

   111   \end{equation}

   112   %

   113   \noindent

   114   Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ

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

   116   %

   117   \begin{equation}\label{ex3}

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

   119   \end{equation}

   120   %

   121   \noindent

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

   123   give a general binding mechanism and associated notion of $\alpha$-equivalence

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

   125   Isabelle.  

   126   %The difficulty of finding the right notion for $\alpha$-equivalence

   127   %can be appreciated in this case by considering that the definition given by

   128   %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 

   129 

   130   However, the notion of $\alpha$-equivalence that is preserved by vacuous

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

   132   %

   133   \begin{equation}\label{one}

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

   135   \end{equation}

   136 

   137   \noindent

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

   139   \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard

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

   141   %

   142   \begin{center}

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

   144   \end{center}

   145   %

   146   \noindent

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

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

   149   binders has to agree.

   150 

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

   152   language constructs frequently occurring in programming language

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

   154   %

   155   \begin{equation}\label{two}

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

   157   \end{equation}

   158   %

   159   \noindent

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

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

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

   163   %

   164   \begin{center}

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

   166   \end{center}

   167   %

   168   \noindent

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

   170   multiple variables at once, and let the user chose which one is intended

   171   in a formalisation.

   172   %%when formalising a term-calculus.

   173 

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

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

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

   177   %

   178   \begin{center}

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

   180   \end{center}

   181   %

   182   \noindent

   183   we care about the 

   184   information that there are as many bound variables @{text

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

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

   187   %

   188   \begin{center}

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

   190   \end{center}

   191   %

   192   \noindent

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

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

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

   196   instance, but the lengths of the two lists do not agree. To exclude such

   197   terms, additional predicates about well-formed terms are needed in order to

   198   ensure that the two lists are of equal length. This can result in very messy

   199   reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will

   200   allow type specifications for @{text "\<LET>"}s as follows

   201   %

   202   \begin{center}

   203   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}

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

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

   206                                  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm]

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

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

   209   \end{tabular}

   210   \end{center}

   211   %

   212   \noindent

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

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

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

   216   assn} as follows

   217   %

   218   \begin{center}

   219   @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} 

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

   221   \end{center}

   222   %

   223   \noindent

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

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

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

   227   clause states that all the names the function @{text

   228   "bn(as)"} returns should be bound in @{text s}.  This style of specifying terms and bindings is heavily

   229   inspired by the syntax of the Ott-tool \cite{ott-jfp}. 

   230 

   231   %Though, Ott

   232   %has only one binding mode, namely the one where the order of

   233   %binders matters. Consequently, type-schemes with binding sets

   234   %of names cannot be modelled in Ott.

   235 

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

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

   238   types like @{text "t ::= t t | \<lambda>x. t"}

   239   where no clause for variables is given. Arguably, such specifications make

   240   some sense in the context of Coq's type theory (which Ott supports), but not

   241   at all in a HOL-based environment where every datatype must have a non-empty

   242   set-theoretic model. % \cite{Berghofer99}.

   243 

   244   Another reason is that we establish the reasoning infrastructure

   245   for $\alpha$-\emph{equated} terms. In contrast, Ott produces  a reasoning 

   246   infrastructure in Isabelle/HOL for

   247   \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms

   248   and the raw terms produced by Ott use names for bound variables,

   249   there is a key difference: working with $\alpha$-equated terms means, for example,  

   250   that the two type-schemes

   251 

   252   \begin{center}

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

   254   \end{center}

   255   

   256   \noindent

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

   258   only support specifications that make sense on the level of $\alpha$-equated

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

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

   261   to).  

   262 

   263   %Our insistence on reasoning with $\alpha$-equated terms comes from the

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

   265   %for non-trivial properties, reasoning with $\alpha$-equated terms is much

   266   %easier than reasoning with raw terms. The fundamental reason for this is

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

   268   %``equals-by-equals''. In contrast, replacing

   269   %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms

   270   %requires a lot of extra reasoning work.

   271 

   272   Although in informal settings a reasoning infrastructure for $\alpha$-equated

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

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

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

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

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

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

   279   %

   280   \begin{center}

   281   \begin{tikzpicture}[scale=0.89]

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

   283   

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

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

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

   287   

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

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

   290 

   291   \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};

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

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

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

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

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

   297   

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

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

   300 

   301   \end{tikzpicture}

   302   \end{center}

   303   %

   304   \noindent

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

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

   307   the type of sets of raw terms according to our $\alpha$-equivalence relation,

   308   and finally define the new type as these $\alpha$-equivalence classes

   309   (non-emptiness is satisfied whenever the raw terms are definable as datatype

   310   in Isabelle/HOL and our relation for $\alpha$-equivalence is

   311   an equivalence relation).

   312 

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

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

   315   %$\alpha$-equated terms. That is not the case for example for terms using the

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

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

   318   %reasoning about a well-formedness predicate.

   319 

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

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

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

   323   task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package

   324   described by Homeier \cite{Homeier05} for the HOL4 system. This package

   325   allows us to lift definitions and theorems involving raw terms to

   326   definitions and theorems involving $\alpha$-equated terms. For example if we

   327   define the free-variable function over raw lambda-terms

   328 

   329   \begin{center}

   330   @{text "fv(x) = {x}"}\hspace{8mm}

   331   @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}

   332   @{text "fv(\<lambda>x.t) = fv(t) - {x}"}

   333   \end{center}

   334   

   335   \noindent

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

   337   operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This

   338   lifted function is characterised by the equations

   339 

   340   \begin{center}

   341   @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}

   342   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}

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

   344   \end{center}

   345 

   346   \noindent

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

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

   349   only works if $\alpha$-equivalence is indeed an equivalence relation, and the

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

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

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

   353   %$\alpha$-equivalence and therefore cannot be lifted. 

   354   To sum up, every lifting

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

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

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

   358   infrastructure for $\alpha$-equated terms.\smallskip

   359 

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

   361   %helpful includes the term language of Core-Haskell. This term language

   362   %involves patterns that have lists of type-, coercion- and term-variables,

   363   %all of which are bound in @{text "\<CASE>"}-expressions. In these

   364   %patterns we do not know in advance how many variables need to

   365   %be bound. Another example is the specification of SML, which includes

   366   %includes bindings as in type-schemes.\medskip

   367 

   368   \noindent

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

   370   involving general binders are $\alpha$-equivalent. These definitions are

   371   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic

   372   proofs, we establish a reasoning infrastructure for $\alpha$-equated

   373   terms, including properties about support, freshness and equality

   374   conditions for $\alpha$-equated terms. We are also able to derive strong 

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

   376   The method behind our specification of general binders is taken 

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

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

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

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

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

   382   for our specifications from ``first principles''.

   383 

   384 

   385   %\begin{figure}

   386   %\begin{boxedminipage}{\linewidth}

   387   %%\begin{center}

   388   %\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}

   389   %\multicolumn{3}{@ {}l}{Type Kinds}\\

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

   391   %\multicolumn{3}{@ {}l}{Coercion Kinds}\\

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

   393   %\multicolumn{3}{@ {}l}{Types}\\

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

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

   396   %\multicolumn{3}{@ {}l}{Coercion Types}\\

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

   398   %@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\

   399   %& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\

   400   %& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\

   401   %\multicolumn{3}{@ {}l}{Terms}\\

   402   %@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\

   403   %& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\

   404   %& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\

   405   %\multicolumn{3}{@ {}l}{Patterns}\\

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

   407   %\multicolumn{3}{@ {}l}{Constants}\\

   408   %& @{text C} & coercion constants\\

   409   %& @{text T} & value type constructors\\

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

   411   %& @{text K} & data constructors\smallskip\\

   412   %\multicolumn{3}{@ {}l}{Variables}\\

   413   %& @{text a} & type variables\\

   414   %& @{text c} & coercion variables\\

   415   %& @{text x} & term variables\\

   416   %\end{tabular}

   417   %\end{center}

   418   %\end{boxedminipage}

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

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

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

   422   %grammars for type kinds and coercion kinds, as well as for types and coercion

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

   424   %which binds multiple type-, coercion- and term-variables.\label{corehas}}

   425   %\end{figure}

   426 *}

   427 

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

   429 

   430 text {*

   431   At its core, Nominal Isabelle is an adaption of the nominal logic work by

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

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

   434   to aid the description of what follows. 

   435 

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

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

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

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

   440   %The sorts of atoms can be used to represent different kinds of

   441   %variables, such as the term-, coercion- and type-variables in Core-Haskell.

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

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

   444   in what follows to only one sort of atoms.

   445 

   446   Permutations are bijective functions from atoms to atoms that are 

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

   448   two-place permutation operation written

   449   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

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

   451   over which the permutation 

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

   453   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 

   454   and the inverse permutation of @{term p} as @{text "- p"}. The permutation

   455   operation is defined over the type-hierarchy \cite{HuffmanUrban10};

   456   for example permutations acting on products, lists, sets, functions and booleans are

   457   given by:

   458   %

   459   %\begin{equation}\label{permute}

   460   %\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}

   461   %\begin{tabular}{@ {}l@ {}}

   462   %@{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]

   463   %@{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\

   464   %@{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\

   465   %\end{tabular} &

   466   %\begin{tabular}{@ {}l@ {}}

   467   %@{thm permute_set_eq[no_vars, THEN eq_reflection]}\\

   468   %@{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\

   469   %@{thm permute_bool_def[no_vars, THEN eq_reflection]}

   470   %\end{tabular}

   471   %\end{tabular}}

   472   %\end{equation}

   473   %

   474   \begin{center}

   475   \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}

   476   \begin{tabular}{@ {}l@ {}}

   477   @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\

   478   @{thm permute_bool_def[no_vars, THEN eq_reflection]}

   479   \end{tabular} &

   480   \begin{tabular}{@ {}l@ {}}

   481   @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\

   482   @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\

   483   \end{tabular} &

   484   \begin{tabular}{@ {}l@ {}}

   485   @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\

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

   487   \end{tabular}

   488   \end{tabular}}

   489   \end{center}

   490 

   491   \noindent

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

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

   494   as follows:

   495   %

   496   \begin{center}

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

   498   \end{center}

   499 

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

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

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

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

   504   products, sets and even functions. The definition depends only on the

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

   506   @{text x}, namely:

   507   %

   508   \begin{equation}\label{suppdef}

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

   510   \end{equation}

   511 

   512   \noindent

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

   514   for an @{text x}, defined as @{thm fresh_def[no_vars]}.

   515   We use for sets of atoms the abbreviation 

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

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

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

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

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

   521   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}

   522   then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   523   %

   524   %\begin{myproperty}\label{swapfreshfresh}

   525   %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}

   526   %\end{myproperty}

   527   %

   528   %While often the support of an object can be relatively easily 

   529   %described, for example for atoms, products, lists, function applications, 

   530   %booleans and permutations as follows

   531   %%

   532   %\begin{center}

   533   %\begin{tabular}{c@ {\hspace{10mm}}c}

   534   %\begin{tabular}{rcl}

   535   %@{term "supp a"} & $=$ & @{term "{a}"}\\

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

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

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

   539   %\end{tabular}

   540   %&

   541   %\begin{tabular}{rcl}

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

   543   %@{term "supp b"} & $=$ & @{term "{}"}\\

   544   %@{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}

   545   %\end{tabular}

   546   %\end{tabular}

   547   %\end{center}

   548   %

   549   %\noindent 

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

   551   %only an approximation can be established (as for functions above). 

   552   %

   553   %Reasoning about

   554   %such approximations can be simplified with the notion \emph{supports}, defined 

   555   %as follows:

   556   %

   557   %\begin{definition}

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

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

   560   %\end{definition}

   561   %

   562   %\noindent

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

   564   %two properties.

   565   %

   566   %\begin{myproperty}\label{supportsprop}

   567   %Given a set @{text "as"} of atoms.

   568   %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}

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

   570   %\end{myproperty}

   571   %

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

   573   %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 

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

   575   %%

   576   %\begin{equation}\label{equivariancedef}

   577   %@{term "\<forall>p. p \<bullet> f = f"}

   578   %\end{equation}

   579   %

   580   %\noindent or equivalently that a permutation applied to the application

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

   582   %functions @{text f}, we have for all permutations @{text p}:

   583   %%

   584   %\begin{equation}\label{equivariance}

   585   %@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;

   586   %@{text "p \<bullet> (f x) = f (p \<bullet> x)"}

   587   %\end{equation}

   588   % 

   589   %\noindent

   590   %From property \eqref{equivariancedef} and the definition of @{text supp}, we 

   591   %can easily deduce that equivariant functions have empty support. There is

   592   %also a similar notion for equivariant relations, say @{text R}, namely the property

   593   %that

   594   %%

   595   %\begin{center}

   596   %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}

   597   %\end{center}

   598   %

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

   600   %binders. 

   601   %

   602   %\noindent

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

   604   %Property~\ref{swapfreshfresh}

   605   this property to rename single binders, it %%this property 

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

   607   following generalisations turned out to be easier to use.

   608 

   609   \begin{myproperty}\label{supppermeq}

   610   @{thm[mode=IfThen] supp_perm_eq[no_vars]}

   611   \end{myproperty}

   612 

   613   \begin{myproperty}\label{avoiding}

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

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

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

   617   @{term "supp x \<sharp>* p"}.

   618   \end{myproperty}

   619 

   620   \noindent

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

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

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

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

   625   as long as it is finitely supported) and also @{text "p"} does not affect anything

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

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

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

   629 

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

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

   632   extensive use of these properties in order to define $\alpha$-equivalence in 

   633   the presence of multiple binders.

   634 *}

   635 

   636 

   637 section {* General Bindings\label{sec:binders} *}

   638 

   639 text {*

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

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

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

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

   644 

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

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

   647   on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code. % that

   648   %generates them anew for each specification. 

   649   To that end, we will consider

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

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

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

   653 

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

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

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

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

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

   659   set"}}, then @{text x} and @{text y} need to have the same set of free

   660   atoms; moreover there must be a permutation @{text p} such that {\it

   661   (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but

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

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

   664   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The

   665   requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:

   666   %

   667   \begin{equation}\label{alphaset}

   668   \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}

   669   \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]

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

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

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

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

   674   \end{array}

   675   \end{equation}

   676   %

   677   \noindent

   678   Note that this relation depends on the permutation @{text

   679   "p"}; $\alpha$-equivalence between two pairs is then the relation where we

   680   existentially quantify over this @{text "p"}. Also note that the relation is

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

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

   683   $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In

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

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

   686 

   687   The definition in \eqref{alphaset} does not make any distinction between the

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

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

   690   as follows

   691   %

   692   \begin{equation}\label{alphalist}

   693   \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}

   694   \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]

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

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

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

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

   699   \end{array}

   700   \end{equation}

   701   %

   702   \noindent

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

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

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

   706 

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

   708   also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop 

   709   condition {\it (iv)} in \eqref{alphaset}:

   710   %

   711   \begin{equation}\label{alphares}

   712   \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}

   713   \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]

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

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

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

   717   \end{array}

   718   \end{equation}

   719 

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

   721   of $\alpha$-equivalence pan out in practice.  For this consider the case of

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

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

   724   define

   725   %

   726   \begin{center}

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

   728   \end{center}

   729 

   730   \noindent

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

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

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

   734   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to

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

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

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

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

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

   740   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity

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

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

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

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

   745   shown that all three notions of $\alpha$-equivalence coincide, if we only

   746   abstract a single atom.

   747 

   748   In the rest of this section we are going to introduce three abstraction 

   749   types. For this we define 

   750   %

   751   \begin{equation}

   752   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}

   753   \end{equation}

   754   

   755   \noindent

   756   (similarly for $\approx_{\,\textit{abs\_set+}}$ 

   757   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 

   758   relations. %% and equivariant.

   759 

   760   \begin{lemma}\label{alphaeq} 

   761   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$

   762   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 

   763   %@{term "abs_set (as, x) (bs, y)"} then also 

   764   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).

   765   \end{lemma}

   766 

   767   \begin{proof}

   768   Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have

   769   a permutation @{text p} and for the proof obligation take @{term "-p"}. In case 

   770   of transitivity, we have two permutations @{text p} and @{text q}, and for the

   771   proof obligation use @{text "q + p"}. All conditions are then by simple

   772   calculations. 

   773   \end{proof}

   774 

   775   \noindent

   776   This lemma allows us to use our quotient package for introducing 

   777   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}

   778   representing $\alpha$-equivalence classes of pairs of type 

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

   780   (in the third case). 

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

   782   %

   783   %\begin{center}

   784   @{term "Abs_set as x"}, %\hspace{5mm} 

   785   @{term "Abs_res as x"} and %\hspace{5mm}

   786   @{term "Abs_lst as x"}, 

   787   %\end{center}

   788   %

   789   %\noindent

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

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

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

   793   abstractions, namely:

   794 

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

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

   797 

   798   \begin{center}

   799   \begin{tabular}{l}

   800   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$

   801   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\

   802   @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$

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

   804   \end{tabular}

   805   \end{center}

   806   \end{theorem}

   807 

   808   \noindent

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

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

   811   our formalisation in Isabelle/HOL.

   812 

   813   %\noindent

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

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

   816   %we have 

   817   %%

   818   %\begin{equation}\label{abseqiff}

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

   820   %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]}

   821   %\end{equation}

   822   %

   823   %\noindent

   824   %and also

   825   %

   826   %\begin{equation}\label{absperm}

   827   %%@%{%thm %permute_Abs[no_vars]}%

   828   %\end{equation}

   829 

   830   %\noindent

   831   %The second fact derives from the definition of permutations acting on pairs 

   832   %\eqref{permute} and $\alpha$-equivalence being equivariant 

   833   %(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 

   834   %the following lemma about swapping two atoms in an abstraction.

   835   %

   836   %\begin{lemma}

   837   %@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}

   838   %\end{lemma}

   839   %

   840   %\begin{proof}

   841   %This lemma is straightforward using \eqref{abseqiff} and observing that

   842   %the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.

   843   %Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).

   844   %\end{proof}

   845   %

   846   %\noindent

   847   %Assuming that @{text "x"} has finite support, this lemma together 

   848   %with \eqref{absperm} allows us to show

   849   %

   850   %\begin{equation}\label{halfone}

   851   %@{thm Abs_supports(1)[no_vars]}

   852   %\end{equation}

   853   %

   854   %\noindent

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

   856   %Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 

   857   %it, we use a trick from \cite{Pitts04} and first define an auxiliary 

   858   %function @{text aux}, taking an abstraction as argument:

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

   860   %

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

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

   863   %and therefore has empty support. 

   864   %This in turn means

   865   %

   866   %\begin{center}

   867   %@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}

   868   %\end{center}

   869   %

   870   %\noindent

   871   %using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,

   872   %we further obtain

   873   %

   874   %\begin{equation}\label{halftwo}

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

   876   %\end{equation}

   877   %

   878   %\noindent

   879   %since for finite sets of atoms, @{text "bs"}, we have 

   880   %@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.

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

   882   %Theorem~\ref{suppabs}. 

   883 

   884   The method of first considering abstractions of the

   885   form @{term "Abs_set as x"} etc is motivated by the fact that 

   886   we can conveniently establish  at the Isabelle/HOL level

   887   properties about them.  It would be

   888   laborious to write custom ML-code that derives automatically such properties 

   889   for every term-constructor that binds some atoms. Also the generality of

   890   the definitions for $\alpha$-equivalence will help us in the next sections.

   891 *}

   892 

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

   894 

   895 text {*

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

   897   datatype package of Isabelle/HOL %\cite{Berghofer99} 

   898   and by the syntax of the

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

   900   collection of (possibly mutual recursive) type declarations, say @{text

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

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

   903   syntax in Nominal Isabelle for such specifications is roughly as follows:

   904   %

   905   \begin{equation}\label{scheme}

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

   907   type \mbox{declaration part} &

   908   $\begin{cases}

   909   \mbox{\small\begin{tabular}{l}

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

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

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

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

   914   \end{tabular}}

   915   \end{cases}$\\

   916   binding \mbox{function part} &

   917   $\begin{cases}

   918   \mbox{\small\begin{tabular}{l}

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

   920   \isacommand{where}\\

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

   922   \end{tabular}}

   923   \end{cases}$\\

   924   \end{tabular}}

   925   \end{equation}

   926 

   927   \noindent

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

   929   term-constructors, each of which comes with a list of labelled 

   930   types that stand for the types of the arguments of the term-constructor.

   931   For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with

   932 

   933   \begin{center}

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

   935   \end{center}

   936   

   937   \noindent

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

   939   can be contained

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

   941   \eqref{scheme}. 

   942   In this case we will call the corresponding argument a

   943   \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. 

   944   %The types of such recursive 

   945   %arguments need to satisfy a  ``positivity''

   946   %restriction, which ensures that the type has a set-theoretic semantics 

   947   %\cite{Berghofer99}.  

   948   The labels

   949   annotated on the types are optional. Their purpose is to be used in the

   950   (possibly empty) list of \emph{binding clauses}, which indicate the binders

   951   and their scope in a term-constructor.  They come in three \emph{modes}:

   952   %

   953   \begin{center}

   954   \begin{tabular}{@ {}l@ {}}

   955   \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,

   956   \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,

   957   \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}

   958   \end{tabular}

   959   \end{center}

   960   %

   961   \noindent

   962   The first mode is for binding lists of atoms (the order of binders matters);

   963   the second is for sets of binders (the order does not matter, but the

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

   965   preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding

   966   clause will be called \emph{bodies}; the

   967   ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to

   968   Ott, we allow multiple labels in binders and bodies. 

   969 

   970   %For example we allow

   971   %binding clauses of the form:

   972   %

   973   %\begin{center}

   974   %\begin{tabular}{@ {}ll@ {}}

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

   976   %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\

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

   978   %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 

   979   %    \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\

   980   %\end{tabular}

   981   %\end{center}

   982 

   983   \noindent

   984   %Similarly for the other binding modes. 

   985   %Interestingly, in case of \isacommand{bind (set)}

   986   %and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics

   987   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 

   988   %show this later with an example.

   989   

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

   991   the ones of Ott. The

   992   main idea behind these restrictions is that we obtain a sensible notion of

   993   $\alpha$-equivalence where it is ensured that within a given scope an 

   994   atom occurrence cannot be both bound and free at the same time.  The first

   995   restriction is that a body can only occur in

   996   \emph{one} binding clause of a term constructor (this ensures that the bound

   997   atoms of a body cannot be free at the same time by specifying an

   998   alternative binder for the same body). 

   999 

  1000   For binders we distinguish between

  1001   \emph{shallow} and \emph{deep} binders.  Shallow binders are just

  1002   labels. The restriction we need to impose on them is that in case of

  1003   \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either

  1004   refer to atom types or to sets of atom types; in case of \isacommand{bind}

  1005   the labels must refer to atom types or lists of atom types. Two examples for

  1006   the use of shallow binders are the specification of lambda-terms, where a

  1007   single name is bound, and type-schemes, where a finite set of names is

  1008   bound:

  1009 

  1010   \begin{center}\small

  1011   \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}

  1012   \begin{tabular}{@ {}l}

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

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

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

  1016   \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\

  1017   \end{tabular} &

  1018   \begin{tabular}{@ {}l@ {}}

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

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

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

  1022   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%

  1023   \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\

  1024   \end{tabular}

  1025   \end{tabular}

  1026   \end{center}

  1027 

  1028   \noindent

  1029   In these specifications @{text "name"} refers to an atom type, and @{text

  1030   "fset"} to the type of finite sets.

  1031   Note that for @{text lam} it does not matter which binding mode we use. The

  1032   reason is that we bind only a single @{text name}. However, having

  1033   \isacommand{bind (set)} or \isacommand{bind} in the second case makes a

  1034   difference to the semantics of the specification (which we will define in the next section).

  1035 

  1036 

  1037   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

  1038   the atoms in one argument of the term-constructor, which can be bound in

  1039   other arguments and also in the same argument (we will call such binders

  1040   \emph{recursive}, see below). The binding functions are

  1041   expected to return either a set of atoms (for \isacommand{bind (set)} and

  1042   \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can

  1043   be defined by recursion over the corresponding type; the equations

  1044   must be given in the binding function part of the scheme shown in

  1045   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

  1046   tuple patterns might be specified as:

  1047   %

  1048   \begin{equation}\label{letpat}

  1049   \mbox{\small%

  1050   \begin{tabular}{l}

  1051   \isacommand{nominal\_datatype} @{text trm} $=$\\

  1052   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\

  1053   \hspace{5mm}$\mid$~@{term "App trm trm"}\\

  1054   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 

  1055      \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\

  1056   \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 

  1057      \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\

  1058   \isacommand{and} @{text pat} $=$

  1059   @{text PNil}

  1060   $\mid$~@{text "PVar name"}

  1061   $\mid$~@{text "PTup pat pat"}\\ 

  1062   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\

  1063   \isacommand{where}~@{text "bn(PNil) = []"}\\

  1064   \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\

  1065   \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 

  1066   \end{tabular}}

  1067   \end{equation}

  1068   %

  1069   \noindent

  1070   In this specification the function @{text "bn"} determines which atoms of

  1071   the pattern @{text p} are bound in the argument @{text "t"}. Note that in the

  1072   second-last @{text bn}-clause the function @{text "atom"} coerces a name

  1073   into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This

  1074   allows us to treat binders of different atom type uniformly.

  1075 

  1076   As said above, for deep binders we allow binding clauses such as

  1077   %

  1078   %\begin{center}

  1079   %\begin{tabular}{ll}

  1080   @{text "Bar p::pat t::trm"} %%%&  

  1081      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} %%\\

  1082   %\end{tabular}

  1083   %\end{center}

  1084   %

  1085   %\noindent

  1086   where the argument of the deep binder also occurs in the body. We call such

  1087   binders \emph{recursive}.  To see the purpose of such recursive binders,

  1088   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following

  1089   specification:

  1090   %

  1091   \begin{equation}\label{letrecs}

  1092   \mbox{\small%

  1093   \begin{tabular}{@ {}l@ {}}

  1094   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\

  1095   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 

  1096      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\

  1097   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}

  1098      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\

  1099   \isacommand{and} @{text "assn"} $=$

  1100   @{text "ANil"}

  1101   $\mid$~@{text "ACons name trm assn"}\\

  1102   \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\

  1103   \isacommand{where}~@{text "bn(ANil) = []"}\\

  1104   \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\

  1105   \end{tabular}}

  1106   \end{equation}

  1107   %

  1108   \noindent

  1109   The difference is that with @{text Let} we only want to bind the atoms @{text

  1110   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms

  1111   inside the assignment. This difference has consequences for the associated

  1112   notions of free-atoms and $\alpha$-equivalence.

  1113   

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

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

  1116   Consequently we exclude specifications such as

  1117   %

  1118   \begin{center}\small

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

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

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

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

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

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

  1125   \end{tabular}

  1126   \end{center}

  1127 

  1128   \noindent

  1129   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 

  1130   out different atoms to become bound, respectively be free, in @{text "p"}.

  1131   (Since the Ott-tool does not derive a reasoning infrastructure for 

  1132   $\alpha$-equated terms with deep binders, it can permit such specifications.)

  1133   

  1134   We also need to restrict the form of the binding functions in order