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: