updated section on ordered rewriting;
authorwenzelm
Sun Nov 11 16:19:55 2012 +0100 (2012-11-11)
changeset 50080200f749c96db
parent 50079 5c36db9db335
child 50081 9b92ee8dec98
updated section on ordered rewriting;
src/Doc/IsarRef/Generic.thy
src/Doc/ROOT
src/Doc/Ref/document/root.tex
src/Doc/Ref/document/simplifier.tex
     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: