95 smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into |
95 smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into |
96 simplification rules in the usual manner via the \isa{simp} attribute; the |
96 simplification rules in the usual manner via the \isa{simp} attribute; the |
97 simplifier recognizes their special status automatically. |
97 simplifier recognizes their special status automatically. |
98 |
98 |
99 Permutative rewrite rules are most effective in the case of |
99 Permutative rewrite rules are most effective in the case of |
100 associative-commutative operators. (Associativity by itself is not |
100 associative-commutative functions. (Associativity by itself is not |
101 permutative.) When dealing with an AC-operator~$f$, keep the |
101 permutative.) When dealing with an AC-function~$f$, keep the |
102 following points in mind: |
102 following points in mind: |
103 \begin{itemize}\index{associative-commutative operators} |
103 \begin{itemize}\index{associative-commutative function} |
104 |
104 |
105 \item The associative law must always be oriented from left to right, |
105 \item The associative law must always be oriented from left to right, |
106 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
106 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
107 used with commutativity, can lead to nontermination. |
107 used with commutativity, can lead to nontermination. |
108 |
108 |