(*<*)+
−
theory Paper+
−
imports "../Nominal/Test" "LaTeXsugar"+
−
begin+
−
+
−
consts+
−
  fv :: "'a \<Rightarrow> 'b"+
−
  abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" +
−
  Abs_lst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"+
−
  Abs_res :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"+
−
+
−
definition+
−
 "equal \<equiv> (op =)" +
−
+
−
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) and+
−
  alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and+
−
  alpha_lst ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and+
−
  alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and+
−
  abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and+
−
  fv ("fv'(_')" [100] 100) and+
−
  equal ("=") and+
−
  alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and +
−
  Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and+
−
  Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and+
−
  Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") +
−
(*>*)+
−
+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  So far, Nominal Isabelle provides a mechanism for constructing+
−
  alpha-equated terms, for example+
−
+
−
  \begin{center}+
−
  @{text "t ::= x | t t | \<lambda>x. t"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where free and bound variables have names.  For such terms Nominal Isabelle+
−
  derives automatically a reasoning infrastructure that 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}+
−
  @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}+
−
  @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>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}+
−
  @{text "\<forall>{x,y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y,x}. y \<rightarrow> x"} +
−
  \end{equation}+
−
+
−
  \noindent+
−
  but assuming that @{text x}, @{text y} and @{text z} are distinct variables,+
−
  the following two should \emph{not} be alpha-equivalent+
−
  %+
−
  \begin{equation}\label{ex2}+
−
  @{text "\<forall>{x,y}. x \<rightarrow> y  \<notapprox>\<^isub>\<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}+
−
  @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x,z}. x \<rightarrow> y"}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  where @{text 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+
−
  can be appreciated in this case 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}+
−
  @{text "\<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}+
−
  @{text "\<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 @{text "\<LET>"}s containing patterns+
−
  %+
−
  \begin{equation}\label{two}+
−
  @{text "\<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}+
−
  @{text "\<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 \cite{Pottier06} and+
−
  Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form+
−
  %+
−
  \begin{center}+
−
  @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care+
−
  about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,+
−
  but we do care about the information that there are as many @{text+
−
  "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if+
−
  we represent the @{text "\<LET>"}-constructor by something like+
−
  %+
−
  \begin{center}+
−
  @{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}+
−
  become bound in @{text s}. In this representation the term +
−
  \mbox{@{text "\<LET> [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal+
−
  instance. To exclude such terms, additional predicates about well-formed+
−
  terms are 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}+
−
  @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ +
−
              & @{text "|"}    & @{text "\<LET> a::assn s::trm"}\hspace{4mm} +
−
                                 \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm]+
−
  @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\+
−
               & @{text "|"}   & @{text "\<ACONS> name trm assn"}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where @{text assn} is an auxiliary type representing a list of assignments+
−
  and @{text bn} an auxiliary function identifying the variables to be bound+
−
  by the @{text "\<LET>"}. This function is defined by recursion over @{text+
−
  assn} as follows+
−
+
−
  \begin{center}+
−
  @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} +
−
  @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} +
−
  \end{center}+
−
  +
−
  \noindent+
−
  The scope of the binding is indicated by labels given to the types, for+
−
  example @{text "s::trm"}, and a binding clause, in this case+
−
  \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states+
−
  to bind in @{text s} all the names the function call @{text "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 lets the user to specify ``empty'' +
−
  types like+
−
+
−
  \begin{center}+
−
  @{text "t ::= t t | \<lambda>x. t"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  where no clause for variables is given. Arguably, such specifications make+
−
  some sense in the context of Coq's type theory (which Ott supports), but not+
−
  at all in a HOL-based environment 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}+
−
  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x,z}. x \<rightarrow> y"} +
−
  \end{center}+
−
  +
−
  \noindent+
−
  are not just alpha-equal, but actually \emph{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 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 can be 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-equivalence is+
−
  indeed an equivalence relation).+
−
+
−
  The fact that we obtain an isomorphism 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 for terms using the+
−
  locally nameless representation of binders \cite{McKinnaPollack99}: in this+
−
  representation 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} for the HOL4 system. 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 raw lambda-terms+
−
+
−
  \begin{center}+
−
  @{text "fv(x) = {x}"}\hspace{10mm}+
−
  @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]+
−
  @{text "fv(\<lambda>x.t) = fv(t) - {x}"}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}+
−
  operating on quotients, or alpha-equivalence classes of lambda-terms. This+
−
  lifted function is characterised by the equations+
−
+
−
  \begin{center}+
−
  @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}+
−
  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]+
−
  @{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<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-equivalence is indeed an equivalence relation, and the lifted+
−
  definitions and theorems are respectful w.r.t.~alpha-equivalence.  Accordingly, we+
−
  will not be able to lift a bound-variable function to alpha-equated terms+
−
  (since it does not respect alpha-equivalence). To sum up, every lifting of+
−
  theorems to the quotient level needs proofs of some respectfulness+
−
  properties. In the paper we show that we are able to automate these+
−
  proofs and therefore can establish a reasoning infrastructure for+
−
  alpha-equated 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{Pitts04}. 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 are also able to derive, at the moment +
−
  only manually, strong induction principles that +
−
  have 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 one 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> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+
−
+
−
  \noindent +
−
  in which the generic type @{text "\<beta>"} stands 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}). Concrete  permutations are build up from +
−
  swappings, written as @{text "(a b)"},+
−
  which are permutations that behave as follows:+
−
  %+
−
  @{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}+
−
  +
−
+
−
  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\label{sec: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 specification (remember that Nominal Isabelle is a definitional+
−
  extension of Isabelle/HOL, which does not introduce any new axioms).+
−
+
−
  In order to keep our work with deriving the reasoning infrastructure+
−
  manageable, we will wherever possible state definitions and perform proofs+
−
  on the user-level of Isabelle/HOL, as opposed to write custom ML-code that+
−
  generates them anew for each specification. To that end, we will consider+
−
  first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs+
−
  are intended to represent the abstraction, or binding, of the set @{text+
−
  "as"} in the body @{text "x"}.+
−
+
−
  The first question we have to answer is when the pairs @{text "(as, x)"} and+
−
  @{text "(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 @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom+
−
  set"}}, then @{text x} and @{text y} need to have the same set of free+
−
  variables; moreover there must be a permutation @{text p} such that {\it+
−
  ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but+
−
  {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,+
−
  say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that+
−
  @{text p} makes the abstracted sets @{text as} and @{text 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}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\+
−
               & @{term "fv(x) - as = fv(y) - bs"}\\+
−
  @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\+
−
  @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\+
−
  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\ +
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  Note that this relation is dependent on the permutation @{text+
−
  "p"}. Alpha-equivalence between two pairs is then the relation where we+
−
  existentially quantify over this @{text "p"}. Also note that the relation is+
−
  dependent on a free-variable function @{text "fv"} and a relation @{text+
−
  "R"}. The reason for this extra generality is that we will use+
−
  $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In+
−
  the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we+
−
  will prove that @{text "fv"} is equal to the support of @{text+
−
  x} and @{text y}.+
−
+
−
  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}{@{term "(as, x) \<approx>lst R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]+
−
             & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\+
−
  \wedge     & @{term "(fv(x) - set as) \<sharp>* p"}\\+
−
  \wedge     & @{text "(p \<bullet> x) R y"}\\+
−
  \wedge     & @{term "(p \<bullet> as) = bs"}\\ +
−
  \end{array}+
−
  \end{equation}+
−
  +
−
  \noindent+
−
  where @{term set} is a function that coerces a list of atoms into a set of atoms.+
−
  Now the last clause ensures that the order of the binders matters.+
−
+
−
  If we do not want to make any difference between the order of binders \emph{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}{@{term "(as, x) \<approx>res R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]+
−
             & @{term "fv(x) - as = fv(y) - bs"}\\+
−
  \wedge     & @{term "(fv(x) - as) \<sharp>* 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 @{text R} to be the equality and for @{text "fv(T)"} we define+
−
+
−
  \begin{center}+
−
  @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>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_{\textit{set}}$ and+
−
  $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>+
−
  y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}+
−
  $\not\approx_{\textit{list}}$ @{text "([y,x], x \<rightarrow> y)"} since there is no permutation+
−
  that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also+
−
  leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is+
−
  @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by +
−
  taking @{text p} to be the+
−
  identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}+
−
  $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation +
−
  that makes the+
−
  sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$).+
−
  \end{exmple}+
−
+
−
  % looks too ugly+
−
  %\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}+
−
+
−
+
−
  In the rest of this section we are going to introduce a type- and term-constructor +
−
  for abstractions. For this we define +
−
  %+
−
  \begin{equation}+
−
  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}+
−
  \end{equation}+
−
  +
−
  \noindent+
−
  Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these +
−
  relations are equivalence relations and equivariant +
−
  (we only show the $\approx_{\textit{abs\_set}}$-case).+
−
+
−
  \begin{lemma}+
−
  $\approx_{\textit{abs\_set}}$ is an equivalence+
−
  relations, and if @{term "abs_set (as, x) (bs, x)"} then also+
−
  @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have+
−
  a permutation @{text p} and for the proof obligation take @{term "-p"}. In case +
−
  of transitivity we have two permutations @{text p} and @{text q}, and for the+
−
  proof obligation use @{text "q + p"}. All the conditions are then by simple+
−
  calculations. +
−
  \end{proof}+
−
+
−
  \noindent+
−
  The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and +
−
  $\approx_{\textit{abs\_res}}$) will be crucial below: +
−
+
−
  \begin{lemma}+
−
  @{thm[mode=IfThen] alpha_abs_swap[no_vars]}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  This lemma is straightforward by observing that the assumptions give us+
−
  @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}+
−
  is equivariant.+
−
  \end{proof}+
−
+
−
  \noindent +
−
  We are also define the following  +
−
+
−
  @{text "aux (as, x) \<equiv> supp x - as"}+
−
+
−
  +
−
+
−
  \noindent+
−
  This allows us to use our quotient package and introduce new types+
−
  @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}+
−
  representing the alpha-equivalence classes. Elements in these types +
−
  we will, respectively, write as:+
−
+
−
  \begin{center}+
−
  @{term "Abs as x"} \hspace{5mm} +
−
  @{term "Abs_lst as x"} \hspace{5mm}+
−
  @{term "Abs_res as x"}+
−
  \end{center}+
−
+
−
+
−
  \begin{lemma}+
−
  $supp ([as]set. x) = supp x - as$ +
−
  \end{lemma}+
−
*}+
−
+
−
section {* Alpha-Equivalence and Free Variables *}+
−
+
−
text {*+
−
  Our specifications for term-calculi are heavily inspired by the existing+
−
  datatype package of Isabelle/HOL and by the syntax of the Ott-tool+
−
  \cite{ott-jfp}. A specification is a collection of (possibly mutual+
−
  recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots, +
−
  @{text ty}$^\alpha_n$, and an associated collection+
−
  of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text+
−
  bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is+
−
  rougly as follows:+
−
  %+
−
  \begin{equation}\label{scheme}+
−
  \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}+
−
  type \mbox{declaration part} &+
−
  $\begin{cases}+
−
  \mbox{\begin{tabular}{l}+
−
  \isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\+
−
  \isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\+
−
  $\ldots$\\ +
−
  \isacommand{and} @{text ty}$^\alpha_n = \ldots$\\ +
−
  \end{tabular}}+
−
  \end{cases}$\\+
−
  binding \mbox{function part} &+
−
  $\begin{cases}+
−
  \mbox{\begin{tabular}{l}+
−
  \isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\+
−
  \isacommand{where}\\+
−
  $\ldots$\\+
−
  \end{tabular}}+
−
  \end{cases}$\\+
−
  \end{tabular}}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of +
−
  term-constructors, each of which comes with a list of labelled +
−
  types that stand for the types of the arguments of the term-constructor.+
−
  For example a term-constructor @{text "C\<^sup>\<alpha>"} might have+
−
+
−
  \begin{center}+
−
  @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} +
−
  \end{center}+
−
  +
−
  \noindent+
−
  whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained in the collection+
−
  of @{text ty}$^\alpha_{1..n}$ declared in \eqref{scheme}. In this case we will call the+
−
  corresponding argument a \emph{recursive argument}.  The labels annotated on+
−
  the types are optional and can be used in the (possibly empty) list of+
−
  \emph{binding clauses}.  These clauses indicate the binders and their scope of+
−
  in a term-constructor.  They come in three \emph{modes}:+
−
+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\+
−
  \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\+
−
  \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The first mode is for binding lists of atoms (the order of binders matters); the second is for sets+
−
  of binders (the order does not matter, but the cardinality does) and the last is for  +
−
  sets of binders (with vacuous binders preserving alpha-equivalence).+
−
+
−
  In addition we distinguish between \emph{shallow} binders and \emph{deep}+
−
  binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;+
−
  \isacommand{in}\; {\it label'} (similar for the other two modes). The+
−
  restriction we impose on shallow binders is that the {\it label} must either+
−
  refer to a type that is an atom type or to a type that is a finite set or+
−
  list of an atom type. Two examples for the use of shallow binders are the+
−
  specification of lambda-terms, where a single name is bound, and of+
−
  type-schemes, where a finite set of names is bound:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{@ {}cc@ {}}+
−
  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}+
−
  \isacommand{nominal\_datatype} {\it lam} =\\+
−
  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\+
−
  \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\+
−
  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\+
−
  \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\+
−
  \end{tabular} &+
−
  \begin{tabular}{@ {}l@ {}}+
−
  \isacommand{nominal\_datatype} {\it ty} =\\+
−
  \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\+
−
  \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\+
−
  \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\+
−
  \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\+
−
  \end{tabular}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  Note that in this specification \emph{name} refers to an atom type.+
−
  If we have shallow binders that ``share'' a body, for instance $t$ in+
−
  the following term-constructor+
−
+
−
  \begin{center}+
−
  \begin{tabular}{ll}+
−
  \it {\rm Foo} x::name y::name t::lam & \it +
−
                              \isacommand{bind}\;x\;\isacommand{in}\;t,\;+
−
                              \isacommand{bind}\;y\;\isacommand{in}\;t  +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  then we have to make sure the modes of the binders agree. We cannot+
−
  have, for instance, in the first binding clause the mode \isacommand{bind} +
−
  and in the second \isacommand{bind\_set}.+
−
+
−
  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out+
−
  the atoms in one argument of the term-constructor, which can be bound in  +
−
  other arguments and also in the same argument (we will+
−
  call such binders \emph{recursive}, see below). +
−
  The binding functions are expected to return either a set of atoms+
−
  (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms+
−
  (for \isacommand{bind}). They can be defined by primitive recursion over the+
−
  corresponding type; the equations must be given in the binding function part of+
−
  the scheme shown in \eqref{scheme}. For example for a calculus containing lets +
−
  with tuple patterns, you might specify+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  \isacommand{nominal\_datatype} {\it trm} =\\+
−
  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\+
−
  \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\+
−
  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} +
−
     \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\+
−
  \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} +
−
     \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\+
−
  \isacommand{and} {\it pat} =\\+
−
  \hspace{5mm}\phantom{$\mid$} PNil\\+
−
  \hspace{5mm}$\mid$ PVar\;{\it name}\\+
−
  \hspace{5mm}$\mid$ PTup\;{\it pat}\;{\it pat}\\ +
−
  \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\+
−
  \isacommand{where} $\textit{bn}(\textrm{PNil}) = []$\\+
−
  \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PVar}\;x) = [\textit{atom}\; x]$\\+
−
  \hspace{5mm}$\mid$ $\textit{bn}(\textrm{PTup}\;p_1\;p_2) = \textit{bn}(p_1)\; @\;\textit{bn}(p_2)$\\ +
−
  \end{tabular}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  In this specification the function @{text "bn"} determines which atoms of @{text  p} are+
−
  bound in the argument @{text "t"}. Note that the second last clause the function @{text "atom"}+
−
  coerces a name into the generic atom type of Nominal Isabelle. This allows+
−
  us to treat binders of different atom type uniformly. +
−
+
−
  As will shortly become clear, we cannot return an atom in a binding function+
−
  that is also bound in the corresponding term-constructor. That means in the+
−
  example above that the term-constructors PVar and PTup must not have a+
−
  binding clause.  In the present version of Nominal Isabelle, we also adopted+
−
  the restriction from the Ott-tool that binding functions can only return:+
−
  the empty set or empty list (as in case PNil), a singleton set or singleton+
−
  list containing an atom (case PVar), or unions of atom sets or appended atom+
−
  lists (case PTup). This restriction will simplify proofs later on.+
−
  The the most drastic restriction we have to impose on deep binders is that +
−
  we cannot have ``overlapping'' deep binders. Consider for example the +
−
  term-constructors:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{ll}+
−
  \it {\rm Foo} p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;+
−
                              \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\+
−
  \it {\rm Foo}$'$x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\;+
−
                              \isacommand{bind}\;bn(p)\;\isacommand{in}\;t +
−
  +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  In the first case we bind all atoms from the pattern @{text p} in @{text t}+
−
  and also all atoms from @{text q} in @{text t}. As a result we have no way+
−
  to determine whether the binder came from the binding function @{text+
−
  "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder+
−
  @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why+
−
  we must exclude such specifiactions is that they cannot be represent by+
−
  the general binders described in Section \ref{sec:binders}. However+
−
  the following two term-constructors are allowed+
−
+
−
  \begin{center}+
−
  \begin{tabular}{ll}+
−
  \it {\rm Bar} p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\;+
−
                                            \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\+
−
  \it {\rm Bar}$'$p::pat t::trm &  \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\;+
−
                                      \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  since there is no overlap of binders.+
−
  +
−
  Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.+
−
  Whenver such a binding clause is present, we will call the binder \emph{recursive}.+
−
  To see the purpose for this, consider ``plain'' Lets and Let\_recs:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{@ {}l@ {}}+
−
  \isacommand{nominal\_datatype} {\it trm} =\\+
−
  \hspace{5mm}\phantom{$\mid$}\ldots\\+
−
  \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} +
−
     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\+
−
  \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm} +
−
     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},+
−
         \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\+
−
  \isacommand{and} {\it assn} =\\+
−
  \hspace{5mm}\phantom{$\mid$} ANil\\+
−
  \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\+
−
  \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\+
−
  \isacommand{where} $bn(\textrm{ANil}) = []$\\+
−
  \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The difference is that with Let we only want to bind the atoms @{text+
−
  "bn(a)"} in the term @{text t}, but with Let\_rec we also want to bind the atoms+
−
  inside the assignment. This requires recursive binders and also has+
−
  consequences for the free variable function and alpha-equivalence relation,+
−
  which we are going to explain in the rest of this section.+
−
 +
−
  Having dealt with all syntax matters, the problem now is how we can turn+
−
  specifications into actual type definitions in Isabelle/HOL and then+
−
  establish a reasoning infrastructure for them. Because of the problem+
−
  Pottier and Cheney pointed out, we cannot in general re-arrange arguments of+
−
  term-constructors so that binders and their bodies are next to each other, and+
−
  then use the type constructors @{text "abs_set"}, @{text "abs_res"} and+
−
  @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first+
−
  extract datatype definitions from the specification and then define an+
−
  alpha-equiavlence relation over them.+
−
+
−
+
−
  The datatype definition can be obtained by just stripping off the +
−
  binding clauses and the labels on the types. We also have to invent+
−
  new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}+
−
  given by user. In our implementation we just use an affix like+
−
+
−
  \begin{center}+
−
  @{text "ty\<^sup>\<alpha> \<mapsto> ty_raw"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C_raw"}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are +
−
  non-empty and the types in the constructors only occur in positive +
−
  position (see \cite{} for an indepth explanataion of the datatype package+
−
  in Isabelle/HOL). We then define the user-specified binding +
−
  functions by primitive recursion over the raw datatypes. We can also+
−
  easily define a permutation operation by primitive recursion so that for each+
−
  term constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"} we have that+
−
+
−
  \begin{center}+
−
  @{text "p \<bullet> (C_raw x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C_raw (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  From this definition we can easily show that the raw datatypes are +
−
  all permutation types (Def ??) by a simple structural induction over+
−
  the @{text "ty_raw"}s.+
−
+
−
  The first non-trivial step we have to perform is the generatation free-variable +
−
  functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}+
−
  we need to define the free-variable functions+
−
+
−
  \begin{center}+
−
  @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define +
−
  the free-variable functions+
−
+
−
  \begin{center}+
−
  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The basic idea behind these free-variable functions is to collect all atoms+
−
  that are not bound in a term constructor, but because of the rather+
−
  complicated binding mechanisms the details are somewhat involved. +
−
+
−
  Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with +
−
  some  binding clauses, the function @{text "fv_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n)"} will be +
−
  the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}. +
−
  From the binding clause of this term constructor, we can determine whether the +
−
  argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also +
−
  whether it is a recursive or non-recursive of a binder. In these cases the value is: +
−
+
−
  \begin{center}+
−
  \begin{tabular}{cp{7cm}}+
−
  $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\+
−
  $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\+
−
  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of+
−
  one or more abstractions. There are two cases: either the +
−
  corresponding binders are all shallow or there is a single deep binder. +
−
  In the former case we build the union of all shallow binders; in the +
−
  later case we just take set or list of atoms the specified binding+
−
  function returns. Let @{text "bnds"} be an abbreviation of the bound+
−
  atoms. Then the value is given by:  +
−
 +
−
  \begin{center}+
−
  \begin{tabular}{cp{7cm}}+
−
  $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\+
−
  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\+
−
  $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\+
−
  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\+
−
  $\bullet$ & @{term "{}"} otherwise +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  If the argument is neither a binder, nor a body of an abstraction, then the +
−
  value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms+
−
  are abstracted.+
−
+
−
  TODO+
−
+
−
  Given a clause of a binding function of the form +
−
+
−
  \begin{center}+
−
  @{text "bn_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the+
−
  union of the values calculated for the @{text "x\<^isub>j"} as follows:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{cp{7cm}}+
−
  $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\+
−
  $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} +
−
    with the recursive call @{text "bn_ty x\<^isub>j"}\\+
−
  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\+
−
  $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\+
−
  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\+
−
  $\bullet$ & @{term "{}"} otherwise +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
*}+
−
+
−
section {* The Lifting of Definitions and Properties *} +
−
+
−
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+
−
(*>*)+
−