60 

    60   %

    61   \begin{center}

    61   \begin{equation}\label{ex1}

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

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

    63   \end{center}

    63   \end{equation}

    67 

    67   %

    68   \begin{center}

    68   \begin{equation}\label{ex2}

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

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

    70   \end{center}

    70   \end{equation}

    75 

    75   %

    76   \begin{center}

    76   \begin{equation}\label{ex3}

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

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

    78   \end{center}

    78   \end{equation}

   271   a resoning infrastructure needs to be ``lifted'' from the underlying subset to 

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

   282   lifting needs some respectulness proofs which we automated.\medskip

   282   lifting needs some respectfulness proofs which we automated.\medskip

   366   In order to keep our work managable we give need to give definitions  

   366   In order to keep our work manageable we give need to give definitions  

   367   and perform proofs inside Isabelle whereever possible, as opposed to write

   367   and perform proofs inside Isabelle wherever possible, as opposed to write

   381   $(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in

   381   $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in

   383   vacuous binders.) For this we identify four conditions: i) given a free-variable function

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

   384   of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ 

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

   385   need to have the same set of free variables; ii) there must be a permutation,

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

   386   say $p$, that leaves the free variables $x$ and $y$ unchanged, but ``moves'' their bound names 

   386   $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, 

   387   so that we obtain modulo a relation, say @{text "_ R _"}, 

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

   388   two equal terms. We also require that $p$ makes the abstracted sets equal. These 

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

   389   requirements can be stated formally as

   389   the abstracted sets $as$ and $bs$ equal (since at the moment we do not want 

   390 

   390   that the sets $as$ and $bs$ differ on vacuous binders). These requirements can 

   391   \begin{center}

   391   be stated formally as follows

   392   \begin{tabular}{rcl}

   392   %

   393   a

   393   \begin{equation}\label{alphaset}

   394   \end{tabular}

   394   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}

   395   \end{center}

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

   396 

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

   397 

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

   398   Assuming we are given a free-variable function, say 

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

   399   \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then we expect for two alpha-equivelent

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

   400   pairs that their sets of free variables aggree. That is

   400   \end{array}

   401   %

   401   \end{equation}

   402   \begin{equation}\label{four}

   402 

   403   \mbox{@{text "(as, x) \<approx> (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}} 

   403   \noindent

   404   \end{equation}

   404   Alpha equivalence between such pairs is then the relation with the additional 

   405 

   405   existential quantification over $p$. Note that this relation is additionally 

   406   \noindent

   406   dependent on the free-variable function $\fv$ and the relation $R$. The reason 

   407   Next we expect that there is a permutation, say $p$, that leaves the 

   407   for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms

   408   free variables unchanged, but ``moves'' the bound names in $x$ so that

   408   and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and

   409   we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two

   409   we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.

   410   elments of type $\beta$ are equivalent. We also expect that $p$ 

   410 

   411   makes the binders equal. We can formulate these requirements as: there

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

   412   exists a $p$ such that $i)$  @{term "(fv(x) - as) \<sharp>* p"}, $ii)$ @{text "(p \<bullet> x) R y"} and

   412   order of abstracted variables. If we do want this then we can define alpha-equivalence 

   413   $iii)$ @{text "(p \<bullet> as) = bs"}. 

   413   for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by

   414 

   414   %

   415   We take now \eqref{four} and the three 

   415   \begin{equation}\label{alphalist}

   416  

   416   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}

   417 

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

   418   General notion of alpha-equivalence (depends on a free-variable

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

   419   function and a relation).

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

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

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

   422   \end{array}

   423   \end{equation}

   424   

   425   \noindent

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

   427 

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

   429   allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}

   430   and define

   431   %

   432   \begin{equation}\label{alphaset}

   433   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}

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

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

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

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

   438   \end{array}

   439   \end{equation}

   440 

   441   To get a feeling how these definitions pan out in practise consider the case of 

   442   abstracting names over types (like in type-schemes). For this we set $R$ to be 

   443   the equality and for $\fv(T)$ we define

   444 

   445   \begin{center}

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

   447   \end{center}

   448 

   449   \noindent

   450   Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily 

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

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

   453   be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance 

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

   455   makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}

   456   unchanged.

   428   \item non-emptyness

   465   \item non-emptiness