(*<*)+
−
theory Paper+
−
imports "../Nominal/Test" "LaTeXsugar"+
−
begin+
−
+
−
notation (latex output)+
−
  swap ("'(_ _')" [1000, 1000] 1000) and+
−
  fresh ("_ # _" [51, 51] 50) and+
−
  fresh_star ("_ #* _" [51, 51] 50) and+
−
  supp ("supp _" [78] 73) and+
−
  uminus ("-_" [78] 73) and+
−
  If  ("if _ then _ else _" 10)+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  So far, Nominal Isabelle provides a mechanism for constructing+
−
  alpha-equated terms such as+
−
+
−
  \begin{center}+
−
  $t ::= x \mid t\;t \mid \lambda x. t$+
−
  \end{center}+
−
+
−
  \noindent+
−
  where free and bound variables have names.  For such terms Nominal Isabelle+
−
  derives automatically a reasoning infrastructure, which has been used+
−
  successfully in formalisations of an equivalence checking algorithm for LF+
−
  \cite{UrbanCheneyBerghofer08}, Typed+
−
  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency+
−
  \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result+
−
  for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been+
−
  used by Pollack for formalisations in the locally-nameless approach to+
−
  binding \cite{SatoPollack10}.+
−
+
−
  However, Nominal Isabelle has fared less well in a formalisation of+
−
  the algorithm W \cite{UrbanNipkow09}, where types and type-schemes+
−
  are of the form+
−
  %+
−
  \begin{equation}\label{tysch}+
−
  \begin{array}{l}+
−
  T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T+
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  and the quantification $\forall$ binds a finite (possibly empty) set of+
−
  type-variables.  While it is possible to implement this kind of more general+
−
  binders by iterating single binders, this leads to a rather clumsy+
−
  formalisation of W. The need of iterating single binders is also one reason+
−
  why Nominal Isabelle and similar theorem provers that only provide+
−
  mechanisms for binding single variables have not fared extremely well with the+
−
  more advanced tasks in the POPLmark challenge \cite{challenge05}, because+
−
  also there one would like to bind multiple variables at once.+
−
+
−
  Binding multiple variables has interesting properties that cannot be captured+
−
  easily by iterating single binders. For example in case of type-schemes we do not+
−
  want to make a distinction about the order of the bound variables. Therefore+
−
  we would like to regard the following two type-schemes as alpha-equivalent+
−
  %+
−
  \begin{equation}\label{ex1}+
−
  \forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x +
−
  \end{equation}+
−
+
−
  \noindent+
−
  but assuming that $x$, $y$ and $z$ are distinct variables,+
−
  the following two should \emph{not} be alpha-equivalent+
−
  %+
−
  \begin{equation}\label{ex2}+
−
  \forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z +
−
  \end{equation}+
−
+
−
  \noindent+
−
  Moreover, we like to regard type-schemes as +
−
  alpha-equivalent, if they differ only on \emph{vacuous} binders, such as+
−
  %+
−
  \begin{equation}\label{ex3}+
−
  \forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y+
−
  \end{equation}+
−
+
−
  \noindent+
−
  where $z$ does not occur freely in the type.+
−
  In this paper we will give a general binding mechanism and associated+
−
  notion of alpha-equivalence that can be used to faithfully represent+
−
  this kind of binding in Nominal Isabelle.  The difficulty of finding the right notion +
−
  for alpha-equivalence in this case can be appreciated by considering that the +
−
  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).+
−
+
−
  However, the notion of alpha-equivalence that is preserved by vacuous binders is not+
−
  always wanted. For example in terms like+
−
  %+
−
  \begin{equation}\label{one}+
−
  \LET x = 3 \AND y = 2 \IN x\,-\,y \END+
−
  \end{equation}+
−
+
−
  \noindent+
−
  we might not care in which order the assignments $x = 3$ and $y = 2$ are+
−
  given, but it would be unusual to regard \eqref{one} as alpha-equivalent +
−
  with+
−
  %+
−
  \begin{center}+
−
  $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$+
−
  \end{center}+
−
+
−
  \noindent+
−
  Therefore we will also provide a separate binding mechanism for cases in+
−
  which the order of binders does not matter, but the ``cardinality'' of the+
−
  binders has to agree.+
−
+
−
  However, we found that this is still not sufficient for dealing with+
−
  language constructs frequently occurring in programming language+
−
  research. For example in $\mathtt{let}$s containing patterns+
−
  %+
−
  \begin{equation}\label{two}+
−
  \LET (x, y) = (3, 2) \IN x\,-\,y \END+
−
  \end{equation}+
−
+
−
  \noindent+
−
  we want to bind all variables from the pattern inside the body of the+
−
  $\mathtt{let}$, but we also care about the order of these variables, since+
−
  we do not want to regard \eqref{two} as alpha-equivalent with+
−
  %+
−
  \begin{center}+
−
  $\LET (y, x) = (3, 2) \IN x\,- y\,\END$+
−
  \end{center}+
−
+
−
  \noindent+
−
  As a result, we provide three general binding mechanisms each of which binds multiple+
−
  variables at once, and let the user chose which one is intended when formalising a+
−
  programming language calculus.+
−
+
−
  By providing these general binding mechanisms, however, we have to work around +
−
  a problem that has been pointed out by Pottier in \cite{Pottier06}: in +
−
  $\mathtt{let}$-constructs of the form+
−
  %+
−
  \begin{center}+
−
  $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$+
−
  \end{center}+
−
+
−
  \noindent+
−
  which bind all the $x_i$ in $s$, we might not care about the order in +
−
  which the $x_i = t_i$ are given, but we do care about the information that there are +
−
  as many $x_i$ as there are $t_i$. We lose this information if we represent the +
−
  $\mathtt{let}$-constructor by something like +
−
  %+
−
  \begin{center}+
−
  $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$+
−
  \end{center}+
−
+
−
  \noindent+
−
  where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound+
−
  in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}+
−
  would be a perfectly legal instance. To exclude such terms an additional+
−
  predicate about well-formed terms is needed in order to ensure that the two+
−
  lists are of equal length. This can result into very messy reasoning (see+
−
  for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications+
−
  for $\mathtt{let}$s as follows+
−
  %+
−
  \begin{center}+
−
  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}+
−
  $trm$ & $::=$  & \ldots\\ +
−
        & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]+
−
  $assn$ & $::=$  & $\mathtt{anil}$\\+
−
         & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where $assn$ is an auxiliary type representing a list of assignments +
−
  and $bn$ an auxiliary function identifying the variables to be bound by +
−
  the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows+
−
+
−
  \begin{center}+
−
  $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ +
−
  \end{center}+
−
  +
−
  \noindent+
−
  The scope of the binding is indicated by labels given to the types, for+
−
  example \mbox{$s\!::\!trm$}, and a binding clause, in this case+
−
  $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the+
−
  function $bn\,(a)$ returns.  This style of specifying terms and bindings is+
−
  heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.+
−
+
−
  However, we will not be able to deal with all specifications that are+
−
  allowed by Ott. One reason is that Ott allows ``empty'' specifications+
−
  like+
−
+
−
  \begin{center}+
−
  $t ::= t\;t \mid \lambda x. t$+
−
  \end{center}+
−
+
−
  \noindent+
−
  where no clause for variables is given. Such specifications make some sense in+
−
  the context of Coq's type theory (which Ott supports), but not at al in a HOL-based +
−
  theorem prover where every datatype must have a non-empty set-theoretic model.+
−
+
−
  Another reason is that we establish the reasoning infrastructure+
−
  for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning +
−
  infrastructure in Isabelle/HOL for+
−
  \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms+
−
  and the raw terms produced by Ott use names for bound variables,+
−
  there is a key difference: working with alpha-equated terms means that the+
−
  two type-schemes with $x$, $y$ and $z$ being distinct+
−
+
−
  \begin{center}+
−
  $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$ +
−
  \end{center}+
−
  +
−
  \noindent+
−
  are not just alpha-equal, but actually equal. As a+
−
  result, we can only support specifications that make sense on the level of+
−
  alpha-equated terms (offending specifications, which for example bind a variable+
−
  according to a variable bound somewhere else, are not excluded by Ott, but we +
−
  have to).  Our+
−
  insistence on reasoning with alpha-equated terms comes from the wealth of+
−
  experience we gained with the older version of Nominal Isabelle: for+
−
  non-trivial properties, reasoning about alpha-equated terms is much easier+
−
  than reasoning with raw terms. The fundamental reason for this is that the+
−
  HOL-logic underlying Nominal Isabelle allows us to replace+
−
  ``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals''+
−
  in a representation based on raw terms requires a lot of extra reasoning work.+
−
+
−
  Although in informal settings a reasoning infrastructure for alpha-equated +
−
  terms (that have names for bound variables) is nearly always taken for granted, establishing +
−
  it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. +
−
  For every specification we will need to construct a type containing as +
−
  elements the alpha-equated terms. To do so, we use +
−
  the standard HOL-technique of defining a new type by  +
−
  identifying a non-empty subset of an existing type.   The construction we +
−
  perform in HOL is illustrated by the following picture:+
−
 +
−
  \begin{center}+
−
  \begin{tikzpicture}+
−
  %\draw[step=2mm] (-4,-1) grid (4,1);+
−
  +
−
  \draw[very thick] (0.7,0.4) circle (4.25mm);+
−
  \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);+
−
  \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);+
−
  +
−
  \draw (-2.0, 0.845) --  (0.7,0.845);+
−
  \draw (-2.0,-0.045)  -- (0.7,-0.045);+
−
+
−
  \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};+
−
  \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};+
−
  \draw (1.8, 0.48) node[right=-0.1mm]+
−
    {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};+
−
  \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};+
−
  \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};+
−
  +
−
  \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);+
−
  \draw (-0.95, 0.3) node[above=0mm] {isomorphism};+
−
+
−
  \end{tikzpicture}+
−
  \end{center}+
−
+
−
  \noindent+
−
  We take as the starting point a definition of raw terms (defined as a +
−
  datatype in Isabelle/HOL); identify then the +
−
  alpha-equivalence classes in the type of sets of raw terms, according to our +
−
  alpha-equivalence relation and finally define the new type as these +
−
  alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are +
−
  definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an +
−
  equivalence relation).+
−
+
−
  The fact that we obtain an isomorphism between between the new type and the non-empty +
−
  subset shows that the new type is a faithful representation of alpha-equated terms. +
−
  That is not the case for example in the representation of terms using the locally +
−
  nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to+
−
  be excluded by reasoning about a well-formedness predicate.+
−
+
−
  The problem with introducing a new type in Isabelle/HOL is that in order to be useful, +
−
  a reasoning infrastructure needs to be ``lifted'' from the underlying subset to +
−
  the new type. This is usually a tricky and arduous task. To ease it+
−
  we re-implemented in Isabelle/HOL the quotient package described by Homeier +
−
  \cite{Homeier05}. This package +
−
  allows us to  lift definitions and theorems involving raw terms+
−
  to definitions and theorems involving alpha-equated terms. For example+
−
  if we define the free-variable function over lambda terms+
−
+
−
  \begin{center}+
−
  $\fv(x) = \{x\}$\hspace{10mm}+
−
  $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]+
−
  $\fv(\lambda x.t) = \fv(t) - \{x\}$+
−
  \end{center}+
−
  +
−
  \noindent+
−
  then with not too great effort we obtain a function $\fv_\alpha$+
−
  operating on quotients, or alpha-equivalence classes of terms, as follows+
−
+
−
  \begin{center}+
−
  $\fv_\alpha(x) = \{x\}$\hspace{10mm}+
−
  $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]+
−
  $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$+
−
  \end{center}+
−
+
−
  \noindent+
−
  (Note that this means also the term-constructors for variables, applications+
−
  and lambda are lifted to the quotient level.)  This construction, of course,+
−
  only works if alpha is an equivalence relation, and the definitions and theorems +
−
  are respectful w.r.t.~alpha-equivalence.  Hence we will not be able to lift this+
−
  a bound-variable function to alpha-equated terms (since it does not respect+
−
  alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness+
−
  properties. These proofs we are able automate and therefore establish a +
−
  useful reasoning infrastructure for alpha-equated lambda terms.\medskip+
−
+
−
+
−
  \noindent+
−
  {\bf Contributions:}  We provide new definitions for when terms+
−
  involving multiple binders are alpha-equivalent. These definitions are+
−
  inspired by earlier work of Pitts \cite{}. By means of automatic+
−
  proofs, we establish a reasoning infrastructure for alpha-equated+
−
  terms, including properties about support, freshness and equality+
−
  conditions for alpha-equated terms. We re also able to derive, at the moment +
−
  only manually, for these terms a strong induction principle that +
−
  has the variable convention already built in.+
−
*}+
−
+
−
section {* A Short Review of the Nominal Logic Work *}+
−
+
−
text {*+
−
  At its core, Nominal Isabelle is an adaption of the nominal logic work by+
−
  Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in+
−
  \cite{HuffmanUrban10}, which we review here briefly to aid the description+
−
  of what follows. Two central notions in the nominal logic work are sorted+
−
  atoms and sort-respecting permutations of atoms. The sorts can be used to+
−
  represent different kinds of variables, such as term- and type-variables in+
−
  Core-Haskell, and it is assumed that there is an infinite supply of atoms+
−
  for each sort. However, in order to simplify the description, we shall+
−
  assume in what follows that there is only a single sort of atoms.+
−
+
−
+
−
  Permutations are bijective functions from atoms to atoms that are +
−
  the identity everywhere except on a finite number of atoms. There is a +
−
  two-place permutation operation written+
−
+
−
  @{text[display,indent=5] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+
−
+
−
  \noindent +
−
  with a generic type in which @{text "\<alpha>"} stands for the type of atoms +
−
  and @{text "\<beta>"} for the type of the object on which the permutation +
−
  acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},+
−
  the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}} +
−
  and the inverse permutation of @{term p} as @{text "- p"}. The permutation+
−
  operation is defined for products, lists, sets, functions, booleans etc +
−
  (see \cite{HuffmanUrban10}).+
−
+
−
  The most original aspect of the nominal logic work of Pitts is a general+
−
  definition for the notion of ``the set of free variables of an object @{text+
−
  "x"}''.  This notion, written @{term "supp x"}, is general in the sense that+
−
  it applies not only to lambda-terms alpha-equated or not, but also to lists,+
−
  products, sets and even functions. The definition depends only on the+
−
  permutation operation and on the notion of equality defined for the type of+
−
  @{text x}, namely:+
−
+
−
  @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}+
−
+
−
  \noindent+
−
  There is also the derived notion for when an atom @{text a} is \emph{fresh}+
−
  for an @{text x}, defined as+
−
  +
−
  @{thm[display,indent=5] fresh_def[no_vars]}+
−
+
−
  \noindent+
−
  We also use for sets of atoms the abbreviation +
−
  @{thm (lhs) fresh_star_def[no_vars]} defined as +
−
  @{thm (rhs) fresh_star_def[no_vars]}.+
−
  A striking consequence of these definitions is that we can prove+
−
  without knowing anything about the structure of @{term x} that+
−
  swapping two fresh atoms, say @{text a} and @{text b}, leave +
−
  @{text x} unchanged. +
−
+
−
  \begin{property}+
−
  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}+
−
  \end{property}+
−
+
−
  \noindent+
−
  For a proof see \cite{HuffmanUrban10}.+
−
+
−
  \begin{property}+
−
  @{thm[mode=IfThen] at_set_avoiding[no_vars]}+
−
  \end{property}+
−
+
−
*}+
−
+
−
+
−
section {* General Binders *}+
−
+
−
text {*+
−
  In Nominal Isabelle, the user is expected to write down a specification of a+
−
  term-calculus and then a reasoning infrastructure is automatically derived+
−
  from this specifcation (remember that Nominal Isabelle is a definitional+
−
  extension of Isabelle/HOL, which does not introduce any new axioms).+
−
+
−
+
−
  In order to keep our work manageable, we will wherever possible state+
−
  definitions and perform proofs inside Isabelle, as opposed to write custom+
−
  ML-code that generates them for each instance of a term-calculus. To that+
−
  end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.+
−
  These pairs are intended to represent the abstraction, or binding, of the set $as$ +
−
  in the body $x$.+
−
+
−
  The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are+
−
  alpha-equivalent? (At the moment we are interested in+
−
  the notion of alpha-equivalence that is \emph{not} preserved by adding +
−
  vacuous binders.) To answer this, we identify four conditions: {\it i)} given +
−
  a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$ +
−
  need to have the same set of free variables; moreover there must be a permutation,+
−
  $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, +
−
  but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, +
−
  say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes +
−
  the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can +
−
  be stated formally as follows:+
−
  %+
−
  \begin{equation}\label{alphaset}+
−
  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+
−
  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]+
−
             & @{text "fv(x) - as = fv(y) - bs"}\\+
−
  \wedge     & @{text "fv(x) - as #* p"}\\+
−
  \wedge     & @{text "(p \<bullet> x) R y"}\\+
−
  \wedge     & @{text "(p \<bullet> as) = bs"}\\ +
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where +
−
  we existentially quantify over this $p$. +
−
  Also note that the relation is dependent on a free-variable function $\fv$ and a relation +
−
  $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both +
−
  ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by +
−
  equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support +
−
  of $x$ and $y$. To have these parameters means, however, we can derive properties about +
−
  them generically.+
−
+
−
  The definition in \eqref{alphaset} does not make any distinction between the+
−
  order of abstracted variables. If we want this, then we can define alpha-equivalence +
−
  for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} +
−
  as follows+
−
  %+
−
  \begin{equation}\label{alphalist}+
−
  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+
−
  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]+
−
             & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\+
−
  \wedge     & @{text "fv(x) - (set as) #* p"}\\+
−
  \wedge     & @{text "(p \<bullet> x) R y"}\\+
−
  \wedge     & @{text "(p \<bullet> as) = bs"}\\ +
−
  \end{array}+
−
  \end{equation}+
−
  +
−
  \noindent+
−
  where $set$ is just the function that coerces a list of atoms into a set of atoms.+
−
+
−
  If we do not want to make any difference between the order of binders and+
−
  also allow vacuous binders, then we keep sets of binders, but drop the fourth +
−
  condition in \eqref{alphaset}:+
−
  %+
−
  \begin{equation}\label{alphares}+
−
  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}+
−
  \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]+
−
             & @{text "fv(x) - as = fv(y) - bs"}\\+
−
  \wedge     & @{text "fv(x) - as #* p"}\\+
−
  \wedge     & @{text "(p \<bullet> x) R y"}\\+
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \begin{exmple}\rm+
−
  It might be useful to consider some examples for how these definitions pan out in practise.+
−
  For this consider the case of abstracting a set of variables over types (as in type-schemes). +
−
  We set $R$ to be the equality and for $\fv(T)$ we define+
−
+
−
  \begin{center}+
−
  $\fv(x) = \{x\}  \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$+
−
  \end{center}+
−
+
−
  \noindent+
−
  Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily +
−
  checked that @{text "({x, y}, x \<rightarrow> y)"} and+
−
  @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to+
−
  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then +
−
  $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that +
−
  makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the +
−
  type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that+
−
   $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.+
−
  However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes+
−
  the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).+
−
  \end{exmple}+
−
+
−
  \noindent+
−
  Let $\star$ range over $\{set, res, list\}$. We prove next under which +
−
  conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence +
−
  relations and equivariant:+
−
+
−
  \begin{lemma}+
−
  {\it i)} Given the fact that $x\;R\;x$ holds, then +
−
  $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given+
−
  that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then+
−
  $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies+
−
  $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given+
−
  that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies +
−
  @{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$+
−
  and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies+
−
  $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given+
−
  @{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and+
−
  @{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then+
−
  $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies+
−
  $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star +
−
  (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.+
−
  \end{lemma}+
−
  +
−
  \begin{proof}+
−
  All properties are by unfolding the definitions and simple calculations. +
−
  \end{proof}+
−
+
−
+
−
  \begin{lemma}+
−
  $supp ([as]set. x) = supp x - as$ +
−
  \end{lemma}+
−
*}+
−
+
−
section {* Alpha-Equivalence and Free Variables *}+
−
+
−
text {*+
−
  A specification of a term-calculus in Nominal Isabelle is a collection+
−
  of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ +
−
  written as follows:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  \isacommand{nominal\_datatype} $ty_1 =$\\+
−
  \isacommand{and} $ty_2 =$\\+
−
  $\ldots$\\ +
−
  \isacommand{and} $ty_n =$\\ +
−
  $\ldots$\\+
−
  \isacommand{with}\\+
−
  $\ldots$\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The section below the \isacommand{with} are binding functions, which+
−
  will be explained below.+
−
  +
−
+
−
+
−
  A specification of a term-calculus in Nominal Isabell is very similar to +
−
  the usual datatype definition of Isabelle/HOL: +
−
+
−
+
−
  Because of the problem Pottier pointed out in \cite{Pottier06}, the general +
−
  binders from the previous section cannot be used directly to represent w +
−
  be used directly +
−
*}+
−
+
−
+
−
+
−
text {*+
−
  Restrictions+
−
+
−
  \begin{itemize}+
−
  \item non-emptiness+
−
  \item positive datatype definitions+
−
  \item finitely supported abstractions+
−
  \item respectfulness of the bn-functions\bigskip+
−
  \item binders can only have a ``single scope''+
−
  \item all bindings must have the same mode+
−
  \end{itemize}+
−
*}+
−
+
−
section {* Examples *}+
−
+
−
section {* Adequacy *}+
−
+
−
section {* Related Work *}+
−
+
−
text {*+
−
  Ott is better with list dot specifications; subgrammars+
−
+
−
  untyped; +
−
  +
−
*}+
−
+
−
+
−
section {* Conclusion *}+
−
+
−
text {*+
−
  Complication when the single scopedness restriction is lifted (two +
−
  overlapping permutations)+
−
*}+
−
+
−
text {*+
−
+
−
  TODO: function definitions:+
−
  \medskip+
−
+
−
  \noindent+
−
  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  +
−
  many discussions about Nominal Isabelle. We thank Peter Sewell for +
−
  making the informal notes \cite{SewellBestiary} available to us and +
−
  also for patiently explaining some of the finer points about the abstract +
−
  definitions and about the implementation of the Ott-tool.+
−
+
−
  Lookup: Merlin paper by James Cheney; Mark Shinwell PhD+
−
+
−
  Future work: distinct list abstraction+
−
+
−
  +
−
*}+
−
+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−