60   about syntax involving binders, such as lambda terms or type schemes:

    60   about syntax involving binders, such as lambda terms or type schemes in Mini-ML:

   199   whereby the string argument specifies the sort of the atom.\footnote{A

   199   whereby the string argument specifies the sort of the

   200   similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09}

   200   atom.\footnote{A similar design choice was made by Gunter et al

   201   for their variables.}  The use of type \emph{string} for sorts is merely for

   201   \cite{GunterOsbornPopescu09} for their variables.}  The use of type

   202   convenience; any countably infinite type would work as well. 

   202   \emph{string} for sorts is merely for convenience; any countably

   203   The set of all atoms we shall write as @{term "UNIV::atom set"}.

   203   infinite type would work as well.  In what follows we shall write

   204   We have two auxiliary functions for atoms, namely @{text sort} 

   204   @{term "UNIV::atom set"} for the set of all atoms.  We also have two

   205   and @{const nat_of} which are defined as 

   205   auxiliary functions for atoms, namely @{text sort} and @{const

   206   nat_of} which are defined as

   224   "atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the

   225   "atom => atom"} that are bijective; are the

   225   identity on all atoms, except a finite number of them; and @{text "iii)"} map

   226   identity on all atoms, except a finite number of them; and map

   244   @{text "i"}-@{text "iii"}. 

   245   (\ref{permtype}.@{text "i"}-@{text "iii"}). 

   302   are \emph{equal}. Another advantage of the function representation is that

   303   are \emph{equal} and can be used interchangeably. Another advantage of the function 

   303   they form a (non-com\-mu\-ta\-tive) group provided we define

   304   representation is that they form a (non-com\-mu\-ta\-tive) group provided we define

   337   @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}

   338   @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}\;.

   346   applies a permutation @{text "\<pi>"} to an object @{text "x"} of type

   347   applies a permutation @{text "\<pi>"} to an object @{text "x"}.  This 

   347   @{text \<beta>}, say.  This operation has the type

   348   operation has the type

   354   and will be defined over the hierarchie of types.

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

   355   Isabelle/HOL allows us to give a definition of this operation for

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

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

   380   In order to reason abstractly about this operation, 

   382   \noindent

   381   we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two 

   383   The type classes also allow us to reason abstractly about the permutation operation. 

   384   For this we state the following two 

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

   452   The main benefit of the use of type classes is that it allows us to delegate 

   450   resoning involved in determining whether the permutation properties

   453   much of the routine resoning involved in determining whether the permutation properties

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

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

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

   510   variables. 

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

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

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

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

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

   525   applies to just constants.  

   529   this definition to just these cases.

   545   applied form are always interderivable.

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

   556   \end{tabular}

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

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

   565   \eqref{permuteequ}. 

   566   Lemma~\ref{permutecompose} establishes that the

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

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

   580 

   585 

   586   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   587   \begin{tabular}{@ {}lcl}

   588   @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\

   589   @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\

   590   \end{tabular}

   591   \end{isabelle}

   592 

   593   \noindent

   594   by the definition of the permutation operation acting on booleans.

   595   

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

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

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

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

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

   600   constants are equivariant. We have implemented this rewrite system

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

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

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

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

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

   603   equivariance is already established, we can automatically establish 

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

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

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

   605   make sure that the definiens of this constant 

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

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

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

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

   593 

   608   is correct (in the sense of pushing a 

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

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

   595   pushed into applications and abstractions as follows

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

   596 

   611 

   597   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   598   \begin{tabular}{@ {}lrcl}

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

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

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

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

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

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

   616   be pushed into applications and abstractions as follows

   617 

   618   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   619   \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}

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

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

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

   626   The first equation we established in \eqref{permutefunapp};

   610   following two rules

   630   following two equations

   611 

   631 

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

   632   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

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

   633   \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}

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

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

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

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

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

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

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

   641   in order to remove permuations in front of bound variables and

   622   

   642   equivariant constants.  Unfortunately, we have to be careful with

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

   643   the rules {\it i)} and {\it iv}): they can lead to a loop whenever

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

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

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

   645   that we usually write this application using infix notation as

   626   for example the infinite reduction sequence

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

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

   648   reduction sequence

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

   652   @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}

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

   653   $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$

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

   654   @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}

   655   $\;\;\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it i)}}{\rrh}\stackrel{\text{\it iv)}}{\rrh}\;\;$

   656   @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> t)"}~~\ldots%

   657   

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

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

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

   663   is bigger.  To avoid this loop we need to apply our rewrite rule

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

   664   using an `outside to inside' strategy.  This strategy is sufficient

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

   665   since we are only interested of rewriting terms of the form @{term

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

   666   "\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.

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

   667 

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

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

   644 

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

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

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

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

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

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

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

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

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

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

   674   vanish. However, the subterm @{text

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   685 

   661   namely as

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

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

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

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

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

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

   692   \<bullet> x"}, namely as

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

   699   The point is that now we can formulate the rewrite rules as follows

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

   670   our rewrite rules as follows

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

   703   i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & 

   676   \multicolumn{4}{r}{provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\

   705   \multicolumn{4}{r}{\rm provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\

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

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

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

   707   iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & \rrh & @{term x}\\

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

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

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

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

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

   714   and @{text unpermutes} are only generated in case of bound variables.

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

   715   Clearly none of these rules overlap. Moreover, given our

   687   consisting of lexicographically ordered pairs whose first component

   716   outside-to-inside strategy, they terminate. To see this, notice that

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

   717   the permutation on the right-hand side of the rewrite rules is

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

   718   always applied to a smaller term, provided we take the measure consisting

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

   719   of lexicographically ordered pairs whose first component is the size

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

   720   of a term (counting terms of the form @{text "unpermute \<pi> x"} as

   692 

   721   leaves) and the second is the number of occurences of @{text

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

   722   "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.

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

   723 

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

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

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

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

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

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

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

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

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

   728   being equal to @{text t} except that every free variable @{text x}

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

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

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

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

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

   733   treated specially.

   726   \begin{proof}

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

   727   By induction on the grammar of HOL-terms. The case for variables cannot arise since

   728   equivariant HOL-terms are closed. The case for constants is clear by Definition 

   729   \ref{equivariance}. The case for applications is also straightforward since by

   730   \eqref{permutefunapp} we have @{term "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2) = (\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}.

   731   For the case of abstractions we can reason as follows

   732   

   733   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%

   734   \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}

   735   & @{text "\<pi> \<bullet> (\<lambda>x. t)"}\\

   736   @{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefsconstrs}\\

   737 

   738   \end{tabular}\hfill\qed

   739   \end{isabelle}

   740   \end{proof}

   741 

   742   database of equivariant functions

   743 

   744   Such a rewrite system is often very helpful

   745   in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ???

   746  

   747   For this we have implemented in Isabelle/HOL a

   748   database of equivariant constants that can be used to rewrite

   749   HOL-terms.