(*<*)
theory Paper
imports "../Nominal-General/Nominal2_Base" 
        "../Nominal-General/Nominal2_Atoms" 
        "../Nominal-General/Nominal2_Eqvt" 
        "../Nominal-General/Atoms" 
        "LaTeXsugar"
begin

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

abbreviation
  "sort_ty \<equiv> sort_of_ty"

(*>*)

section {* Introduction *}

text {*
  Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
  prover providing a proving infrastructure for convenient reasoning about
  programming languages. It has been used to formalise an equivalence checking
  algorithm for LF \cite{UrbanCheneyBerghofer08}, 
  Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
  \cite{BengtsonParrow07} 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}.

  At its core Nominal Isabelle is based on the nominal logic work of Pitts et
  al \cite{GabbayPitts02,Pitts03}.  The most basic notion in this work is a
  sort-respecting permutation operation defined over a countably infinite
  collection of sorted atoms. The atoms are used for representing variables
  that might be bound. 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 and bound type variables; each kind
  needs to be represented by a different sort of atoms.

  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
  atoms and sorts are used in the original formulation of the nominal logic work.
  Therefore it was decided in earlier versions of Nominal Isabelle to use a
  separate type for each sort of atoms and let the type system enforce the
  sort-respecting property of permutations. Inspired by the work on nominal
  unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
  implement permutations concretely as lists of pairs of atoms. Thus Nominal
  Isabelle used the two-place permutation operation with the generic type

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

  \noindent 
  where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type
  of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} 
  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}\\
  \end{tabular}\hspace{12mm}
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  @{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 of different type, the permutation operation
  is defined as @{text "\<pi> \<bullet> c \<equiv> c"}.

  With the list representation of permutations it is impossible to state an
  ``ill-sorted'' permutation, since the type system excludes lists containing
  atoms of different type. Another advantage of the list representation is that
  the basic operations on permutations are already defined in the 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. A disadvantage is that permutations do not have unique
  representations as lists; we had to explicitly identify permutations 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}

  When lifting the permutation operation to other types, for example sets,
  functions and so on, we needed to ensure that every definition is
  well-behaved in the sense that it satisfies the following three 
  \emph{permutation properties}:

  \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
  From these properties we were able to derive most facts about permutations, and 
  the type classes of Isabelle/HOL allowed us to reason abstractly about these
  three properties, and then let the type system automatically enforce these
  properties for each type.

  The major problem with Isabelle/HOL's type classes, however, is that they
  support operations with only a single type parameter and the permutation
  operations @{text "_ \<bullet> _"} used above in the permutation properties
  contain two! To work around this obstacle, Nominal Isabelle 
  required the user to
  declare up-front the collection of \emph{all} atom types, say @{text
  "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. From this collection it used custom ML-code to
  generate @{text n} type classes corresponding to the permutation properties,
  whereby in these type classes the permutation operation is restricted to

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

  \noindent
  This operation has only a single type parameter @{text "\<beta>"} (the @{text "\<alpha>\<^isub>i"} are the
  atom types given by the user). 

  While the representation of permutations-as-lists solved the
  ``sort-respecting'' requirement and the declaration of all atom types
  up-front solved the problem with Isabelle/HOL's type classes, this setup
  caused several problems for formalising the nominal logic work: First,
  Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the
  permutation operation over @{text "n"} types of atoms.  Second, whenever we
  need to generalise induction hypotheses by quantifying over permutations, we
  have to build cumbersome 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"}. Third, although the notion of support

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

  \noindent
  which we will define later, has a generic type @{text "\<alpha> set"}, it cannot be
  used to express the support of an object over \emph{all} atoms. The reason
  is again 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
  Sometimes we can avoid such premises completely, if @{text x} is a member of a
  \emph{finitely supported type}.  However, keeping track of finitely supported
  types requires another @{text n} type classes, and for technical reasons not
  all types can be shown to be finitely supported.

  The real pain of having a separate type for each atom sort arises, however, 
  from another permutation property

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
  iv) & @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}
  \end{tabular}
  \end{isabelle}

  \noindent
  where permutation @{text "\<pi>\<^isub>1"} has type @{text "(\<alpha> \<times> \<alpha>) list"},
  @{text "\<pi>\<^isub>2"} type @{text "(\<alpha>' \<times> \<alpha>') list"} and @{text x} type @{text
  "\<beta>"}. This property is needed in order to derive facts about how
  permutations of different types interact, which is not covered by the
  permutation properties @{text "i"}-@{text "iii"} shown in
  \eqref{permprops}. The problem is that this property involves three type
  parameters. In order to use again Isabelle/HOL's type class mechanism with
  only permitting a single type parameter, we have to instantiate the atom
  types. Consequently we end up with an additional @{text "n\<^sup>2"}
  slightly different type classes for this permutation property.
  
  While the problems and pain can be almost completely hidden from the user in
  the existing implementation of Nominal Isabelle, the work is \emph{not}
  pretty. It requires a large amount of custom ML-code and also forces the
  user to declare up-front all atom-types that are ever going to be used in a
  formalisation. In this paper we set out to solve the problems with multiple
  type parameters in the permutation operation, and in this way can dispense
  with the large amounts of custom ML-code for generating multiple variants
  for some basic definitions. The result is that we can implement a pleasingly
  simple formalisation of the nominal logic work.\smallskip

  \noindent
  {\bf Contributions of the paper:} Using a single atom type to represent
  atoms of different sorts and representing permutations as functions are not
  new ideas.  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.
*}

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

text {*
  In the nominal logic work of Pitts, binders and bound variables are
  represented by \emph{atoms}.  As stated above, we need to have different
  \emph{sorts} of atoms to be able to bind different kinds of variables.  A
  basic requirement is that there must be a countably infinite number of atoms
  of each sort.  Unlike in our earlier work, where we identified each sort with
  a separate type, we implement here atoms to be
*}

          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 type
  \emph{string} is merely for convenience; any countably infinite type would work
  as well.) 
  We have an auxiliary function @{text sort} that is defined as @{thm
  sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
  atoms and every sort @{text s} the property:
  
  \begin{proposition}\label{choosefresh}
  @{text "If finite X then there exists an atom a such that
  sort a = s and a \<notin> X"}.
  \end{proposition}

  For implementing sort-respecting permutations, we use functions of type @{typ
  "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the
  identity on all atoms, except a finite number of them; and @{text "iii)"} map
  each atom to one of the same sort. These properties can be conveniently stated
  for a function @{text \<pi>} as follows:
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  i)~~~@{term "bij \<pi>"}\hspace{5mm}
  ii)~~~@{term "finite {a. \<pi> a \<noteq> a}"}\hspace{5mm}
  iii)~~~@{term "\<forall>a. sort (\<pi> a) = sort a"}\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 
  @{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.  In earlier versions of Nominal Isabelle, we avoided this problem by
  using different types for different sorts; the type system prevented users
  from stating ill-sorted swappings.  Here, however, definitions such 
  as\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 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"}.}

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

  \noindent
  do not work in general, because the type system does not prevent @{text a}
  and @{text b} from having different sorts---in which case the function would
  violate property @{text iii}.  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 instead of lists as a representation for
  permutations is that 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}.  We do not have to use the equivalence relation shown
  in~\eqref{permequ} to identify them, as we would if they had been represented
  as lists of pairs.  Another advantage of the function representation is that
  they form a (non-commutative) group, provided we define

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
  @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
  @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
  @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} 
  \end{tabular}
  \end{isabelle}

  \noindent
  and verify the simple properties

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
  @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
  \end{tabular}
  \end{isabelle}

  \noindent
  Again this is in contrast to the list-of-pairs representation which does not
  form a group.  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---@{text
  "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  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.

  By formalising permutations abstractly as functions, and using a single type
  for all atoms, we can now restate the \emph{permutation properties} from
  \eqref{permprops} as just the two equations
  
  \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
  in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
  have only a single type parameter.  Consequently, these properties are
  compatible with the one-parameter restriction of Isabelle/HOL's type classes.
  There is no need to introduce a separate type class instantiated for each
  sort, like in the old approach.

  The next notion allows us to establish generic lemmas involving the
  permutation operation.

  \begin{definition}
  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
  First, it follows from the laws governing
  groups that a permutation and its inverse cancel each other.  That is, for any
  @{text "x"} of a permutation type:

  
  \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, in a permutation type 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
  In order to lift the permutation operation to other types, we can define for:

  \begin{isabelle}
  \begin{tabular}{@ {}c@ {\hspace{-1mm}}c@ {}}
  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  \end{tabular} &
  \begin{tabular}{@ {}r@ {\hspace{2mm}}l@ {}}
  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]}\\[2mm]
  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
  \end{tabular}
  \end{tabular}
  \end{isabelle}

  \noindent
  and then establish:

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

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

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}[b]{@ {}rcl}
  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
  @{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}

  \noindent
  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. We can also show once and for all that the following
  property---which caused so many headaches in our earlier setup---holds for any
  permutation type.

  \begin{lemma}\label{permutecompose} 
  Given @{term x} is of permutation type, then 
  @{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]{@ {}rcl@ {\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}

%* }
%
%section { * Equivariance * }
%
%text { *

  An \emph{equivariant} function or predicate is one that is invariant under
  the swapping of atoms.  Having a notion of equivariance with nice logical
  properties is a major advantage of bijective permutations over traditional
  renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined
  uniformly for all permutation types, and it is satisfied by most HOL
  functions and constants.

  \begin{definition}\label{equivariance}
  A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
  \end{definition}

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

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

  \noindent
  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 
  the fact 
  
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "\<pi> \<bullet> (f x) = (\<pi> \<bullet> f) (\<pi> \<bullet> x)"}
  \end{tabular}\hfill\numbered{permutefunapp}
  \end{isabelle} 

  \noindent
  which follows again directly 
  from the definition of the permutation operation for functions and the cancellation 
  property. Similarly for functions with more than one argument. 

  Both formulations of equivariance have their advantages and disadvantages:
  \eqref{altequivariance} is often easier to establish. 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}
  \end{isabelle} 

  \noindent
  using the permutation operation on booleans and property \eqref{permuteequ}. 
  Lemma~\ref{permutecompose} establishes that the permutation operation is 
  equivariant. It is also easy to see that the boolean operators, like 
  @{text "\<and>"}, @{text "\<or>"} and @{text "\<longrightarrow>"} are all 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>}.  These equivariance properties
  are tremendously helpful later on when we have to push permutations inside
  terms.
*}


section {* Support and Freshness *}

text {*
  The most original aspect of the nominal logic work of Pitts et al is a general
  definition for ``the set of free variables of an object @{text "x"}''.  This
  definition is general in the sense that it applies not only to lambda-terms,
  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=10] supp_def[no_vars, THEN eq_reflection]}

  \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}, defined as
  
  @{thm [display,indent=10] fresh_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 @{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}
  & \multicolumn{2}{@ {}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 \eqref{permutecompose} and \eqref{swapeqvt}\\
  @{text "\<Leftrightarrow>"}
  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} @{text "\<equiv>"}
    @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
  & by \eqref{permuteequ}\\
  \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.

  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{center}
  \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}
  \begin{tabular}{@ {}r@ {\hspace{2mm}}l}
  @{text "booleans"}: & @{term "supp b = {}"}\\
  @{text "nats"}:     & @{term "supp n = {}"}\\
  @{text "products"}: & @{thm supp_Pair[no_vars]}\\
  \end{tabular} &
  \begin{tabular}{r@ {\hspace{2mm}}l@ {}}
  @{text "lists:"} & @{thm supp_Nil[no_vars]}\\
                   & @{thm supp_Cons[no_vars]}\\
  \end{tabular}
  \end{tabular}
  \end{center}

  \noindent
  But establishing the support of atoms and permutations in our setup here is a bit 
  trickier. To do so we will use the following notion about a \emph{supporting set}.
  
  \begin{definition}
  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 \emph{one} premise
  of the form @{text "finite (supp x)"}
  for each @{text x}. Compare that with the sequence of premises in our earlier
  version of Nominal Isabelle (see~\eqref{fssequence}). 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. Then \emph{no} premise is needed,
  as the type system of Isabelle/HOL can figure out automatically when an object
  is finitely supported.

  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 the function that returns the natural number of an atom
  
  @{text [display, indent=10] "nat_of (Atom s i) \<equiv> i"}

  \noindent
  This function's support is the set of \emph{all} atoms. 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}. 
  Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
*}

section {* Concrete Atom Types *}

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}\ \ \ \ \ \ \ \ \ \ %%%
  i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}
  ii)  \hspace{1mm}@{thm atom_eqvt[where p="\<pi>", no_vars]}\hspace{4mm}
  iii) \hspace{1mm}@{thm sort_of_atom_eq [no_vars]}
  \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 {* Multi-Sorted Concrete Atoms *}

(*<*)
datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _") 
(*>*)

text {*
  The formalisation presented so far allows us to streamline proofs and reduce
  the amount of custom ML-code in the existing implementation of Nominal
  Isabelle. In this section we describe a mechanism that extends the
  capabilities of Nominal Isabelle. This mechanism is about variables with 
  additional information, for example typing constraints.
  While we leave a detailed treatment of binders and binding of variables for a 
  later paper, we will have a look here at how such variables can be 
  represented by concrete atoms.
  
  In the previous section we considered concrete atoms that can be used in
  simple binders like \emph{@{text "\<lambda>x. x"}}.  Such concrete atoms do
  not carry any information beyond their identities---comparing for equality
  is really the only way to analyse ordinary concrete atoms.
  However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
  underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
  more complicated structure. For example in the ``Church-style'' lambda-term

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
  \end{tabular}\hfill\numbered{church}
  \end{isabelle}

  \noindent
  both variables and binders include typing information indicated by @{text \<alpha>}
  and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
  "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
  variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
  @{text "x\<^isub>\<beta>"}.

  To illustrate how we can deal with this phenomenon, let us represent object
  types like @{text \<alpha>} and @{text \<beta>} by the datatype

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
  \end{tabular}
  \end{isabelle}

  \noindent
  If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the 
  problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
  will always permute \emph{both} occurrences of @{text x}, even if the types
  @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
  eventually mean that both occurrences of @{text x} will become bound by a
  corresponding binder. 

  Another attempt might be to define variables as an instance of the concrete
  atom type class, where a @{text ty} is somehow encoded within each variable.
  Remember we defined atoms as the datatype:
*}

          datatype  atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
  
text {*
  \noindent
  Considering our method of defining concrete atom types, the usage of a string
  for the sort of atoms seems a natural choice.  However, none of the results so
  far depend on this choice and we are free to change it.
  One possibility is to encode types or any other information by making the sort
  argument parametric as follows:
*}

          datatype  'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat

text {*
  \noindent
  The problem with this possibility is that we are then back in the old
  situation where our permutation operation is parametric in two types and
  this would require to work around Isabelle/HOL's restriction on type
  classes. Fortunately, encoding the types in a separate parameter is not
  necessary for what we want to achieve, as we only have to know when two
  types are equal or not. The solution is to use a different sort for each
  object type.  Then we can use the fact that permutations respect \emph{sorts} to
  ensure that permutations also respect \emph{object types}.  In order to do
  this, we must define an injective function @{text "sort_ty"} mapping from
  object types to sorts.  For defining functions like @{text "sort_ty"}, it is
  more convenient to use a tree datatype for sorts. Therefore we define
*}

          datatype  sort = Sort string "(sort list)"
          datatype  atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat

text {*
  \noindent
  With this definition,
  the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
  The point, however, is that we can now define the function @{text sort_ty} simply as

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \begin{tabular}{@ {}l}
  @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun''  [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
  \end{tabular}\hfill\numbered{sortty}
  \end{isabelle}

  \noindent
  which can easily be shown to be injective.  
  
  Having settled on what the sorts should be for ``Church-like'' atoms, we have to
  give a subtype definition for concrete atoms. Previously we identified a subtype consisting 
  of atoms of only one specified sort. This must be generalised to all sorts the
  function @{text "sort_ty"} might produce, i.e.~the
  range of @{text "sort_ty"}. Therefore we define

  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
  \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
  \end{isabelle}

  \noindent
  This command gives us again injective representation and abstraction
  functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively. 

  We can define the permutation operation for @{text var} as @{thm
  permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
  injective function to type @{typ atom} as @{thm atom_var_def[THEN
  eq_reflection, no_vars]}. Finally, we can define a constructor function that
  makes a @{text var} from a variable name and an object type:

  @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}

  \noindent
  With these definitions we can verify all the properties for concrete atom
  types except Property \ref{atomprops}@{text ".iii)"}, which requires every
  atom to have the same sort.  This last property is clearly not true for type
  @{text "var"}.
  This fact is slightly unfortunate since this
  property allowed us to use the type-checker in order to shield the user from
  all sort-constraints.  But this failure is expected here, because we cannot
  burden the type-system of Isabelle/HOL with the task of deciding when two
  object types are equal.  This means we sometimes need to explicitly state sort
  constraints or explicitly discharge them, but as we will see in the lemma
  below this seems a natural price to pay in these circumstances.

  To sum up this section, the encoding of type-information into atoms allows us 
  to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following 
  lemma
*}

          lemma
	    assumes asm: "\<alpha> \<noteq> \<beta>" 
	    shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
	    using asm by simp

text {*
  \noindent 
  As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
  swapping. With this we can faithfully represent bindings in languages
  involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
  expect that the creation of such atoms can be easily automated so that the
  user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
  where the argument, or arguments, are datatypes for which we can automatically
  define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
  Our hope is that with this approach Benzmueller and Paulson can make
  headway with formalising their results
  about simple type theory \cite{PaulsonBenzmueller}.
  Because of its limitations, they did not attempt this with the old version 
  of Nominal Isabelle. We also hope we can make progress with formalisations of
  HOL-based languages.
*}


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
(*>*)