
diff -r 651355113eee -r f1192e3474e0 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue Mar 08 09:07:49 2011 +0000
+++ b/Pearl-jv/Paper.thy	Fri Mar 11 08:51:39 2011 +0000
@@ -6,6 +6,11 @@
         "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
@@ -22,7 +27,7 @@
   Abs_name ("\<lceil>_\<rceil>") and
   Rep_var ("\<lfloor>_\<rfloor>") and
   Abs_var ("\<lceil>_\<rceil>") and
-  sort_of_ty ("sort'_ty _")
+  sort_of_ty ("sort'_ty _") 
 
 (* BH: uncomment if you really prefer the dot notation
 syntax (latex output)
@@ -35,8 +40,16 @@
 abbreviation
   "sort \<equiv> sort_of"
 
-abbreviation
-  "sort_ty \<equiv> sort_of_ty"
+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
+
 
 (*>*)
 
@@ -47,8 +60,7 @@
   about syntax involving binders, such as lambda terms or type schemes:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
-  \hfill\numbered{atomperm}
+  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} 
   \end{isabelle}
   
   \noindent
@@ -64,20 +76,21 @@
 
   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 teh work by Urban
+  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 and even functions. The notion of support
-  is derived from the permutation operation defined over atoms. This
-  permutation operation, written @{text "_ \<bullet> _"}, has proved to be very
+  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. The reason is that permutations are
+  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 exist in general, since renaming substitutions are only injective.  
-  Permutations also preserve many constructions when reasoning about syntax. 
-  For example validity of a typing context is preserved under permutations. 
+  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 the validity of a typing context is preserved under any permutation. 
   Suppose a typing context @{text "\<Gamma>"} of the form
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -88,38 +101,54 @@
   is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}
   occur twice. Then validity is preserved under
   permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
-  all permutations @{text "\<pi>"}. This is \emph{not} the case for arbitrary
-  renaming substitutions, as they might identify some variables in @{text \<Gamma>}. 
-  Permutations fit well with HOL's definitions. For example 
+  all permutations @{text "\<pi>"}. This is again \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}
 
-  Because
-  of the good properties of permutations, we will be able to automate reasoning 
-  steps determining when a construction in HOL is
-  \emph{equivariant}. By equivariance we mean the property that every
-  permutation leaves an object unchanged, that is @{term "\<forall>\<pi>. \<pi> \<bullet> x = x"}.
-  This will often simplify arguments involving the notion of support.
+  \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 an object unchanged, that is @{term "\<pi> \<bullet> x = x"}
+  for all @{text "\<pi>"}. This will often simplify arguments involving support 
+  and functions, since equivariant objects 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.
 
 
-  There are a number of subtle differences between the nominal logic work by Pitts 
-  and the one we will present in this paper. Nominal 
 
-  In the nominal logic work, the `new quantifier' plays a prominent role.
-  
+  In the nominal logic woworkrk, the `new quantifier' plays a prominent role.
+  $\new$
 
 
-  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
 
 
   Two binders
@@ -128,21 +157,19 @@
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 
 text {*
-  The two most basic notions in the nominal logic work are
-  sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. 
-  The existing nominal logic work usually leaves implicit the sorting
-  information for atoms and as far as we know 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 the different kinds of atoms, say types @{text
-  "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. However, this does not blend well with the
-  resoning infrastructure of type-classes in Isabelle/HOL (see Section ??? 
-  about related work).  Therefore we use here a single unified atom type to
-  represent atoms of different sorts. A basic requirement is that there must
-  be a countably infinite number of atoms of each sort.  This can be
-  implemented as the datatype
+  The two most basic notions in the nominal logic work are a countably
+  infinite collection of sorted atoms and sort-respecting permutations. 
+  The existing nominal logic work usually leaves implicit
+  the sorting information for atoms and as far as we know 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 the different sorts of
+  atoms. However, we found that this does not blend well with type-classes in
+  Isabelle/HOL (see Section~\ref{related} about related work).  Therefore we use here a
+  single unified atom type to represent atoms of different sorts. A basic
+  requirement is that there must be a countably infinite number of atoms of
+  each sort.  This can be implemented as the datatype
 
 *}
 
@@ -153,15 +180,20 @@
   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. We have an
-  auxiliary function @{text sort} that is defined as 
+  convenience; any countably infinite type would work as well. 
+  The set of all atoms we shall write as @{term "UNIV::atom set"}.
+  We have two
+  auxiliary functions @{text sort} and @{const nat_of} that are defined as 
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  @{thm sort_of.simps[no_vars, THEN eq_reflection]}
+  \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
-  and we clearly have for every finite set @{text S}
+  We clearly have for every finite set @{text S}
   of atoms and every sort @{text s} the property:
 
   \begin{proposition}\label{choosefresh}\mbox{}\\
@@ -173,7 +205,7 @@
   "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:
+  in Isabelle/HOL for a function @{text \<pi>} as follows:
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{r@ {\hspace{4mm}}l}
@@ -202,29 +234,27 @@
   \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 early 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"}.}
+  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 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
-  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:
+  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}
@@ -240,7 +270,7 @@
   a function in @{typ perm}. 
 
   One advantage of using functions as a representation for
-  permutations is that for example the swappings
+  permutations is that it is unique. For example the swappings
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -250,29 +280,28 @@
   \end{isabelle}
 
   \noindent
-  are \emph{equal}.  Therfore we can use for permutations HOL's built-in
-  principle of `replacing equals by equals in any context'. Another advantage
-  of the function representation is that they form a (non-commutative) group
-  provided we define
+  are \emph{equal}. 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}
-  @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm}
-  @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
-  @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
-  @{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{5mm}
-  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
-  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
+  @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+  @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
+  @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
   @{thm group_add_class.left_minus[where a="\<pi>::perm"]} 
   \end{tabular}
   \end{isabelle}
@@ -288,8 +317,9 @@
   nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
   the non-standard notation in order to reuse the existing libraries.
 
-  In order to reason abstractly about permutations, we state the following two 
-  \emph{permutation properties} 
+  In order to reason abstractly about permutations, we use Isabelle/HOL's
+  type classes~\cite{Wenzel04} and state the following two 
+  \emph{permutation properties}: 
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
@@ -299,20 +329,20 @@
   \end{isabelle} 
 
   \noindent
-  We state these properties in terms of Isabelle/HOL's type class 
-  mechanism \cite{}.
-  This allows us to delegate much of the resoning involved in 
-  determining whether these properties are satisfied to the type system.
-  For this we define
+  The use of type classes allows us to delegate much of the routine resoning involved in 
+  determining whether these properties are satisfied to Isabelle/HOL's type system:
+  we only have to establish that `base' types, such as @{text booleans} and 
+  @{text atoms}, satisfy them and that type-constructors, such as products and lists, 
+  preserve them.  For this we define
 
-  \begin{definition}
+  \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
-  The type class also allows us to establish generic lemmas involving the
+  The type classes also allows us to establish generic lemmas involving the
   permutation operation. 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:
@@ -326,7 +356,6 @@
   \end{isabelle} 
   
   \noindent
-  ??? Proof
   Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 
   which in turn implies the property
 
@@ -337,43 +366,23 @@
   @{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 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}
 
   \noindent
   In order to lift the permutation operation to other types, we can define for:
 
-  \begin{equation}\label{permdefs}
-  \mbox{
-  \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}}
-  a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
-  b) & functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
-  c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
-  d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  f) & 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]}\\
-  g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
-  \end{tabular}}
-  \end{equation}
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l@ {\hspace{4mm}}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]}\\
+  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]}\\
+  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+  \end{tabular}\hfill\numbered{permdefs}
+  \end{isabelle}
 
   \noindent
   and then establish:
@@ -399,18 +408,48 @@
   \end{tabular}\hfill\qed
   \end{isabelle}
   \end{proof}
+
+  \noindent
+  Note that the permutation operation for functions is defined so that we have the property
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  @{text "\<pi> \<bullet> (f x) ="}
+  @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
+  \hfill\numbered{permutefunapp}
+  \end{isabelle}
+
+  \noindent
+  which is a simple consequence of the definition and the cancellation property in \eqref{cancel}.
+  We can also show that the following property 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]{@ {}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}
+
 *}
 
 section {* Equivariance *}
 
 text {*
   An important notion in the nominal logic work is \emph{equivariance}.
-  An equivariant function or predicate is one that is invariant under
-  the swapping of atoms. This notion can be defined
+  An equivariant function is one that is invariant under
+  permutations of atoms. This notion can be defined
   uniformly as follows:
 
 
-  \begin{definition}\label{equivariance}
+  \begin{definition}[Equivariance]\label{equivariance}
   A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
   \end{definition}
 
@@ -429,28 +468,12 @@
   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. 
+  \eqref{permutefunapp}. Similarly for functions with more than one argument. 
 
   Both formulations of equivariance have their advantages and disadvantages:
-  the definition, \eqref{permutefunapp} and (\ref{permdefs}.2) lead to a simple
-  rewrite system that pushes permutations inside a term until they reach
-  either function constants or variables. The permutations in front of
-  equivariant functions disappear. Such a rewrite system is often very helpful
-  in determining whether @{text "p \<bullet> t = t"} holds for a compound term @{text t}. In contrast
   \eqref{altequivariance} is usually easier to establish, since statements are
-  commonly given in a form where functions are fully applied. For example we can
-  easily show that equality is equivariant
+  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}
@@ -462,7 +485,7 @@
   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 
+  @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore 
   a simple calculation will show that our swapping functions are equivariant, that is
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -473,26 +496,36 @@
 
   \noindent
   for all @{text a}, @{text b} and @{text \<pi>}.  
+
+  In contrast, Definition~\ref{equivariance} together with the permutation 
+  operation for functions and \eqref{permutefunapp} lead to a simple
+  rewrite system that pushes permutations inside a term until they reach
+  either function constants or variables. The permutations in front of
+  equivariant functions disappear. Such a rewrite system is often very helpful
+  in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ???
+ 
 *}
 
 
 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:
+  The most original aspect of the nominal logic work of Pitts is a general
+  definition for `the set of free variables, or free atoms, of an object @{text "x"}'.  This
+  definition is general in the sense that it applies not only to lambda terms,
+  but to any type for which a permutation operation is defined 
+  (like lists, sets, functions and so on). 
 
+  \begin{definition}[Support] Given @{text x} is of permutation type, then 
+  
   @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}
+  \end{definition}
 
   \noindent
   (Note that due to the definition of swapping in \eqref{swapdef}, we do not
   need to explicitly restrict @{text a} and @{text b} to have the same sort.)
   There is also the derived notion for when an atom @{text a} is \emph{fresh}
-  for an @{text x}, defined as
+  for an @{text x} of permutation type, defined as
   
   @{thm [display,indent=10] fresh_def[no_vars]}
 
@@ -502,6 +535,7 @@
   
   @{thm [display,indent=10] fresh_star_def[no_vars]}
 
+
   \noindent
   A striking consequence of these definitions is that we can prove
   without knowing anything about the structure of @{term x} that
@@ -511,7 +545,7 @@
 
   \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 
+  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}
 
@@ -524,7 +558,7 @@
   
   \noindent
   are equal. The lemma is then by application of the second permutation 
-  property shown in \eqref{newpermprops}.\hfill\qed
+  property shown in~\eqref{newpermprops}.\hfill\qed
   \end{proof}
 
   \begin{theorem}\label{swapfreshfresh}
@@ -554,18 +588,20 @@
   \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}"}}\\
+  & @{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}\\
+  & by Lemma~\ref{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]}
+  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}
   & by \eqref{permuteequ}\\
+   @{text "\<equiv>"}
+  & @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}
   \end{tabular}
   \end{isabelle}\hfill\qed
   \end{proof}
@@ -583,29 +619,54 @@
   
   \noindent
   is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and 
-  the logical connectives are equivariant.
+  the logical connectives are equivariant. ??? Equivariance
+
+  A simple consequence of the definition of support and equivariance is that 
+  if a function @{text f} is equivariant then we have 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm  (concl) supp_fun_eqvt[no_vars]}
+  \end{tabular}\hfill\numbered{suppeqvtfun}
+  \end{isabelle} 
+
+  \noindent 
+  For function applications we can establish the two following properties.
+
+  \begin{lemma} Let @{text f} and @{text x} be of permutation type, then
+  \begin{isabelle}
+  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}
+  @{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\
+  @{text "ii)"} & @{thm supp_fun_app[no_vars]}\\
+  \end{tabular}
+  \end{isabelle}
+  \end{lemma}
+
+  \begin{proof}
+  ???
+  \end{proof}
+
 
   While the abstract properties of support and freshness, particularly 
   Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, 
   one often has to calculate the support of some concrete object. This is 
   straightforward for example for booleans, nats, products and lists:
 
-  \begin{equation}
-  \mbox{
-  \begin{tabular}{@ {}r@ {\hspace{2mm}}l}
+  \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{equation}
+  \end{tabular}
+  \end{isabelle}
 
   \noindent
   But establishing the support of atoms and permutations is a bit 
   trickier. To do so we will use the following notion about a \emph{supporting set}.
   
-  \begin{definition}
+  \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}
@@ -644,7 +705,7 @@
   \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)"} 
+  permutations we found  the following `optimised' variant of @{text "iii)"} 
   more useful:
 
   \begin{lemma}\label{optimised} Let @{text x} be of permutation type.
@@ -729,22 +790,18 @@
   booleans are instances of this type class. 
 
   Unfortunately, this does not work for sets or Isabelle/HOL's function
-  type.\footnote{Isabelle/HOL takes the type @{text "\<alpha> set"} as an abbreviation
-  of @{text "\<alpha> \<Rightarrow> bool"}.}  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:
+  type. There are functions and sets definable in Isabelle/HOL for which the
+  finite support property does not hold.  A simple example of a function with
+  infinite support is @{const nat_of} shown in \eqref{sortnatof}.  This
+  function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. 
+  To establish this we show
+  @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term
+  "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a
+  contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons>
+  b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use
+  Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term
+  "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of =
+  nat_of"}.  Now we can reason as follows:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}
@@ -757,28 +814,68 @@
   \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.
+  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 {*
-  As shown above, sets is one instance of a type that is not generally finitely supported. 
-  However, we can easily show that finite sets of atoms are finitely
+  Also the set type is one instance whose elements are not generally finitely 
+  supported (we will give an example in Section~\ref{concrete}). 
+  However, we can easily show that finite sets and co-finite sets of atoms are finitely
   supported, because their support can be characterised as:
 
-  \begin{lemma}\label{finatomsets}
-  If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
+  \begin{lemma}\label{finatomsets}\mbox{}\\
+  @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\
+  @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then 
+  @{thm (concl) supp_cofinite_atom_set[no_vars]}.
   \end{lemma}
 
   \begin{proof}
-  finite-supp-unique
+  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. 
+  supported objects are finitely supported. For this we first show that
+  the union of the suports of finitely many and finitely supported  objects 
+  is finite, namely
+
+  \begin{lemma}\label{unionsupp}
+  If @{text S} is a finite set whose elements are all finitely supported, then\\
+  @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\
+  @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}.
+  \end{lemma}
+
+  \begin{proof}
+  The first part is by a straightforward induction on the finiteness of @{text S}. 
+  For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which
+  by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"}
+  that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be
+  \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}.
+  Since @{text "f"} is an equivariant function, we have that 
+  @{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed
+  \end{proof}
+
+  \noindent
+  With this lemma in place we can establish that
+
+  \begin{lemma}
+  @{thm[mode=IfThen] supp_of_finite_sets[no_vars]}
+  \end{lemma}
+
+  \begin{proof}
+  The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion 
+  in the other direction we have to show Lemma~\ref{supports}.@{text "i)"}
+  \end{proof}
 *}
 
 
@@ -1011,7 +1108,7 @@
 *}
 
 
-section {* Concrete Atom Types *}
+section {* Concrete Atom Types\label{concrete} *}
 
 text {*
 
@@ -1147,11 +1244,25 @@
 
 
 
-section {* Related Work *}
+section {* Related Work\label{related} *}
 
 text {*
   Add here comparison with old work.
 
+    Using a single atom type to represent atoms of different sorts and
+  representing permutations as functions are not new ideas; see
+  \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
+  of this paper is to show an example of how to make better theorem proving
+  tools by choosing the right level of abstraction for the underlying
+  theory---our design choices take advantage of Isabelle's type system, type
+  classes and reasoning infrastructure.  The novel technical contribution is a
+  mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and
+  HOL-based languages \cite{PittsHOL4} where variables and variable binding
+  depend on type annotations.
+
+  The paper is organised as follows\ldots
+
+
   The main point is that the above reasoning blends smoothly with the reasoning
   infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
   type class suffices. 




