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 =)" 

  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>._") 

  @{text "t ::= x | t t | \<lambda>x. t"}

  derives automatically a reasoning infrastructure that has been used

  @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}

  @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}

  @{text "\<forall>{x,y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y,x}. y \<rightarrow> x"} 

  but assuming that @{text x}, @{text y} and @{text z} are distinct variables,

  @{text "\<forall>{x,y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 

  Moreover, we like to regard type-schemes as alpha-equivalent, if they differ

  only on \emph{vacuous} binders, such as

  @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x,z}. x \<rightarrow> y"}

  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

  @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}

  @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}

  research. For example in @{text "\<LET>"}s containing patterns

  @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}

  @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}

  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

  @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}

  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

  @{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}

  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

  @{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"}

  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

  @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} 

  @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 

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

  @{text "t ::= t t | \<lambda>x. t"}

  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x,z}. x \<rightarrow> y"} 

  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:

  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

  @{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}"}

  then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}

  @{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}"}

  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:

  \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"}\\ 

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

  \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     & @{term "(p \<bullet> as) = bs"}\\