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

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

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

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

   390   custom ML-code that generates them  for each 

   390   from this specifcation (remember that Nominal Isabelle is a definitional

   391   instance of a term-calculus. To this end we will first consider pairs

   391   extension of Isabelle/HOL and cannot introduce new axioms).

   392 

   392 

   393   \begin{equation}\label{three}

   393 

   394   \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}

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

   395   \end{equation}

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

   396  

   396   ML-code that generates them for each instance of a term-calculus. To that

   397   \noindent

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

   398   consisting of a set of atoms and an object of generic type. These pairs

   398   These pairs are intended to represent the abstraction, or binding, of the set $as$ 

   399   are intended to represent the abstraction or binding of the set $as$ 

   399   in the body $x$.

   400   in the body $x$ (similarly to type-schemes given in \eqref{tysch}). 

   400 

   401 

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

   402   The first question we have to answer is when we should consider pairs such as

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

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

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

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

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

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

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

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

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

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

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

   410   the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can 

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

   411   be stated formally as follows:

   413   be stated formally as follows

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

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

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

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

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

   425   we existentially quantify over this $p$. 

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

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

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

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

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

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

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

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

   430   of $x$ and $y$. To have these parameters means, however, we can derive properties about 

   431   them generically.

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

   434   order of abstracted variables. If we want this, then we can define alpha-equivalence 

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

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

   436   as follows

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

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

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

   452   also allow vacuous binders, then we keep sets of binders, but drop the fourth 

   452   and define

   453   condition in \eqref{alphaset}:

   453   %

   454   %

   454   \begin{equation}\label{alphaset}

   455   \begin{equation}\label{alphares}

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

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

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

   464   \begin{exmple}\rm

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

   465   It might be useful to consider some examples for how these definitions pan out in practise.

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

   466   For this consider the case of abstracting a set of variables over types (as in type-schemes). 

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

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

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

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

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

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

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

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

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

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

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

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

   479   makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the 

   478   unchanged.

   480   type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that

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

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

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

   484   \end{exmple}

   485 

   486   \noindent

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

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

   489   relations and equivariant:

   490 

   491   \begin{lemma}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   506   \end{lemma}

   507   

   508   \begin{proof}

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

   510   \end{proof}