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   Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 

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

    14 

    15 definition

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

    17 

    18 notation (latex output)

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

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

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

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

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

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

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

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

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

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

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

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

    31   equal ("=") and

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

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

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

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

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

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

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

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

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

    41 

    42 consts alpha_trm ::'a

    43 consts fa_trm :: 'a

    44 consts alpha_trm2 ::'a

    45 consts fa_trm2 :: 'a

    46 consts ast :: 'a

    47 consts ast' :: 'a

    48 notation (latex output) 

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

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

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

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

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

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

    55 

    56 (*>*)

    57 

    58 

    59 section {* Introduction *}

    60 

    61 text {*

    62 

    63   So far, Nominal Isabelle provided a mechanism for constructing

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

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

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

    67   Nominal Isabelle derives automatically a reasoning infrastructure that has

    68   been used successfully in formalisations of an equivalence checking

    69   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

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

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

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

    73   formalisations in the locally-nameless approach to binding

    74   \cite{SatoPollack10}.

    75 

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

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

    78   respectively, of the form

    79   %

    80   \begin{equation}\label{tysch}

    81   \begin{array}{l}

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

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

    84   \end{array}

    85   \end{equation}

    86   %

    87   \noindent

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

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

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

    91   formalisation of W. 

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

    93   %why Nominal Isabelle 

    94   % and similar theorem provers that only provide

    95   %mechanisms for binding single variables 

    96   %has not fared extremely well with the

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

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

    99 

   100   Binding multiple variables has interesting properties that cannot be captured

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

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

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

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

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

   106   %

   107   \begin{equation}\label{ex1}

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

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

   110   \end{equation}

   111   %

   112   \noindent

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

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

   115   %

   116   \begin{equation}\label{ex3}

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

   118   \end{equation}

   119   %

   120   \noindent

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

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

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

   124   Isabelle.  

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

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

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

   128 

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

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

   131   %

   132   \begin{equation}\label{one}

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

   134   \end{equation}

   135 

   136   \noindent

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

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

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

   140   %

   141   \begin{center}

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

   143   \end{center}

   144   %

   145   \noindent

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

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

   148   binders has to agree.

   149 

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

   151   language constructs frequently occurring in programming language

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

   153   %

   154   \begin{equation}\label{two}

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

   156   \end{equation}

   157   %

   158   \noindent

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

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

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

   162   %

   163   \begin{center}

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

   165   \end{center}

   166   %

   167   \noindent

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

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

   170   in a formalisation.

   171   %%when formalising a term-calculus.

   172 

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

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

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

   176   %

   177   \begin{center}

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

   179   \end{center}

   180   %

   181   \noindent

   182   we care about the 

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

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

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

   186   %

   187   \begin{center}

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

   189   \end{center}

   190   %

   191   \noindent

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

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

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

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

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

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

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

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

   200   %

   201   \begin{center}

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

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

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

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

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

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

   208   \end{tabular}

   209   \end{center}

   210   %

   211   \noindent

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

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

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

   215   assn} as follows

   216   %

   217   \begin{center}

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

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

   220   \end{center}

   221   %

   222   \noindent

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

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

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

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

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

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

   229 

   230   %Though, Ott

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

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

   233   %of names cannot be modelled in Ott.

   234 

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

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

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

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

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

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

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

   242 

   243   Another reason is that we establish the reasoning infrastructure

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

   245   infrastructure in Isabelle/HOL for

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

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

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

   249   that the two type-schemes

   250 

   251   \begin{center}

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

   253   \end{center}

   254   

   255   \noindent

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

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

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

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

   260   to).  

   261 

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

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

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

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

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

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

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

   269   %requires a lot of extra reasoning work.

   270 

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

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

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

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

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

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

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

   278   %

   279   \begin{center}

   280   \begin{tikzpicture}[scale=0.89]

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

   282   

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

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

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

   286   

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

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

   289 

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

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

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

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

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

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

   296   

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

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

   299 

   300   \end{tikzpicture}

   301   \end{center}

   302   %

   303   \noindent

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

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

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

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

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

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

   310   an equivalence relation).

   311 

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

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

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

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

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

   317   %reasoning about a well-formedness predicate.

   318 

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

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

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

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

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

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

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

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

   327 

   328   \begin{center}

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

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

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

   332   \end{center}

   333   

   334   \noindent

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

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

   337   lifted function is characterised by the equations

   338 

   339   \begin{center}

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

   341   @{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}

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

   343   \end{center}

   344 

   345   \noindent

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

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

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

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

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

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

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

   353   To sum up, every lifting

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

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

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

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

   358 

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

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

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

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

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

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

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

   366 

   367   \noindent

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

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

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

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

   372   terms, including properties about support, freshness and equality

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

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

   375   The method behind our specification of general binders is taken 

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

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

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

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

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

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

   382 

   383 

   384   %\begin{figure}

   385   %\begin{boxedminipage}{\linewidth}

   386   %%\begin{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   415   %\end{tabular}

   416   %\end{center}

   417   %\end{boxedminipage}

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

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

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

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

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

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

   424   %\end{figure}

   425 *}

   426 

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

   428 

   429 text {*

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

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

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

   433   to aid the description of what follows. 

   434 

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

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

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

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

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

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

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

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

   443   in what follows to only one sort of atoms.

   444 

   445   Permutations are bijective functions from atoms to atoms that are 

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

   447   two-place permutation operation written

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

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

   450   over which the permutation 

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

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

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

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

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

   456   given by:

   457   %

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

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

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

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

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

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

   464   %\end{tabular} &

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

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

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

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

   469   %\end{tabular}

   470   %\end{tabular}}

   471   %\end{equation}

   472   %

   473   \begin{center}

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

   475   \begin{tabular}{@ {}l@ {}}

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

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

   478   \end{tabular} &

   479   \begin{tabular}{@ {}l@ {}}

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

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

   482   \end{tabular} &

   483   \begin{tabular}{@ {}l@ {}}

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

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

   486   \end{tabular}

   487   \end{tabular}}

   488   \end{center}

   489 

   490   \noindent

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

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

   493   as follows:

   494   %

   495   \begin{center}

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

   497   \end{center}

   498 

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

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

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

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

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

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

   505   @{text x}, namely:

   506   %

   507   \begin{equation}\label{suppdef}

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

   509   \end{equation}

   510 

   511   \noindent

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

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

   514   We use for sets of atoms the abbreviation 

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

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

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

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

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

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

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

   522   %

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

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

   525   %\end{myproperty}

   526   %

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

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

   529   %booleans and permutations as follows

   530   %%

   531   %\begin{center}

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

   533   %\begin{tabular}{rcl}

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

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

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

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

   538   %\end{tabular}

   539   %&

   540   %\begin{tabular}{rcl}

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

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

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

   544   %\end{tabular}

   545   %\end{tabular}

   546   %\end{center}

   547   %

   548   %\noindent 

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

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

   551   %

   552   %Reasoning about

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

   554   %as follows:

   555   %

   556   %\begin{definition}

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

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

   559   %\end{definition}

   560   %

   561   %\noindent

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

   563   %two properties.

   564   %

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

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

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

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

   569   %\end{myproperty}

   570   %

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

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

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

   574   %%

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

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

   577   %\end{equation}

   578   %

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

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

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

   582   %%

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

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

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

   586   %\end{equation}

   587   % 

   588   %\noindent

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

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

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

   592   %that

   593   %%

   594   %\begin{center}

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

   596   %\end{center}

   597   %

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

   599   %binders. 

   600   %

   601   %\noindent

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

   603   %Property~\ref{swapfreshfresh}

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

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

   606   following generalisations turned out to be easier to use.

   607 

   608   \begin{myproperty}\label{supppermeq}

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

   610   \end{myproperty}

   611 

   612   \begin{myproperty}\label{avoiding}

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

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

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

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

   617   \end{myproperty}

   618 

   619   \noindent

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

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

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

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

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

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

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

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

   628 

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

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

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

   632   the presence of multiple binders.

   633 *}

   634 

   635 

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

   637 

   638 text {*

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

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

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

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

   643 

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

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

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

   647   %generates them anew for each specification. 

   648   To that end, we will consider

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

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

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

   652 

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

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

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

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

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

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

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

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

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

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

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

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

   665   %

   666   \begin{equation}\label{alphaset}

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

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

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

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

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

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

   673   \end{array}

   674   \end{equation}

   675   %

   676   \noindent

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

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

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

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

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

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

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

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

   685 

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

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

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

   689   as follows

   690   %

   691   \begin{equation}\label{alphalist}

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

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

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

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

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

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

   698   \end{array}

   699   \end{equation}

   700   %

   701   \noindent

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

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

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

   705 

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

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

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

   709   %

   710   \begin{equation}\label{alphares}

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

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

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

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

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

   716   \end{array}

   717   \end{equation}

   718 

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

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

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

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

   723   define

   724   %

   725   \begin{center}

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

   727   \end{center}

   728 

   729   \noindent

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   745   abstract a single atom.

   746 

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

   748   types. For this we define 

   749   %

   750   \begin{equation}

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

   752   \end{equation}

   753   

   754   \noindent

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

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

   757   relations. %% and equivariant.

   758 

   759   \begin{lemma}\label{alphaeq} 

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

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

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

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

   764   \end{lemma}

   765 

   766   \begin{proof}

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

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

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

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

   771   calculations. 

   772   \end{proof}

   773 

   774   \noindent

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

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

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

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

   779   (in the third case). 

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

   781   %

   782   %\begin{center}

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

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

   785   @{term "Abs_lst as x"}, 

   786   %\end{center}

   787   %

   788   %\noindent

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

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

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

   792   abstractions, namely:

   793 

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

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

   796 

   797   \begin{center}

   798   \begin{tabular}{l}

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

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

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

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

   803   \end{tabular}

   804   \end{center}

   805   \end{theorem}

   806 

   807   \noindent

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

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

   810   our formalisation in Isabelle/HOL.

   811 

   812   %\noindent

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

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

   815   %we have 

   816   %%

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

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

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

   820   %\end{equation}

   821   %

   822   %\noindent

   823   %and also

   824   %

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

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

   827   %\end{equation}

   828 

   829   %\noindent

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

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

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

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

   834   %

   835   %\begin{lemma}

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

   837   %\end{lemma}

   838   %

   839   %\begin{proof}

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

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

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

   843   %\end{proof}

   844   %

   845   %\noindent

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

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

   848   %

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

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

   851   %\end{equation}

   852   %

   853   %\noindent

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

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

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

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

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

   859   %

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

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

   862   %and therefore has empty support. 

   863   %This in turn means

   864   %

   865   %\begin{center}

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

   867   %\end{center}

   868   %

   869   %\noindent

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

   871   %we further obtain

   872   %

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

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

   875   %\end{equation}

   876   %

   877   %\noindent

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

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

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

   881   %Theorem~\ref{suppabs}. 

   882 

   883   The method of first considering abstractions of the

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

   885   we can conveniently establish  at the Isabelle/HOL level

   886   properties about them.  It would be

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

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

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

   890 *}

   891 

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

   893 

   894 text {*

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

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

   897   and by the syntax of the

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

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

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

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

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

   903   %

   904   \begin{equation}\label{scheme}

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

   906   type \mbox{declaration part} &

   907   $\begin{cases}

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

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

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

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

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

   913   \end{tabular}}

   914   \end{cases}$\\

   915   binding \mbox{function part} &

   916   $\begin{cases}

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

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

   919   \isacommand{where}\\

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

   921   \end{tabular}}

   922   \end{cases}$\\

   923   \end{tabular}}

   924   \end{equation}

   925 

   926   \noindent

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

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

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

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

   931 

   932   \begin{center}

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

   934   \end{center}

   935   

   936   \noindent

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

   938   can be contained

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

   940   \eqref{scheme}. 

   941   In this case we will call the corresponding argument a

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

   943   %The types of such recursive 

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

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

   946   %\cite{Berghofer99}.  

   947   The labels

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

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

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

   951   %

   952   \begin{center}

   953   \begin{tabular}{@ {}l@ {}}

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

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

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

   957   \end{tabular}

   958   \end{center}

   959   %

   960   \noindent

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

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

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

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

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

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

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

   968 

   969   %For example we allow

   970   %binding clauses of the form:

   971   %

   972   %\begin{center}

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

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

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

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

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

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

   979   %\end{tabular}

   980   %\end{center}

   981 

   982   \noindent

   983   %Similarly for the other binding modes. 

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

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

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

   987   %show this later with an example.

   988   

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

   990   the ones of Ott. The

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

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

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

   994   restriction is that a body can only occur in

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

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

   997   alternative binder for the same body). 

   998 

   999   For binders we distinguish between

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

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

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

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

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

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

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

  1007   bound:

  1008 

  1009   \begin{center}\small

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

  1011   \begin{tabular}{@ {}l}

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

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

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

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

  1016   \end{tabular} &

  1017   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

  1023   \end{tabular}

  1024   \end{tabular}

  1025   \end{center}

  1026 

  1027   \noindent

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

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

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

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

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

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

  1034 

  1035 

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

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

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

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

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

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

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

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

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

  1045   tuple patterns might be specified as:

  1046   %

  1047   \begin{equation}\label{letpat}

  1048   \mbox{\small%

  1049   \begin{tabular}{l}

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

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

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

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

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

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

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

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

  1058   @{text PNil}

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

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

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

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

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

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

  1065   \end{tabular}}

  1066   \end{equation}

  1067   %

  1068   \noindent

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

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

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

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

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

  1074 

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

  1076   %

  1077   %\begin{center}

  1078   %\begin{tabular}{ll}

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

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

  1081   %\end{tabular}

  1082   %\end{center}

  1083   %

  1084   %\noindent

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

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

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

  1088   specification:

  1089   %

  1090   \begin{equation}\label{letrecs}

  1091   \mbox{\small%

  1092   \begin{tabular}{@ {}l@ {}}

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

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

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

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

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

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

  1099   @{text "ANil"}

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

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

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

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

  1104   \end{tabular}}

  1105   \end{equation}

  1106   %

  1107   \noindent

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

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

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

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

  1112   

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

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

  1115   Consequently we exclude specifications such as

  1116   %

  1117   \begin{center}\small

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

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

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

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

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

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

  1124   \end{tabular}

  1125   \end{center}

  1126 

  1127   \noindent

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

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

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

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

  1132   

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

  1134   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated