# HG changeset patch # User wenzelm # Date 1352647195 -3600 # Node ID 200f749c96db95f1106ad774ba9c4b0102ea1b7e # Parent 5c36db9db335bb2ae05426abd6230894480925a0 updated section on ordered rewriting; diff -r 5c36db9db335 -r 200f749c96db src/Doc/IsarRef/Generic.thy --- a/src/Doc/IsarRef/Generic.thy Sat Nov 10 20:16:16 2012 +0100 +++ b/src/Doc/IsarRef/Generic.thy Sun Nov 11 16:19:55 2012 +0100 @@ -766,6 +766,105 @@ *} +subsection {* Ordered rewriting with permutative rules *} + +text {* A rewrite rule is \emph{permutative} if the left-hand side and + right-hand side are the equal up to renaming of variables. The most + common permutative rule is commutativity: @{text "?x + ?y = ?y + + ?x"}. Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) - + ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y + (insert ?x ?A)"} for sets. Such rules are common enough to merit + special attention. + + Because ordinary rewriting loops given such rules, the Simplifier + employs a special strategy, called \emph{ordered rewriting}. + Permutative rules are detected and only applied if the rewriting + step decreases the redex wrt.\ a given term ordering. For example, + commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then + stops, because the redex cannot be decreased further in the sense of + the term ordering. + + The default is lexicographic ordering of term structure, but this + could be also changed locally for special applications via + @{index_ML Simplifier.set_termless} in Isabelle/ML. + + \medskip Permutative rewrite rules are declared to the Simplifier + just like other rewrite rules. Their special status is recognized + automatically, and their application is guarded by the term ordering + accordingly. *} + + +subsubsection {* Rewriting with AC operators *} + +text {* Ordered rewriting is particularly effective in the case of + associative-commutative operators. (Associativity by itself is not + permutative.) When dealing with an AC-operator @{text "f"}, keep + the following points in mind: + + \begin{itemize} + + \item The associative law must always be oriented from left to + right, namely @{text "f (f x y) z = f x (f y z)"}. The opposite + orientation, if used with commutativity, leads to looping in + conjunction with the standard term order. + + \item To complete your set of rewrite rules, you must add not just + associativity (A) and commutativity (C) but also a derived rule + \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}. + + \end{itemize} + + Ordered rewriting with the combination of A, C, and LC sorts a term + lexicographically --- the rewriting engine imitates bubble-sort. +*} + +locale AC_example = + fixes f :: "'a \ 'a \ 'a" (infix "\" 60) + assumes assoc: "(x \ y) \ z = x \ (y \ z)" + assumes commute: "x \ y = y \ x" +begin + +lemma left_commute: "x \ (y \ z) = y \ (x \ z)" +proof - + have "(x \ y) \ z = (y \ x) \ z" by (simp only: commute) + then show ?thesis by (simp only: assoc) +qed + +lemmas AC_rules = assoc commute left_commute + +text {* Thus the Simplifier is able to establish equalities with + arbitrary permutations of subterms, by normalizing to a common + standard form. For example: *} + +lemma "(b \ c) \ a = xxx" + apply (simp only: AC_rules) + txt {* @{subgoals} *} + oops + +lemma "(b \ c) \ a = a \ (b \ c)" by (simp only: AC_rules) +lemma "(b \ c) \ a = c \ (b \ a)" by (simp only: AC_rules) +lemma "(b \ c) \ a = (c \ b) \ a" by (simp only: AC_rules) + +end + +text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and + give many examples; other algebraic structures are amenable to + ordered rewriting, such as boolean rings. The Boyer-Moore theorem + prover \cite{bm88book} also employs ordered rewriting. +*} + + +subsubsection {* Re-orienting equalities *} + +text {* Another application of ordered rewriting uses the derived rule + @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to + reverse equations. + + This is occasionally useful to re-orient local assumptions according + to the term ordering, when other built-in mechanisms of + reorientation and mutual simplification fail to apply. *} + + subsection {* Configuration options \label{sec:simp-config} *} text {* diff -r 5c36db9db335 -r 200f749c96db src/Doc/ROOT --- a/src/Doc/ROOT Sat Nov 10 20:16:16 2012 +0100 +++ b/src/Doc/ROOT Sun Nov 11 16:19:55 2012 +0100 @@ -262,7 +262,6 @@ "../manual.bib" "document/build" "document/root.tex" - "document/simplifier.tex" "document/substitution.tex" "document/syntax.tex" "document/thm.tex" diff -r 5c36db9db335 -r 200f749c96db src/Doc/Ref/document/root.tex --- a/src/Doc/Ref/document/root.tex Sat Nov 10 20:16:16 2012 +0100 +++ b/src/Doc/Ref/document/root.tex Sun Nov 11 16:19:55 2012 +0100 @@ -43,7 +43,6 @@ \input{thm} \input{syntax} \input{substitution} -\input{simplifier} %%seealso's must be last so that they appear last in the index entries \index{meta-rewriting|seealso{tactics, theorems}} diff -r 5c36db9db335 -r 200f749c96db src/Doc/Ref/document/simplifier.tex --- a/src/Doc/Ref/document/simplifier.tex Sat Nov 10 20:16:16 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,91 +0,0 @@ - -\chapter{Simplification} -\label{chap:simplification} - -\section{Permutative rewrite rules} -\index{rewrite rules!permutative|(} - -A rewrite rule is {\bf permutative} if the left-hand side and right-hand -side are the same up to renaming of variables. The most common permutative -rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = -(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ -for sets. Such rules are common enough to merit special attention. - -Because ordinary rewriting loops given such rules, the simplifier -employs a special strategy, called {\bf ordered - rewriting}\index{rewriting!ordered}. There is a standard -lexicographic ordering on terms. This should be perfectly OK in most -cases, but can be changed for special applications. - -\begin{ttbox} -settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} -\end{ttbox} -\begin{ttdescription} - -\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as - term order in simpset $ss$. - -\end{ttdescription} - -\medskip - -A permutative rewrite rule is applied only if it decreases the given -term with respect to this ordering. For example, commutativity -rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less -than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also -employs ordered rewriting. - -Permutative rewrite rules are added to simpsets just like other -rewrite rules; the simplifier recognizes their special status -automatically. They are most effective in the case of -associative-commutative operators. (Associativity by itself is not -permutative.) When dealing with an AC-operator~$f$, keep the -following points in mind: -\begin{itemize}\index{associative-commutative operators} - -\item The associative law must always be oriented from left to right, - namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if - used with commutativity, leads to looping in conjunction with the - standard term order. - -\item To complete your set of rewrite rules, you must add not just - associativity~(A) and commutativity~(C) but also a derived rule, {\bf - left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. -\end{itemize} -Ordered rewriting with the combination of A, C, and~LC sorts a term -lexicographically: -\[\def\maps#1{\stackrel{#1}{\longmapsto}} - (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] -Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many -examples; other algebraic structures are amenable to ordered rewriting, -such as boolean rings. - - -\subsection{Re-orienting equalities} -Ordered rewriting with the derived rule \texttt{eq_commute} can reverse -equations: -\begin{ttbox} -val eq_commute = prove_goal HOL.thy "(x=y) = (y=x)" - (fn _ => [Blast_tac 1]); -\end{ttbox} -This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs -in the conclusion but not~$s$, can often be brought into the right form. -For example, ordered rewriting with \texttt{eq_commute} can prove the goal -\[ f(a)=b \conj f(a)=c \imp b=c. \] -Here \texttt{eq_commute} reverses both $f(a)=b$ and $f(a)=c$ -because $f(a)$ is lexicographically greater than $b$ and~$c$. These -re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the -conclusion by~$f(a)$. - -Another example is the goal $\neg(t=u) \imp \neg(u=t)$. -The differing orientations make this appear difficult to prove. Ordered -rewriting with \texttt{eq_commute} makes the equalities agree. (Without -knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ -or~$u=t$.) Then the simplifier can prove the goal outright. - -\index{rewrite rules!permutative|)} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "ref" -%%% End: