equal
deleted
inserted
replaced
578 it leads to a simple rewrite system that allows us to `push' a |
578 it leads to a simple rewrite system that allows us to `push' a |
579 permutation towards the leaves in a HOL-term (i.e.~constants and free |
579 permutation towards the leaves in a HOL-term (i.e.~constants and free |
580 variables). The permutation disappears in cases where the |
580 variables). The permutation disappears in cases where the |
581 constants are equivariant. Given a database of equivariant constants, |
581 constants are equivariant. Given a database of equivariant constants, |
582 we can implement a decision procedure that helps to find out when |
582 we can implement a decision procedure that helps to find out when |
583 a compound term is equivariant. A permutation @{text \<pi>} can be pushed over |
583 a compound term is equivariant. A permutation @{text \<pi>} can be pushed into |
584 applications and abstractions in a HOL-term as follows |
584 applications and abstractions in a HOL-term as follows |
585 |
585 |
586 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
586 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
587 \begin{tabular}{@ {}lrcl} |
587 \begin{tabular}{@ {}lrcl} |
588 i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\ |
588 i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\ |
614 \end{isabelle} |
614 \end{isabelle} |
615 |
615 |
616 |
616 |
617 \noindent |
617 \noindent |
618 By a meta-argument, that means one we cannot formalise inside |
618 By a meta-argument, that means one we cannot formalise inside |
619 Isabelle/HOL, we can convince ourselves that the rewriting process |
619 Isabelle/HOL, we can convince ourselves that the strategy of |
620 of first pushing a permutation inside a term using |
620 of first pushing a permutation inside a term using |
621 \eqref{rewriteapplam}, then removing permutation in front of bound |
621 \eqref{rewriteapplam}, then removing permutation in front of bound |
622 variables using \eqref{rewriteunpermute} and finally removing all |
622 variables using \eqref{rewriteunpermute} and finally removing all |
623 permutations in front of equivariant constants must terminate: the |
623 permutations in front of equivariant constants must terminate: the |
624 size of the term gets smaller in \eqref{rewriteapplam} if we do not |
624 size of the term gets smaller in \eqref{rewriteapplam} if we do not |