159 

   159   Obstacles for Coq; no type-classes, difficulties with quotient types,

   160   need for classical reasoning

   191   This can be implemented as the datatype

   192   This can be implemented in Isabelle/HOL as the datatype

   293   permutations is that it is unique. For example the swappings

   297   permutations is that it is a unique representation. For example the swappings

   355   whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be 

   359   whereby @{text "\<beta>"} is a generic type for the object @{text

   356   given by in terms of `induction' over this generic type. The type-class mechanism

   360   x}.\footnote{We will use the standard notation @{text "((op \<bullet>) \<pi>)

   357   of Isabelle/HOL \cite{Wenzel04} allows us to give a definition for

   361   x"} for this operation in the few cases where we need to indicate

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

   362   that it is a function applied with two arguments.}  The definition

   363   of this operation will be given by in terms of `induction' over this

   364   generic type. The type-class mechanism of Isabelle/HOL

   365   \cite{Wenzel04} allows us to give a definition for `base' types,

   366   such as atoms, permutations, booleans and natural numbers:

   438   we have for applications the property

   446   we have for applications the equation

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

   455   provided the permutation properties hold for @{text x}. This equation can

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

   457   the right-hand side of the equation, simplifying the resulting beta-redex 

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

   458   and eliminating the permutations in front of @{text x} using \eqref{cancel}.

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

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

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

   465   whether an object @{text x} with a compound type, like @{typ "atom \<Rightarrow> (atom set * nat)"}, satisfies the

   461   \begin{definition}[Permutation type]

   469   \begin{definition}[Permutation Type]

   497   An important notion in the nominal logic work is

   505   Two important notions in the nominal logic work are what Pitts calls

   498   \emph{equivariance}.  This notion allows us to characterise how

   506   \emph{equivariance} and the \emph{equivariance principle}.  These

   499   permutations act upon compound statements in HOL by analysing how

   507   notions allows us to characterise how permutations act upon compound

   500   these statements are constructed.  To do so, let us first define

   508   statements in HOL by analysing how these statements are constructed.

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

   509   The notion of equivariance can defined as follows:

   502 

   503   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   505   \hfill\numbered{holterms}

   506   \end{isabelle} 

   507 

   508   \noindent

   509   where @{text c} stands for constants and @{text x} for

   510   variables. 

   511   We assume HOL-terms are fully typed, but for the sake of

   512   greater legibility we leave the typing information implicit.  We

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

   514   HOL-term.  Furthermore, it is custom in HOL to regard terms as equal

   515   modulo alpha-, beta- and eta-equivalence.

   516 

   517   An \emph{equivariant} HOL-term is one that is invariant under the

   518   permutation operation. This can be defined in Isabelle/HOL 

   519   as follows:

   522   A  HOL-term @{text t} is \emph{equivariant} provided 

   512   An object @{text "x"} of permutation type is \emph{equivariant} provided 

   523   @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.

   513   for all permutations @{text "\<pi>"}, \mbox{@{term "\<pi> \<bullet> x = x"}} holds.

   527   In what follows we will primarily be interested in the cases where @{text t} 

   517   In what follows we will primarily be interested in the cases where

   528   is a constant, but of course there is no way in Isabelle/HOL to restrict 

   518   @{text x} is a constant, but of course there is no way in

   529   this definition to just these cases.

   519   Isabelle/HOL to restrict this definition to just these cases.

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

   522   property.  For example, assuming @{text f} is a function of permutation 

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

   523   type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance can also be stated as

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

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

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

   537   \eqref{permutefunapp}. Similarly for functions that take more than

   549   applied form are (for permutation types) always interderivable.

   539   applied form are always interderivable (for permutation types).

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

   543   establish, since statements in HOL are commonly given in a

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

   572   of the permutation operation for booleans. Given this definition, it 

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

   573   is also easy to see that the boolean operators, like @{text "\<and>"}, 

   584   "\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have

   574   @{text "\<or>"}, @{text "\<longrightarrow>"} and  @{text "\<not>"} are equivariant:

   597   it leads to a relatively simple rewrite system that allows us to `push' a permutation

   586   it allows us to state a general principle how permutations act on

   598   towards the leaves of a HOL-term (i.e.~constants and

   587   statements in HOL.  For this we will define a rewrite system that

   599   variables).  Then the permutation disappears in cases where the

   588   `pushes' a permutation towards the leaves of statements (i.e.~constants

   600   constants are equivariant. We have implemented this rewrite system

   589   and variables).  Then the permutations disappear in cases where the

   601   as a simplification tactic on the ML-level of Isabelle/HOL.  Having this tactic 

   590   constants are equivariant.  To do so, let us first define

   602   at our disposal, together with a collection of constants for which 

   591   \emph{HOL-terms}, which are the building blocks of statements in HOL.

   603   equivariance is already established, we can automatically establish 

   592   They are given by the grammar

   604   equivariance of a constant for which equivariance is not yet known. For this we only have to 

   593 

   605   make sure that the definiens of this constant 

   594   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   606   is a HOL-term whose constants are all equivariant.  In what follows 

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

   607   we shall specify this tactic and argue that it terminates and 

   596   \hfill\numbered{holterms}

   608   is correct (in the sense of pushing a 

   597   \end{isabelle} 

   609   permutation @{text "\<pi>"} inside a term and the only remaining 

   598 

   610   instances of @{text "\<pi>"} are in front of the term's free variables). 

   599   \noindent

   611 

   600   where @{text c} stands for constants and @{text x} for variables.

   612   The simplifiaction tactic is a rewrite systems consisting of four `oriented' 

   601   We assume HOL-terms are fully typed, but for the sake of better

   613   equations. We will first give a naive version of this tactic, which however 

   602   legibility we leave the typing information implicit.  We also assume

   614   is in some cornercases incorrect and does not terminate, and then modify 

   603   the usual notions for free and bound variables of a HOL-term.

   615   it in order to obtain the desired properties. A permutation @{text \<pi>} can 

   604   Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-

   616   be pushed into applications and abstractions as follows

   605   and eta-equivalence. The equivariance principle can now be stated

   617 

   606   formally as follows:

   607 

   608   \begin{theorem}[Equivariance Principle]\label{eqvtprin}

   609   Suppose a HOL-term @{text t} whose constants are all equivariant. For any 

   610   permutation @{text \<pi>}, let @{text t'} be @{text t} except every 

   611   free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then 

   612   @{text "\<pi> \<bullet> t = t'"}.

   613   \end{theorem}

   614   

   615   \noindent

   616   The significance of this principle is that we can automatically establish

   617   the equivariance of a constant for which equivariance is not yet

   618   known. For this we only have to make sure that the definiens of this

   619   constant is a HOL-term whose constants are all equivariant. For example

   620   the universal quantifier @{text "\<forall>"} is definied in HOL as 

   621 

   622   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   623   @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}

   624   \end{isabelle} 

   625 

   626   \noindent

   627   The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="}

   628   and @{text "True"}, are equivariant (we shown this above). Therefore

   629   the equivariance principle gives us

   630 

   631   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   632   @{text "\<pi> \<bullet> (\<forall>x. P x)  \<equiv>  \<pi> \<bullet> (P = (\<lambda>x. True))  =  ((\<pi> \<bullet> P) = (\<lambda>x. True))  \<equiv>  \<forall>x. (\<pi> \<bullet> P) x"}

   633   \end{isabelle} 

   634 

   635   \noindent

   636   and consequently, the constant @{text "\<forall>"} must be equivariant. From this

   637   we can deduce that the existential quantifier @{text "\<exists>"} is equivariant. 

   638   Its definition in HOL is

   639 

   640   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   641   @{text "\<exists>x. P x \<equiv> "}~@{thm (rhs) Ex_def[no_vars]}

   642   \end{isabelle} 

   643 

   644   \noindent

   645   where again the HOL-term on the right-hand side only contains equivariant constants 

   646   (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). Taking both facts together, we can deduce that

   647   the unique existential quantifier @{text "\<exists>!"} is equivariant. Its definition 

   648   is

   649 

   650   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   651   @{text "\<exists>!x. P x \<equiv> "}~@{thm (rhs) Ex1_def[no_vars]}

   652   \end{isabelle} 

   653 

   654   \noindent

   655   with all constants on the right-hand side being equivariant. With this kind

   656   of reasoning we can build up a database of equivariant constants.

   657 

   658   Before we proceed, let us give a justification for the equivariance principle. 

   659   For this we will use a rewrite system consisting of a series of equalities 

   660   

   661   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   662   @{text "\<pi> \<cdot> t  =  ...  =  t'"}

   663   \end{isabelle}

   664   

   665   \noindent 

   666   that establish the equality between @{term "\<pi> \<bullet> t"} and

   667   @{text "t'"}. The idea of the rewrite system is to push the

   668   permutation inside the term @{text t}. We have implemented this as a

   669   conversion tactic on the ML-level of Isabelle/HOL.  In what follows,

   670   we will show that this tactic produces only finitely many equations

   671   and also show that is correct (in the sense of pushing a permutation

   672   @{text "\<pi>"} inside a term and the only remaining instances of @{text

   673   "\<pi>"} are in front of the term's free variables).  The tactic applies

   674   four `oriented' equations. We will first give a naive version of

   675   this tactic, which however in some cornercases produces incorrect

   676   results or does not terminate.  We then give a modification in order

   677   to obtain the desired properties.

   678 

   679   Consider the following oriented equations

   680   

   629   Once the permutations are pushed towards the leaves we need the

   697   Once the permutations are pushed towards the leaves, we need the

   634   iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & \rrh & @{term "x"}\\

   702   

   635   iv) &  @{term "\<pi> \<bullet> c"} & \rrh & 

   636             {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\

   644   \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}. Note

   710   \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}, where

   645   that we usually write this application using infix notation as

   711   we do not write the permutation operation infix, as usual, but

   646   @{text "\<pi> \<bullet> t"} and recall that by Lemma \ref{permutecompose} the

   712   as an application. Recall that we established in Lemma \ref{permutecompose} that the

   647   constant @{text "(op \<bullet>)"} is equivariant. Now consider the infinite

   713   constant @{text "(op \<bullet>)"} is equivariant and consider the infinite

   662   where the last step is again an instance of the first term, but it

   728   The last term is again an instance of rewrite rule {\it i}), but the term

   668   Another problem we have to avoid is that the rules {\it i)} and

   734   Another problem we have to avoid is that the rules {\it i)} and {\it

   669   {\it iii)} can `overlap'. For this note that

   735   iii)} can `overlap'. For this note that the term @{term "\<pi>

   670   the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to 

   736   \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to

   671   @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply rule {\it iii)} 

   737   which we can apply rule {\it iii)} in order to obtain @{term

   672   in order to obtain @{term "\<lambda>x. x"}, as is desired---there is no 

   738   "\<lambda>x. x"}, as is desired---there is no free variable in the original

   673   free variable in the original term and so the permutation should completely

   739   term and so the permutation should completely vanish. However, the

   674   vanish. However, the subterm @{text

   740   subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,

   675   "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term 

   741   the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi>

   676   @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using

   742   \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}.  Given our strategy we cannot

   677   {\it i)}.  Given our strategy we cannot apply rule {\it iii)} anymore and 

   743   apply rule {\it iii)} anymore and even worse the measure we will

   678   even worse the measure we will introduce shortly increased. On the

   744   introduce shortly increased. On the other hand, if we had started

   679   other hand, if we had started with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}

   745   with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"} where @{text \<pi>} and @{text

   680   where @{text \<pi>} and @{text x} are free variables, then we \emph{do}

   746   x} are free variables, then we \emph{do} want to apply rule {\it i)}

   681   want to apply rule  {\it i)} and not rule {\it iii)}. The latter 

   747   and not rule {\it iii)}. The latter would eliminate @{text \<pi>}

   682   would eliminate @{text \<pi>} completely. The problem is that rule {\it iii)}

   748   completely. The problem is that rule {\it iii)} should only apply to

   683   should only apply to instances where the variable is to bound; for free variables 

   749   instances where the variable is to bound; for free variables we want

   684   we want to use {\it ii)}. 

   750   to use {\it ii)}.  In order to distinguish these cases we have to

   685 

   751   maintain the information which variable is bound when inductively

   686   The problem is that in order to distinguish both cases when

   752   taking a term `apart'. This, unfortunately, does not mesh well with

   687   inductively taking a term `apart', we have to maintain the

   753   the way how conversion tactics are implemented in Isabelle/HOL.

   688   information which variable is bound. This, unfortunately, does not

   754 

   689   mesh well with the way how simplification tactics are implemented in

   755   Our remedy is to use a standard trick in HOL: we introduce a

   690   Isabelle/HOL. Our remedy is to use a standard trick in HOL: we

   756   separate definition for terms of the form @{text "(- \<pi>) \<bullet> x"},

   691   introduce a separate definition for terms of the form @{text "(- \<pi>)

   757   namely as

   692   \<bullet> x"}, namely as

   724   With the definition of the simplification tactic in place, we can

   789   With the rules of the conversions tactic in place, we can

   725   establish its correctness. The property we are after is that for for

   790   establish its correctness. The property we are after is that 

   726   a HOL-term @{text t} whose constants are all equivariant, the

   791   for a HOL-term @{text t} whose constants are all equivariant the 

   727   HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} with @{text "t'"}

   792   term \mbox{@{text "\<pi> \<bullet> t"}} is equal to @{text "t'"} with @{text "t'"}

   729   in @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls this

   794   in @{text t} is replaced by \mbox{@{text "\<pi> \<bullet> x"}}. Let us call

   730   property \emph{equivariance principle} (book ref ???). In our

   795   a variable @{text x} \emph{really free}, if it is free and not occuring

   731   setting the precise statement of this property is a slightly more

   796   in an unpermute, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.

   732   involved because of the fact that @{text unpermutes} needs to be

   797   We need the following technical notion characterising a \emph{@{text "\<pi>"}-proper} HOL-term

   733   treated specially.

   798 

   734   

   799   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   735   \begin{theorem}[Equivariance Principle]

   800   \begin{tabular}{@ {}ll}

   736   Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all

   801   $\bullet$ & variables and constants are @{text \<pi>}-proper,\\

   737   its constants are equivariant. For any permutation @{text \<pi>}, let @{text t'} 

   802   $\bullet$ & @{term "unpermute \<pi> x"} is @{text \<pi>}-proper,\\

   738   be the HOL-term @{text t} except every free variable @{text x} in @{term t} is 

   803   $\bullet$ & @{term "\<lambda>x. t"} is @{text \<pi>}-proper, if @{text t} is @{text \<pi>}-proper and @{text x} is 

   739   replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.

   804   really free in @{text t}, and\\

   740   \end{theorem}

   805   $\bullet$ & @{term "t\<^isub>1 t\<^isub>2"} is @{text \<pi>}-proper, if @{text "t\<^isub>1"} and @{text "t\<^isub>2"} are 

   741   

   806   @{text \<pi>}-proper.

   742 

   807   \end{tabular}

   743 

   808   \end{isabelle}

   744   With these definitions in place we can define the notion of an \emph{equivariant}

   809 

   745   HOL-term

   810   \begin{proof}[Theorem~\ref{eqvtprin}] We establish the property if @{text t} 

   746 

   811   is @{text \<pi>}-proper and only contains equivaraint constants, then 

   747   \begin{definition}[Equivariant HOL-term]

   812   @{text "\<pi> \<bullet> t = t'"} where @{text "t'"} is equal to @{text "t"} except all really

   748   A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, 

   813   free variables @{text x} are replaced by @{text "\<pi> \<bullet> x"}, and all semi-free variables 

   749   abstractions and equivariant constants only.

   814   @{text "unpermute \<pi> x"} by @{text "x"}. We establish this property by induction

   750   \end{definition}

   815   on the size of HOL-terms, counting terms like @{text "unpermuting \<pi> x"} as leafes,

   751   

   816   like variables and constants. The cases for variables, constants and @{text unpermutes}

   752   \noindent

   817   are routine. In the case of abstractions we have by induction hypothesis that 

   753   For equivariant terms we have

   818   @{text "\<pi> \<bullet> (t[x := unpermute \<pi> x]) = t'"} with @{text "t'"} satisfying our

   754 

   819   correctness property. This implies that @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x]) = \<lambda>x. t'"}

   755   \begin{lemma}

   820   and hence @{text "\<pi> \<bullet> (\<lambda>x. t) = \<lambda>x. t'"} as needed.\hfill\qed  

   756   For an equivariant HOL-term @{text "t"},  @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.

   821   \end{proof}

   757   \end{lemma}

   822 

   758 

   823   Pitts calls this property \emph{equivariance principle} (book ref ???). 

   759   Let us now see how to use the equivariance principle. We have 

   824   

   760 

   825   Problems with @{text undefined}

   826   

   827   Lines of code

   773   \begin{definition}[Support] Given @{text x} is of permutation type, then 

   840   \begin{definition}[Support] \label{support} 

   841   Given @{text x} is of permutation type, then 

   792 

   860   \noindent

   793   \noindent

   861   Using the equivariance principle, it can be easily checked that all three notions

   794   A striking consequence of these definitions is that we can prove

   862   are equivariant. A simple consequence of the definition of support and equivariance 

   795   without knowing anything about the structure of @{term x} that

   863   is that if @{text x} is equivariant then we have 

   796   swapping two fresh atoms, say @{text a} and @{text b}, leave 

   864 

   797   @{text x} unchanged. For the proof we use the following lemma 

   865   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   798   about swappings applied to an @{text x}:

   866   \begin{tabular}{@ {}l}

   867   @{thm  (concl) supp_fun_eqvt[where f="x", no_vars]}

   868   \end{tabular}\hfill\numbered{suppeqvtfun}

   869   \end{isabelle} 

   870 

   871   \noindent

   872   For function applications we can establish the following two properties.

   873 

   874   \begin{lemma}\label{suppfunapp} Let @{text f} and @{text x} be of permutation type, then

   875   \begin{isabelle}

   876   \begin{tabular}{r@ {\hspace{4mm}}p{10cm}}

   877   {\it i)} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\

   878   {\it ii)} & @{thm supp_fun_app[no_vars]}\\

   879   \end{tabular}

   880   \end{isabelle}

   881   \end{lemma}

   882 

   883   \begin{proof}

   884   For the first property, we know from the assumption that @{term

   885   "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}"} and @{term "finite {b . (a \<rightleftharpoons> b) \<bullet> x \<noteq>

   886   x}"} hold. That means for all, but finitely many @{text b} we have

   887   @{term "(a \<rightleftharpoons> b) \<bullet> f = f"} and @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. Similarly,

   888   we have to show that for but, but finitely @{text b} the equation

   889   @{term "(a \<rightleftharpoons> b) \<bullet> f x = f x"} holds. The left-hand side of this

   890   equation is equal to @{term "((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x)"} by

   891   \eqref{permutefunapp}, which we know by the previous two facts for

   892   @{text f} and @{text x} is equal to the right-hand side for all,

   893   but finitely many @{text b}. This establishes the first

   894   property. The second is a simple corollary of {\it i)} by

   895   unfolding the definition of freshness.\qed

   896   \end{proof}

   897 

   898   A striking consequence of the definitions for support and freshness

   899   is that we can prove without knowing anything about the structure of

   900   @{term x} that swapping two fresh atoms, say @{text a} and @{text

   901   b}, leave @{text x} unchanged. For the proof we use the following

   902   lemma about swappings applied to an @{text x}:

   815   property shown in~\eqref{newpermprops}.\hfill\qed

   919   property shown in~\eqref{newpermprops}.\qed

   906   one often has to calculate the support of some concrete object. This is 

   939   one often has to calculate the support of concrete objects.

   907   straightforward for example for booleans, nats, products and lists:

   940   For booleans, nats, products and lists it is easy to check that

   919   \noindent

   952   \noindent 

   920   But establishing the support of atoms and permutations is a bit 

   953   hold.  Establishing the support of atoms and permutations is a bit 

   948   For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a}

   981   For {\it i)} we derive a contradiction by assuming there is an atom @{text a}

   953   Property @{text "ii)"} is by a direct application of 

   986   Property {\it ii)} is by a direct application of 

   954   Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves

   987   Theorem~\ref{swapfreshfresh}. For the last property, part {\it i)} proves

   956   @{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed  

   989   {\it ii)} and the fact that @{term "supp x"} is finite by {\it i)}.\hfill\qed  

   962   permutations we found  the following `optimised' variant of @{text "iii)"} 

   995   permutations we found  the following `optimised' variant of {\it iii)} 

  1038   fresh atom with arbitrary sort. This is an important operation in Nominal

  1071   fresh atom with arbitrary sort. This is a crucial operation in Nominal

  1042   can define a type class for types where every element has finite support, and

  1075   can define a type class in Isabelle/HOL corresponding to the 

  1043   prove that the types @{term "atom"}, @{term "perm"}, lists, products and

  1076   property:

  1044   booleans are instances of this type class. 

  1077   

  1045 

  1078   \begin{definition}[Finitely Supported Type]

  1046   Unfortunately, this does not work for sets or Isabelle/HOL's function

  1079   A type @{text "\<beta>"} is \emph{finitely supported} if @{term "finite (supp x)"}

  1047   type. There are functions and sets definable in Isabelle/HOL for which the

  1080   holds for all @{text x} of type @{text "\<beta>"}.

  1048   finite support property does not hold.  A simple example of a function with

  1081   \end{definition}

  1049   infinite support is @{const nat_of} shown in \eqref{sortnatof}.  This

  1082  

  1050   function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. 

  1083   \noindent

  1051   To establish this we show

  1084   By the calculations above we can easily establish 

  1052   @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term

  1085 

  1053   "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a

  1086   \begin{theorem}\label{finsuptype} 

  1054   contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons>

  1087   The types @{type atom}, @{type perm}, @{type bool} and @{type nat}

  1055   b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use

  1088   are fintitely supported, and assuming @{text \<beta>}, @{text "\<beta>\<^isub>1"} and

  1056   Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term

  1089   @{text "\<beta>\<^isub>2"} are finitely supported types, then @{text "\<beta> list"} and

  1057   "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of =

  1090   @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"} are finitely supported.

  1058   nat_of"}.  Now we can reason as follows:

  1091   \end{theorem}

  1092 

  1093   \noindent

  1094   The main benefit of using the finite support property for choosing a

  1095   fresh atom is that the reasoning is `compositional'. To see this,

  1096   assume we have a list of atoms and a method of choosing a fresh atom

  1097   that is not a member in this list---for example the maximum plus

  1098   one.  Then if we enlarge this list \emph{after} the choice, then

  1099   obviously the fresh atom might not be fresh anymore. In contrast, by

  1100   the classical reasoning of Proposition~\ref{choosefresh} we know a

  1101   fresh atom exists for every list of atoms and no matter how we

  1102   extend this list of atoms, we always preserve the property of being

  1103   finitely supported. Consequently the existence of a fresh atom is

  1104   still guarantied by Proposition~\ref{choosefresh}.  Using the method

  1105   of `maximum plus one' we might have to adapt the choice of a fresh

  1106   atom.

  1107 

  1108   Unfortunately, Theorem~\ref{finsuptype} does not work in general for the

  1109   types of sets and functions.  There are functions definable in HOL

  1110   for which the finite support property does not hold.  A simple

  1111   example of a function with infinite support is @{const nat_of} shown

  1112   in \eqref{sortnatof}.  This function's support is the set of

  1113   \emph{all} atoms @{term "UNIV::atom set"}.  To establish this we

  1114   show @{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set

  1115   @{term "{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a

  1116   contradiction. From the assumption we also know that @{term "{a} \<union>

  1117   {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use

  1118   Proposition~\ref{choosefresh} to choose an atom @{text c} such that

  1119   @{term "c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c)

  1120   \<bullet> nat_of = nat_of"}.  Now we can reason as follows:

  1078   Also the set type is one instance whose elements are not generally finitely 

  1140   Also the set type is an instance whose elements are not generally finitely 

  1081   supported, because their support can be characterised as:

  1143   supported. Their support can be characterised as:

  1082 

  1144 

  1083   \begin{lemma}\label{finatomsets}\mbox{}\\

  1145   \begin{lemma}\label{finatomsets}

  1084   @{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\

  1146   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  1085   @{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then 

  1147   \begin{tabular}[b]{@ {}rl}

  1148   {\it i)} & If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\

  1149   {\it ii)} & If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then 

  1103   the union of the suports of finitely many and finitely supported  objects 

  1169   the union of the supports of finitely many and finitely supported  objects 

  1107   If @{text S} is a finite set whose elements are all finitely supported, then\\

  1173   If @{text S} is a finite set whose elements are all finitely supported, then

  1108   @{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\

  1174   %

  1109   @{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}.

  1175   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

  1176   \begin{tabular}[b]{@ {}rl}

  1177   {\it i)} & @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\

  1178   {\it ii)} & @{thm (concl) Union_included_in_supp[no_vars]}.

  1179   \end{tabular}

  1180   \end{isabelle}

  1113   The first part is by a straightforward induction on the finiteness of @{text S}. 

  1184   The first part is by a straightforward induction on the finiteness

  1114   For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which

  1185   of @{text S}.  For the second part, we know that @{term "\<Union>x\<in>S. supp

  1115   by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"}

  1186   x"} is a set of atoms, which by the first part is finite. Therefore

  1116   that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be

  1187   we know by Lemma~\ref{finatomsets}.{\it i)} that @{term "(\<Union>x\<in>S. supp

  1117   \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}.

  1188   x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be the function

  1118   Since @{text "f"} is an equivariant function, we have that 

  1189   \mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right-hand side

  1119   @{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed

  1190   as @{text "supp (f S)"}.  Since @{text "f"} is an equivariant

  1191   function (can be easily checked by the equivariance principle), we

  1192   have that @{text "supp (f S) \<subseteq> supp S"} by

  1193   Lemma~\ref{suppfunapp}.{\it ii)}. This completes the second

  1194   part.\hfill\qed

  1130   The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion 

  1205   The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.{\it ii)}. To show the inclusion 

  1131   in the other direction we have to show Lemma~\ref{supports}.@{text "i)"}

  1206   in the other direction we can use Lemma~\ref{supports}.{\it i)}. This means

  1207   for all @{text a} and @{text b} that are not in @{text S} we have to show that

  1208   @{term "(a \<rightleftharpoons> b) \<bullet> (\<Union>x \<in> S. supp x) = (\<Union>x \<in> S. supp x)"} holds. By the equivariance

  1209   principle, the left-hand side is equal to @{term "\<Union>x \<in> ((a \<rightleftharpoons> b) \<bullet> S). supp x"}. Now

  1210   the swapping in front of @{text S} disappears, since @{term "a \<sharp> S"} and @{term "b \<sharp> S"}

  1211   whenever @{text "a, b \<notin> S"}. Thus we are done.\hfill\qed

  1136 section {* Induction Principles *}

  1224 section {* Induction Principles for Permutations *}

  1140   representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and 

  1228   representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and

  1141   @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has 

  1229   @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation does

  1142   one draw back: it does not come readily with an induction principle. 

  1230   not come automatically with an induction principle.  Such an

  1143   Such an induction principle is handy for deriving properties like

  1231   induction principle is however handy for generalising

  1144   

  1232   Lemma~\ref{swapfreshfresh} from swappings to permutations

  1145   @{thm [display, indent=10] supp_perm_eq[no_vars]}

  1233   

  1146 

  1234   \begin{lemma}

  1147   \noindent

  1235   @{thm [mode=IfThen] perm_supp_eq[no_vars]}

  1148   However, it is not too difficult to derive an induction principle, 

  1236   \end{lemma}

  1149   given the fact that we allow only permutations with a finite domain. 

  1237 

  1238   \noindent

  1239   In this section we will establish an induction principle for permutations

  1240   with which this lemma can be easily proved. It is not too difficult to derive 

  1241   an induction principle for permutations, given the fact that we allow only 

  1242   permutations having a finite support. 

  1243 

  1244   Using a the property from \cite{???}

  1245 

  1246   \begin{lemma}\label{smallersupp}

  1247   @{thm [mode=IfThen] smaller_supp[no_vars]}

  1248   \end{lemma}

  1373   free atoms of \emph{all} sorts together; the flexibility offered by the new

  1472   free atoms of \emph{all} sorts together.

  1374   atom type makes this possible.  

  1379   means subgoals involving sorts must be discharged explicitly within proof

  1477   means for example that subgoals involving sorts must be discharged explicitly within proof

  1380   scripts, instead of being inferred by Isabelle/HOL's type checker.  In other

  1478   scripts, instead of being inferred automatically.  In other

  1436   \begin{tabular}{r@ {\hspace{3mm}}l}

  1534   \begin{tabular}{@ {}r@ {\hspace{3mm}}l}

  1437   i)   if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\

  1535   i)   & if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\

  1438   ii)  @{thm atom_eqvt[where p="\<pi>", no_vars]}\\

  1536   ii)  & @{thm atom_eqvt[where p="\<pi>", no_vars]}\\

  1439   iii) @{thm sort_of_atom_eq [no_vars]}

  1537   iii) & @{thm sort_of_atom_eq [no_vars]}

  1448   The whole point of defining the concrete atom type class was to let users

  1546   The whole point of defining the concrete atom type class is to let users