--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<bullet>" 60)
+ assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
+ assumes commute: "x \<bullet> y = y \<bullet> x"
+begin
+
+lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"
+proof -
+ have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> 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 \<bullet> c) \<bullet> a = xxx"
+ apply (simp only: AC_rules)
+ txt {* @{subgoals} *}
+ oops
+
+lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules)
+lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules)
+lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> 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 {*
--- 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"
--- 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}}
--- 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: