(*<*)
theory Paper
imports "../Nominal/Nominal2_Base" 
        "../Nominal/Atoms" 
        "../Nominal/Nominal2_Abs"
        "~~/src/HOL/Library/LaTeXsugar"
begin

abbreviation
 UNIV_atom ("\<allatoms>")
where
 "UNIV_atom \<equiv> UNIV::atom set" 

notation (latex output)
  sort_of ("sort _" [1000] 100) and
  Abs_perm ("_") and
  Rep_perm ("_") and
  swap ("'(_ _')" [1000, 1000] 1000) and
  fresh ("_ # _" [51, 51] 50) and
  fresh_star ("_ #\<^sup>* _" [51, 51] 50) and
  Cons ("_::_" [78,77] 73) and
  supp ("supp _" [78] 73) and
  uminus ("-_" [78] 73) and
  atom ("|_|") and
  If  ("if _ then _ else _" 10) and
  Rep_name ("\<lfloor>_\<rfloor>") and
  Abs_name ("\<lceil>_\<rceil>") and
  Rep_var ("\<lfloor>_\<rfloor>") and
  Abs_var ("\<lceil>_\<rceil>") and
  sort_of_ty ("sort'_ty _") 

(* BH: uncomment if you really prefer the dot notation
syntax (latex output)
  "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")
*)

(* sort is used in Lists for sorting *)
hide_const sort

abbreviation
  "sort \<equiv> sort_of"

lemma infinite_collect:
  assumes "\<forall>x \<in> S. P x" "infinite S"
  shows "infinite {x \<in> S. P x}"
using assms
apply(subgoal_tac "infinite {x. x \<in> S}")
apply(simp only: Inf_many_def[symmetric])
apply(erule INFM_mono)
apply(auto)
done


(*>*)

section {* Introduction *}

text {*
  Nominal Isabelle provides a proving infratructure for convenient reasoning
  about syntax involving binders, such as lambda terms or type schemes in Mini-ML:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} 
  \end{isabelle}
  
  \noindent
  At its core Nominal Isabelle is based on the nominal logic work by
  Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is
  a sort-respecting permutation operation defined over a countably
  infinite collection of sorted atoms. 



  The aim of this paper is to
  describe how we adapted this work so that it can be implemented in a
  theorem prover based on Higher-Order Logic (HOL). For this we
  present the definition we made in the implementation and also review
  many proofs. There are a two main design choices to be made. One is
  how to represent sorted atoms. We opt here for a single unified atom
  type to represent atoms of different sorts. The other is how to
  present sort-respecting permutations. For them we use the standard
  technique of HOL-formalisations of introducing an appropriate
  substype of functions from atoms to atoms.

  The nominal logic work has been the starting point for a number of proving
  infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
  Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban
  and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very
  general notion, called \emph{support}, for the `set of free variables, or
  atoms, of an object' that applies not just to lambda terms and type schemes,
  but also to sets, products, lists, booleans and even functions. The notion of support
  is derived from the permutation operation defined over the 
  hierarchy of types. This
  permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more
  convenient for reasoning about syntax, in comparison to, say, arbitrary
  renaming substitutions of atoms. One reason is that permutations are
  bijective renamings of atoms and thus they can be easily `undone'---namely
  by applying the inverse permutation. A corresponding inverse substitution 
  might not always exist, since renaming substitutions are in general only injective.  
  Another reason is that permutations preserve many constructions when reasoning about syntax. 
  For example, suppose a typing context @{text "\<Gamma>"} of the form

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}
  \end{isabelle}

  \noindent
  is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}
  occur twice. Then validity of typing contexts is preserved under
  permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for
  all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary
  renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. 

  Permutations also behave uniformly with respect to HOL's logic connectives. 
  Applying a permutation to a formula gives, for example 
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}lcl}
  @{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
  @{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
  \end{tabular}
  \end{isabelle}

  \noindent
  This uniform behaviour can also be extended to quantifiers and functions. 
  Because of these good properties of permutations, we are able to automate 
  reasoning to do with \emph{equivariance}. By equivariance we mean the property 
  that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}
  for all @{text "\<pi>"}. This will often simplify arguments involving support 
  of functions, since if they are equivariant then they have empty support---or
  `no free atoms'.

  There are a number of subtle differences between the nominal logic work by
  Pitts and the formalisation we will present in this paper. One difference 
  is that our
  formalisation is compatible with HOL, in the sense that we only extend
  HOL by some definitions, withouth the introduction of any new axioms.
  The reason why the original nominal logic work is
  incompatible with HOL has to do with the way how the finite support property
  is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set
  in the FM-set-universe has finite support.  In nominal logic \cite{Pitts03},
  the axioms (E3) and (E4) imply that every function symbol and proposition
  has finite support. However, there are notions in HOL that do \emph{not}
  have finite support (we will give some examples).  In our formalisation, we 
  will avoid the incompatibility of the original nominal logic work by not a
  priory restricting our discourse to only finitely supported entities, rather
  we will explicitly assume this property whenever it is needed in proofs. One
  consequence is that we state our basic definitions not in terms of nominal
  sets (as done for example in \cite{Pitts06}), but in terms of the weaker
  notion of permutation types---essentially sets equipped with a ``sensible''
  notion of permutation operation.



  In the nominal logic woworkrk, the `new quantifier' plays a prominent role.
  $\new$




  Two binders

  A preliminary version 
*}

section {* Sorted Atoms and Sort-Respecting Permutations *}

text {*
  The two most basic notions in the nominal logic work are a countably
  infinite collection of sorted atoms and sort-respecting permutations
  of atoms.  The atoms are used for representing variable names that
  might be bound or free. Multiple sorts are necessary for being able
  to represent different kinds of variables. For example, in the
  language Mini-ML there are bound term variables in lambda
  abstractions and bound type variables in type schemes. In order to
  be able to separate them, each kind of variables needs to be
  represented by a different sort of atoms.


  The existing nominal logic work usually leaves implicit the sorting
  information for atoms and leaves out a description of how sorts are
  represented.  In our formalisation, we therefore have to make a
  design decision about how to implement sorted atoms and
  sort-respecting permutations. One possibility, which we described in
  \cite{Urban08}, is to have separate types for different sorts of
  atoms. However, we found that this does not blend well with
  type-classes in Isabelle/HOL (see Section~\ref{related} about
  related work).  Therefore we use here a single unified atom type to
  represent atoms of different sorts. A basic requirement is that
  there must be a countably infinite number of atoms of each sort.
  This can be implemented as the datatype

*}

          datatype atom\<iota> = Atom\<iota> string nat

text {*
  \noindent
  whereby the string argument specifies the sort of the
  atom.\footnote{A similar design choice was made by Gunter et al
  \cite{GunterOsbornPopescu09} for their variables.}  The use of type
  \emph{string} for sorts is merely for convenience; any countably
  infinite type would work as well.  In what follows we shall write
  @{term "UNIV::atom set"} for the set of all atoms.  We also have two
  auxiliary functions for atoms, namely @{text sort} and @{const
  nat_of} which are defined as

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  @{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\
  @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"}  & @{thm (rhs) nat_of.simps[no_vars]}
  \end{tabular}\hfill\numbered{sortnatof}
  \end{isabelle}

  \noindent
  We clearly have for every finite set @{text S}
  of atoms and every sort @{text s} the property:

  \begin{proposition}\label{choosefresh}\mbox{}\\
  @{text "For a finite set of atoms S, there exists an atom a such that
  sort a = s and a \<notin> S"}.
  \end{proposition}

  For implementing sort-respecting permutations, we use functions of type @{typ
  "atom => atom"} that are bijective; are the
  identity on all atoms, except a finite number of them; and map
  each atom to one of the same sort. These properties can be conveniently stated
  in Isabelle/HOL for a function @{text \<pi>} as follows:
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{r@ {\hspace{4mm}}l}
  i)   & @{term "bij \<pi>"}\\
  ii)  & @{term "finite {a. \<pi> a \<noteq> a}"}\\
  iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}
  \end{tabular}\hfill\numbered{permtype}
  \end{isabelle}

  \noindent
  Like all HOL-based theorem provers, Isabelle/HOL allows us to
  introduce a new type @{typ perm} that includes just those functions
  satisfying all three properties. For example the identity function,
  written @{term id}, is included in @{typ perm}. Also function composition, 
  written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's 
  inverse operator and written \mbox{@{text "inv _"}}, preserve the properties 
  (\ref{permtype}.@{text "i"}-@{text "iii"}). 

  However, a moment of thought is needed about how to construct non-trivial
  permutations. In the nominal logic work it turned out to be most convenient
  to work with swappings, written @{text "(a b)"}.  In our setting the
  type of swappings must be

  @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}

  \noindent
  but since permutations are required to respect sorts, we must carefully
  consider what happens if a user states a swapping of atoms with different
  sorts.  The following definition\footnote{To increase legibility, we omit
  here and in what follows the @{term Rep_perm} and @{term "Abs_perm"}
  wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation
  not to be the full function space, but only those functions of type @{typ
  perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.}


  @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}

  \noindent
  does not work in general, because @{text a} and @{text b} may have different
  sorts---in which case the function would violate property @{text iii} in \eqref{permtype}.  We
  could make the definition of swappings partial by adding the precondition
  @{term "sort a = sort b"}, which would mean that in case @{text a} and
  @{text b} have different sorts, the value of @{text "(a b)"} is unspecified.
  However, this looked like a cumbersome solution, since sort-related side
  conditions would be required everywhere, even to unfold the definition.  It
  turned out to be more convenient to actually allow the user to state
  `ill-sorted' swappings but limit their `damage' by defaulting to the
  identity permutation in the ill-sorted case:


  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}rl}
  @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ 
   & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ 
   & \hspace{3mm}@{text "else id"}
  \end{tabular}\hfill\numbered{swapdef}
  \end{isabelle}

  \noindent
  This function is bijective, the identity on all atoms except
  @{text a} and @{text b}, and sort respecting. Therefore it is 
  a function in @{typ perm}. 

  One advantage of using functions as a representation for
  permutations is that it is unique. For example the swappings

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm swap_commute[no_vars]}\hspace{10mm}
  @{text "(a a) = id"}
  \end{tabular}\hfill\numbered{swapeqs}
  \end{isabelle}

  \noindent
  are \emph{equal} and can be used interchangeably. Another advantage of the function 
  representation is that they form a (non-com\-mu\-ta\-tive) group provided we define

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  @{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} &
  @{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & 
     @{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\
  @{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} &
  @{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &
     @{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
  \end{tabular}\hfill\numbered{groupprops}
  \end{isabelle}

  \noindent
  and verify the four simple properties

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
  ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
  iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
  iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
  \end{tabular}\hfill\numbered{grouplaws}
  \end{isabelle}

  \noindent
  The technical importance of this fact is that we can rely on
  Isabelle/HOL's existing simplification infrastructure for groups, which will
  come in handy when we have to do calculations with permutations.
  Note that Isabelle/HOL defies standard conventions of mathematical notation
  by using additive syntax even for non-commutative groups.  Obviously,
  composition of permutations is not commutative in general; for example

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.
  \end{isabelle} 

  \noindent
  But since the point of this paper is to implement the
  nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
  the non-standard notation in order to reuse the existing libraries.

  A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},
  applies a permutation @{text "\<pi>"} to an object @{text "x"}.  This 
  operation has the type

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
  \end{isabelle} 

  \noindent
  whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be 
  given by in terms of `induction' over this generic type. The type-class mechanism
  of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for
  `base' types, such as atoms, permutations, booleans and natural numbers:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
  booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  \end{tabular}\hfill\numbered{permdefsbase}
  \end{isabelle}

  \noindent
  and for type-constructors, such as functions, sets, lists and products:
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
         & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  \end{tabular}\hfill\numbered{permdefsconstrs}
  \end{isabelle}

  \noindent
  The type classes also allow us to reason abstractly about the permutation operation. 
  For this we state the following two 
  \emph{permutation properties}: 
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
  i) & @{thm permute_zero[no_vars]}\\
  ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}
  \end{tabular}\hfill\numbered{newpermprops}
  \end{isabelle} 

  \noindent
  From these properties and law (\ref{grouplaws}.{\it iv}) about groups 
  follows that a permutation and its inverse cancel each other. That is

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}
  @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}
  \end{tabular}\hfill\numbered{cancel}
  \end{isabelle} 
  
  \noindent
  Consequently, the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 
  which in turn implies the property

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}
  $\;$if and only if$\;$
  @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.
  \end{tabular}\hfill\numbered{permuteequ}
  \end{isabelle} 

  \noindent
  We can also show that the following property holds for the permutation 
  operation.

  \begin{lemma}\label{permutecompose} 
  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
  \end{lemma}

  \begin{proof} The proof is as follows:
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
  & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\
  @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
  @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
  @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
  \end{tabular}\hfill\qed
  \end{isabelle}
  \end{proof}

  \noindent
  Note that the permutation operation for functions is defined so that
  we have for applications the property

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "\<pi> \<bullet> (f x) ="}
  @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
  \hfill\numbered{permutefunapp}
  \end{isabelle}

  \noindent
  whenever the permutation properties hold for @{text x}. This property can
  be easily shown by unfolding the permutation operation for functions on
  the right-hand side, simplifying the beta-redex and eliminating the permutations
  in front of @{text x} using \eqref{cancel}.

  The main benefit of the use of type classes is that it allows us to delegate 
  much of the routine resoning involved in determining whether the permutation properties
  are satisfied to Isabelle/HOL's type system: we only have to
  establish that base types satisfy them and that type-constructors
  preserve them. Isabelle/HOL will use this information and determine
  whether an object @{text x} with a compound type satisfies the
  permutation properties.  For this we define the notion of a
  \emph{permutation type}:

  \begin{definition}[Permutation type]
  A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
  properties in \eqref{newpermprops} are satisfied for every @{text
  "x"} of type @{text "\<beta>"}.
  \end{definition}
 
  \noindent
  and establish:

  \begin{theorem}
  The types @{type atom}, @{type perm}, @{type bool} and @{type nat}
  are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text
  "\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}},
  @{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}.
  \end{theorem}

  \begin{proof}
  All statements are by unfolding the definitions of the permutation
  operations and simple calculations involving addition and
  minus. In case of permutations for example we have

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}[b]{@ {}rcl}
  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\
  @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
  & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\
  & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 
  \end{tabular}\hfill\qed
  \end{isabelle}
  \end{proof}
*}

section {* Equivariance *}

text {*
  An important notion in the nominal logic work is
  \emph{equivariance}.  It will enable us to characterise how
  permutations act upon compound statements in HOL by analysing how
  these statements are constructed.  To do so, let us first define
  \emph{HOL-terms}. They are given by the grammar

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
  \hfill\numbered{holterms}
  \end{isabelle} 

  \noindent
  where @{text c} stands for constants and @{text x} for
  variables. 
  We assume HOL-terms are fully typed, but for the sake of
  greater legibility we leave the typing information implicit.  We
  also assume the usual notions for free and bound variables of a
  HOL-term.  Furthermore, it is custom in HOL to regard terms as equal
  modulo alpha-, beta- and eta-equivalence.

  An \emph{equivariant} HOL-term is one that is invariant under the
  permutation operation. This can be defined in Isabelle/HOL 
  as follows:

  \begin{definition}[Equivariance]\label{equivariance}
  A  HOL-term @{text t} is \emph{equivariant} provided 
  @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.
  \end{definition}

  \noindent
  In what follows we will primarily be interested in the cases where @{text t} 
  is a constant, but of course there is no way in Isabelle/HOL to restrict 
  this definition to just these cases.

  There are a number of equivalent formulations for the equivariance
  property.  For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
  \<beta>"}, then equivariance can also be stated as

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "\<forall>\<pi> x.  \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"}
  \end{tabular}\hfill\numbered{altequivariance}
  \end{isabelle} 

  \noindent
  We will call this formulation of equivariance in \emph{fully applied form}.
  To see that this formulation implies the definition, we just unfold
  the definition of the permutation operation for functions and
  simplify with the equation and the cancellation property shown in
  \eqref{cancel}. To see the other direction, we use
  \eqref{permutefunapp}. Similarly for HOL-terms that take more than
  one argument. The point to note is that equivariance and equivariance in fully
  applied form are (for permutation types) always interderivable.

  Both formulations of equivariance have their advantages and
  disadvantages: \eqref{altequivariance} is usually more convenient to
  establish, since statements in Isabelle/HOL are commonly given in a
  form where functions are fully applied. For example we can easily
  show that equality is equivariant

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm eq_eqvt[where p="\<pi>", no_vars]}
  \end{tabular}\hfill\numbered{eqeqvt}
  \end{isabelle} 

  \noindent
  using the permutation operation on booleans and property
  \eqref{permuteequ}. 
  Lemma~\ref{permutecompose} establishes that the
  permutation operation is equivariant. The permutation operation for
  lists and products, shown in \eqref{permdefsconstrs}, state that the
  constructors for products, @{text "Nil"} and @{text Cons} are
  equivariant. Furthermore a simple calculation will show that our
  swapping functions are equivariant, that is

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm swap_eqvt[where p="\<pi>", no_vars]}
  \end{tabular}\hfill\numbered{swapeqvt}
  \end{isabelle} 

  \noindent
  for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans
  @{const True} and @{const False} are equivariant by the definition
  of the permutation operation for booleans. It is easy to see
  that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
  "\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}lcl}
  @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
  @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
  \end{tabular}
  \end{isabelle}

  \noindent
  by the definition of the permutation operation acting on booleans.
  
  In contrast, the advantage of Definition \ref{equivariance} is that
  it leads to a relatively simple rewrite system that allows us to `push' a permutation
  towards the leaves of a HOL-term (i.e.~constants and
  variables).  Then the permutation disappears in cases where the
  constants are equivariant. We have implemented this rewrite system
  as a simplification tactic on the ML-level of Isabelle/HOL.  Having this tactic 
  at our disposal, together with a collection of constants for which 
  equivariance is already established, we can automatically establish 
  equivariance of a constant for which equivariance is not yet known. For this we only have to 
  make sure that the definiens of this constant 
  is a HOL-term whose constants are all equivariant.  In what follows 
  we shall specify this tactic and argue that it terminates and 
  is correct (in the sense of pushing a 
  permutation @{text "\<pi>"} inside a term and the only remaining 
  instances of @{text "\<pi>"} are in front of the term's free variables). 

  The simplifiaction tactic is a rewrite systems consisting of four `oriented' 
  equations. We will first give a naive version of this tactic, which however 
  is in some cornercases incorrect and does not terminate, and then modify 
  it in order to obtain the desired properties. A permutation @{text \<pi>} can 
  be pushed into applications and abstractions as follows

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\
  \end{tabular}\hfill\numbered{rewriteapplam}
  \end{isabelle}

  \noindent
  The first equation we established in \eqref{permutefunapp};
  the second follows from the definition of permutations acting on functions
  and the fact that HOL-terms are equal modulo beta-equivalence.
  Once the permutations are pushed towards the leaves we need the
  following two equations

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
  iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\
  iv) &  @{term "\<pi> \<bullet> c"} & \rrh & 
            {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\
  \end{tabular}\hfill\numbered{rewriteother}
  \end{isabelle}

  \noindent
  in order to remove permuations in front of bound variables and
  equivariant constants.  Unfortunately, we have to be careful with
  the rules {\it i)} and {\it iv}): they can lead to a loop whenever
  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note
  that we usually write this application using infix notation as
  @{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the
  constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite
  reduction sequence

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}
  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$
  @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}
  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$
  @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%
  
  \end{tabular}
  \end{isabelle}

  \noindent
  where the last step is again an instance of the first term, but it
  is bigger.  To avoid this loop we need to apply our rewrite rule
  using an `outside to inside' strategy.  This strategy is sufficient
  since we are only interested of rewriting terms of the form @{term
  "\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.

  Another problem we have to avoid is that the rules {\it i)} and
  {\it iii)} can `overlap'. For this note that
  the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to 
  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply rule {\it iii)} 
  in order to obtain @{term "\<lambda>x. x"}, as is desired---there is no 
  free variable in the original term and so the permutation should completely
  vanish. However, the subterm @{text
  "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term 
  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using
  {\it i)}.  Given our strategy we cannot apply rule {\it iii)} anymore and 
  even worse the measure we will introduce shortly increased. On the
  other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}
  where @{text \<pi>} and @{text x} are free variables, then we \emph{do}
  want to apply rule  {\it i)} and not rule {\it iii)}. The latter 
  would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}
  should only apply to instances where the variable is to bound; for free variables 
  we want to use {\it ii)}. 

  The problem is that in order to distinguish both cases when
  inductively taking a term `apart', we have to maintain the
  information which variable is bound. This, unfortunately, does not
  mesh well with the way how simplification tactics are implemented in
  Isabelle/HOL. Our remedy is to use a standard trick in HOL: we
  introduce a separate definition for terms of the form @{text "(- \<pi>)
  \<bullet> x"}, namely as

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}
  \end{isabelle}

  \noindent
  The point is that now we can formulate the rewrite rules as follows
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}lrcl}
  i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & 
    @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\
  \multicolumn{4}{r}{\rm provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\
  ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
  iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\
  iv') &  @{term "\<pi> \<bullet> c"} & \rrh & @{term "c"}
    \hspace{6mm}{\rm provided @{text c} is equivariant}\\
  \end{tabular}
  \end{isabelle}

  \noindent
  and @{text unpermutes} are only generated in case of bound variables.
  Clearly none of these rules overlap. Moreover, given our
  outside-to-inside strategy, they terminate. To see this, notice that
  the permutation on the right-hand side of the rewrite rules is
  always applied to a smaller term, provided we take the measure consisting
  of lexicographically ordered pairs whose first component is the size
  of a term (counting terms of the form @{text "unpermute \<pi> x"} as
  leaves) and the second is the number of occurences of @{text
  "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.

  With the definition of the simplification tactic in place, we can
  establish its correctness. The property we are after is that for for
  a HOL-term @{text t} whose constants are all equivariant, the
  HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}
  being equal to @{text t} except that every free variable @{text x}
  in @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls this
  property \emph{equivariance principle} (book ref ???). In our
  setting the precise statement of this property is a slightly more
  involved because of the fact that @{text unpermutes} needs to be
  treated specially.
  
  \begin{theorem}[Equivariance Principle]
  Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all
  its constants are equivariant. For any permutation @{text \<pi>}, let @{text t'} 
  be the HOL-term @{text t} except every free variable @{text x} in @{term t} is 
  replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.
  \end{theorem}
  


  With these definitions in place we can define the notion of an \emph{equivariant}
  HOL-term

  \begin{definition}[Equivariant HOL-term]
  A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, 
  abstractions and equivariant constants only.
  \end{definition}
  
  \noindent
  For equivariant terms we have

  \begin{lemma}
  For an equivariant HOL-term @{text "t"},  @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.
  \end{lemma}

  Let us now see how to use the equivariance principle. We have 

*}


section {* Support and Freshness *}

text {*
  The most original aspect of the nominal logic work of Pitts is a general
  definition for `the set of free variables, or free atoms, of an object @{text "x"}'.  This
  definition is general in the sense that it applies not only to lambda terms,
  but to any type for which a permutation operation is defined 
  (like lists, sets, functions and so on). 

  \begin{definition}[Support] Given @{text x} is of permutation type, then 
  
  @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}
  \end{definition}

  \noindent
  (Note that due to the definition of swapping in \eqref{swapdef}, we do not
  need to explicitly restrict @{text a} and @{text b} to have the same sort.)
  There is also the derived notion for when an atom @{text a} is \emph{fresh}
  for an @{text x} of permutation type, defined as
  
  @{thm [display,indent=10] fresh_def[no_vars]}

  \noindent
  We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms 
  defined as follows
  
  @{thm [display,indent=10] fresh_star_def[no_vars]}


  \noindent
  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. For the proof we use the following lemma 
  about swappings applied to an @{text x}:

  \begin{lemma}\label{swaptriple}
  Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} 
  have the same sort, then \mbox{@{thm (prem 3) swap_rel_trans[no_vars]}} and 
  @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.
  \end{lemma}

  \begin{proof}
  The cases where @{text "a = c"} and @{text "b = c"} are immediate.
  For the remaining case it is, given our assumptions, easy to calculate 
  that the permutations

  @{thm [display,indent=10] (concl) swap_triple[no_vars]}
  
  \noindent
  are equal. The lemma is then by application of the second permutation 
  property shown in~\eqref{newpermprops}.\hfill\qed
  \end{proof}

  \begin{theorem}\label{swapfreshfresh}
  Let @{text x} be of permutation type.
  @{thm [mode=IfThen] swap_fresh_fresh[no_vars]}
  \end{theorem}

  \begin{proof}
  If @{text a} and @{text b} have different sort, then the swapping is the identity.
  If they have the same sort, we know by definition of support that both
  @{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and  @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}
  hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} 
  that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, 
  that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. 
  Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed
  \end{proof}
  
  \noindent
  Two important properties that need to be established for later calculations is 
  that @{text "supp"} and freshness are equivariant. For this we first show that:

  \begin{lemma}\label{half}
  If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} 
  if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.
  \end{lemma}

  \begin{proof}
  \begin{isabelle}
  \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}
  & @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}\\ 
  @{text "\<equiv>"} & 
    @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}\\
  @{text "\<Leftrightarrow>"}
  & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} 
  & since @{text "\<pi> \<bullet> _"} is bijective\\ 
  @{text "\<Leftrightarrow>"}
  & @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}
  & by Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\
  @{text "\<Leftrightarrow>"}
  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}
  & by \eqref{permuteequ}\\
   @{text "\<equiv>"}
  & @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
  \end{tabular}
  \end{isabelle}\hfill\qed
  \end{proof}

  \noindent
  Together with the definition of the permutation operation on booleans,
  we can immediately infer equivariance of freshness: 

  @{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}

  \noindent
  Now equivariance of @{text "supp"}, namely
  
  @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}
  
  \noindent
  is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and 
  the logical connectives are equivariant. ??? Equivariance

  A simple consequence of the definition of support and equivariance is that 
  if a function @{text f} is equivariant then we have 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm  (concl) supp_fun_eqvt[no_vars]}
  \end{tabular}\hfill\numbered{suppeqvtfun}
  \end{isabelle} 

  \noindent 
  For function applications we can establish the two following properties.

  \begin{lemma} Let @{text f} and @{text x} be of permutation type, then
  \begin{isabelle}
  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
  @{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\
  @{text "ii)"} & @{thm supp_fun_app[no_vars]}\\
  \end{tabular}
  \end{isabelle}
  \end{lemma}

  \begin{proof}
  ???
  \end{proof}


  While the abstract properties of support and freshness, particularly 
  Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, 
  one often has to calculate the support of some concrete object. This is 
  straightforward for example for booleans, nats, products and lists:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
  @{text "booleans"}: & @{term "supp b = {}"}\\
  @{text "nats"}:     & @{term "supp n = {}"}\\
  @{text "products"}: & @{thm supp_Pair[no_vars]}\\
  @{text "lists:"} & @{thm supp_Nil[no_vars]}\\
                   & @{thm supp_Cons[no_vars]}\\
  \end{tabular}
  \end{isabelle}

  \noindent
  But establishing the support of atoms and permutations is a bit 
  trickier. To do so we will use the following notion about a \emph{supporting set}.
  
  \begin{definition}[Supporting Set]
  A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
  not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
  \end{definition}

  \noindent
  The main motivation for this notion is that we can characterise @{text "supp x"} 
  as the smallest finite set that supports @{text "x"}. For this we prove:

  \begin{lemma}\label{supports} Let @{text x} be of permutation type.
  \begin{isabelle}
  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
  i)    & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
  ii)   & @{thm[mode=IfThen] supp_supports[no_vars]}\\
  iii)  & @{thm (concl) supp_is_least_supports[no_vars]}
         provided @{thm (prem 1) supp_is_least_supports[no_vars]},
         @{thm (prem 2) supp_is_least_supports[no_vars]}
         and @{text "S"} is the least such set, that means formally,
         for all @{text "S'"}, if @{term "finite S'"} and 
         @{term "S' supports x"} then @{text "S \<subseteq> S'"}.
  \end{tabular}
  \end{isabelle} 
  \end{lemma}

  \begin{proof}
  For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}
  with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the 
  assumption that @{term "S supports x"} gives us that @{text S} is a superset of 
  @{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}
  being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.
  Property @{text "ii)"} is by a direct application of 
  Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves
  one ``half'' of the claimed equation. The other ``half'' is by property 
  @{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed  
  \end{proof}

  \noindent
  These are all relatively straightforward proofs adapted from the existing 
  nominal logic work. However for establishing the support of atoms and 
  permutations we found  the following `optimised' variant of @{text "iii)"} 
  more useful:

  \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
  We have that @{thm (concl) finite_supp_unique[no_vars]}
  provided @{thm (prem 1) finite_supp_unique[no_vars]},
  @{thm (prem 2) finite_supp_unique[no_vars]}, and for
  all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
  \end{lemma}

  \begin{proof}
  By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite
  set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will
  assume that there is an atom @{text "a"} that is element of @{text S}, but
  not @{text "S'"} and derive a contradiction.  Since both @{text S} and
  @{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom
  @{text b}, which has the same sort as @{text "a"} and for which we know
  @{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and
  we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x
  = x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply
  @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the
  contradiction.\hfill\qed
  \end{proof}

  \noindent
  Using this lemma we only have to show the following three proof-obligations

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{4mm}}l}
  i)   & @{term "{c} supports c"}\\
  ii)  & @{term "finite {c}"}\\
  iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}
  \end{tabular}
  \end{isabelle} 

  \noindent
  in order to establish that @{thm supp_atom[where a="c", no_vars]} holds.  In
  Isabelle/HOL these proof-obligations can be discharged by easy
  simplifications. Similar proof-obligations arise for the support of
  permutations, which is

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm supp_perm[where p="\<pi>", no_vars]}
  \end{tabular}
  \end{isabelle}

  \noindent
  The only proof-obligation that is 
  interesting is the one where we have to show that

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.
  \end{tabular}
  \end{isabelle}

  \noindent
  For this we observe that 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}rcl}
  @{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} &
  if and only if &
  @{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]}
  \end{tabular}
  \end{isabelle}

  \noindent
  holds by a simple calculation using the group properties of permutations.
  The proof-obligation can then be discharged by analysing the inequality
  between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.

  The main point about support is that whenever an object @{text x} has finite
  support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a 
  fresh atom with arbitrary sort. This is an important operation in Nominal
  Isabelle in situations where, for example, a bound variable needs to be
  renamed. To allow such a choice, we only have to assume that 
  @{text "finite (supp x)"} holds. For more convenience we
  can define a type class for types where every element has finite support, and
  prove that the types @{term "atom"}, @{term "perm"}, lists, products and
  booleans are instances of this type class. 

  Unfortunately, this does not work for sets or Isabelle/HOL's function
  type. There are functions and sets definable in Isabelle/HOL for which the
  finite support property does not hold.  A simple example of a function with
  infinite support is @{const nat_of} shown in \eqref{sortnatof}.  This
  function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. 
  To establish this we show
  @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term
  "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a
  contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons>
  b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use
  Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term
  "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of =
  nat_of"}.  Now we can reason as follows:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}
  @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\
  & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\
  & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\
  \end{tabular}
  \end{isabelle}
  
  \noindent
  But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.
  This implies that atoms @{term a} and @{term c} must be equal, which clashes with our
  assumption @{term "c \<noteq> a"} about how we chose @{text c}.\footnote{Cheney \cite{Cheney06} 
  gives similar examples for constructions that have infinite support.}
*}

section {* Support of Finite Sets *}

text {*
  Also the set type is one instance whose elements are not generally finitely 
  supported (we will give an example in Section~\ref{concrete}). 
  However, we can easily show that finite sets and co-finite sets of atoms are finitely
  supported, because their support can be characterised as:

  \begin{lemma}\label{finatomsets}\mbox{}\\
  @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\
  @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then 
  @{thm (concl) supp_cofinite_atom_set[no_vars]}.
  \end{lemma}

  \begin{proof}
  Both parts can be easily shown by Lemma~\ref{optimised}.  We only have to observe
  that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both
  @{text a} and @{text b} are elements in @{text S} or both are not in @{text S}.
  However if the sorts of a @{text a} and @{text b} agree, then the swapping will
  change @{text S} if either of them is an element in @{text S} and the other is 
  not.\hfill\qed
  \end{proof}

  \noindent
  Note that a consequence of the second part of this lemma is that 
  @{term "supp (UNIV::atom set) = {}"}.
  More difficult, however, is it to establish that finite sets of finitely 
  supported objects are finitely supported. For this we first show that
  the union of the suports of finitely many and finitely supported  objects 
  is finite, namely

  \begin{lemma}\label{unionsupp}
  If @{text S} is a finite set whose elements are all finitely supported, then\\
  @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\
  @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}.
  \end{lemma}

  \begin{proof}
  The first part is by a straightforward induction on the finiteness of @{text S}. 
  For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which
  by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"}
  that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be
  \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}.
  Since @{text "f"} is an equivariant function, we have that 
  @{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed
  \end{proof}

  \noindent
  With this lemma in place we can establish that

  \begin{lemma}
  @{thm[mode=IfThen] supp_of_finite_sets[no_vars]}
  \end{lemma}

  \begin{proof}
  The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion 
  in the other direction we have to show Lemma~\ref{supports}.@{text "i)"}
  \end{proof}
*}


section {* Induction Principles *}

text {*
  While the use of functions as permutation provides us with a unique
  representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and 
  @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has 
  one draw back: it does not come readily with an induction principle. 
  Such an induction principle is handy for deriving properties like
  
  @{thm [display, indent=10] supp_perm_eq[no_vars]}

  \noindent
  However, it is not too difficult to derive an induction principle, 
  given the fact that we allow only permutations with a finite domain. 
*}


section {* An Abstraction Type *}

text {*
  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 of atoms @{text
  "as"} in the body @{text "x"}.

  The first question we have to answer is when two pairs @{text "(as, x)"} and
  @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
  the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
  vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
  given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
  set"}}, then @{text x} and @{text y} need to have the same set of free
  atoms; moreover there must be a permutation @{text p} such that {\it
  (ii)} @{text p} leaves the free atoms 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 equivalent terms. We also require that {\it (iv)}
  @{text p} makes the sets of abstracted atoms @{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@ {\hspace{4mm}}r}
  \multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
              & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
  @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
  @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
  \end{array}
  \end{equation}

  \noindent
  Note that this relation depends 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-atom function @{text "fa"} 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, @{text R} will be replaced by equality @{text "="} and we
  will prove that @{text "fa"} is equal to @{text "supp"}.

  It might be useful to consider first some examples about how these definitions
  of $\alpha$-equivalence pan out in practice.  For this consider the case of
  abstracting a set of atoms over types (as in type-schemes). We set
  @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
  define

  \begin{center}
  @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(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 $\alpha$-equivalent 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}}$).  It can also relatively easily be
  shown that all three notions of $\alpha$-equivalence coincide, if we only
  abstract a single atom.

  In the rest of this section we are going to introduce three abstraction 
  types. For this we define 
  %
  \begin{equation}
  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
  \end{equation}
  
  \noindent
  (similarly for $\approx_{\,\textit{abs\_res}}$ 
  and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
  relations and equivariant.

  \begin{lemma}\label{alphaeq} 
  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
  "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
  bs, p \<bullet> y)"} (similarly for the other two relations).
  \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 conditions are then by simple
  calculations. 
  \end{proof}

  \noindent
  This lemma allows us to use our quotient package for introducing 
  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
  representing $\alpha$-equivalence classes of pairs of type 
  @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
  (in the third case). 
  The elements in these types will be, respectively, written as:

  \begin{center}
  @{term "Abs_set as x"} \hspace{5mm} 
  @{term "Abs_res as x"} \hspace{5mm}
  @{term "Abs_lst as x"} 
  \end{center}

  \noindent
  indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
  call the types \emph{abstraction types} and their elements
  \emph{abstractions}. The important property we need to derive is the support of 
  abstractions, namely:

  \begin{theorem}[Support of Abstractions]\label{suppabs} 
  Assuming @{text x} has finite support, then\\[-6mm] 
  \begin{center}
  \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  %@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\
  %@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\
  %@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]}
  \end{tabular}
  \end{center}
  \end{theorem}

  \noindent
  Below we will show the first equation. The others 
  follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
  we have 
  %
  \begin{equation}\label{abseqiff}
  %@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
  %@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
  \end{equation}

  \noindent
  and also
  %
  \begin{equation}\label{absperm}
  @{thm permute_Abs[no_vars]}
  \end{equation}

  \noindent
  The second fact derives from the definition of permutations acting on pairs 
  \eqref{permute} and $\alpha$-equivalence being equivariant 
  (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
  the following lemma about swapping two atoms in an abstraction.
  
  \begin{lemma}
  %@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
  \end{lemma}

  \begin{proof}
  This lemma is straightforward using \eqref{abseqiff} and observing that
  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
  Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
  \end{proof}

  \noindent
  Assuming that @{text "x"} has finite support, this lemma together 
  with \eqref{absperm} allows us to show
  %
  \begin{equation}\label{halfone}
  %@ {thm abs_supports(1)[no_vars]}
  \end{equation}
  
  \noindent
  which by Property~\ref{supportsprop} gives us ``one half'' of
  Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
  it, we use a trick from \cite{Pitts04} and first define an auxiliary 
  function @{text aux}, taking an abstraction as argument:
  %
  \begin{center}
  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
  \end{center}
  
  \noindent
  Using the second equation in \eqref{equivariance}, we can show that 
  @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
  (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. 
  This in turn means
  %
  \begin{center}
  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
  \end{center}

  \noindent
  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
  we further obtain
  %
  \begin{equation}\label{halftwo}
  %@ {thm (concl) supp_abs_subset1(1)[no_vars]}
  \end{equation}

  \noindent
  since for finite sets of atoms, @{text "bs"}, we have 
  @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
  Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
  Theorem~\ref{suppabs}. 

  The method of first considering abstractions of the
  form @{term "Abs_set as x"} etc is motivated by the fact that 
  we can conveniently establish  at the Isabelle/HOL level
  properties about them.  It would be
  laborious to write custom ML-code that derives automatically such properties 
  for every term-constructor that binds some atoms. Also the generality of
  the definitions for $\alpha$-equivalence will help us in the next section. 
*}


section {* Concrete Atom Types\label{concrete} *}

text {*

  So far, we have presented a system that uses only a single multi-sorted atom
  type.  This design gives us the flexibility to define operations and prove
  theorems that are generic with respect to atom sorts.  For example, as
  illustrated above the @{term supp} function returns a set that includes the
  free atoms of \emph{all} sorts together; the flexibility offered by the new
  atom type makes this possible.  

  However, the single multi-sorted atom type does not make an ideal interface
  for end-users of Nominal Isabelle.  If sorts are not distinguished by
  Isabelle's type system, users must reason about atom sorts manually.  That
  means subgoals involving sorts must be discharged explicitly within proof
  scripts, instead of being inferred by Isabelle/HOL's type checker.  In other
  cases, lemmas might require additional side conditions about sorts to be true.
  For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,
  b)"}} will only produce the expected result if we state the lemma in
  Isabelle/HOL as:
*}

          lemma
	    fixes a b :: "atom"
	    assumes asm: "sort a = sort b"
	    shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" 
          using asm by simp

text {*
  \noindent
  Fortunately, it is possible to regain most of the type-checking automation
  that is lost by moving to a single atom type.  We accomplish this by defining
  \emph{subtypes} of the generic atom type that only include atoms of a single
  specific sort.  We call such subtypes \emph{concrete atom types}.

  The following Isabelle/HOL command defines a concrete atom type called
  \emph{name}, which consists of atoms whose sort equals the string @{term
  "''name''"}.

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
  \end{isabelle}

  \noindent
  This command automatically generates injective functions that map from the
  concrete atom type into the generic atom type and back, called
  representation and abstraction functions, respectively. We will write these
  functions as follows:

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l@ {\hspace{10mm}}l}
  @{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & 
  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}
  \end{tabular}
  \end{isabelle}

  \noindent
  With the definition @{thm permute_name_def [where p="\<pi>", THEN
  eq_reflection, no_vars]}, it is straightforward to verify that the type 
  @{typ name} is a permutation type.

  In order to reason uniformly about arbitrary concrete atom types, we define a
  type class that characterises type @{typ name} and other similarly-defined
  types.  The definition of the concrete atom type class is as follows: First,
  every concrete atom type must be a permutation type.  In addition, the class
  defines an overloaded function that maps from the concrete type into the
  generic atom type, which we will write @{text "|_|"}.  For each class
  instance, this function must be injective and equivariant, and its outputs
  must all have the same sort, that is

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{r@ {\hspace{3mm}}l}
  i)   if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\
  ii)  @{thm atom_eqvt[where p="\<pi>", no_vars]}\\
  iii) @{thm sort_of_atom_eq [no_vars]}
  \end{tabular}\hfill\numbered{atomprops}
  \end{isabelle}

  \noindent
  With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can
  show that @{typ name} satisfies all the above requirements of a concrete atom
  type.

  The whole point of defining the concrete atom type class was to let users
  avoid explicit reasoning about sorts.  This benefit is realised by defining a
  special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>
  \<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:

  @{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]}

  \noindent
  As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping
  operation works just like the generic swapping operation, but it does not
  require any sort-checking side conditions---the sort-correctness is ensured by
  the types!  For @{text "\<leftrightarrow>"} we can establish the following
  simplification rule:

  @{thm [display,indent=10] permute_flip_at[no_vars]} 

  \noindent
  If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}
  in the pair @{term "(a, b)"} we can establish the lemma as follows:
*}

          lemma
	    fixes a b :: "name"
	    shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" 
	  by simp

text {*
  \noindent
  There is no need to state an explicit premise involving sorts.

  We can automate the process of creating concrete atom types, so that users 
  can define a new one simply by issuing the command 

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  \isacommand{atom\_decl}~~@{text "name"}
  \end{tabular}
  \end{isabelle}

  \noindent
  This command can be implemented using less than 100 lines of custom ML-code.
  In comparison, the old version of Nominal Isabelle included more than 1000
  lines of ML-code for creating concrete atom types, and for defining various
  type classes and instantiating generic lemmas for them.  In addition to
  simplifying the ML-code, the setup here also offers user-visible improvements:
  Now concrete atoms can be declared at any point of a formalisation, and
  theories that separately declare different atom types can be merged
  together---it is no longer required to collect all atom declarations in one
  place.
*}



section {* Related Work\label{related} *}

text {*
  Add here comparison with old work.

    Using a single atom type to represent atoms of different sorts and
  representing permutations as functions are not new ideas; see
  \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
  of this paper is to show an example of how to make better theorem proving
  tools by choosing the right level of abstraction for the underlying
  theory---our design choices take advantage of Isabelle's type system, type
  classes and reasoning infrastructure.  The novel technical contribution is a
  mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and
  HOL-based languages \cite{PittsHOL4} where variables and variable binding
  depend on type annotations.

  The paper is organised as follows\ldots


  The main point is that the above reasoning blends smoothly with the reasoning
  infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
  type class suffices. 

  With this
  design one can represent permutations as lists of pairs of atoms and the
  operation of applying a permutation to an object as the function


  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

  \noindent 
  where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
  of the objects on which the permutation acts. For atoms 
  the permutation operation is defined over the length of lists as follows

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
  @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & 
     $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ 
                    @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
                    @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
  \end{tabular}\hfill\numbered{atomperm}
  \end{isabelle}

  \noindent
  where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
  @{text "b"}. For atoms with different type than the permutation, we 
  define @{text "\<pi> \<bullet> c \<equiv> c"}.

  With the separate atom types and the list representation of permutations it
  is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
  permutation, since the type system excludes lists containing atoms of
  different type. However, a disadvantage is that whenever we need to
  generalise induction hypotheses by quantifying over permutations, we have to
  build quantifications like

  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}

  \noindent
  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. 
  The reason is that the permutation operation behaves differently for 
  every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
  single quantification to stand for all permutations. Similarly, the 
  notion of support

  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}

  \noindent
  which we will define later, cannot be
  used to express the support of an object over \emph{all} atoms. The reason
  is that support can behave differently for each @{text
  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
  a statement that an object, say @{text "x"}, is finitely supported we end up
  with having to state premises of the form

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
  \end{tabular}\hfill\numbered{fssequence}
  \end{isabelle}

  \noindent
  Because of these disadvantages, we will use in this paper a single unified atom type to 
  represent atoms of different sorts. Consequently, we have to deal with the
  case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
  the type systems to exclude them. 

  We also will not represent permutations as lists of pairs of atoms (as done in
  \cite{Urban08}).  Although an
  advantage of this representation is that the basic operations on
  permutations are already defined in Isabelle's list library: composition of
  two permutations (written @{text "_ @ _"}) is just list append, and
  inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
  list reversal, and another advantage is that there is a well-understood
  induction principle for lists, a disadvantage is that permutations 
  do not have unique representations as lists. We have to explicitly identify
  them according to the relation

  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
  \end{tabular}\hfill\numbered{permequ}
  \end{isabelle}

  \noindent
  This is a problem when lifting the permutation operation to other types, for
  example sets, functions and so on. For this we need to ensure that every definition
  is well-behaved in the sense that it satisfies some
  \emph{permutation properties}. In the list representation we need
  to state these properties as follows:


  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
  i) & @{text "[] \<bullet> x = x"}\\
  ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
  iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
  \end{tabular}\hfill\numbered{permprops}
  \end{isabelle}

  \noindent
  where the last clause explicitly states that the permutation operation has
  to produce the same result for related permutations.  Moreover, 
  ``permutations-as-lists'' do not satisfy the group properties. This means by
  using this representation we will not be able to reuse the extensive
  reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
  in this paper permutations as functions from atoms to atoms. This representation
  is unique and satisfies the laws of non-commutative groups.
*}


section {* Conclusion *}

text {*
  This proof pearl describes a new formalisation of the nominal logic work by
  Pitts et al. With the definitions we presented here, the formal reasoning blends 
  smoothly with the infrastructure of the Isabelle/HOL theorem prover. 
  Therefore the formalisation will be the underlying theory for a 
  new version of Nominal Isabelle.

  The main difference of this paper with respect to existing work on Nominal
  Isabelle is the representation of atoms and permutations. First, we used a
  single type for sorted atoms. This design choice means for a term @{term t},
  say, that its support is completely characterised by @{term "supp t"}, even
  if the term contains different kinds of atoms. Also, whenever we have to
  generalise an induction so that a property @{text P} is not just established
  for all @{text t}, but for all @{text t} \emph{and} under all permutations
  @{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is
  that permutations can now consist of multiple swapping each of which can
  swap different kinds of atoms. This simplifies considerably the reasoning
  involved in building Nominal Isabelle.

  Second, we represented permutations as functions so that the associated
  permutation operation has only a single type parameter. This is very convenient
  because the abstract reasoning about permutations fits cleanly
  with Isabelle/HOL's type classes. No custom ML-code is required to work
  around rough edges. Moreover, by establishing that our permutations-as-functions
  representation satisfy the group properties, we were able to use extensively 
  Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs 
  to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.
  An interesting point is that we defined the swapping operation so that a 
  swapping of two atoms with different sorts is \emph{not} excluded, like 
  in our older work on Nominal Isabelle, but there is no ``effect'' of such 
  a swapping (it is defined as the identity). This is a crucial insight
  in order to make the approach based on a single type of sorted atoms to work.
  But of course it is analogous to the well-known trick of defining division by 
  zero to return zero.

  We noticed only one disadvantage of the permutations-as-functions: Over
  lists we can easily perform inductions. For permutations made up from
  functions, we have to manually derive an appropriate induction principle. We
  can establish such a principle, but we have no real experience yet whether ours
  is the most useful principle: such an induction principle was not needed in
  any of the reasoning we ported from the old Nominal Isabelle, except
  when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.

  Finally, our implementation of sorted atoms turned out powerful enough to
  use it for representing variables that carry on additional information, for
  example typing annotations. This information is encoded into the sorts. With
  this we can represent conveniently binding in ``Church-style'' lambda-terms
  and HOL-based languages. While dealing with such additional information in 
  dependent type-theories, such as LF or Coq, is straightforward, we are not 
  aware of any  other approach in a non-dependent HOL-setting that can deal 
  conveniently with such binders.
 
  The formalisation presented here will eventually become part of the Isabelle 
  distribution, but for the moment it can be downloaded from the 
  Mercurial repository linked at 
  \href{http://isabelle.in.tum.de/nominal/download}
  {http://isabelle.in.tum.de/nominal/download}.\smallskip

  \noindent
  {\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan 
  Berghofer and Cezary Kaliszyk for their comments on earlier versions 
  of this paper. We are also grateful to the anonymous referee who helped us to
  put the work into the right context.  
*}


(*<*)
end
(*>*)