(*<*)+
−
theory Paper+
−
imports "../Nominal/Nominal2_Base" +
−
        "../Nominal/Atoms" +
−
        "../Nominal/Nominal2_Abs"+
−
        "~~/src/HOL/Library/LaTeXsugar"+
−
begin+
−
+
−
abbreviation+
−
 UNIV_atom ("\<allatoms>")+
−
where+
−
 "UNIV_atom \<equiv> UNIV::atom set" +
−
+
−
notation (latex output)+
−
  sort_of ("sort _" [1000] 100) and+
−
  Abs_perm ("_") and+
−
  Rep_perm ("_") and+
−
  swap ("'(_ _')" [1000, 1000] 1000) and+
−
  fresh ("_ # _" [51, 51] 50) and+
−
  fresh_star ("_ #\<^sup>* _" [51, 51] 50) and+
−
  Cons ("_::_" [78,77] 73) and+
−
  supp ("supp _" [78] 73) and+
−
  uminus ("-_" [78] 73) and+
−
  atom ("|_|") and+
−
  If  ("if _ then _ else _" 10) and+
−
  Rep_name ("\<lfloor>_\<rfloor>") and+
−
  Abs_name ("\<lceil>_\<rceil>") and+
−
  Rep_var ("\<lfloor>_\<rfloor>") and+
−
  Abs_var ("\<lceil>_\<rceil>") and+
−
  sort_of_ty ("sort'_ty _") +
−
+
−
(* BH: uncomment if you really prefer the dot notation+
−
syntax (latex output)+
−
  "_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})")+
−
*)+
−
+
−
(* sort is used in Lists for sorting *)+
−
hide_const sort+
−
+
−
abbreviation+
−
  "sort \<equiv> sort_of"+
−
+
−
lemma infinite_collect:+
−
  assumes "\<forall>x \<in> S. P x" "infinite S"+
−
  shows "infinite {x \<in> S. P x}"+
−
using assms+
−
apply(subgoal_tac "infinite {x. x \<in> S}")+
−
apply(simp only: Inf_many_def[symmetric])+
−
apply(erule INFM_mono)+
−
apply(auto)+
−
done+
−
+
−
+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
  Nominal Isabelle provides a proving infratructure for convenient reasoning+
−
  about syntax involving binders, such as lambda terms or type schemes in Mini-ML:+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} +
−
  \end{isabelle}+
−
  +
−
  \noindent+
−
  At its core Nominal Isabelle is based on the nominal logic work by+
−
  Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is+
−
  a sort-respecting permutation operation defined over a countably+
−
  infinite collection of sorted atoms. +
−
+
−
+
−
+
−
  The aim of this paper is to+
−
  describe how we adapted this work so that it can be implemented in a+
−
  theorem prover based on Higher-Order Logic (HOL). For this we+
−
  present the definition we made in the implementation and also review+
−
  many proofs. There are a two main design choices to be made. One is+
−
  how to represent sorted atoms. We opt here for a single unified atom+
−
  type to represent atoms of different sorts. The other is how to+
−
  present sort-respecting permutations. For them we use the standard+
−
  technique of HOL-formalisations of introducing an appropriate+
−
  substype of functions from atoms to atoms.+
−
+
−
  The nominal logic work has been the starting point for a number of proving+
−
  infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by+
−
  Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban+
−
  and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very+
−
  general notion, called \emph{support}, for the `set of free variables, or+
−
  atoms, of an object' that applies not just to lambda terms and type schemes,+
−
  but also to sets, products, lists, booleans and even functions. The notion of support+
−
  is derived from the permutation operation defined over the +
−
  hierarchy of types. This+
−
  permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more+
−
  convenient for reasoning about syntax, in comparison to, say, arbitrary+
−
  renaming substitutions of atoms. One reason is that permutations are+
−
  bijective renamings of atoms and thus they can be easily `undone'---namely+
−
  by applying the inverse permutation. A corresponding inverse substitution +
−
  might not always exist, since renaming substitutions are in general only injective.  +
−
  Another reason is that permutations preserve many constructions when reasoning about syntax. +
−
  For example, suppose a typing context @{text "\<Gamma>"} of the form+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}+
−
  occur twice. Then validity of typing contexts is preserved under+
−
  permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for+
−
  all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary+
−
  renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. +
−
+
−
  Permutations also behave uniformly with respect to HOL's logic connectives. +
−
  Applying a permutation to a formula gives, for example +
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lcl}+
−
  @{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\+
−
  @{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This uniform behaviour can also be extended to quantifiers and functions. +
−
  Because of these good properties of permutations, we are able to automate +
−
  reasoning to do with \emph{equivariance}. By equivariance we mean the property +
−
  that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}+
−
  for all @{text "\<pi>"}. This will often simplify arguments involving support +
−
  of functions, since if they are equivariant then they have empty support---or+
−
  `no free atoms'.+
−
+
−
  There are a number of subtle differences between the nominal logic work by+
−
  Pitts and the formalisation we will present in this paper. One difference +
−
  is that our+
−
  formalisation is compatible with HOL, in the sense that we only extend+
−
  HOL by some definitions, withouth the introduction of any new axioms.+
−
  The reason why the original nominal logic work is+
−
  incompatible with HOL has to do with the way how the finite support property+
−
  is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set+
−
  in the FM-set-universe has finite support.  In nominal logic \cite{Pitts03},+
−
  the axioms (E3) and (E4) imply that every function symbol and proposition+
−
  has finite support. However, there are notions in HOL that do \emph{not}+
−
  have finite support (we will give some examples).  In our formalisation, we +
−
  will avoid the incompatibility of the original nominal logic work by not a+
−
  priory restricting our discourse to only finitely supported entities, rather+
−
  we will explicitly assume this property whenever it is needed in proofs. One+
−
  consequence is that we state our basic definitions not in terms of nominal+
−
  sets (as done for example in \cite{Pitts06}), but in terms of the weaker+
−
  notion of permutation types---essentially sets equipped with a ``sensible''+
−
  notion of permutation operation.+
−
+
−
+
−
+
−
  In the nominal logic woworkrk, the `new quantifier' plays a prominent role.+
−
  $\new$+
−
+
−
+
−
+
−
+
−
  Two binders+
−
+
−
  A preliminary version +
−
*}+
−
+
−
section {* Sorted Atoms and Sort-Respecting Permutations *}+
−
+
−
text {*+
−
  The two most basic notions in the nominal logic work are a countably+
−
  infinite collection of sorted atoms and sort-respecting permutations+
−
  of atoms.  The atoms are used for representing variable names that+
−
  might be bound or free. Multiple sorts are necessary for being able+
−
  to represent different kinds of variables. For example, in the+
−
  language Mini-ML there are bound term variables in lambda+
−
  abstractions and bound type variables in type schemes. In order to+
−
  be able to separate them, each kind of variables needs to be+
−
  represented by a different sort of atoms.+
−
+
−
+
−
  The existing nominal logic work usually leaves implicit the sorting+
−
  information for atoms and leaves out a description of how sorts are+
−
  represented.  In our formalisation, we therefore have to make a+
−
  design decision about how to implement sorted atoms and+
−
  sort-respecting permutations. One possibility, which we described in+
−
  \cite{Urban08}, is to have separate types for different sorts of+
−
  atoms. However, we found that this does not blend well with+
−
  type-classes in Isabelle/HOL (see Section~\ref{related} about+
−
  related work).  Therefore we use here a single unified atom type to+
−
  represent atoms of different sorts. A basic requirement is that+
−
  there must be a countably infinite number of atoms of each sort.+
−
  This can be implemented as the datatype+
−
+
−
*}+
−
+
−
          datatype atom\<iota> = Atom\<iota> string nat+
−
+
−
text {*+
−
  \noindent+
−
  whereby the string argument specifies the sort of the+
−
  atom.\footnote{A similar design choice was made by Gunter et al+
−
  \cite{GunterOsbornPopescu09} for their variables.}  The use of type+
−
  \emph{string} for sorts is merely for convenience; any countably+
−
  infinite type would work as well.  In what follows we shall write+
−
  @{term "UNIV::atom set"} for the set of all atoms.  We also have two+
−
  auxiliary functions for atoms, namely @{text sort} and @{const+
−
  nat_of} which are defined as+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+
−
  @{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\+
−
  @{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"}  & @{thm (rhs) nat_of.simps[no_vars]}+
−
  \end{tabular}\hfill\numbered{sortnatof}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  We clearly have for every finite set @{text S}+
−
  of atoms and every sort @{text s} the property:+
−
+
−
  \begin{proposition}\label{choosefresh}\mbox{}\\+
−
  @{text "For a finite set of atoms S, there exists an atom a such that+
−
  sort a = s and a \<notin> S"}.+
−
  \end{proposition}+
−
+
−
  For implementing sort-respecting permutations, we use functions of type @{typ+
−
  "atom => atom"} that are bijective; are the+
−
  identity on all atoms, except a finite number of them; and map+
−
  each atom to one of the same sort. These properties can be conveniently stated+
−
  in Isabelle/HOL for a function @{text \<pi>} as follows:+
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{r@ {\hspace{4mm}}l}+
−
  i)   & @{term "bij \<pi>"}\\+
−
  ii)  & @{term "finite {a. \<pi> a \<noteq> a}"}\\+
−
  iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"}+
−
  \end{tabular}\hfill\numbered{permtype}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  Like all HOL-based theorem provers, Isabelle/HOL allows us to+
−
  introduce a new type @{typ perm} that includes just those functions+
−
  satisfying all three properties. For example the identity function,+
−
  written @{term id}, is included in @{typ perm}. Also function composition, +
−
  written  \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's +
−
  inverse operator and written \mbox{@{text "inv _"}}, preserve the properties +
−
  (\ref{permtype}.@{text "i"}-@{text "iii"}). +
−
+
−
  However, a moment of thought is needed about how to construct non-trivial+
−
  permutations. In the nominal logic work it turned out to be most convenient+
−
  to work with swappings, written @{text "(a b)"}.  In our setting the+
−
  type of swappings must be+
−
+
−
  @{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"}+
−
+
−
  \noindent+
−
  but since permutations are required to respect sorts, we must carefully+
−
  consider what happens if a user states a swapping of atoms with different+
−
  sorts.  The following definition\footnote{To increase legibility, we omit+
−
  here and in what follows the @{term Rep_perm} and @{term "Abs_perm"}+
−
  wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation+
−
  not to be the full function space, but only those functions of type @{typ+
−
  perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.}+
−
+
−
+
−
  @{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"}+
−
+
−
  \noindent+
−
  does not work in general, because @{text a} and @{text b} may have different+
−
  sorts---in which case the function would violate property @{text iii} in \eqref{permtype}.  We+
−
  could make the definition of swappings partial by adding the precondition+
−
  @{term "sort a = sort b"}, which would mean that in case @{text a} and+
−
  @{text b} have different sorts, the value of @{text "(a b)"} is unspecified.+
−
  However, this looked like a cumbersome solution, since sort-related side+
−
  conditions would be required everywhere, even to unfold the definition.  It+
−
  turned out to be more convenient to actually allow the user to state+
−
  `ill-sorted' swappings but limit their `damage' by defaulting to the+
−
  identity permutation in the ill-sorted case:+
−
+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}rl}+
−
  @{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ +
−
   & \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ +
−
   & \hspace{3mm}@{text "else id"}+
−
  \end{tabular}\hfill\numbered{swapdef}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This function is bijective, the identity on all atoms except+
−
  @{text a} and @{text b}, and sort respecting. Therefore it is +
−
  a function in @{typ perm}. +
−
+
−
  One advantage of using functions as a representation for+
−
  permutations is that it is unique. For example the swappings+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm swap_commute[no_vars]}\hspace{10mm}+
−
  @{text "(a a) = id"}+
−
  \end{tabular}\hfill\numbered{swapeqs}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  are \emph{equal} and can be used interchangeably. Another advantage of the function +
−
  representation is that they form a (non-com\-mu\-ta\-tive) group provided we define+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+
−
  @{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} &+
−
  @{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & +
−
     @{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\+
−
  @{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} &+
−
  @{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} &+
−
     @{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}+
−
  \end{tabular}\hfill\numbered{groupprops}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  and verify the four simple properties+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\+
−
  ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}+
−
  iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}+
−
  iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]} +
−
  \end{tabular}\hfill\numbered{grouplaws}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The technical importance of this fact is that we can rely on+
−
  Isabelle/HOL's existing simplification infrastructure for groups, which will+
−
  come in handy when we have to do calculations with permutations.+
−
  Note that Isabelle/HOL defies standard conventions of mathematical notation+
−
  by using additive syntax even for non-commutative groups.  Obviously,+
−
  composition of permutations is not commutative in general; for example+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  But since the point of this paper is to implement the+
−
  nominal theory as smoothly as possible in Isabelle/HOL, we tolerate+
−
  the non-standard notation in order to reuse the existing libraries.+
−
+
−
  A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},+
−
  applies a permutation @{text "\<pi>"} to an object @{text "x"}.  This +
−
  operation has the type+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be +
−
  given by in terms of `induction' over this generic type. The type-class mechanism+
−
  of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for+
−
  `base' types, such as atoms, permutations, booleans and natural numbers:+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}+
−
  atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\+
−
  permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\+
−
  booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
  nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
  \end{tabular}\hfill\numbered{permdefsbase}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  and for type-constructors, such as functions, sets, lists and products:+
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}+
−
  functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\+
−
  sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
  lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
         & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
  products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\+
−
  \end{tabular}\hfill\numbered{permdefsconstrs}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The type classes also allow us to reason abstractly about the permutation operation. +
−
  For this we state the following two +
−
  \emph{permutation properties}: +
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}+
−
  i) & @{thm permute_zero[no_vars]}\\+
−
  ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]}+
−
  \end{tabular}\hfill\numbered{newpermprops}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  From these properties and law (\ref{grouplaws}.{\it iv}) about groups +
−
  follows that a permutation and its inverse cancel each other. That is+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm}+
−
  @{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]}+
−
  \end{tabular}\hfill\numbered{cancel}+
−
  \end{isabelle} +
−
  +
−
  \noindent+
−
  Consequently, the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, +
−
  which in turn implies the property+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]}+
−
  $\;$if and only if$\;$+
−
  @{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}.+
−
  \end{tabular}\hfill\numbered{permuteequ}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  We can also show that the following property holds for the permutation +
−
  operation.+
−
+
−
  \begin{lemma}\label{permutecompose} +
−
  @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.+
−
  \end{lemma}+
−
+
−
  \begin{proof} The proof is as follows:+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}+
−
  & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\+
−
  @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\+
−
  @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}  & by {\rm(\ref{newpermprops}.@{text "ii"})}\\+
−
  @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\+
−
  \end{tabular}\hfill\qed+
−
  \end{isabelle}+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Note that the permutation operation for functions is defined so that+
−
  we have for applications the property+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "\<pi> \<bullet> (f x) ="}+
−
  @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}+
−
  \hfill\numbered{permutefunapp}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  whenever the permutation properties hold for @{text x}. This property can+
−
  be easily shown by unfolding the permutation operation for functions on+
−
  the right-hand side, simplifying the beta-redex and eliminating the permutations+
−
  in front of @{text x} using \eqref{cancel}.+
−
+
−
  The main benefit of the use of type classes is that it allows us to delegate +
−
  much of the routine resoning involved in determining whether the permutation properties+
−
  are satisfied to Isabelle/HOL's type system: we only have to+
−
  establish that base types satisfy them and that type-constructors+
−
  preserve them. Isabelle/HOL will use this information and determine+
−
  whether an object @{text x} with a compound type satisfies the+
−
  permutation properties.  For this we define the notion of a+
−
  \emph{permutation type}:+
−
+
−
  \begin{definition}[Permutation type]+
−
  A type @{text "\<beta>"} is a \emph{permutation type} if the permutation+
−
  properties in \eqref{newpermprops} are satisfied for every @{text+
−
  "x"} of type @{text "\<beta>"}.+
−
  \end{definition}+
−
 +
−
  \noindent+
−
  and establish:+
−
+
−
  \begin{theorem}+
−
  The types @{type atom}, @{type perm}, @{type bool} and @{type nat}+
−
  are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text+
−
  "\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}},+
−
  @{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}.+
−
  \end{theorem}+
−
+
−
  \begin{proof}+
−
  All statements are by unfolding the definitions of the permutation+
−
  operations and simple calculations involving addition and+
−
  minus. In case of permutations for example we have+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}[b]{@ {}rcl}+
−
  @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\+
−
  @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\+
−
  & @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\+
−
  & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\+
−
  & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} +
−
  \end{tabular}\hfill\qed+
−
  \end{isabelle}+
−
  \end{proof}+
−
*}+
−
+
−
section {* Equivariance *}+
−
+
−
text {*+
−
  An important notion in the nominal logic work is+
−
  \emph{equivariance}.  It will enable us to characterise how+
−
  permutations act upon compound statements in HOL by analysing how+
−
  these statements are constructed.  To do so, let us first define+
−
  \emph{HOL-terms}. They are given by the grammar+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}+
−
  \hfill\numbered{holterms}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  where @{text c} stands for constants and @{text x} for+
−
  variables. +
−
  We assume HOL-terms are fully typed, but for the sake of+
−
  greater legibility we leave the typing information implicit.  We+
−
  also assume the usual notions for free and bound variables of a+
−
  HOL-term.  Furthermore, it is custom in HOL to regard terms as equal+
−
  modulo alpha-, beta- and eta-equivalence.+
−
+
−
  An \emph{equivariant} HOL-term is one that is invariant under the+
−
  permutation operation. This can be defined in Isabelle/HOL +
−
  as follows:+
−
+
−
  \begin{definition}[Equivariance]\label{equivariance}+
−
  A  HOL-term @{text t} is \emph{equivariant} provided +
−
  @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.+
−
  \end{definition}+
−
+
−
  \noindent+
−
  In what follows we will primarily be interested in the cases where @{text t} +
−
  is a constant, but of course there is no way in Isabelle/HOL to restrict +
−
  this definition to just these cases.+
−
+
−
  There are a number of equivalent formulations for the equivariance+
−
  property.  For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>+
−
  \<beta>"}, then equivariance can also be stated as+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{text "\<forall>\<pi> x.  \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"}+
−
  \end{tabular}\hfill\numbered{altequivariance}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  We will call this formulation of equivariance in \emph{fully applied form}.+
−
  To see that this formulation implies the definition, we just unfold+
−
  the definition of the permutation operation for functions and+
−
  simplify with the equation and the cancellation property shown in+
−
  \eqref{cancel}. To see the other direction, we use+
−
  \eqref{permutefunapp}. Similarly for HOL-terms that take more than+
−
  one argument. The point to note is that equivariance and equivariance in fully+
−
  applied form are (for permutation types) always interderivable.+
−
+
−
  Both formulations of equivariance have their advantages and+
−
  disadvantages: \eqref{altequivariance} is usually more convenient to+
−
  establish, since statements in Isabelle/HOL are commonly given in a+
−
  form where functions are fully applied. For example we can easily+
−
  show that equality is equivariant+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm eq_eqvt[where p="\<pi>", no_vars]}+
−
  \end{tabular}\hfill\numbered{eqeqvt}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  using the permutation operation on booleans and property+
−
  \eqref{permuteequ}. +
−
  Lemma~\ref{permutecompose} establishes that the+
−
  permutation operation is equivariant. The permutation operation for+
−
  lists and products, shown in \eqref{permdefsconstrs}, state that the+
−
  constructors for products, @{text "Nil"} and @{text Cons} are+
−
  equivariant. Furthermore a simple calculation will show that our+
−
  swapping functions are equivariant, that is+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm swap_eqvt[where p="\<pi>", no_vars]}+
−
  \end{tabular}\hfill\numbered{swapeqvt}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans+
−
  @{const True} and @{const False} are equivariant by the definition+
−
  of the permutation operation for booleans. It is easy to see+
−
  that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text+
−
  "\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lcl}+
−
  @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\+
−
  @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  by the definition of the permutation operation acting on booleans.+
−
  +
−
  In contrast, the advantage of Definition \ref{equivariance} is that+
−
  it leads to a relatively simple rewrite system that allows us to `push' a permutation+
−
  towards the leaves of a HOL-term (i.e.~constants and+
−
  variables).  Then the permutation disappears in cases where the+
−
  constants are equivariant. We have implemented this rewrite system+
−
  as a simplification tactic on the ML-level of Isabelle/HOL.  Having this tactic +
−
  at our disposal, together with a collection of constants for which +
−
  equivariance is already established, we can automatically establish +
−
  equivariance of a constant for which equivariance is not yet known. For this we only have to +
−
  make sure that the definiens of this constant +
−
  is a HOL-term whose constants are all equivariant.  In what follows +
−
  we shall specify this tactic and argue that it terminates and +
−
  is correct (in the sense of pushing a +
−
  permutation @{text "\<pi>"} inside a term and the only remaining +
−
  instances of @{text "\<pi>"} are in front of the term's free variables). +
−
+
−
  The simplifiaction tactic is a rewrite systems consisting of four `oriented' +
−
  equations. We will first give a naive version of this tactic, which however +
−
  is in some cornercases incorrect and does not terminate, and then modify +
−
  it in order to obtain the desired properties. A permutation @{text \<pi>} can +
−
  be pushed into applications and abstractions as follows+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}+
−
  i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\+
−
  ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\+
−
  \end{tabular}\hfill\numbered{rewriteapplam}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The first equation we established in \eqref{permutefunapp};+
−
  the second follows from the definition of permutations acting on functions+
−
  and the fact that HOL-terms are equal modulo beta-equivalence.+
−
  Once the permutations are pushed towards the leaves we need the+
−
  following two equations+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}+
−
  iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\+
−
  iv) &  @{term "\<pi> \<bullet> c"} & \rrh & +
−
            {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\+
−
  \end{tabular}\hfill\numbered{rewriteother}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  in order to remove permuations in front of bound variables and+
−
  equivariant constants.  Unfortunately, we have to be careful with+
−
  the rules {\it i)} and {\it iv}): they can lead to a loop whenever+
−
  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note+
−
  that we usually write this application using infix notation as+
−
  @{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the+
−
  constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite+
−
  reduction sequence+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}+
−
  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$+
−
  @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}+
−
  $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$+
−
  @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%+
−
  +
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  where the last step is again an instance of the first term, but it+
−
  is bigger.  To avoid this loop we need to apply our rewrite rule+
−
  using an `outside to inside' strategy.  This strategy is sufficient+
−
  since we are only interested of rewriting terms of the form @{term+
−
  "\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.+
−
+
−
  Another problem we have to avoid is that the rules {\it i)} and+
−
  {\it iii)} can `overlap'. For this note that+
−
  the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to +
−
  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply rule {\it iii)} +
−
  in order to obtain @{term "\<lambda>x. x"}, as is desired---there is no +
−
  free variable in the original term and so the permutation should completely+
−
  vanish. However, the subterm @{text+
−
  "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term +
−
  @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using+
−
  {\it i)}.  Given our strategy we cannot apply rule {\it iii)} anymore and +
−
  even worse the measure we will introduce shortly increased. On the+
−
  other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}+
−
  where @{text \<pi>} and @{text x} are free variables, then we \emph{do}+
−
  want to apply rule  {\it i)} and not rule {\it iii)}. The latter +
−
  would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}+
−
  should only apply to instances where the variable is to bound; for free variables +
−
  we want to use {\it ii)}. +
−
+
−
  The problem is that in order to distinguish both cases when+
−
  inductively taking a term `apart', we have to maintain the+
−
  information which variable is bound. This, unfortunately, does not+
−
  mesh well with the way how simplification tactics are implemented in+
−
  Isabelle/HOL. Our remedy is to use a standard trick in HOL: we+
−
  introduce a separate definition for terms of the form @{text "(- \<pi>)+
−
  \<bullet> x"}, namely as+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The point is that now we can formulate the rewrite rules as follows+
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}lrcl}+
−
  i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & +
−
    @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\+
−
  \multicolumn{4}{r}{\rm provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\+
−
  ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\+
−
  iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\+
−
  iv') &  @{term "\<pi> \<bullet> c"} & \rrh & @{term "c"}+
−
    \hspace{6mm}{\rm provided @{text c} is equivariant}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  and @{text unpermutes} are only generated in case of bound variables.+
−
  Clearly none of these rules overlap. Moreover, given our+
−
  outside-to-inside strategy, they terminate. To see this, notice that+
−
  the permutation on the right-hand side of the rewrite rules is+
−
  always applied to a smaller term, provided we take the measure consisting+
−
  of lexicographically ordered pairs whose first component is the size+
−
  of a term (counting terms of the form @{text "unpermute \<pi> x"} as+
−
  leaves) and the second is the number of occurences of @{text+
−
  "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.+
−
+
−
  With the definition of the simplification tactic in place, we can+
−
  establish its correctness. The property we are after is that for for+
−
  a HOL-term @{text t} whose constants are all equivariant, the+
−
  HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}+
−
  being equal to @{text t} except that every free variable @{text x}+
−
  in @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls this+
−
  property \emph{equivariance principle} (book ref ???). In our+
−
  setting the precise statement of this property is a slightly more+
−
  involved because of the fact that @{text unpermutes} needs to be+
−
  treated specially.+
−
  +
−
  \begin{theorem}[Equivariance Principle]+
−
  Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all+
−
  its constants are equivariant. For any permutation @{text \<pi>}, let @{text t'} +
−
  be the HOL-term @{text t} except every free variable @{text x} in @{term t} is +
−
  replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.+
−
  \end{theorem}+
−
  +
−
+
−
+
−
  With these definitions in place we can define the notion of an \emph{equivariant}+
−
  HOL-term+
−
+
−
  \begin{definition}[Equivariant HOL-term]+
−
  A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, +
−
  abstractions and equivariant constants only.+
−
  \end{definition}+
−
  +
−
  \noindent+
−
  For equivariant terms we have+
−
+
−
  \begin{lemma}+
−
  For an equivariant HOL-term @{text "t"},  @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.+
−
  \end{lemma}+
−
+
−
  Let us now see how to use the equivariance principle. We have +
−
+
−
*}+
−
+
−
+
−
section {* Support and Freshness *}+
−
+
−
text {*+
−
  The most original aspect of the nominal logic work of Pitts is a general+
−
  definition for `the set of free variables, or free atoms, of an object @{text "x"}'.  This+
−
  definition is general in the sense that it applies not only to lambda terms,+
−
  but to any type for which a permutation operation is defined +
−
  (like lists, sets, functions and so on). +
−
+
−
  \begin{definition}[Support] Given @{text x} is of permutation type, then +
−
  +
−
  @{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]}+
−
  \end{definition}+
−
+
−
  \noindent+
−
  (Note that due to the definition of swapping in \eqref{swapdef}, we do not+
−
  need to explicitly restrict @{text a} and @{text b} to have the same sort.)+
−
  There is also the derived notion for when an atom @{text a} is \emph{fresh}+
−
  for an @{text x} of permutation type, defined as+
−
  +
−
  @{thm [display,indent=10] fresh_def[no_vars]}+
−
+
−
  \noindent+
−
  We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms +
−
  defined as follows+
−
  +
−
  @{thm [display,indent=10] fresh_star_def[no_vars]}+
−
+
−
+
−
  \noindent+
−
  A striking consequence of these definitions is that we can prove+
−
  without knowing anything about the structure of @{term x} that+
−
  swapping two fresh atoms, say @{text a} and @{text b}, leave +
−
  @{text x} unchanged. For the proof we use the following lemma +
−
  about swappings applied to an @{text x}:+
−
+
−
  \begin{lemma}\label{swaptriple}+
−
  Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} +
−
  have the same sort, then \mbox{@{thm (prem 3) swap_rel_trans[no_vars]}} and +
−
  @{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  The cases where @{text "a = c"} and @{text "b = c"} are immediate.+
−
  For the remaining case it is, given our assumptions, easy to calculate +
−
  that the permutations+
−
+
−
  @{thm [display,indent=10] (concl) swap_triple[no_vars]}+
−
  +
−
  \noindent+
−
  are equal. The lemma is then by application of the second permutation +
−
  property shown in~\eqref{newpermprops}.\hfill\qed+
−
  \end{proof}+
−
+
−
  \begin{theorem}\label{swapfreshfresh}+
−
  Let @{text x} be of permutation type.+
−
  @{thm [mode=IfThen] swap_fresh_fresh[no_vars]}+
−
  \end{theorem}+
−
+
−
  \begin{proof}+
−
  If @{text a} and @{text b} have different sort, then the swapping is the identity.+
−
  If they have the same sort, we know by definition of support that both+
−
  @{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and  @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"}+
−
  hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} +
−
  that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, +
−
  that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. +
−
  Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed+
−
  \end{proof}+
−
  +
−
  \noindent+
−
  Two important properties that need to be established for later calculations is +
−
  that @{text "supp"} and freshness are equivariant. For this we first show that:+
−
+
−
  \begin{lemma}\label{half}+
−
  If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} +
−
  if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  \begin{isabelle}+
−
  \begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l}+
−
  & @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}\\ +
−
  @{text "\<equiv>"} & +
−
    @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}\\+
−
  @{text "\<Leftrightarrow>"}+
−
  & @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} +
−
  & since @{text "\<pi> \<bullet> _"} is bijective\\ +
−
  @{text "\<Leftrightarrow>"}+
−
  & @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"}+
−
  & by Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\+
−
  @{text "\<Leftrightarrow>"}+
−
  & @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}+
−
  & by \eqref{permuteequ}\\+
−
   @{text "\<equiv>"}+
−
  & @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}+
−
  \end{tabular}+
−
  \end{isabelle}\hfill\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Together with the definition of the permutation operation on booleans,+
−
  we can immediately infer equivariance of freshness: +
−
+
−
  @{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]}+
−
+
−
  \noindent+
−
  Now equivariance of @{text "supp"}, namely+
−
  +
−
  @{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]}+
−
  +
−
  \noindent+
−
  is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and +
−
  the logical connectives are equivariant. ??? Equivariance+
−
+
−
  A simple consequence of the definition of support and equivariance is that +
−
  if a function @{text f} is equivariant then we have +
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm  (concl) supp_fun_eqvt[no_vars]}+
−
  \end{tabular}\hfill\numbered{suppeqvtfun}+
−
  \end{isabelle} +
−
+
−
  \noindent +
−
  For function applications we can establish the two following properties.+
−
+
−
  \begin{lemma} Let @{text f} and @{text x} be of permutation type, then+
−
  \begin{isabelle}+
−
  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}+
−
  @{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\+
−
  @{text "ii)"} & @{thm supp_fun_app[no_vars]}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  ???+
−
  \end{proof}+
−
+
−
+
−
  While the abstract properties of support and freshness, particularly +
−
  Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, +
−
  one often has to calculate the support of some concrete object. This is +
−
  straightforward for example for booleans, nats, products and lists:+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}+
−
  @{text "booleans"}: & @{term "supp b = {}"}\\+
−
  @{text "nats"}:     & @{term "supp n = {}"}\\+
−
  @{text "products"}: & @{thm supp_Pair[no_vars]}\\+
−
  @{text "lists:"} & @{thm supp_Nil[no_vars]}\\+
−
                   & @{thm supp_Cons[no_vars]}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  But establishing the support of atoms and permutations is a bit +
−
  trickier. To do so we will use the following notion about a \emph{supporting set}.+
−
  +
−
  \begin{definition}[Supporting Set]+
−
  A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}+
−
  not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.+
−
  \end{definition}+
−
+
−
  \noindent+
−
  The main motivation for this notion is that we can characterise @{text "supp x"} +
−
  as the smallest finite set that supports @{text "x"}. For this we prove:+
−
+
−
  \begin{lemma}\label{supports} Let @{text x} be of permutation type.+
−
  \begin{isabelle}+
−
  \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}+
−
  i)    & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\+
−
  ii)   & @{thm[mode=IfThen] supp_supports[no_vars]}\\+
−
  iii)  & @{thm (concl) supp_is_least_supports[no_vars]}+
−
         provided @{thm (prem 1) supp_is_least_supports[no_vars]},+
−
         @{thm (prem 2) supp_is_least_supports[no_vars]}+
−
         and @{text "S"} is the least such set, that means formally,+
−
         for all @{text "S'"}, if @{term "finite S'"} and +
−
         @{term "S' supports x"} then @{text "S \<subseteq> S'"}.+
−
  \end{tabular}+
−
  \end{isabelle} +
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}+
−
  with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the +
−
  assumption that @{term "S supports x"} gives us that @{text S} is a superset of +
−
  @{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S}+
−
  being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption.+
−
  Property @{text "ii)"} is by a direct application of +
−
  Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves+
−
  one ``half'' of the claimed equation. The other ``half'' is by property +
−
  @{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed  +
−
  \end{proof}+
−
+
−
  \noindent+
−
  These are all relatively straightforward proofs adapted from the existing +
−
  nominal logic work. However for establishing the support of atoms and +
−
  permutations we found  the following `optimised' variant of @{text "iii)"} +
−
  more useful:+
−
+
−
  \begin{lemma}\label{optimised} Let @{text x} be of permutation type.+
−
  We have that @{thm (concl) finite_supp_unique[no_vars]}+
−
  provided @{thm (prem 1) finite_supp_unique[no_vars]},+
−
  @{thm (prem 2) finite_supp_unique[no_vars]}, and for+
−
  all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}+
−
  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite+
−
  set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will+
−
  assume that there is an atom @{text "a"} that is element of @{text S}, but+
−
  not @{text "S'"} and derive a contradiction.  Since both @{text S} and+
−
  @{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom+
−
  @{text b}, which has the same sort as @{text "a"} and for which we know+
−
  @{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and+
−
  we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x+
−
  = x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply+
−
  @{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the+
−
  contradiction.\hfill\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Using this lemma we only have to show the following three proof-obligations+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{4mm}}l}+
−
  i)   & @{term "{c} supports c"}\\+
−
  ii)  & @{term "finite {c}"}\\+
−
  iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"}+
−
  \end{tabular}+
−
  \end{isabelle} +
−
+
−
  \noindent+
−
  in order to establish that @{thm supp_atom[where a="c", no_vars]} holds.  In+
−
  Isabelle/HOL these proof-obligations can be discharged by easy+
−
  simplifications. Similar proof-obligations arise for the support of+
−
  permutations, which is+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{thm supp_perm[where p="\<pi>", no_vars]}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  The only proof-obligation that is +
−
  interesting is the one where we have to show that+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}.+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  For this we observe that +
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}rcl}+
−
  @{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} &+
−
  if and only if &+
−
  @{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  holds by a simple calculation using the group properties of permutations.+
−
  The proof-obligation can then be discharged by analysing the inequality+
−
  between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}.+
−
+
−
  The main point about support is that whenever an object @{text x} has finite+
−
  support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a +
−
  fresh atom with arbitrary sort. This is an important operation in Nominal+
−
  Isabelle in situations where, for example, a bound variable needs to be+
−
  renamed. To allow such a choice, we only have to assume that +
−
  @{text "finite (supp x)"} holds. For more convenience we+
−
  can define a type class for types where every element has finite support, and+
−
  prove that the types @{term "atom"}, @{term "perm"}, lists, products and+
−
  booleans are instances of this type class. +
−
+
−
  Unfortunately, this does not work for sets or Isabelle/HOL's function+
−
  type. There are functions and sets definable in Isabelle/HOL for which the+
−
  finite support property does not hold.  A simple example of a function with+
−
  infinite support is @{const nat_of} shown in \eqref{sortnatof}.  This+
−
  function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. +
−
  To establish this we show+
−
  @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term+
−
  "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a+
−
  contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons>+
−
  b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use+
−
  Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term+
−
  "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of =+
−
  nat_of"}.  Now we can reason as follows:+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l}+
−
  @{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\+
−
  & @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\+
−
  & @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\+
−
  \end{tabular}+
−
  \end{isabelle}+
−
  +
−
  \noindent+
−
  But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}.+
−
  This implies that atoms @{term a} and @{term c} must be equal, which clashes with our+
−
  assumption @{term "c \<noteq> a"} about how we chose @{text c}.\footnote{Cheney \cite{Cheney06} +
−
  gives similar examples for constructions that have infinite support.}+
−
*}+
−
+
−
section {* Support of Finite Sets *}+
−
+
−
text {*+
−
  Also the set type is one instance whose elements are not generally finitely +
−
  supported (we will give an example in Section~\ref{concrete}). +
−
  However, we can easily show that finite sets and co-finite sets of atoms are finitely+
−
  supported, because their support can be characterised as:+
−
+
−
  \begin{lemma}\label{finatomsets}\mbox{}\\+
−
  @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\+
−
  @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then +
−
  @{thm (concl) supp_cofinite_atom_set[no_vars]}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  Both parts can be easily shown by Lemma~\ref{optimised}.  We only have to observe+
−
  that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both+
−
  @{text a} and @{text b} are elements in @{text S} or both are not in @{text S}.+
−
  However if the sorts of a @{text a} and @{text b} agree, then the swapping will+
−
  change @{text S} if either of them is an element in @{text S} and the other is +
−
  not.\hfill\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Note that a consequence of the second part of this lemma is that +
−
  @{term "supp (UNIV::atom set) = {}"}.+
−
  More difficult, however, is it to establish that finite sets of finitely +
−
  supported objects are finitely supported. For this we first show that+
−
  the union of the suports of finitely many and finitely supported  objects +
−
  is finite, namely+
−
+
−
  \begin{lemma}\label{unionsupp}+
−
  If @{text S} is a finite set whose elements are all finitely supported, then\\+
−
  @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\+
−
  @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}.+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  The first part is by a straightforward induction on the finiteness of @{text S}. +
−
  For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which+
−
  by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"}+
−
  that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be+
−
  \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}.+
−
  Since @{text "f"} is an equivariant function, we have that +
−
  @{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  With this lemma in place we can establish that+
−
+
−
  \begin{lemma}+
−
  @{thm[mode=IfThen] supp_of_finite_sets[no_vars]}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion +
−
  in the other direction we have to show Lemma~\ref{supports}.@{text "i)"}+
−
  \end{proof}+
−
*}+
−
+
−
+
−
section {* Induction Principles *}+
−
+
−
text {*+
−
  While the use of functions as permutation provides us with a unique+
−
  representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and +
−
  @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has +
−
  one draw back: it does not come readily with an induction principle. +
−
  Such an induction principle is handy for deriving properties like+
−
  +
−
  @{thm [display, indent=10] supp_perm_eq[no_vars]}+
−
+
−
  \noindent+
−
  However, it is not too difficult to derive an induction principle, +
−
  given the fact that we allow only permutations with a finite domain. +
−
*}+
−
+
−
+
−
section {* An Abstraction Type *}+
−
+
−
text {*+
−
  To that end, we will consider+
−
  first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs+
−
  are intended to represent the abstraction, or binding, of the set of atoms @{text+
−
  "as"} in the body @{text "x"}.+
−
+
−
  The first question we have to answer is when two pairs @{text "(as, x)"} and+
−
  @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in+
−
  the notion of $\alpha$-equivalence that is \emph{not} preserved by adding+
−
  vacuous binders.) To answer this question, we identify four conditions: {\it (i)}+
−
  given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom+
−
  set"}}, then @{text x} and @{text y} need to have the same set of free+
−
  atoms; moreover there must be a permutation @{text p} such that {\it+
−
  (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but+
−
  {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,+
−
  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}+
−
  @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The+
−
  requirements {\it (i)} to {\it (iv)} can be stated formally as follows:+
−
  %+
−
  \begin{equation}\label{alphaset}+
−
  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}+
−
  \multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]+
−
              & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\+
−
  @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\+
−
  @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\+
−
  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ +
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  Note that this relation depends on the permutation @{text+
−
  "p"}; $\alpha$-equivalence between two pairs is then the relation where we+
−
  existentially quantify over this @{text "p"}. Also note that the relation is+
−
  dependent on a free-atom function @{text "fa"} and a relation @{text+
−
  "R"}. The reason for this extra generality is that we will use+
−
  $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In+
−
  the latter case, @{text R} will be replaced by equality @{text "="} and we+
−
  will prove that @{text "fa"} is equal to @{text "supp"}.+
−
+
−
  It might be useful to consider first some examples about how these definitions+
−
  of $\alpha$-equivalence pan out in practice.  For this consider the case of+
−
  abstracting a set of atoms over types (as in type-schemes). We set+
−
  @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we+
−
  define+
−
+
−
  \begin{center}+
−
  @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and+
−
  \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and+
−
  @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to+
−
  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to+
−
  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text+
−
  "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}+
−
  since there is no permutation that makes the lists @{text "[x, y]"} and+
−
  @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}+
−
  unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$+
−
  @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity+
−
  permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}+
−
  $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no+
−
  permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal+
−
  (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be+
−
  shown that all three notions of $\alpha$-equivalence coincide, if we only+
−
  abstract a single atom.+
−
+
−
  In the rest of this section we are going to introduce three abstraction +
−
  types. For this we define +
−
  %+
−
  \begin{equation}+
−
  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}+
−
  \end{equation}+
−
  +
−
  \noindent+
−
  (similarly for $\approx_{\,\textit{abs\_res}}$ +
−
  and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence +
−
  relations and equivariant.+
−
+
−
  \begin{lemma}\label{alphaeq} +
−
  The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$+
−
  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term+
−
  "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>+
−
  bs, p \<bullet> y)"} (similarly for the other two relations).+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have+
−
  a permutation @{text p} and for the proof obligation take @{term "-p"}. In case +
−
  of transitivity, we have two permutations @{text p} and @{text q}, and for the+
−
  proof obligation use @{text "q + p"}. All conditions are then by simple+
−
  calculations. +
−
  \end{proof}+
−
+
−
  \noindent+
−
  This lemma allows us to use our quotient package for introducing +
−
  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}+
−
  representing $\alpha$-equivalence classes of pairs of type +
−
  @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}+
−
  (in the third case). +
−
  The elements in these types will be, respectively, written as:+
−
+
−
  \begin{center}+
−
  @{term "Abs_set as x"} \hspace{5mm} +
−
  @{term "Abs_res as x"} \hspace{5mm}+
−
  @{term "Abs_lst as x"} +
−
  \end{center}+
−
+
−
  \noindent+
−
  indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will+
−
  call the types \emph{abstraction types} and their elements+
−
  \emph{abstractions}. The important property we need to derive is the support of +
−
  abstractions, namely:+
−
+
−
  \begin{theorem}[Support of Abstractions]\label{suppabs} +
−
  Assuming @{text x} has finite support, then\\[-6mm] +
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+
−
  %@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\+
−
  %@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\+
−
  %@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]}+
−
  \end{tabular}+
−
  \end{center}+
−
  \end{theorem}+
−
+
−
  \noindent+
−
  Below we will show the first equation. The others +
−
  follow by similar arguments. By definition of the abstraction type @{text "abs_set"} +
−
  we have +
−
  %+
−
  \begin{equation}\label{abseqiff}+
−
  %@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; +
−
  %@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  and also+
−
  %+
−
  \begin{equation}\label{absperm}+
−
  @{thm permute_Abs[no_vars]}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  The second fact derives from the definition of permutations acting on pairs +
−
  \eqref{permute} and $\alpha$-equivalence being equivariant +
−
  (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show +
−
  the following lemma about swapping two atoms in an abstraction.+
−
  +
−
  \begin{lemma}+
−
  %@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  This lemma is straightforward using \eqref{abseqiff} and observing that+
−
  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.+
−
  Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).+
−
  \end{proof}+
−
+
−
  \noindent+
−
  Assuming that @{text "x"} has finite support, this lemma together +
−
  with \eqref{absperm} allows us to show+
−
  %+
−
  \begin{equation}\label{halfone}+
−
  %@ {thm abs_supports(1)[no_vars]}+
−
  \end{equation}+
−
  +
−
  \noindent+
−
  which by Property~\ref{supportsprop} gives us ``one half'' of+
−
  Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish +
−
  it, we use a trick from \cite{Pitts04} and first define an auxiliary +
−
  function @{text aux}, taking an abstraction as argument:+
−
  %+
−
  \begin{center}+
−
  @{thm supp_set.simps[THEN eq_reflection, no_vars]}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  Using the second equation in \eqref{equivariance}, we can show that +
−
  @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =+
−
  (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. +
−
  This in turn means+
−
  %+
−
  \begin{center}+
−
  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}+
−
  \end{center}+
−
+
−
  \noindent+
−
  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,+
−
  we further obtain+
−
  %+
−
  \begin{equation}\label{halftwo}+
−
  %@ {thm (concl) supp_abs_subset1(1)[no_vars]}+
−
  \end{equation}+
−
+
−
  \noindent+
−
  since for finite sets of atoms, @{text "bs"}, we have +
−
  @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.+
−
  Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes +
−
  Theorem~\ref{suppabs}. +
−
+
−
  The method of first considering abstractions of the+
−
  form @{term "Abs_set as x"} etc is motivated by the fact that +
−
  we can conveniently establish  at the Isabelle/HOL level+
−
  properties about them.  It would be+
−
  laborious to write custom ML-code that derives automatically such properties +
−
  for every term-constructor that binds some atoms. Also the generality of+
−
  the definitions for $\alpha$-equivalence will help us in the next section. +
−
*}+
−
+
−
+
−
section {* Concrete Atom Types\label{concrete} *}+
−
+
−
text {*+
−
+
−
  So far, we have presented a system that uses only a single multi-sorted atom+
−
  type.  This design gives us the flexibility to define operations and prove+
−
  theorems that are generic with respect to atom sorts.  For example, as+
−
  illustrated above the @{term supp} function returns a set that includes the+
−
  free atoms of \emph{all} sorts together; the flexibility offered by the new+
−
  atom type makes this possible.  +
−
+
−
  However, the single multi-sorted atom type does not make an ideal interface+
−
  for end-users of Nominal Isabelle.  If sorts are not distinguished by+
−
  Isabelle's type system, users must reason about atom sorts manually.  That+
−
  means subgoals involving sorts must be discharged explicitly within proof+
−
  scripts, instead of being inferred by Isabelle/HOL's type checker.  In other+
−
  cases, lemmas might require additional side conditions about sorts to be true.+
−
  For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a,+
−
  b)"}} will only produce the expected result if we state the lemma in+
−
  Isabelle/HOL as:+
−
*}+
−
+
−
          lemma+
−
	    fixes a b :: "atom"+
−
	    assumes asm: "sort a = sort b"+
−
	    shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" +
−
          using asm by simp+
−
+
−
text {*+
−
  \noindent+
−
  Fortunately, it is possible to regain most of the type-checking automation+
−
  that is lost by moving to a single atom type.  We accomplish this by defining+
−
  \emph{subtypes} of the generic atom type that only include atoms of a single+
−
  specific sort.  We call such subtypes \emph{concrete atom types}.+
−
+
−
  The following Isabelle/HOL command defines a concrete atom type called+
−
  \emph{name}, which consists of atoms whose sort equals the string @{term+
−
  "''name''"}.+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This command automatically generates injective functions that map from the+
−
  concrete atom type into the generic atom type and back, called+
−
  representation and abstraction functions, respectively. We will write these+
−
  functions as follows:+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l@ {\hspace{10mm}}l}+
−
  @{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & +
−
  @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  With the definition @{thm permute_name_def [where p="\<pi>", THEN+
−
  eq_reflection, no_vars]}, it is straightforward to verify that the type +
−
  @{typ name} is a permutation type.+
−
+
−
  In order to reason uniformly about arbitrary concrete atom types, we define a+
−
  type class that characterises type @{typ name} and other similarly-defined+
−
  types.  The definition of the concrete atom type class is as follows: First,+
−
  every concrete atom type must be a permutation type.  In addition, the class+
−
  defines an overloaded function that maps from the concrete type into the+
−
  generic atom type, which we will write @{text "|_|"}.  For each class+
−
  instance, this function must be injective and equivariant, and its outputs+
−
  must all have the same sort, that is+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{r@ {\hspace{3mm}}l}+
−
  i)   if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\+
−
  ii)  @{thm atom_eqvt[where p="\<pi>", no_vars]}\\+
−
  iii) @{thm sort_of_atom_eq [no_vars]}+
−
  \end{tabular}\hfill\numbered{atomprops}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can+
−
  show that @{typ name} satisfies all the above requirements of a concrete atom+
−
  type.+
−
+
−
  The whole point of defining the concrete atom type class was to let users+
−
  avoid explicit reasoning about sorts.  This benefit is realised by defining a+
−
  special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha>+
−
  \<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type:+
−
+
−
  @{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]}+
−
+
−
  \noindent+
−
  As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping+
−
  operation works just like the generic swapping operation, but it does not+
−
  require any sort-checking side conditions---the sort-correctness is ensured by+
−
  the types!  For @{text "\<leftrightarrow>"} we can establish the following+
−
  simplification rule:+
−
+
−
  @{thm [display,indent=10] permute_flip_at[no_vars]} +
−
+
−
  \noindent+
−
  If we now want to swap the \emph{concrete} atoms @{text a} and @{text b}+
−
  in the pair @{term "(a, b)"} we can establish the lemma as follows:+
−
*}+
−
+
−
          lemma+
−
	    fixes a b :: "name"+
−
	    shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" +
−
	  by simp+
−
+
−
text {*+
−
  \noindent+
−
  There is no need to state an explicit premise involving sorts.+
−
+
−
  We can automate the process of creating concrete atom types, so that users +
−
  can define a new one simply by issuing the command +
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  \isacommand{atom\_decl}~~@{text "name"}+
−
  \end{tabular}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This command can be implemented using less than 100 lines of custom ML-code.+
−
  In comparison, the old version of Nominal Isabelle included more than 1000+
−
  lines of ML-code for creating concrete atom types, and for defining various+
−
  type classes and instantiating generic lemmas for them.  In addition to+
−
  simplifying the ML-code, the setup here also offers user-visible improvements:+
−
  Now concrete atoms can be declared at any point of a formalisation, and+
−
  theories that separately declare different atom types can be merged+
−
  together---it is no longer required to collect all atom declarations in one+
−
  place.+
−
*}+
−
+
−
+
−
+
−
section {* Related Work\label{related} *}+
−
+
−
text {*+
−
  Add here comparison with old work.+
−
+
−
    Using a single atom type to represent atoms of different sorts and+
−
  representing permutations as functions are not new ideas; see+
−
  \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution+
−
  of this paper is to show an example of how to make better theorem proving+
−
  tools by choosing the right level of abstraction for the underlying+
−
  theory---our design choices take advantage of Isabelle's type system, type+
−
  classes and reasoning infrastructure.  The novel technical contribution is a+
−
  mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and+
−
  HOL-based languages \cite{PittsHOL4} where variables and variable binding+
−
  depend on type annotations.+
−
+
−
  The paper is organised as follows\ldots+
−
+
−
+
−
  The main point is that the above reasoning blends smoothly with the reasoning+
−
  infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single+
−
  type class suffices. +
−
+
−
  With this+
−
  design one can represent permutations as lists of pairs of atoms and the+
−
  operation of applying a permutation to an object as the function+
−
+
−
+
−
  @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}+
−
+
−
  \noindent +
−
  where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type+
−
  of the objects on which the permutation acts. For atoms +
−
  the permutation operation is defined over the length of lists as follows+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}+
−
  @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\+
−
  @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & +
−
     $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ +
−
                    @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\+
−
                    @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$+
−
  \end{tabular}\hfill\numbered{atomperm}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and+
−
  @{text "b"}. For atoms with different type than the permutation, we +
−
  define @{text "\<pi> \<bullet> c \<equiv> c"}.+
−
+
−
  With the separate atom types and the list representation of permutations it+
−
  is impossible in systems like Isabelle/HOL to state an ``ill-sorted''+
−
  permutation, since the type system excludes lists containing atoms of+
−
  different type. However, a disadvantage is that whenever we need to+
−
  generalise induction hypotheses by quantifying over permutations, we have to+
−
  build quantifications like+
−
+
−
  @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}+
−
+
−
  \noindent+
−
  where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. +
−
  The reason is that the permutation operation behaves differently for +
−
  every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a+
−
  single quantification to stand for all permutations. Similarly, the +
−
  notion of support+
−
+
−
  @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}+
−
+
−
  \noindent+
−
  which we will define later, cannot be+
−
  used to express the support of an object over \emph{all} atoms. The reason+
−
  is that support can behave differently for each @{text+
−
  "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in+
−
  a statement that an object, say @{text "x"}, is finitely supported we end up+
−
  with having to state premises of the form+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}+
−
  \end{tabular}\hfill\numbered{fssequence}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  Because of these disadvantages, we will use in this paper a single unified atom type to +
−
  represent atoms of different sorts. Consequently, we have to deal with the+
−
  case that a swapping of two atoms is ill-sorted: we cannot rely anymore on+
−
  the type systems to exclude them. +
−
+
−
  We also will not represent permutations as lists of pairs of atoms (as done in+
−
  \cite{Urban08}).  Although an+
−
  advantage of this representation is that the basic operations on+
−
  permutations are already defined in Isabelle's list library: composition of+
−
  two permutations (written @{text "_ @ _"}) is just list append, and+
−
  inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just+
−
  list reversal, and another advantage is that there is a well-understood+
−
  induction principle for lists, a disadvantage is that permutations +
−
  do not have unique representations as lists. We have to explicitly identify+
−
  them according to the relation+
−
+
−
  +
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}l}+
−
  @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}+
−
  \end{tabular}\hfill\numbered{permequ}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  This is a problem when lifting the permutation operation to other types, for+
−
  example sets, functions and so on. For this we need to ensure that every definition+
−
  is well-behaved in the sense that it satisfies some+
−
  \emph{permutation properties}. In the list representation we need+
−
  to state these properties as follows:+
−
+
−
+
−
  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%+
−
  \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}+
−
  i) & @{text "[] \<bullet> x = x"}\\+
−
  ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\+
−
  iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}+
−
  \end{tabular}\hfill\numbered{permprops}+
−
  \end{isabelle}+
−
+
−
  \noindent+
−
  where the last clause explicitly states that the permutation operation has+
−
  to produce the same result for related permutations.  Moreover, +
−
  ``permutations-as-lists'' do not satisfy the group properties. This means by+
−
  using this representation we will not be able to reuse the extensive+
−
  reasoning infrastructure in Isabelle about groups.  Because of this, we will represent+
−
  in this paper permutations as functions from atoms to atoms. This representation+
−
  is unique and satisfies the laws of non-commutative groups.+
−
*}+
−
+
−
+
−
section {* Conclusion *}+
−
+
−
text {*+
−
  This proof pearl describes a new formalisation of the nominal logic work by+
−
  Pitts et al. With the definitions we presented here, the formal reasoning blends +
−
  smoothly with the infrastructure of the Isabelle/HOL theorem prover. +
−
  Therefore the formalisation will be the underlying theory for a +
−
  new version of Nominal Isabelle.+
−
+
−
  The main difference of this paper with respect to existing work on Nominal+
−
  Isabelle is the representation of atoms and permutations. First, we used a+
−
  single type for sorted atoms. This design choice means for a term @{term t},+
−
  say, that its support is completely characterised by @{term "supp t"}, even+
−
  if the term contains different kinds of atoms. Also, whenever we have to+
−
  generalise an induction so that a property @{text P} is not just established+
−
  for all @{text t}, but for all @{text t} \emph{and} under all permutations+
−
  @{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is+
−
  that permutations can now consist of multiple swapping each of which can+
−
  swap different kinds of atoms. This simplifies considerably the reasoning+
−
  involved in building Nominal Isabelle.+
−
+
−
  Second, we represented permutations as functions so that the associated+
−
  permutation operation has only a single type parameter. This is very convenient+
−
  because the abstract reasoning about permutations fits cleanly+
−
  with Isabelle/HOL's type classes. No custom ML-code is required to work+
−
  around rough edges. Moreover, by establishing that our permutations-as-functions+
−
  representation satisfy the group properties, we were able to use extensively +
−
  Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs +
−
  to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}.+
−
  An interesting point is that we defined the swapping operation so that a +
−
  swapping of two atoms with different sorts is \emph{not} excluded, like +
−
  in our older work on Nominal Isabelle, but there is no ``effect'' of such +
−
  a swapping (it is defined as the identity). This is a crucial insight+
−
  in order to make the approach based on a single type of sorted atoms to work.+
−
  But of course it is analogous to the well-known trick of defining division by +
−
  zero to return zero.+
−
+
−
  We noticed only one disadvantage of the permutations-as-functions: Over+
−
  lists we can easily perform inductions. For permutations made up from+
−
  functions, we have to manually derive an appropriate induction principle. We+
−
  can establish such a principle, but we have no real experience yet whether ours+
−
  is the most useful principle: such an induction principle was not needed in+
−
  any of the reasoning we ported from the old Nominal Isabelle, except+
−
  when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}.+
−
+
−
  Finally, our implementation of sorted atoms turned out powerful enough to+
−
  use it for representing variables that carry on additional information, for+
−
  example typing annotations. This information is encoded into the sorts. With+
−
  this we can represent conveniently binding in ``Church-style'' lambda-terms+
−
  and HOL-based languages. While dealing with such additional information in +
−
  dependent type-theories, such as LF or Coq, is straightforward, we are not +
−
  aware of any  other approach in a non-dependent HOL-setting that can deal +
−
  conveniently with such binders.+
−
 +
−
  The formalisation presented here will eventually become part of the Isabelle +
−
  distribution, but for the moment it can be downloaded from the +
−
  Mercurial repository linked at +
−
  \href{http://isabelle.in.tum.de/nominal/download}+
−
  {http://isabelle.in.tum.de/nominal/download}.\smallskip+
−
+
−
  \noindent+
−
  {\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan +
−
  Berghofer and Cezary Kaliszyk for their comments on earlier versions +
−
  of this paper. We are also grateful to the anonymous referee who helped us to+
−
  put the work into the right context.  +
−
*}+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−