equal
deleted
inserted
replaced
358 though. |
358 though. |
359 \end{warn} |
359 \end{warn} |
360 \index{rewrite rules|)} |
360 \index{rewrite rules|)} |
361 |
361 |
362 |
362 |
363 \subsection{Simplification procedures} |
363 \subsection{*Simplification procedures} |
364 \begin{ttbox} |
364 \begin{ttbox} |
365 addsimprocs : simpset * simproc list -> simpset |
365 addsimprocs : simpset * simproc list -> simpset |
366 delsimprocs : simpset * simproc list -> simpset |
366 delsimprocs : simpset * simproc list -> simpset |
367 \end{ttbox} |
367 \end{ttbox} |
368 |
368 |
924 \end{warn} |
924 \end{warn} |
925 |
925 |
926 |
926 |
927 \section{Permutative rewrite rules} |
927 \section{Permutative rewrite rules} |
928 \index{rewrite rules!permutative|(} |
928 \index{rewrite rules!permutative|(} |
929 \begin{ttbox} |
|
930 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} |
|
931 \end{ttbox} |
|
932 |
929 |
933 A rewrite rule is {\bf permutative} if the left-hand side and right-hand |
930 A rewrite rule is {\bf permutative} if the left-hand side and right-hand |
934 side are the same up to renaming of variables. The most common permutative |
931 side are the same up to renaming of variables. The most common permutative |
935 rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = |
932 rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = |
936 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ |
933 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ |
940 employs a special strategy, called {\bf ordered |
937 employs a special strategy, called {\bf ordered |
941 rewriting}\index{rewriting!ordered}. There is a standard |
938 rewriting}\index{rewriting!ordered}. There is a standard |
942 lexicographic ordering on terms. This should be perfectly OK in most |
939 lexicographic ordering on terms. This should be perfectly OK in most |
943 cases, but can be changed for special applications. |
940 cases, but can be changed for special applications. |
944 |
941 |
|
942 \begin{ttbox} |
|
943 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} |
|
944 \end{ttbox} |
945 \begin{ttdescription} |
945 \begin{ttdescription} |
946 |
946 |
947 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as |
947 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as |
948 term order in simpset $ss$. |
948 term order in simpset $ss$. |
949 |
949 |