67   At its core Nominal Isabelle is based on the nominal logic work by Pitts at

    67   At its core Nominal Isabelle is based on the nominal logic work by

    68   al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a

    68   Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is

    69   sort-respecting permutation operation defined over a countably infinite

    69   a sort-respecting permutation operation defined over a countably

    70   collection of sorted atoms. The aim of this paper is to describe how to

    70   infinite collection of sorted atoms. The aim of this paper is to

    71   adapt this work so that it can be implemented in a theorem prover based

    71   describe how to adapt this work so that it can be implemented in a

    72   on Higher-Order Logic (HOL). For this we present the definition we made

    72   theorem prover based on Higher-Order Logic (HOL). For this we

    73   in the implementation and also review many proofs. There are a two main 

    73   present the definition we made in the implementation and also review

    74   design choices to be made. One is

    74   many proofs. There are a two main design choices to be made. One is

    75   how to represent sorted atoms. We opt here for a single unified atom type to

    75   how to represent sorted atoms. We opt here for a single unified atom

    76   represent atoms of different sorts. The other is how to present sort-respecting

    76   type to represent atoms of different sorts. The other is how to

    77   permutations. For them we use the standard technique of

    77   present sort-respecting permutations. For them we use the standard

    78   HOL-formalisations of introducing an appropriate substype of functions from 

    78   technique of HOL-formalisations of introducing an appropriate

    79   atoms to atoms.

    79   substype of functions from atoms to atoms.

    80 

   167   infinite collection of sorted atoms and sort-respecting permutations of atoms. 

   166   infinite collection of sorted atoms and sort-respecting permutations

   168   The atoms are used for representing variable names

   167   of atoms.  The atoms are used for representing variable names that

   169   that might be bound or free. Multiple sorts are necessary for being able to

   168   might be bound or free. Multiple sorts are necessary for being able

   170   represent different kinds of variables. For example, in the language Mini-ML

   169   to represent different kinds of variables. For example, in the

   171   there are bound term variables in lambda abstractions and bound type variables in

   170   language Mini-ML there are bound term variables in lambda

   172   type schemes. In order to be able to separate them, each kind of variables needs to be

   171   abstractions and bound type variables in type schemes. In order to

   173   represented by a different sort of atoms. 

   172   be able to separate them, each kind of variables needs to be

   174 

   173   represented by a different sort of atoms.

   175   The existing nominal logic work usually leaves implicit

   174 

   176   the sorting information for atoms and as far as we know leaves out a

   175 

   177   description of how sorts are represented.  In our formalisation, we

   176   The existing nominal logic work usually leaves implicit the sorting

   178   therefore have to make a design decision about how to implement sorted atoms

   177   information for atoms and leaves out a description of how sorts are

   179   and sort-respecting permutations. One possibility, which we described in

   178   represented.  In our formalisation, we therefore have to make a

   180   \cite{Urban08}, is to have separate types for the different sorts of

   179   design decision about how to implement sorted atoms and

   181   atoms. However, we found that this does not blend well with type-classes in

   180   sort-respecting permutations. One possibility, which we described in

   182   Isabelle/HOL (see Section~\ref{related} about related work).  Therefore we use here a

   181   \cite{Urban08}, is to have separate types for different sorts of

   183   single unified atom type to represent atoms of different sorts. A basic

   182   atoms. However, we found that this does not blend well with

   184   requirement is that there must be a countably infinite number of atoms of

   183   type-classes in Isabelle/HOL (see Section~\ref{related} about

   185   each sort.  This can be implemented as the datatype

   184   related work).  Therefore we use here a single unified atom type to

   185   represent atoms of different sorts. A basic requirement is that

   186   there must be a countably infinite number of atoms of each sort.

   187   This can be implemented as the datatype

   333   

   335   A \emph{permutation operation}, written @{text "\<pi> \<bullet> x"}, applies a permutation 

   334   A permutation operation, written @{text "\<pi> \<bullet> x"}, applies a permutation 

   336   @{text "\<pi>"} to an object @{text "x"} of type @{text \<beta>}, say. 

   335   @{text "\<pi>"} to an object @{text "x"}. This operation has the generic type

   337   This operation has the type

   342   and Isabelle/HOL will allow us to give a definition of this operation for

   344   Isabelle/HOL will allow us to give a definition of this operation for

   343   `base' types, such as booleans and atoms, and for type-constructors, such as 

   345   `base' types, such as atoms, permutations, booleans and natural numbers, 

   344   products and lists. In order to reason abstractly about this operation, 

   346   and for type-constructors, such as functions, sets, lists and products. 

   347 

   348   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   349   \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}

   350   atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\

   351   permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\

   352   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   353   nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   354   functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\

   355   sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   356   lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   357          & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   358   products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   359   \end{tabular}\hfill\numbered{permdefs}

   360   \end{isabelle}

   361 

   362   In order to reason abstractly about this operation, 

   356   The use of type classes allows us to delegate much of the routine resoning involved in 

   374   From these properties and the laws about groups follows that a 

   357   determining whether these properties are satisfied to Isabelle/HOL's type system:

   375   permutation and its inverse cancel each other. That is

   358   we only have to establish that base types satisfy them and that type-constructors

   376 

   359   preserve them. Isabelle/HOL will use this information and determine whether

   360   an object @{text x} with a compound type satisfies the permutation properties.

   361   For this we define the notion of a \emph{permutation type}:

   362 

   363   \begin{definition}[Permutation type]

   364   A type @{text "\<beta>"} is a \emph{permutation type} if the permutation

   365   properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type

   366   @{text "\<beta>"}.  

   367   \end{definition}

   368 

   369   \noindent

   370   The type classes also allows us to establish generic lemmas involving the

   371   permutation operation. First, it follows from the laws governing

   372   groups that a permutation and its inverse cancel each other.  That is, for any

   373   @{text "x"} of a permutation type:

   374 

   375   

   384   Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 

   385   Consequently, the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, 

   396   We can also show that the following property holds for any permutation type.

   397   We can also show that the following property holds for the permutation 

   398   operation.

   415   Next we define the permutation operation for some types:

   416   Note that the permutation operation for functions is defined so that

   416 

   417   we have for applications the property

   417   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   418 

   418   \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}

   419   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   419   atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\

   420   @{text "\<pi> \<bullet> (f x) ="}

   420   functions: &  @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\

   421   @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}

   421   permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\

   422   \hfill\numbered{permutefunapp}

   422   sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   423   \end{isabelle}

   423   booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   424 

   424   lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   425   \noindent

   425          & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   426   whenever the permutation properties hold for @{text x}. This property can

   426   products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   427   be easily shown by unfolding the permutation operation for functions on

   427   nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\

   428   the right-hand side, simplifying the beta-redex and eliminating the permutations

   428   \end{tabular}\hfill\numbered{permdefs}

   429   in front of @{text x} using \eqref{cancel}.

   429   \end{isabelle}

   430 

   430 

   431   The use of type classes allows us to delegate much of the routine

   432   resoning involved in determining whether the permutation properties

   433   are satisfied to Isabelle/HOL's type system: we only have to

   434   establish that base types satisfy them and that type-constructors

   435   preserve them. Isabelle/HOL will use this information and determine

   436   whether an object @{text x} with a compound type satisfies the

   437   permutation properties.  For this we define the notion of a

   438   \emph{permutation type}:

   439 

   440   \begin{definition}[Permutation type]

   441   A type @{text "\<beta>"} is a \emph{permutation type} if the permutation

   442   properties in \eqref{newpermprops} are satisfied for every @{text

   443   "x"} of type @{text "\<beta>"}.

   444   \end{definition}

   445  

   442   All statements are by unfolding the definitions of the permutation operations and simple 

   457   All statements are by unfolding the definitions of the permutation

   443   calculations involving addition and minus. With permutations for example we 

   458   operations and simple calculations involving addition and

   444   have

   459   minus. With permutations for example we have

   472   An important notion in the nominal logic work is \emph{equivariance}.

   475   An important notion in the nominal logic work is

   473   An equivariant function is one that is invariant under the

   476   \emph{equivariance}.  To give a definition for this notion, let us

   474   permutation operation. This notion can be defined

   477   define \emph{HOL-terms}. They are given by the grammar

   475   uniformly for all constants in HOL as follows:

   478 

   476 

   479   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   480   @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}

   481   \hfill\numbered{holterms}

   482   \end{isabelle} 

   483 

   484   \noindent

   485   whereby @{text c} stands for constants and @{text x} for

   486   variables. We assume HOL-terms are fully typed, but for the sake of

   487   greater legibility we leave the typing information implicit.  We

   488   also assume the usual notions for free and bound variables of a

   489   HOL-term.

   490 

   491   An equivariant HOL-term is one that is invariant under the

   492   permutation operation. This notion can be defined as follows:

   479   A constant @{text c} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> c = c"}.

   495   A HOL-term @{text t} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> t = t"}.

   483   There are a number of equivalent formulations for the equivariance property. 

   499   There are a number of equivalent formulations for the equivariance

   484   For example, assuming @{text c} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance 

   500   property.  For example, assuming @{text t} is of type @{text "\<alpha> \<Rightarrow>

   485   can also be stated as 

   501   \<beta>"}, then equivariance can also be stated as

   489   @{text "\<forall>\<pi> x.  \<pi> \<bullet> (c x) = c (\<pi> \<bullet> x)"}

   505   @{text "\<forall>\<pi> x.  \<pi> \<bullet> (t x) = t (\<pi> \<bullet> x)"}

   494   To see that this formulation implies the definition, we just unfold the

   510   To see that this formulation implies the definition, we just unfold

   495   definition of the permutation operation for functions and simplify with the equation

   511   the definition of the permutation operation for functions and

   496   and the cancellation property shown in \eqref{cancel}. To see the other direction, we use 

   512   simplify with the equation and the cancellation property shown in

   497   \eqref{permutefunapp}. Similarly for functions with more than one argument. 

   513   \eqref{cancel}. To see the other direction, we use

   498 

   514   \eqref{permutefunapp}. Similarly for HOL-terms that take more than

   499   Both formulations of equivariance have their advantages and disadvantages:

   515   one argument.

   500   \eqref{altequivariance} is usually easier to establish, since statements are

   516 

   501   commonly given in a form where functions are fully applied. For example we

   517   Both formulations of equivariance have their advantages and

   502   can easily show that equality is equivariant

   518   disadvantages: \eqref{altequivariance} is usually easier to

   519   establish, since statements in Isabelle/HOL are commonly given in a

   520   form where functions are fully applied. For example we can easily

   521   show that equality is equivariant

   511   using the permutation operation on booleans and property \eqref{permuteequ}. 

   530   using the permutation operation on booleans and property

   512   Lemma~\ref{permutecompose} establishes that the permutation operation is 

   531   \eqref{permuteequ}.  Lemma~\ref{permutecompose} establishes that the

   513   equivariant. The permutation operation for lists and products, shown in \eqref{permdefs},

   532   permutation operation is equivariant. The permutation operation for

   514   state that the constructors for products, @{text "Nil"} and @{text Cons} are equivariant. Also

   533   lists and products, shown in \eqref{permdefs}, state that the

   515   the booleans @{const True} and @{const False} are equivariant by the permutation

   534   constructors for products, @{text "Nil"} and @{text Cons} are

   516   operation. Furthermore 

   535   equivariant. Furthermore a simple calculation will show that our 

   517   a simple calculation will show that our swapping functions are equivariant, that is

   536   swapping functions are equivariant, that is

   518   

   537 

   526   for all @{text a}, @{text b} and @{text \<pi>}. 

   545   for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans

   527   It is also easy to see that the boolean operators, like 

   546   @{const True} and @{const False} are equivariant by the definition

   528   @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. 

   547   of the permutation operation for booleans.  It is also easy to see

   529 

   548   that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text

   530   In contrast, the equation in Definition~\ref{equivariance} together with the permutation 

   549   "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.

   550 

   551   In contrast, the advantage of Definition \ref{equivariance} is that

   552   it leads to a simple rewrite system. Consider the following oriented

   553   versions

   554 

   555   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   556   \begin{tabular}{@ {}rcl}

   557   @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\

   558   @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\

   559   @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}\\

   560   \end{tabular}\hfill\numbered{swapeqvt}

   561   \end{isabelle}

   562   

   563   of the equations 

   564 

   565 

   566 together with the permutation 

   536   see this let us define \emph{HOL-terms}. They are given by the grammar

   572   see this let us 

   537 

   573 

   538   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   539   @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}

   540   \hfill\numbered{holterms}

   541   \end{isabelle} 

   542 

   543   \noindent

   544   whereby @{text c} stands for constants. We assume HOL-terms are fully typed, but 

   545   for the sake of greater legibility we leave the typing information implicit. 

   546   We also assume the usual notions for free and bound variables of a HOL-term.