author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 48506 | doc-src/TutorialI/Advanced/simp2.thy@af1dabad14c0 |
child 57512 | cc97b347b301 |
permissions | -rw-r--r-- |
9958 | 1 |
(*<*) |
48506
af1dabad14c0
avoid clash of Advanced/simp.thy vs. Misc/simp.thy;
wenzelm
parents:
19792
diff
changeset
|
2 |
theory simp2 imports Main begin |
9958 | 3 |
(*>*) |
4 |
||
5 |
section{*Simplification*} |
|
6 |
||
7 |
text{*\label{sec:simplification-II}\index{simplification|(} |
|
11494 | 8 |
This section describes features not covered until now. It also |
9 |
outlines the simplification process itself, which can be helpful |
|
10 |
when the simplifier does not do what you expect of it. |
|
9958 | 11 |
*} |
12 |
||
10885 | 13 |
subsection{*Advanced Features*} |
9958 | 14 |
|
10885 | 15 |
subsubsection{*Congruence Rules*} |
9958 | 16 |
|
17 |
text{*\label{sec:simp-cong} |
|
11494 | 18 |
While simplifying the conclusion $Q$ |
13191 | 19 |
of $P \Imp Q$, it is legal to use the assumption $P$. |
11494 | 20 |
For $\Imp$ this policy is hardwired, but |
21 |
contextual information can also be made available for other |
|
9958 | 22 |
operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term |
23 |
True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs = |
|
24 |
xs"}. The generation of contextual information during simplification is |
|
25 |
controlled by so-called \bfindex{congruence rules}. This is the one for |
|
26 |
@{text"\<longrightarrow>"}: |
|
27 |
@{thm[display]imp_cong[no_vars]} |
|
28 |
It should be read as follows: |
|
29 |
In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"}, |
|
30 |
simplify @{prop P} to @{prop P'} |
|
31 |
and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}. |
|
32 |
||
33 |
Here are some more examples. The congruence rules for bounded |
|
34 |
quantifiers supply contextual information about the bound variable: |
|
35 |
@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]} |
|
11494 | 36 |
One congruence rule for conditional expressions supplies contextual |
11196 | 37 |
information for simplifying the @{text then} and @{text else} cases: |
9958 | 38 |
@{thm[display]if_cong[no_vars]} |
11494 | 39 |
An alternative congruence rule for conditional expressions |
40 |
actually \emph{prevents} simplification of some arguments: |
|
9958 | 41 |
@{thm[display]if_weak_cong[no_vars]} |
42 |
Only the first argument is simplified; the others remain unchanged. |
|
43 |
This makes simplification much faster and is faithful to the evaluation |
|
44 |
strategy in programming languages, which is why this is the default |
|
19792 | 45 |
congruence rule for @{text "if"}. Analogous rules control the evaluation of |
9958 | 46 |
@{text case} expressions. |
47 |
||
11458 | 48 |
You can declare your own congruence rules with the attribute \attrdx{cong}, |
9958 | 49 |
either globally, in the usual manner, |
50 |
\begin{quote} |
|
51 |
\isacommand{declare} \textit{theorem-name} @{text"[cong]"} |
|
52 |
\end{quote} |
|
53 |
or locally in a @{text"simp"} call by adding the modifier |
|
54 |
\begin{quote} |
|
55 |
@{text"cong:"} \textit{list of theorem names} |
|
56 |
\end{quote} |
|
57 |
The effect is reversed by @{text"cong del"} instead of @{text cong}. |
|
58 |
||
59 |
\begin{warn} |
|
60 |
The congruence rule @{thm[source]conj_cong} |
|
61 |
@{thm[display]conj_cong[no_vars]} |
|
10885 | 62 |
\par\noindent |
63 |
is occasionally useful but is not a default rule; you have to declare it explicitly. |
|
9958 | 64 |
\end{warn} |
65 |
*} |
|
66 |
||
10885 | 67 |
subsubsection{*Permutative Rewrite Rules*} |
9958 | 68 |
|
69 |
text{* |
|
11494 | 70 |
\index{rewrite rules!permutative|bold}% |
71 |
An equation is a \textbf{permutative rewrite rule} if the left-hand |
|
9958 | 72 |
side and right-hand side are the same up to renaming of variables. The most |
73 |
common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples |
|
74 |
include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert |
|
75 |
y A) = insert y (insert x A)"} for sets. Such rules are problematic because |
|
76 |
once they apply, they can be used forever. The simplifier is aware of this |
|
77 |
danger and treats permutative rules by means of a special strategy, called |
|
78 |
\bfindex{ordered rewriting}: a permutative rewrite |
|
10978 | 79 |
rule is only applied if the term becomes smaller with respect to a fixed |
80 |
lexicographic ordering on terms. For example, commutativity rewrites |
|
9958 | 81 |
@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly |
82 |
smaller than @{term"b+a"}. Permutative rewrite rules can be turned into |
|
83 |
simplification rules in the usual manner via the @{text simp} attribute; the |
|
84 |
simplifier recognizes their special status automatically. |
|
85 |
||
86 |
Permutative rewrite rules are most effective in the case of |
|
10281 | 87 |
associative-commutative functions. (Associativity by itself is not |
88 |
permutative.) When dealing with an AC-function~$f$, keep the |
|
9958 | 89 |
following points in mind: |
10281 | 90 |
\begin{itemize}\index{associative-commutative function} |
9958 | 91 |
|
92 |
\item The associative law must always be oriented from left to right, |
|
93 |
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
|
94 |
used with commutativity, can lead to nontermination. |
|
95 |
||
96 |
\item To complete your set of rewrite rules, you must add not just |
|
97 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf |
|
98 |
left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
|
99 |
\end{itemize} |
|
100 |
Ordered rewriting with the combination of A, C, and LC sorts a term |
|
101 |
lexicographically: |
|
102 |
\[\def\maps#1{~\stackrel{#1}{\leadsto}~} |
|
103 |
f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \] |
|
104 |
||
105 |
Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely |
|
10885 | 106 |
necessary because the built-in arithmetic prover often succeeds without |
11196 | 107 |
such tricks. |
9958 | 108 |
*} |
109 |
||
11494 | 110 |
subsection{*How the Simplifier Works*} |
9958 | 111 |
|
112 |
text{*\label{sec:SimpHow} |
|
11494 | 113 |
Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified |
114 |
first. A conditional equation is only applied if its condition can be |
|
115 |
proved, again by simplification. Below we explain some special features of |
|
116 |
the rewriting process. |
|
9958 | 117 |
*} |
118 |
||
10885 | 119 |
subsubsection{*Higher-Order Patterns*} |
9958 | 120 |
|
10186 | 121 |
text{*\index{simplification rule|(} |
122 |
So far we have pretended the simplifier can deal with arbitrary |
|
11494 | 123 |
rewrite rules. This is not quite true. For reasons of feasibility, |
124 |
the simplifier expects the |
|
10186 | 125 |
left-hand side of each rule to be a so-called \emph{higher-order |
11494 | 126 |
pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}. |
127 |
This restricts where |
|
10186 | 128 |
unknowns may occur. Higher-order patterns are terms in $\beta$-normal |
11494 | 129 |
form. (This means there are no subterms of the form $(\lambda x. M)(N)$.) |
130 |
Each occurrence of an unknown is of the form |
|
10186 | 131 |
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound |
10978 | 132 |
variables. Thus all ordinary rewrite rules, where all unknowns are |
11494 | 133 |
of base type, for example @{thm add_assoc}, are acceptable: if an unknown is |
10186 | 134 |
of base type, it cannot have any arguments. Additionally, the rule |
11494 | 135 |
@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in |
10186 | 136 |
both directions: all arguments of the unknowns @{text"?P"} and |
137 |
@{text"?Q"} are distinct bound variables. |
|
138 |
||
11494 | 139 |
If the left-hand side is not a higher-order pattern, all is not lost. |
140 |
The simplifier will still try to apply the rule provided it |
|
141 |
matches directly: without much $\lambda$-calculus hocus |
|
142 |
pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites |
|
15904 | 143 |
@{term"g a \<in> range g"} to @{const True}, but will fail to match |
10186 | 144 |
@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can |
11494 | 145 |
eliminate the offending subterms --- those that are not patterns --- |
146 |
by adding new variables and conditions. |
|
147 |
In our example, we eliminate @{text"?f ?x"} and obtain |
|
148 |
@{text"?y = |
|
149 |
?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine |
|
10186 | 150 |
as a conditional rewrite rule since conditions can be arbitrary |
11494 | 151 |
terms. However, this trick is not a panacea because the newly |
11196 | 152 |
introduced conditions may be hard to solve. |
10186 | 153 |
|
10885 | 154 |
There is no restriction on the form of the right-hand |
10186 | 155 |
sides. They may not contain extraneous term or type variables, though. |
156 |
*} |
|
9958 | 157 |
|
10885 | 158 |
subsubsection{*The Preprocessor*} |
9958 | 159 |
|
10845 | 160 |
text{*\label{sec:simp-preprocessor} |
10885 | 161 |
When a theorem is declared a simplification rule, it need not be a |
10186 | 162 |
conditional equation already. The simplifier will turn it into a set of |
10885 | 163 |
conditional equations automatically. For example, @{prop"f x = |
164 |
g x & h x = k x"} becomes the two separate |
|
165 |
simplification rules @{prop"f x = g x"} and @{prop"h x = k x"}. In |
|
10186 | 166 |
general, the input theorem is converted as follows: |
167 |
\begin{eqnarray} |
|
10885 | 168 |
\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\ |
10186 | 169 |
P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ |
170 |
P \land Q &\mapsto& P,\ Q \nonumber\\ |
|
171 |
\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\ |
|
172 |
\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\ |
|
19792 | 173 |
@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto& |
10186 | 174 |
P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber |
175 |
\end{eqnarray} |
|
176 |
Once this conversion process is finished, all remaining non-equations |
|
10885 | 177 |
$P$ are turned into trivial equations $P =\isa{True}$. |
178 |
For example, the formula |
|
179 |
\begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center} |
|
10845 | 180 |
is converted into the three rules |
10186 | 181 |
\begin{center} |
10885 | 182 |
@{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}. |
10186 | 183 |
\end{center} |
184 |
\index{simplification rule|)} |
|
9958 | 185 |
\index{simplification|)} |
186 |
*} |
|
187 |
(*<*) |
|
188 |
end |
|
189 |
(*>*) |