12   If  ("if _ then _ else _" 10)

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

    22   alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and

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

    24   alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and

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

    26   fv ("fv'(_')" [100] 100) and

    27   equal ("=") and

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

    29   Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and

    30   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and

    31   Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") 

    22   $t ::= x \mid t\;t \mid \lambda x. t$

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

    27   derives automatically a reasoning infrastructure that  has been used

    47   derives automatically a reasoning infrastructure that has been used

    42   T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T

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

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

    62   \forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x 

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

    66   but assuming that $x$, $y$ and $z$ are distinct variables,

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

    70   \forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z 

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

    74   Moreover, we like to regard type-schemes as 

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

    75   alpha-equivalent, if they differ only on \emph{vacuous} binders, such as

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

    78   \forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y

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

    82   where $z$ does not occur freely in the type.

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

    83   In this paper we will give a general binding mechanism and associated

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

    84   notion of alpha-equivalence that can be used to faithfully represent

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

    85   this kind of binding in Nominal Isabelle.  The difficulty of finding the right notion 

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

    86   for alpha-equivalence can be appreciated in this case by considering that the 

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

    87   definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).

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

    88 

   109 

    89   However, the notion of alpha-equivalence that is preserved by vacuous binders is not

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

    90   always wanted. For example in terms like

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

    93   \LET x = 3 \AND y = 2 \IN x\,-\,y \END

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

   102   $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$

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

   112   research. For example in $\mathtt{let}$s containing patterns

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

   115   \LET (x, y) = (3, 2) \IN x\,-\,y \END

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

   124   $\LET (y, x) = (3, 2) \IN x\,- y\,\END$

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

   125   \end{center}

   146   \end{center}

   126 

   147 

   127   \noindent

   148   \noindent

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

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

   129   variables at once, and let the user chose which one is intended when formalising a

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

   130   programming language calculus.

   151   when formalising a programming language calculus.

   131 

   152 

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

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

   133   a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney 

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

   134   \cite{Cheney05}: in $\mathtt{let}$-constructs of the form

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

   135   %

   156   %

   136   \begin{center}

   157   \begin{center}

   137   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$

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

   138   \end{center}

   159   \end{center}

   139 

   160 

   140   \noindent

   161   \noindent

   141   which bind all the $x_i$ in $s$, we might not care about the order in 

   162   which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care

   142   which the $x_i = t_i$ are given, but we do care about the information that there are 

   163   about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,

   143   as many $x_i$ as there are $t_i$. We lose this information if we represent the 

   164   but we do care about the information that there are as many @{text

   144   $\mathtt{let}$-constructor by something like 

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

   145   %

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

   146   \begin{center}

   167   %

   147   $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$

   168   \begin{center}

   148   \end{center}

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

   149 

   170   \end{center}

   150   \noindent

   171 

   151   where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound

   172   \noindent

   152   in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}

   173   where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}

   153   would be a perfectly legal instance. To exclude such terms, additional

   174   become bound in @{text s}. In this representation the term 

   154   predicates about well-formed terms are needed in order to ensure that the two

   175   \mbox{@{text "\<LET> [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal

   155   lists are of equal length. This can result into very messy reasoning (see

   176   instance. To exclude such terms, additional predicates about well-formed

   156   for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications

   177   terms are needed in order to ensure that the two lists are of equal

   157   for $\mathtt{let}$s as follows

   178   length. This can result into very messy reasoning (see for

   179   example~\cite{BengtsonParow09}). To avoid this, we will allow type

   180   specifications for $\mathtt{let}$s as follows

   161   $trm$ & $::=$  & \ldots\\ 

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

   162         & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]

   185               & @{text "|"}    & @{text "\<LET> a::assn s::trm"}\hspace{4mm} 

   163   $assn$ & $::=$  & $\mathtt{anil}$\\

   186                                  \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm]

   164          & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$

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

   165   \end{tabular}

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

   166   \end{center}

   189   \end{tabular}

   167 

   190   \end{center}

   168   \noindent

   191 

   169   where $assn$ is an auxiliary type representing a list of assignments 

   192   \noindent

   170   and $bn$ an auxiliary function identifying the variables to be bound by 

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

   171   the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows

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

   172 

   195   by the @{text "\<LET>"}. This function is defined by recursion over @{text

   173   \begin{center}

   196   assn} as follows

   174   $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ 

   197 

   198   \begin{center}

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

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

   179   example \mbox{$s\!::\!trm$}, and a binding clause, in this case

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

   180   $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the

   206   \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states

   181   function call $bn\,(a)$ returns.  This style of specifying terms and bindings is

   207   to bind in @{text s} all the names the function call @{text "bn(a)"} returns.

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

   208   This style of specifying terms and bindings is heavily inspired by the

   209   syntax of the Ott-tool \cite{ott-jfp}.

   210 

   189   $t ::= t\;t \mid \lambda x. t$

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

   207   $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$ 

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

   208   \end{center}

   236   \end{center}

   209   

   237   

   210   \noindent

   238   \noindent

   211   are not just alpha-equal, but actually \emph{equal}. As a

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

   212   result, we can only support specifications that make sense on the level of

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

   213   alpha-equated terms (offending specifications, which for example bind a variable

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

   214   according to a variable bound somewhere else, are not excluded by Ott, but we 

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

   215   have to).  Our

   243   to).  Our insistence on reasoning with alpha-equated terms comes from the

   216   insistence on reasoning with alpha-equated terms comes from the wealth of

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

   217   experience we gained with the older version of Nominal Isabelle: for

   245   for non-trivial properties, reasoning about alpha-equated terms is much

   218   non-trivial properties, reasoning about alpha-equated terms is much easier

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

   219   than reasoning with raw terms. The fundamental reason for this is that the

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

   220   HOL-logic underlying Nominal Isabelle allows us to replace

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

   221   ``equals-by-equals''. In contrast, replacing ``alpha-equals-by-alpha-equals''

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

   222   in a representation based on raw terms requires a lot of extra reasoning work.

   250   requires a lot of extra reasoning work.

   223 

   251 

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

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

   225   terms is nearly always taken for granted, establishing 

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

   226   it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. 

   254   the Isabelle/HOL theorem prover is a rather non-trivial task. For every

   227   For every specification we will need to construct a type containing as 

   255   specification we will need to construct a type containing as elements the

   228   elements the alpha-equated terms. To do so, we use 

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

   229   the standard HOL-technique of defining a new type by  

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

   230   identifying a non-empty subset of an existing type.   The construction we 

   258   construction we perform in HOL can be illustrated by the following picture:

   231   perform in HOL can be illustrated by the following picture:

   259 

   232  

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

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

   259   datatype in Isabelle/HOL); identify then the 

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

   260   alpha-equivalence classes in the type of sets of raw terms according to our 

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

   261   alpha-equivalence relation and finally define the new type as these 

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

   262   alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are 

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

   263   definable as datatype in Isabelle/HOL and the fact that our relation for 

   290   in Isabelle/HOL and the fact that our relation for alpha-equivalence is

   264   alpha-equivalence is indeed an equivalence relation).

   291   indeed an equivalence relation).

   265 

   292 

   266   The fact that we obtain an isomorphism between the new type and the non-empty 

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

   267   subset shows that the new type is a faithful representation of alpha-equated terms. 

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

   268   That is not the case for example for terms using the locally 

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

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

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

   270   there are ``junk'' terms that need to

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

   271   be excluded by reasoning about a well-formedness predicate.

   298   reasoning about a well-formedness predicate.

   272 

   299 

   273   The problem with introducing a new type in Isabelle/HOL is that in order to be useful, 

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

   274   a reasoning infrastructure needs to be ``lifted'' from the underlying subset to 

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

   275   the new type. This is usually a tricky and arduous task. To ease it,

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

   276   we re-implemented in Isabelle/HOL the quotient package described by Homeier 

   303   task. To ease it, we re-implemented in Isabelle/HOL the quotient package

   277   \cite{Homeier05} for the HOL4 system. This package 

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

   278   allows us to  lift definitions and theorems involving raw terms

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

   279   to definitions and theorems involving alpha-equated terms. For example

   306   definitions and theorems involving alpha-equated terms. For example if we

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

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

   281 

   308 

   282   \begin{center}

   309   \begin{center}

   283   $\fv(x) = \{x\}$\hspace{10mm}

   310   @{text "fv(x) = {x}"}\hspace{10mm}

   284   $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]

   311   @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]

   285   $\fv(\lambda x.t) = \fv(t) - \{x\}$

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

   286   \end{center}

   313   \end{center}

   287   

   314   

   288   \noindent

   315   \noindent

   289   then with not too great effort we obtain a function $\fv^\alpha$

   316   then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}

   294   $\fv^\alpha(x) = \{x\}$\hspace{10mm}

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

   295   $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm]

   322   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]

   296   $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$

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

   403 

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

   404   In order to keep our work manageable, we will wherever possible state

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

   405   definitions and perform proofs inside Isabelle, as opposed to write custom

   432   on the user-level of Isabelle/HOL, as opposed to write custom ML-code that

   406   ML-code that generates them anew for each specification. To that

   433   generates them anew for each specification. To that end, we will consider

   407   end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.

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

   408   These pairs are intended to represent the abstraction, or binding, of the set @{text "as"} 

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

   409   in the body @{text "x"}.

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

   410 

   437 

   411   The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are

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

   412   alpha-equivalent? (At the moment we are interested in

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

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

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

   414   vacuous binders.) To answer this, we identify four conditions: {\it i)} given 

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

   415   a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then @{text x} and @{text y} 

   442   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

   416   need to have the same set of free variables; moreover there must be a permutation

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

   417   @{text p}  such that {\it ii)} it leaves the free variables of @{text x} and @{text y} unchanged, 

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

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

   445   ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but

   419   say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that @{text p} makes 

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

   420   the abstracted sets @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can 

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

   421   be stated formally as follows:

   448   @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The

   449   requirements {\it i)} to {\it iv)} can be stated formally as follows:

   425   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]

   453   \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\

   426              & @{text "fv(x) - as = fv(y) - bs"}\\

   454                & @{term "fv(x) - as = fv(y) - bs"}\\

   427   \wedge     & @{text "(fv(x) - as) #* p"}\\

   455   @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\

   428   \wedge     & @{text "(p \<bullet> x) R y"}\\

   456   @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\

   429   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 

   457   @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\ 

   434   Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where 

   462   Note that this relation is dependent on the permutation @{text

   435   we existentially quantify over this $p$. 

   463   "p"}. Alpha-equivalence between two pairs is then the relation where we

   436   Also note that the relation is dependent on a free-variable function $\fv$ and a relation 

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

   437   $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both 

   465   dependent on a free-variable function @{text "fv"} and a relation @{text

   438   ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by 

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

   439   equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support 

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

   440   of $x$ and $y$. 

   468   the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we

   469   will prove that @{text "fv"} is equal to the support of @{text

   470   x} and @{text y}.

   449   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]

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

   450              & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\

   480              & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\

   451   \wedge     & @{text "(fv(x) - set as) #* p"}\\

   481   \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\

   453   \wedge     & @{text "(p \<bullet> as) = bs"}\\ 

   483   \wedge     & @{term "(p \<bullet> as) = bs"}\\ 

   458   where $set$ is the function that coerces a list of atoms into a set of atoms.

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

   459 

   489   Now the last clause ensures that the order of the binders matters.

   460   If we do not want to make any difference between the order of binders and

   490 

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

   466   \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]

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

   467              & @{text "fv(x) - as = fv(y) - bs"}\\

   498              & @{term "fv(x) - as = fv(y) - bs"}\\

   468   \wedge     & @{text "(fv(x) - as) #* p"}\\

   499   \wedge     & @{term "(fv(x) - as) \<sharp>* p"}\\

   476   We set $R$ to be the equality and for $\fv(T)$ we define

   507   We set @{text R} to be the equality and for @{text "fv(T)"} we define

   477 

   508 

   478   \begin{center}

   509   \begin{center}

   479   $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$

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

   480   \end{center}

   511   \end{center}

   481 

   512 

   482   \noindent

   513   \noindent

   483   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily 

   514   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and

   484   checked that @{text "({x, y}, x \<rightarrow> y)"} and

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

   485   @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to

   516   @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and

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

   517   $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>

   487   $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that 

   518   y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}

   488   makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the 

   519   $\not\approx_{\textit{list}}$ @{text "([y,x], x \<rightarrow> y)"} since there is no permutation

   489   type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another examples is 

   520   that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also

   490    $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation.

   521   leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is

   491   However, if @{text "x \<noteq> y"}, then  

   522   @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by 

   492   $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes

   523   taking @{text p} to be the

   493   the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).

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

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

   526   that makes the

   527   sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$).

   496   \noindent

   530   % looks too ugly

   497   Let $\star$ range over $\{set, res, list\}$. We prove next under which 

   531   %\noindent

   498   conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence 

   532   %Let $\star$ range over $\{set, res, list\}$. We prove next under which 

   499   relations and equivariant:

   533   %conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence 

   534   %relations and equivariant:

   535   %

   536   %\begin{lemma}

   537   %{\it i)} Given the fact that $x\;R\;x$ holds, then 

   538   %$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given

   539   %that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then

   540   %$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies

   541   %$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given

   542   %that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies 

   543   %@{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$

   544   %and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies

   545   %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given

   546   %@{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and

   547   %@{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then

   548   %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies

   549   %$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star 

   550   %(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.

   551   %\end{lemma}

   552   

   553   %\begin{proof}

   554   %All properties are by unfolding the definitions and simple calculations. 

   555   %\end{proof}

   556 

   557 

   558   In the rest of this section we are going to introduce a type- and term-constructor 

   559   for abstractions. For this we define 

   560   %

   561   \begin{equation}

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

   563   \end{equation}

   564   

   565   \noindent

   566   Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these 

   567   relations are equivalence relations and equivariant 

   568   (we only show the $\approx_{\textit{abs\_set}}$-case).

   502   {\it i)} Given the fact that $x\;R\;x$ holds, then 

   571   $\approx_{\textit{abs\_set}}$ is an equivalence

   503   $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given

   572   relations, and if @{term "abs_set (as, x) (bs, x)"} then also

   504   that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then

   573   @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}.

   505   $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies

   506   $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given

   507   that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies 

   508   @{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$

   509   and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies

   510   $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given

   511   @{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and

   512   @{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then

   513   $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies

   514   $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star 

   515   (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.

   517   

   575 

   519   All properties are by unfolding the definitions and simple calculations. 

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

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

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

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

   581   calculations. 

   837   $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\

   932   $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\