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