author wenzelm Sun Nov 11 16:19:55 2012 +0100 (2012-11-11) changeset 50080 200f749c96db parent 50079 5c36db9db335 child 50081 9b92ee8dec98
updated section on ordered rewriting;
 src/Doc/IsarRef/Generic.thy file | annotate | diff | revisions src/Doc/ROOT file | annotate | diff | revisions src/Doc/Ref/document/root.tex file | annotate | diff | revisions src/Doc/Ref/document/simplifier.tex file | annotate | diff | revisions
     1.1 --- a/src/Doc/IsarRef/Generic.thy	Sat Nov 10 20:16:16 2012 +0100
1.2 +++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 11 16:19:55 2012 +0100
1.3 @@ -766,6 +766,105 @@
1.4  *}
1.5
1.6
1.7 +subsection {* Ordered rewriting with permutative rules *}
1.8 +
1.9 +text {* A rewrite rule is \emph{permutative} if the left-hand side and
1.10 +  right-hand side are the equal up to renaming of variables.  The most
1.11 +  common permutative rule is commutativity: @{text "?x + ?y = ?y +
1.12 +  ?x"}.  Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) -
1.13 +  ?y"} in arithmetic and @{text "insert ?x (insert ?y ?A) = insert ?y
1.14 +  (insert ?x ?A)"} for sets.  Such rules are common enough to merit
1.15 +  special attention.
1.16 +
1.17 +  Because ordinary rewriting loops given such rules, the Simplifier
1.18 +  employs a special strategy, called \emph{ordered rewriting}.
1.19 +  Permutative rules are detected and only applied if the rewriting
1.20 +  step decreases the redex wrt.\ a given term ordering.  For example,
1.21 +  commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then
1.22 +  stops, because the redex cannot be decreased further in the sense of
1.23 +  the term ordering.
1.24 +
1.25 +  The default is lexicographic ordering of term structure, but this
1.26 +  could be also changed locally for special applications via
1.27 +  @{index_ML Simplifier.set_termless} in Isabelle/ML.
1.28 +
1.29 +  \medskip Permutative rewrite rules are declared to the Simplifier
1.30 +  just like other rewrite rules.  Their special status is recognized
1.31 +  automatically, and their application is guarded by the term ordering
1.32 +  accordingly. *}
1.33 +
1.34 +
1.35 +subsubsection {* Rewriting with AC operators *}
1.36 +
1.37 +text {* Ordered rewriting is particularly effective in the case of
1.38 +  associative-commutative operators.  (Associativity by itself is not
1.39 +  permutative.)  When dealing with an AC-operator @{text "f"}, keep
1.40 +  the following points in mind:
1.41 +
1.42 +  \begin{itemize}
1.43 +
1.44 +  \item The associative law must always be oriented from left to
1.45 +  right, namely @{text "f (f x y) z = f x (f y z)"}.  The opposite
1.46 +  orientation, if used with commutativity, leads to looping in
1.47 +  conjunction with the standard term order.
1.48 +
1.49 +  \item To complete your set of rewrite rules, you must add not just
1.50 +  associativity (A) and commutativity (C) but also a derived rule
1.51 +  \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.
1.52 +
1.53 +  \end{itemize}
1.54 +
1.55 +  Ordered rewriting with the combination of A, C, and LC sorts a term
1.56 +  lexicographically --- the rewriting engine imitates bubble-sort.
1.57 +*}
1.58 +
1.59 +locale AC_example =
1.60 +  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<bullet>" 60)
1.61 +  assumes assoc: "(x \<bullet> y) \<bullet> z = x \<bullet> (y \<bullet> z)"
1.62 +  assumes commute: "x \<bullet> y = y \<bullet> x"
1.63 +begin
1.64 +
1.65 +lemma left_commute: "x \<bullet> (y \<bullet> z) = y \<bullet> (x \<bullet> z)"
1.66 +proof -
1.67 +  have "(x \<bullet> y) \<bullet> z = (y \<bullet> x) \<bullet> z" by (simp only: commute)
1.68 +  then show ?thesis by (simp only: assoc)
1.69 +qed
1.70 +
1.71 +lemmas AC_rules = assoc commute left_commute
1.72 +
1.73 +text {* Thus the Simplifier is able to establish equalities with
1.74 +  arbitrary permutations of subterms, by normalizing to a common
1.75 +  standard form.  For example: *}
1.76 +
1.77 +lemma "(b \<bullet> c) \<bullet> a = xxx"
1.78 +  apply (simp only: AC_rules)
1.79 +  txt {* @{subgoals} *}
1.80 +  oops
1.81 +
1.82 +lemma "(b \<bullet> c) \<bullet> a = a \<bullet> (b \<bullet> c)" by (simp only: AC_rules)
1.83 +lemma "(b \<bullet> c) \<bullet> a = c \<bullet> (b \<bullet> a)" by (simp only: AC_rules)
1.84 +lemma "(b \<bullet> c) \<bullet> a = (c \<bullet> b) \<bullet> a" by (simp only: AC_rules)
1.85 +
1.86 +end
1.87 +
1.88 +text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and
1.89 +  give many examples; other algebraic structures are amenable to
1.90 +  ordered rewriting, such as boolean rings.  The Boyer-Moore theorem
1.91 +  prover \cite{bm88book} also employs ordered rewriting.
1.92 +*}
1.93 +
1.94 +
1.95 +subsubsection {* Re-orienting equalities *}
1.96 +
1.97 +text {* Another application of ordered rewriting uses the derived rule
1.98 +  @{thm [source] eq_commute}: @{thm [source = false] eq_commute} to
1.99 +  reverse equations.
1.100 +
1.101 +  This is occasionally useful to re-orient local assumptions according
1.102 +  to the term ordering, when other built-in mechanisms of
1.103 +  reorientation and mutual simplification fail to apply.  *}
1.104 +
1.105 +
1.106  subsection {* Configuration options \label{sec:simp-config} *}
1.107
1.108  text {*

     2.1 --- a/src/Doc/ROOT	Sat Nov 10 20:16:16 2012 +0100
2.2 +++ b/src/Doc/ROOT	Sun Nov 11 16:19:55 2012 +0100
2.3 @@ -262,7 +262,6 @@
2.4      "../manual.bib"
2.5      "document/build"
2.6      "document/root.tex"
2.7 -    "document/simplifier.tex"
2.8      "document/substitution.tex"
2.9      "document/syntax.tex"
2.10      "document/thm.tex"

     3.1 --- a/src/Doc/Ref/document/root.tex	Sat Nov 10 20:16:16 2012 +0100
3.2 +++ b/src/Doc/Ref/document/root.tex	Sun Nov 11 16:19:55 2012 +0100
3.3 @@ -43,7 +43,6 @@
3.4  \input{thm}
3.5  \input{syntax}
3.6  \input{substitution}
3.7 -\input{simplifier}
3.8
3.9  %%seealso's must be last so that they appear last in the index entries
3.10  \index{meta-rewriting|seealso{tactics, theorems}}

     4.1 --- a/src/Doc/Ref/document/simplifier.tex	Sat Nov 10 20:16:16 2012 +0100
4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,91 +0,0 @@
4.4 -
4.5 -\chapter{Simplification}
4.6 -\label{chap:simplification}
4.7 -
4.8 -\section{Permutative rewrite rules}
4.9 -\index{rewrite rules!permutative|(}
4.10 -
4.11 -A rewrite rule is {\bf permutative} if the left-hand side and right-hand
4.12 -side are the same up to renaming of variables.  The most common permutative
4.13 -rule is commutativity: $x+y = y+x$.  Other examples include $(x-y)-z = 4.14 -(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
4.15 -for sets.  Such rules are common enough to merit special attention.
4.16 -
4.17 -Because ordinary rewriting loops given such rules, the simplifier
4.18 -employs a special strategy, called {\bf ordered
4.19 -  rewriting}\index{rewriting!ordered}.  There is a standard
4.20 -lexicographic ordering on terms.  This should be perfectly OK in most
4.21 -cases, but can be changed for special applications.
4.22 -
4.23 -\begin{ttbox}
4.24 -settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
4.25 -\end{ttbox}
4.26 -\begin{ttdescription}
4.27 -
4.28 -\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as
4.29 -  term order in simpset $ss$.
4.30 -
4.31 -\end{ttdescription}
4.32 -
4.33 -\medskip
4.34 -
4.35 -A permutative rewrite rule is applied only if it decreases the given
4.36 -term with respect to this ordering.  For example, commutativity
4.37 -rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less
4.38 -than $b+a$.  The Boyer-Moore theorem prover~\cite{bm88book} also
4.39 -employs ordered rewriting.
4.40 -
4.41 -Permutative rewrite rules are added to simpsets just like other
4.42 -rewrite rules; the simplifier recognizes their special status
4.43 -automatically.  They are most effective in the case of
4.44 -associative-commutative operators.  (Associativity by itself is not
4.45 -permutative.)  When dealing with an AC-operator~$f$, keep the
4.46 -following points in mind:
4.47 -\begin{itemize}\index{associative-commutative operators}
4.48 -
4.49 -\item The associative law must always be oriented from left to right,
4.50 -  namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if
4.51 -  used with commutativity, leads to looping in conjunction with the
4.52 -  standard term order.
4.53 -
4.54 -\item To complete your set of rewrite rules, you must add not just
4.55 -  associativity~(A) and commutativity~(C) but also a derived rule, {\bf
4.56 -    left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
4.57 -\end{itemize}
4.58 -Ordered rewriting with the combination of A, C, and~LC sorts a term
4.59 -lexicographically:
4.60 -$\def\maps#1{\stackrel{#1}{\longmapsto}} 4.61 - (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c)$
4.62 -Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
4.63 -examples; other algebraic structures are amenable to ordered rewriting,
4.64 -such as boolean rings.
4.65 -
4.66 -
4.67 -\subsection{Re-orienting equalities}
4.68 -Ordered rewriting with the derived rule \texttt{eq_commute} can reverse
4.69 -equations:
4.70 -\begin{ttbox}
4.71 -val eq_commute = prove_goal HOL.thy "(x=y) = (y=x)"
4.72 -                 (fn _ => [Blast_tac 1]);
4.73 -\end{ttbox}
4.74 -This is frequently useful.  Assumptions of the form $s=t$, where $t$ occurs
4.75 -in the conclusion but not~$s$, can often be brought into the right form.
4.76 -For example, ordered rewriting with \texttt{eq_commute} can prove the goal
4.77 -$f(a)=b \conj f(a)=c \imp b=c.$
4.78 -Here \texttt{eq_commute} reverses both $f(a)=b$ and $f(a)=c$
4.79 -because $f(a)$ is lexicographically greater than $b$ and~$c$.  These
4.80 -re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
4.81 -conclusion by~$f(a)$.
4.82 -
4.83 -Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
4.84 -The differing orientations make this appear difficult to prove.  Ordered
4.85 -rewriting with \texttt{eq_commute} makes the equalities agree.  (Without
4.86 -knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
4.87 -or~$u=t$.)  Then the simplifier can prove the goal outright.
4.88 -
4.89 -\index{rewrite rules!permutative|)}
4.90 -
4.91 -%%% Local Variables:
4.92 -%%% mode: latex
4.93 -%%% TeX-master: "ref"
4.94 -%%% End: