
diff -r fb201e383f1b -r da575186d492 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1231 +0,0 @@
-(*<*)
-theory Paper
-imports "../Nominal/Nominal2_Base" 
-        "../Nominal/Atoms" 
-        "~~/src/HOL/Library/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 minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<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
-(*>*)
\ No newline at end of file




