author wenzelm Sun, 11 Nov 2012 16:19:55 +0100 changeset 50080 200f749c96db parent 50079 5c36db9db335 child 50081 9b92ee8dec98
updated section on ordered rewriting;
 src/Doc/IsarRef/Generic.thy file | annotate | diff | comparison | revisions src/Doc/ROOT file | annotate | diff | comparison | revisions src/Doc/Ref/document/root.tex file | annotate | diff | comparison | revisions src/Doc/Ref/document/simplifier.tex file | annotate | diff | comparison | revisions
--- 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: