391   From these properties and the laws about groups

   392   From these properties and law (\ref{grouplaws}.{\it iv}) about groups 

   392   (\ref{grouplaws}.{\it iv }) follows that a permutation and its inverse

   393   follows that a permutation and its inverse cancel each other. That is

   393   cancel each other. That is

   481   @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\

   481   @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\

   484   & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 

   484   & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\

   485   & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} 

   494   \emph{equivariance}.  In order to prove properties about this notion, 

   495   \emph{equivariance}.  It will enable us to characterise how

   495   let us first define \emph{HOL-terms}. They are given 

   496   permutations act upon compound statements in HOL by analysing how

   496   by the grammar

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

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

   504   whereby @{text c} stands for constant symbols, or short constants, and

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

   505   @{text x} for variables. We assume HOL-terms are fully typed, but for the

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

   506   sake of greater legibility we leave the typing information implicit.  We

   508   greater legibility we leave the typing information implicit.  We

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

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

   508   It is custom in HOL to regard terms equal modulo alpha-, beta- and 

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

   509   eta-equivalence.

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

   510 

   512 

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

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

   512   permutation operation. This notion can be defined in Isabelle/HOL 

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

   516   A  HOL-term @{text t} with permutation type is \emph{equivariant} provided 

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

   521   We will be mainly interested in the case where @{text t} is a constant, but

   523   We will primarily be interested in the cases where @{text t} is a constant, but

   522   of course there is no way to restrict this definition in Isabelle/HOL to just

   524   of course there is no way to restrict this definition in Isabelle/HOL so that it

   523   this case.  

   525   applies to just constants.  

   541   one argument.

   544   one argument. The point to note is that equivariance and equivariance in fully

   545   applied form are always interderivable.

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

   548   disadvantages: \eqref{altequivariance} is usually more convenient to

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

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

   575   "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)

   579   "\<not>"} and @{text "\<longrightarrow>"}, are all equivariant too. (see ??? intro)

   578   it leads to a simple rewrite system that allows us to `push' a

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

   579   permutation towards the leaves in a HOL-term (i.e.~constants and free

   583   say @{text \<pi>}, towards the leaves of a HOL-term (i.e.~constants and

   580   variables).  The permutation disappears in cases where the

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

   581   constants are equivariant. Given a database of equivariant constants, 

   585   constants are equivariant, since by Definition \ref{equivariance} we

   582   we can implement a decision procedure that helps to find out when

   586   have @{term "\<pi> \<bullet> c = c"}. What we will show next is that for a HOL-term

   583   a compound term is equivariant. A permutation @{text \<pi>} can be pushed into

   587   @{term t} containing only equivariant constants, a permutation can be pushed

   584   applications and abstractions in a HOL-term as follows

   588   inside this term and the only instances remaining are in front of

   589   the free variables of @{text t}. We can only show this by a meta-argument, 

   590   that means one we cannot formalise inside Isabelle/HOL. But we can invoke

   591   it in form of a tactic programmed on the ML-level of Isabelle/HOL.

   592   This tactic is a rewrite systems consisting of `oriented' equations. 

   593 

   594   A permutation @{text \<pi>} can be 

   595   pushed into applications and abstractions as follows

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

   599   i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ 

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

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

   601   ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\

   594   The first rewrite rule we established as equation in \eqref{permutefunapp};

   606   The first rule we established in \eqref{permutefunapp};

   596   and the fact that HOL-terms are considered equal modulo beta-reduction.

   608   and the fact that HOL-terms are equal modulo beta-equivalence.

   597   The inverse permutations that are introduced by the second rewrite rule

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

   598   can be removed using the additional rewrite rule

   610   following two rules

   599 

   611 

   600   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   612   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   601   \begin{tabular}{@ {}rcl}

   613   \begin{tabular}{@ {}lrcl}

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

   614   iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & $\stackrel{\rightharpoonup}{=}$ & @{term "x"}\\

   603   \end{tabular}\hfill\numbered{rewriteunpermute}

   615   iv) &  @{term "\<pi> \<bullet> c"} & $\stackrel{\rightharpoonup}{=}$ & 

   604   \end{isabelle}

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

   605 

   617   \end{tabular}\hfill\numbered{rewriteother}

   606   \noindent

   618   \end{isabelle}

   607   and permutations in front of equivariant constants can be removed by the

   619 

   608   rule

   620   \noindent

   609 

   621   in order to remove permuations in front of bound variables and equivariant constants.

   610   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   622   

   611   \begin{tabular}{@ {}rcl}

   623   In order to obtain a terminating rewrite system, we have to be

   612   @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}

   624   careful with rule ({\it i}). It can lead to a loop whenever

   613   \end{tabular}\hfill\numbered{rewriteconsts}

   625   \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "\<pi>' \<bullet> t'"}. Consider

   614   \end{isabelle}

   626   for example the infinite reduction sequence

   615 

   627 

   616 

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

   617   \noindent

   629   \begin{tabular}{@ {}l}

   618   By a meta-argument, that means one we cannot formalise inside

   630   @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\

   619   Isabelle/HOL, we can convince ourselves that the strategy of 

   631   @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\

   620   of first pushing a permutation inside a term using

   632   @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots$\\

   621   \eqref{rewriteapplam}, then removing permutation in front of bound

   633   \end{tabular}

   622   variables using \eqref{rewriteunpermute} and finally removing all

   634   \end{isabelle}

   623   permutations in front of equivariant constants must terminate: the

   635 

   624   size of the term gets smaller in \eqref{rewriteapplam} if we do not

   636   \noindent

   625   count the inverse permutations introduced by the second rewrite rule

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

   626   and there can only be finitely many bound variables in a term

   638   bigger (note that for the permutation operation we have that @{text

   627   (similarly equivariant constants), therefore only finitely many

   639   "\<pi> \<bullet> (op \<bullet>) = (op \<bullet>)"} since as shown in Lemma \ref{permutecompose}

   628   applications of \eqref{rewriteunpermute} and

   640   \mbox{@{text "(op \<bullet>)"}} is equivariant). In order to avoid this loop

   629   \eqref{rewriteconsts}. The only problem is that instances where

   641   we need to apply these rules using an `outside to inside' strategy.

   630   rules (\ref{rewriteapplam}.{\it i}) or rules

   642   This strategy is sufficient since we are only interested of rewriting

   631   \eqref{rewriteunpermute} apply `overlap' and potentially our measure

   643   terms of the form @{term "\<pi> \<bullet> t"}.

   632   increases.  Consider for example the term @{term "\<pi> \<bullet> (\<lambda>x. x)"},

   644 

   633   whose final reduct should just be \mbox{@{term "\<lambda>x. x"}}. Using

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

   634   (\ref{rewriteapplam}.{\it ii}), the term can reduce to @{term

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

   635   "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply \eqref{rewriteunpermute}

   647   the term @{term "\<pi> \<bullet>(\<lambda>x. x)"} reduces to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>

   636   in order to obtain the desired result.  However, the subterm term @{text "(-

   648   x"}, to which we can apply rule ({\it iii}) in order to obtain

   637   \<pi>) \<bullet> x"} is also an application (in fact three nested ones). Therefore

   649   @{term "\<lambda>x. x"}, as is desired.  However, the subterm term @{text

   638   @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"} can also rewrite 

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

   639   to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} to which we cannot apply 

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

   640   (\ref{rewriteapplam}.{\it i}) directly and even worse our measure 

   652   ({\it i}).  Now we cannot apply rule ({\it iii}) anymore and even

   641   increased. In order to distinguish situations where \eqref{rewriteconsts}

   653   worse the measure we will introduce shortly increases. On the

   642   should apply instead of  (\ref{rewriteapplam}.{\it i}) we use a standard

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

   643   trick in HOL. We introduce a separate definition for terms of the form

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

   644   @{text "(- \<pi>) \<bullet> x"}, namely as

   656   want to apply rule  ({\it i}), rather than rule ({\it iii}) which

   657   would eliminate @{text \<pi>} completely. This is a problem because we 

   658   want to keep the shape of the HOL-term intact during rewriting.

   659   As a remedy we use a standard trick in HOL: we introduce 

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

   661   namely as

   651   With this trick, we can reformulate our rewrite rules pushing a permutation @{text \<pi>}

   668   The point is that we will always start with a term that does not

   652   inside a term as follows

   669   contain any @{text unpermutes}.  With this trick we can reformulate

   670   our rewrite rules as follows

   656   i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\

   674   i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ & 

   675     @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\

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

   677   ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\

   659   iii) & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & @{text "\<longmapsto>"} & @{term x}\\

   678   iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & $\stackrel{\rightharpoonup}{=}$ & @{term x}\\

   660   iv) &  @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\

   679   iv') &  @{term "\<pi> \<bullet> c"} & $\stackrel{\rightharpoonup}{=}$ & @{term "c"}

   680     \hspace{6mm}provided @{text c} is equivariant\\

   665   In this rewrite systems no rule overlaps. Taking the measure

   685   None of these rules overlap. To see that the permutation on the

   686   right-hand side is applied to a smaller term, we take the measure

   667   is the size of the term (without counting @{text unpermutes}) and

   688   is the size of a term (without counting @{text unpermutes}) and the

   668   the second is the number of occurences of @{text "unpermute \<pi> x"}

   689   second is the number of occurences of @{text "unpermute \<pi> x"} and

   669   and @{text "\<pi> \<bullet> c"}, then each rule is strictly decreasing.

   690   @{text "\<pi> \<bullet> c"}. This means the process of applying these rules 

   670   Consequently the process of applying these rules must terminate.

   691   with our `outside-to-inside' strategy must terminate.

   671 

   692 

   672 

   693   With the rewriting system in plcae, we are able to establish the

   673   together with the permutation 

   694   fact that for a HOL-term @{text t} whose constants are all equivariant,

   674   operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel}

   695   the HOL-term @{text "\<pi> \<bullet> t"} is equal to @{text "t'"} wherby

   675   leads to a simple rewrite system that pushes permutations inside a term until they reach

   696   @{text "t'"} is equal to @{text t} except that every free variable

   676   either function constants or variables. The permutations in front of

   697   @{text x} of @{text t} is replaced by @{text "\<pi> \<bullet> x"}.  Pitts calls

   677   equivariant constants disappear. This helps us to establish equivariance

   698   this fact \emph{equivariance principle}. In our setting the precise

   678   for any notion in HOL that is defined in terms of more primitive notions. To

   699   statement of this fact is a bit more involved because of the fact

   679   see this let us 

   700   that @{text unpermute} needs to be treated specially.

   701   

   702   \begin{theorem}[Equivariance Principle]

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

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

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

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

   707   \end{theorem}

   708   

   709