56   Binding multiple variables has interesting properties that are not captured

    56   Binding multiple variables has interesting properties that cannot be captured

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

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

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

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

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

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

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

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

   180   $bn$ returns in $s$.  This style of specifying terms and bindings is heavily

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

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

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

   192   where no clause for variables is given. Such specifications make sense in

   192   where no clause for variables is given. Such specifications make some sense in

   193   the context of Coq's type theory (which Ott supports), but not in a HOL-based 

   193   the context of Coq's type theory (which Ott supports), but not at al in a HOL-based 

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

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

   266   That is different for example in the representation of terms using the locally 

   266   That is not the case for example in the representation of terms using the locally 

   267   nameless representation of binders: there are non-well-formed terms that need to

   267   nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to

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

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

   273   we reimplemented in Isabelle/HOL the quotient package described by Homeier 

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

   274   \cite{Homeier05}. Given that alpha is an equivalence relation, this package 

   274   \cite{Homeier05}. This package 

   275   allows us to automatically lift definitions and theorems involving raw terms

   275   allows us to  lift definitions and theorems involving raw terms

   276   to definitions and theorems involving alpha-equated terms. This of course

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

   277   only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.

   277   if we define the free-variable function over lambda terms

   278   Hence we will be able to lift, for instance, the function for free

   278 

   279   variables of raw terms to alpha-equated terms (since this function respects 

   279   \begin{center}

   280   alpha-equivalence), but we will not be able to do this with a bound-variable

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

   281   function (since it does not respect alpha-equivalence). As a result, each

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

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

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

   283   \end{center}

   284   

   285   \noindent

   286   then with not too great effort we obtain a function $\fv_\alpha$

   287   operating on quotients, or alpha-equivalence classes of terms, as follows

   288 

   289   \begin{center}

   290   $\fv_\alpha(x) = \{x\}$\hspace{10mm}

   291   $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]

   292   $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$

   293   \end{center}

   294 

   295   \noindent

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

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

   298   only works if alpha is an equivalence relation, and the definitions and theorems 

   299   are respectful w.r.t.~alpha-equivalence.  Hence we will not be able to lift this

   300   a bound-variable function to alpha-equated terms (since it does not respect

   301   alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness

   302   properties. These proofs we are able automate and therefore establish a 

   303   useful reasoning infrastructure for alpha-equated lambda terms.\medskip

   304 

   366   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

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

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

   368   custom ML-code that generates them  for each 

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

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

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

   370 

   392 

   371   \begin{equation}\label{three}

   393 

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

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

   373   \end{equation}

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

   374  

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

   375   \noindent

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

   376   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$ 

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

   399   in the body $x$.

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

   400 

   379 

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

   380   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

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

   383   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 

   384   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$ 

   386   $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, 

   387   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, 

   389   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 

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

   411   be stated formally as follows:

   391   be stated formally as follows

   395   \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]

   404   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 

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

   425   we existentially quantify over this $p$. 

   406   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 

   407   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 

   408   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 

   409   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.

   412   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 

   413   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

   417   \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]

   429   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 

   430   and define

   453   condition in \eqref{alphaset}:

   431   %

   454   %

   432   \begin{equation}\label{alphaset}

   455   \begin{equation}\label{alphares}

   434   \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]

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

   464   \begin{exmple}\rm

   442   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.

   443   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

   450   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 

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

   475   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

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

   453   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 

   454   $([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 

   455   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 

   456   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}

   506 

   561   Lookup: Merlin paper by James Cheney; Mark Shinwell PhD

   562 

   563   Future work: distinct list abstraction

   564 

   565