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

   355   whereby @{text "\<beta>"} is a generic type for the object @{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:

   447   whenever the permutation properties hold for @{text x}. This equation 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

   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 variables.

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

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

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

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

   514   and eta-equivalence.  Statements in HOL are HOL-terms of type @{text

   515   "bool"}.

   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

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

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

   596   it leads to rewrite system that allows us to

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

   597   `push' a permutation towards the leaves of a HOL-term

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

   598   (i.e.~constants and variables).  Then the permutation disappears in

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

   599   cases where the constants are equivariant. This can be stated more

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

   600   formally as the following \emph{equivariance principle}:

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

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

   592   They are given by the grammar

   593 

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

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

   596   \hfill\numbered{holterms}

   597   \end{isabelle} 

   598 

   599   \noindent

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

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

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

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

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

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

   606   formally as follows:

   604   permutation @{text \<pi>}, let @{text t'} be the HOL-term @{text t} except every 

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

   614   the universal quantifier @{text "All"}, also written @{text "\<forall>"}, is 

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

   615   of type @{text "(\<alpha> \<Rightarrow> bool) \<Rightarrow> bool"} and in HOL is definied as 

   621 

   616 

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

   617   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   618   @{thm All_def[no_vars]}

   622   Now @{text All} must be equivariant, because by the equivariance

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

   623   principle we only have to test whether the contants in the HOL-term

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

   624   @{thm (rhs) All_def[no_vars]}, namely @{text "="} and @{text

   629   the equivariance principle gives us

   625   "True"}, are equivariant. We shown this above. Taking all equations

   630 

   626   together, we can establish

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

   627 

   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"}

   628   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   633   where the equation in the `middle' is given by Theorem~\ref{eqvtprin}.

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

   634   As a consequence, the constant @{text "All"} is equivariant. Given this

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

   635   fact we can further show that the existential quantifier @{text Ex},

   638   Its definition in HOL is

   636   written also as @{text "\<exists>"}, is equivariant, since it is defined as

   639 

   637 

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

   638   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   639   @{thm Ex_def[no_vars]}

   643   and the HOL-term on the right-hand side contains equivariant constants only

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

   644   (namely @{text "\<forall>"} and @{text "\<longrightarrow>"}). In this way we can establish step by step 

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

   645   equivariance for constants in HOL. 

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

   646 

   648   is

   647   In order to establish Theorem~\ref{eqvtprin}, we use a rewrite system

   649 

   648   consisting of a series of equalities 

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

   649   

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

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

   652   \end{isabelle} 

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

   653 

   652   \end{isabelle}

   654   \noindent

   653   

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

   654   \noindent

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

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

   657 

   656   "t'"}.  We have implemented this rewrite system as a conversion

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

   657   tactic on the ML-level of Isabelle/HOL.

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

   658   We shall next specify this tactic and show that it terminates and is

   660   

   659   correct (in the sense of pushing a permutation @{text "\<pi>"} inside a

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

   660   term and the only remaining instances of @{text "\<pi>"} are in front of

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

   661   the term's free variables).  The tactic applies four `oriented'

   663   \end{isabelle}

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

   664   

   663   however in some cornercases produces incorrect resolts or does not

   665   \noindent 

   664   terminate.  We then give a modification it in order to obtain the

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

   665   desired properties. A permutation @{text \<pi>} can be pushed into

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

   666   applications and abstractions as follows

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

   667 

   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   

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

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

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

   702   

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

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

   694   \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

   695   that we usually write this application using infix notation as

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

   696   @{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

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

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

   712   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

   718   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

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

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

   720   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

   721   @{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

   722   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

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

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

   724   vanish. However, the subterm @{text

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

   725   "(- \<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>

   726   @{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

   727   {\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

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

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

   729   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

   730   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)}

   731   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>}

   732   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

   733   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

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

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

   735 

   751   maintain the information which variable is bound when inductively

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

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

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

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

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

   754 

   739   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

   740   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"},

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

   757   namely as

   742   \<bullet> x"}, namely as

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

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

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

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

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

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

   777   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'"}

   779   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

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

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

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

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

   782   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

   783   treated specially.

   798 

   784   

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

   785   

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

   786 

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

   787 

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

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

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

   789   HOL-term

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

   790 

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

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

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

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

   807   \end{tabular}

   793   abstractions and equivariant constants only.

   808   \end{isabelle}

   794   \end{definition}

   809 

   795   

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

   796   \noindent

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

   797   For equivariant terms we have

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

   798 

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

   799   \begin{lemma}

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

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

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

   801   \end{lemma}

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

   802 

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

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

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

   804 

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

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

   821   \end{proof}

   822 

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

   824   

   825   Problems with @{text undefined}

   826   

   827   Lines of code

   817   \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 

   836 

   860   \noindent

   837   \noindent

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

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

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

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

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

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

   864 

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

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

   842   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}:

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

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

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

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

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

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

   963   \noindent

   952   \noindent 

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

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

   992   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}

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

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

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

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

  1000   @{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  

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

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

  1082   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

  1086   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 

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

  1076   property:

  1088   booleans are instances of this type class. 

  1077   

  1089 

  1078   \begin{definition}[Finitely Supported Type]

  1090   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)"}

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

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

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

  1081   \end{definition}

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

  1082  

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

  1083   \noindent

  1095   To establish this we show

  1084   By the calculations above we can easily establish 

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

  1085 

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

  1086   \begin{theorem}\label{finsuptype} 

  1098   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}

  1099   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

  1100   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

  1101   "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.

  1102   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:

  1122   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 

  1125   supported, because their support can be characterised as:

  1143   supported. Their support can be characterised as:

  1126 

  1144 

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

  1145   \begin{lemma}\label{finatomsets}

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

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

  1129   @{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 

  1147   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 

  1151   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

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

  1174   %

  1153   @{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}

  1157   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

  1158   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

  1159   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

  1160   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

  1161   \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

  1162   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

  1163   @{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

  1174   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 

  1175   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

  1180 section {* Induction Principles *}

  1224 section {* Induction Principles for Permutations *}

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

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

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

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

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

  1230   not come automatically with an induction principle.  Such an

  1187   Such an induction principle is handy for deriving properties like

  1231   induction principle is however handy for generalising

  1188   

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

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

  1233   

  1190 

  1234   \begin{lemma}

  1191   \noindent

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

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

  1236   \end{lemma}

  1193   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}

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

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

  1418   atom type makes this possible.  

  1423   means subgoals involving sorts must be discharged explicitly within proof

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

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

  1478   scripts, instead of being inferred automatically.  In other

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

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

  1481   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]}\\

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

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

  1483   iii) @{thm sort_of_atom_eq [no_vars]}

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

  1492   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