
diff -r fb201e383f1b -r da575186d492 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1819 +0,0 @@
-(*<*)
-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
-  subtype 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$
-
-
-  Obstacles for Coq; no type-classes, difficulties with quotient types,
-  need for classical reasoning
-
-  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 in Isabelle/HOL 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}
-
-  \noindent
-  This property will be used later whenever we have to chose a `fresh' atom.
-
-  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 a unique representation. 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"]}\smallskip\\
-  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 the object @{text
-  x}.\footnote{We will write @{text "((op \<bullet>) \<pi>)
-  x"} for this operation in the few cases where we need to indicate
-  that it is a function applied with two arguments.}  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 equation
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<pi> \<bullet> (f x) ="}
-  @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
-  \hfill\numbered{permutefunapp}
-  \end{isabelle}
-
-  \noindent
-  provided the permutation properties hold for @{text x}. This equation can
-  be easily shown by unfolding the permutation operation for functions on
-  the right-hand side of the equation, simplifying the resulting 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. Then Isabelle/HOL will use this information and determine
-  whether an object @{text x} with a compound type, like @{typ "atom \<Rightarrow> (atom set * nat)"}, 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 {*
-  (mention alpha-structural paper by Andy)
-
-  Two important notions in the nominal logic work are what Pitts calls
-  \emph{equivariance} and the \emph{equivariance principle}.  These
-  notions allows us to characterise how permutations act upon compound
-  statements in HOL by analysing how these statements are constructed.
-  The notion of equivariance means that an object is invariant under
-  any permutations. This can be defined as follows:
-
-  \begin{definition}[Equivariance]\label{equivariance}
-  An object @{text "x"} of permutation type is \emph{equivariant} provided 
-  for all permutations @{text "\<pi>"}, \mbox{@{term "\<pi> \<bullet> x = x"}} holds.
-  \end{definition}
-
-  \noindent
-  In what follows we will primarily be interested in the cases where
-  @{text x} 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 equivariance.  
-  For example, assuming @{text f} is a function of permutation 
-  type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} 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
-  We will say this formulation of equivariance is 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 functions that take more than
-  one argument. The point to note is that equivariance and equivariance in fully
-  applied form are always interderivable (for permutation types).
-
-  Both formulations of equivariance have their advantages and
-  disadvantages: \eqref{altequivariance} is usually more convenient to
-  establish, since statements in 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. Given this definition, it 
-  is also easy to see that the boolean operators, like @{text "\<and>"}, 
-  @{text "\<or>"}, @{text "\<longrightarrow>"} and  @{text "\<not>"} are equivariant:
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}lcl}
-  @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
-  @{text "\<pi> \<bullet> (A \<or> B) = (\<pi> \<bullet> A) \<or> (\<pi> \<bullet> B)"}\\
-  @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
-  @{text "\<pi> \<bullet> (\<not>A) = \<not>(\<pi> \<bullet> A)"}\\
-  \end{tabular}
-  \end{isabelle}
-  
-  In contrast, the advantage of Definition \ref{equivariance} is that
-  it allows us to state a general principle how permutations act on
-  statements in HOL.  For this we will define a rewrite system that
-  `pushes' a permutation towards the leaves of statements (i.e.~constants
-  and variables).  Then the permutations disappear in cases where the
-  constants are equivariant.  To do so, let us first define
-  \emph{HOL-terms}, which are the building blocks of statements in HOL.
-  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 better
-  legibility we leave the typing information implicit.  We also assume
-  the usual notions for free and bound variables of a HOL-term.
-  Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
-  and eta-equivalence. The equivariance principle can now 
-  be stated formally as follows:
-
-  \begin{theorem}[Equivariance Principle]\label{eqvtprin}
-  Suppose a HOL-term @{text t} whose constants are all equivariant. For any 
-  permutation @{text \<pi>}, let @{text t'} be @{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}
-  
-  \noindent
-  The significance of this principle is that we can automatically establish
-  the equivariance of a constant for which equivariance is not yet
-  known. For this we only have to establish that the definiens of this
-  constant is a HOL-term whose constants are all equivariant. 
-  This meshes well with how HOL is designed: except for a few axioms, every constant 
-  is defined in terms of existing constants. For example an alternative way
-  to deduce that @{term True} is equivariant is to look at its
-  definition
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{thm True_def}
-  \end{isabelle} 
-
-  \noindent
-  and observing that the only constant in the definiens, namely @{text "="}, is 
-  equivariant. Similarly, the universal quantifier @{text "\<forall>"} is definied in HOL as 
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}
-  \end{isabelle} 
-
-  \noindent
-  The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="}
-  and @{text "True"}, are equivariant (we shown this above). Therefore
-  the equivariance principle gives us
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{text "\<pi> \<bullet> (\<forall>x. P x)"} & @{text "\<equiv>"} & @{text "\<pi> \<bullet> (P = (\<lambda>x. True))"}\\  
-                           & @{text "="} & @{text "(\<pi> \<bullet> P) = (\<lambda>x. True)"}\\  
-                           & @{text "\<equiv>"} & @{text "\<forall>x. (\<pi> \<bullet> P) x"}
-  \end{tabular}
-  \end{isabelle} 
-
-  \noindent
-  which means the constant @{text "\<forall>"} must be equivariant. From this
-  we can deduce that the existential quantifier @{text "\<exists>"} is equivariant. 
-  Its definition in HOL is
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<exists>x. P x \<equiv> "}~@{thm (rhs) Ex_def[no_vars]}
-  \end{isabelle} 
-
-  \noindent
-  where again the HOL-term on the right-hand side only contains equivariant constants 
-  (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). Taking both facts together, we can deduce that
-  the unique existential quantifier @{text "\<exists>!"} is equivariant. Its definition 
-  is
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<exists>!x. P x \<equiv> "}~@{thm (rhs) Ex1_def[no_vars]}
-  \end{isabelle} 
-
-  \noindent
-  with all constants on the right-hand side being equivariant. With this kind
-  of reasoning we can build up a database of equivariant constants, which will
-  be handy for more complex calculations later on. 
-
-  Before we proceed, let us give a justification for the equivariance principle. 
-  This justification cannot be given directly inside Isabelle/HOL since we cannot
-  prove any statement about HOL-terms. Instead, we will use a rewrite 
-  system consisting of a series of equalities 
-  
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<pi> \<cdot> t  =  ...  =  t'"}
-  \end{isabelle}
-  
-  \noindent 
-  that establish the equality between @{term "\<pi> \<bullet> t"} and
-  @{text "t'"}. The idea of the rewrite system is to push the
-  permutation inside the term @{text t}. We have implemented this as a
-  conversion tactic on the ML-level of Isabelle/HOL.  In what follows,
-  we will show that this tactic produces only finitely many equations
-  and also show that it 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 tactic applies four `oriented' equations. 
-  We will first give a naive version of
-  our tactic, which however in some corner cases produces incorrect
-  results or does not terminate.  We then give a modification in order
-  to obtain the desired properties.
-  Consider the following for oriented equations
-  
-  \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])"}\\
-  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{rewriteapplam}
-  \end{isabelle}
-
-  \noindent
-  These equation are oriented in the sense of being applied in the left-to-right
-  direction. 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.
-  The third is a consequence of \eqref{cancel} and the fourth from 
-  Definition~\ref{equivariance}. Unfortunately, we have to be careful with
-  the rules {\it i)} and {\it iv}) since they can lead to loops whenever
-  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.
-  Recall that we established in Lemma \ref{permutecompose} that the
-  constant @{text "(op \<bullet>)"} is equivariant and 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 term is again an instance of rewrite rule {\it i}), but larger.  
-  To avoid this loop we will apply the 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: since there is no free variable in the original
-  term, 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 also 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 in order to eliminate the permutation. 
-  In contrast, if we start 
-  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)}
-  in order to obtain @{text "(\<pi> \<bullet> (- \<pi>)) \<bullet> (\<pi> \<bullet> x)"}
-  and not rule {\it iii)}. The latter would eliminate @{text \<pi>}
-  completely and thus violating our correctness property. The problem is that 
-  rule {\it iii)} should only apply to
-  instances where the corresponding variable is to bound; for free variables we want
-  to use {\it ii)}.  In order to distinguish these cases we have to
-  maintain the information which variable is bound when inductively
-  taking a term `apart'. This, unfortunately, does not mesh well with
-  the way how conversion 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 re-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
-  where @{text unpermutes} are only generated in case of bound variables.
-  Clearly none of these rules overlap. Moreover, given our
-  outside-to-inside strategy, applying them repeatedly must 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 rewrite rules of the conversions tactic in place, we can
-  establish its correctness. The property we are after is that 
-  for a HOL-term @{text t} whose constants are all equivariant the 
-  term \mbox{@{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 \mbox{@{text "\<pi> \<bullet> x"}}. Let us call
-  a variable @{text x} \emph{really free}, if it is free and not occuring
-  in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
-  We need the following technical notion characterising \emph{@{text "\<pi>"}-proper} HOL-terms
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}ll}
-  $\bullet$ & variables and constants are @{text \<pi>}-proper,\\
-  $\bullet$ & @{term "unpermute \<pi> x"} is @{text \<pi>}-proper,\\
-  $\bullet$ & @{term "\<lambda>x. t"} is @{text \<pi>}-proper, if @{text t} is @{text \<pi>}-proper and @{text x} is 
-  really free in @{text t}, and\\
-  $\bullet$ & @{term "t\<^isub>1 t\<^isub>2"} is @{text \<pi>}-proper, if @{text "t\<^isub>1"} and @{text "t\<^isub>2"} are 
-  @{text \<pi>}-proper.
-  \end{tabular}
-  \end{isabelle}
-
-  \begin{proof}[Theorem~\ref{eqvtprin}] We establish the property if @{text t} 
-  is @{text \<pi>}-proper and only contains equivaraint constants, then 
-  @{text "\<pi> \<bullet> t = t'"} where @{text "t'"} is equal to @{text "t"} except all really
-  free variables @{text x} are replaced by @{text "\<pi> \<bullet> x"}, and all semi-free variables 
-  @{text "unpermute \<pi> x"} by @{text "x"}. We establish this property by induction
-  on the size of HOL-terms, counting terms like @{text "unpermuting \<pi> x"} as leafes,
-  like variables and constants. The cases for variables, constants and @{text unpermutes}
-  are routine. In the case of abstractions we have by induction hypothesis that 
-  @{text "\<pi> \<bullet> (t[x := unpermute \<pi> x]) = t'"} with @{text "t'"} satisfying our
-  correctness property. This implies that @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x]) = \<lambda>x. t'"}
-  and hence @{text "\<pi> \<bullet> (\<lambda>x. t) = \<lambda>x. t'"} as needed.\hfill\qed  
-  \end{proof}
-
-  Pitts calls this property \emph{equivariance principle} (book ref ???). 
-  
-  Problems with @{text undefined}
-  
-  Lines of code
-*}
-
-
-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] \label{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
-  Using the equivariance principle, it can be easily checked that all three notions
-  are equivariant. A simple consequence of the definition of support and equivariance 
-  is that if @{text x} is equivariant then we have 
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}l}
-  @{thm  (concl) supp_fun_eqvt[where f="x", no_vars]}
-  \end{tabular}\hfill\numbered{suppeqvtfun}
-  \end{isabelle} 
-
-  \noindent
-  For function applications we can establish the following two properties.
-
-  \begin{lemma}\label{suppfunapp} Let @{text f} and @{text x} be of permutation type, then
-  \begin{isabelle}
-  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
-  {\it i)} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\
-  {\it ii)} & @{thm supp_fun_app[no_vars]}\\
-  \end{tabular}
-  \end{isabelle}
-  \end{lemma}
-
-  \begin{proof}
-  For the first property, we know from the assumption that @{term
-  "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}"} and @{term "finite {b . (a \<rightleftharpoons> b) \<bullet> x \<noteq>
-  x}"} hold. That means for all, but finitely many @{text b} we have
-  @{term "(a \<rightleftharpoons> b) \<bullet> f = f"} and @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. Similarly,
-  we have to show that for but, but finitely @{text b} the equation
-  @{term "(a \<rightleftharpoons> b) \<bullet> f x = f x"} holds. The left-hand side of this
-  equation is equal to @{term "((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x)"} by
-  \eqref{permutefunapp}, which we know by the previous two facts for
-  @{text f} and @{text x} is equal to the right-hand side for all,
-  but finitely many @{text b}. This establishes the first
-  property. The second is a simple corollary of {\it i)} by
-  unfolding the definition of freshness.\qed
-  \end{proof}
-
-  A striking consequence of the definitions for support and freshness
-  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}.\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}
-  
-  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 concrete objects.
-  For booleans, nats, products and lists it is easy to check that
-
-  \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 
-  hold.  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 {\it 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 {\it ii)} is by a direct application of 
-  Theorem~\ref{swapfreshfresh}. For the last property, part {\it i)} proves
-  one ``half'' of the claimed equation. The other ``half'' is by property 
-  {\it ii)} and the fact that @{term "supp x"} is finite by {\it 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 {\it 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 a crucial 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 in Isabelle/HOL corresponding to the 
-  property:
-  
-  \begin{definition}[Finitely Supported Type]
-  A type @{text "\<beta>"} is \emph{finitely supported} if @{term "finite (supp x)"}
-  holds for all @{text x} of type @{text "\<beta>"}.
-  \end{definition}
- 
-  \noindent
-  By the calculations above we can easily establish 
-
-  \begin{theorem}\label{finsuptype} 
-  The types @{type atom}, @{type perm}, @{type bool} and @{type nat}
-  are fintitely supported, and assuming @{text \<beta>}, @{text "\<beta>\<^isub>1"} and
-  @{text "\<beta>\<^isub>2"} are finitely supported types, then @{text "\<beta> list"} and
-  @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"} are finitely supported.
-  \end{theorem}
-
-  \noindent
-  The main benefit of using the finite support property for choosing a
-  fresh atom is that the reasoning is `compositional'. To see this,
-  assume we have a list of atoms and a method of choosing a fresh atom
-  that is not a member in this list---for example the maximum plus
-  one.  Then if we enlarge this list \emph{after} the choice, then
-  obviously the fresh atom might not be fresh anymore. In contrast, by
-  the classical reasoning of Proposition~\ref{choosefresh} we know a
-  fresh atom exists for every list of atoms and no matter how we
-  extend this list of atoms, we always preserve the property of being
-  finitely supported. Consequently the existence of a fresh atom is
-  still guarantied by Proposition~\ref{choosefresh}.  Using the method
-  of `maximum plus one' we might have to adapt the choice of a fresh
-  atom.
-
-  Unfortunately, Theorem~\ref{finsuptype} does not work in general for the
-  types of sets and functions.  There are functions definable in 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 an 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. Their support can be characterised as:
-
-  \begin{lemma}\label{finatomsets}
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}[b]{@ {}rl}
-  {\it i)} & If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\
-  {\it ii)} & If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then 
-  @{thm (concl) supp_cofinite_atom_set[no_vars]}.
-  \end{tabular}
-  \end{isabelle}
-  \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 supports 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
-  %
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}[b]{@ {}rl}
-  {\it i)} & @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\
-  {\it ii)} & @{thm (concl) Union_included_in_supp[no_vars]}.
-  \end{tabular}
-  \end{isabelle}
-  \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}.{\it i)} that @{term "(\<Union>x\<in>S. supp
-  x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be the function
-  \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 (can be easily checked by the equivariance principle), we
-  have that @{text "supp (f S) \<subseteq> supp S"} by
-  Lemma~\ref{suppfunapp}.{\it ii)}. 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}.{\it ii)}. To show the inclusion 
-  in the other direction we can use Lemma~\ref{supports}.{\it i)}. This means
-  for all @{text a} and @{text b} that are not in @{text S} we have to show that
-  @{term "(a \<rightleftharpoons> b) \<bullet> (\<Union>x \<in> S. supp x) = (\<Union>x \<in> S. supp x)"} holds. By the equivariance
-  principle, the left-hand side is equal to @{term "\<Union>x \<in> ((a \<rightleftharpoons> b) \<bullet> S). supp x"}. Now
-  the swapping in front of @{text S} disappears, since @{term "a \<sharp> S"} and @{term "b \<sharp> S"}
-  whenever @{text "a, b \<notin> S"}. Thus we are done.\hfill\qed
-  \end{proof}
-
-  \noindent
-  To sum up, every finite set of finitely supported elements has
-  finite support.  Unfortunately, we cannot use
-  Theorem~\ref{finsuptype} to let Isabelle/HOL find this out
-  automatically. This would require to introduce a separate type of
-  finite sets, which however is not so convenient to reason about as
-  Isabelle's standard set type.
-*}
-
-
-section {* Induction Principles for Permutations *}
-
-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 does
-  not come automatically with an induction principle.  Such an
-  induction principle is however useful for generalising
-  Lemma~\ref{swapfreshfresh} from swappings to permutations, namely
-  
-  \begin{lemma}
-  @{thm [mode=IfThen] perm_supp_eq[where p="\<pi>", no_vars]}
-  \end{lemma}
-
-  \noindent
-  In this section we will establish an induction principle for permutations
-  with which this lemma can be easily proved. It is not too difficult to derive 
-  an induction principle for permutations, given the fact that we allow only 
-  permutations having a finite support. 
-
-  Using a the property from \cite{???}
-
-  \begin{lemma}\label{smallersupp}
-  @{thm [mode=IfThen] smaller_supp[where p="\<pi>", no_vars]}
-  \end{lemma}
-*}
-
-
-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.
-
-  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 for example that subgoals involving sorts must be discharged explicitly within proof
-  scripts, instead of being inferred automatically.  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 is 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.
-  
-*}
-
-
-
-section {* Related Work\label{related} *}
-
-text {*
-  Coq-tries, but failed
-
-  Add here comparison with old work.
-
-  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.
-
-    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
-(*>*)
\ No newline at end of file




