author | wenzelm |
Fri, 21 Dec 2001 19:55:39 +0100 | |
changeset 12582 | b85acd66f715 |
parent 12533 | e417bd7ca8a0 |
child 12631 | 7648ac4a6b95 |
permissions | -rw-r--r-- |
9932 | 1 |
(*<*) |
9922 | 2 |
theory simp = Main: |
9932 | 3 |
(*>*) |
9922 | 4 |
|
11214 | 5 |
subsection{*Simplification Rules*} |
9932 | 6 |
|
11458 | 7 |
text{*\index{simplification rules} |
8 |
To facilitate simplification, |
|
9 |
the attribute @{text"[simp]"}\index{*simp (attribute)} |
|
10 |
declares theorems to be simplification rules, which the simplifier |
|
11 |
will use automatically. In addition, \isacommand{datatype} and |
|
12 |
\isacommand{primrec} declarations (and a few others) |
|
13 |
implicitly declare some simplification rules. |
|
14 |
Explicit definitions are \emph{not} declared as |
|
9932 | 15 |
simplification rules automatically! |
16 |
||
11458 | 17 |
Nearly any theorem can become a simplification |
18 |
rule. The simplifier will try to transform it into an equation. |
|
19 |
For example, the theorem |
|
20 |
@{prop"~P"} is turned into @{prop"P = False"}. The details |
|
9932 | 21 |
are explained in \S\ref{sec:SimpHow}. |
22 |
||
11458 | 23 |
The simplification attribute of theorems can be turned on and off:% |
12489 | 24 |
\index{*simp del (attribute)} |
9932 | 25 |
\begin{quote} |
26 |
\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\ |
|
27 |
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"} |
|
28 |
\end{quote} |
|
11309 | 29 |
Only equations that really simplify, like \isa{rev\ |
30 |
{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and |
|
31 |
\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ |
|
32 |
{\isacharequal}\ xs}, should be declared as default simplification rules. |
|
33 |
More specific ones should only be used selectively and should |
|
34 |
not be made default. Distributivity laws, for example, alter |
|
35 |
the structure of terms and can produce an exponential blow-up instead of |
|
36 |
simplification. A default simplification rule may |
|
37 |
need to be disabled in certain proofs. Frequent changes in the simplification |
|
38 |
status of a theorem may indicate an unwise use of defaults. |
|
9932 | 39 |
\begin{warn} |
11458 | 40 |
Simplification can run forever, for example if both $f(x) = g(x)$ and |
9932 | 41 |
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not |
42 |
to include simplification rules that can lead to nontermination, either on |
|
43 |
their own or in combination with other simplification rules. |
|
44 |
\end{warn} |
|
12332 | 45 |
\begin{warn} |
46 |
It is inadvisable to toggle the simplification attribute of a |
|
47 |
theorem from a parent theory $A$ in a child theory $B$ for good. |
|
48 |
The reason is that if some theory $C$ is based both on $B$ and (via a |
|
49 |
differnt path) on $A$, it is not defined what the simplification attribute |
|
50 |
of that theorem will be in $C$: it could be either. |
|
51 |
\end{warn} |
|
11458 | 52 |
*} |
9932 | 53 |
|
11458 | 54 |
subsection{*The {\tt\slshape simp} Method*} |
9932 | 55 |
|
56 |
text{*\index{*simp (method)|bold} |
|
57 |
The general format of the simplification method is |
|
58 |
\begin{quote} |
|
59 |
@{text simp} \textit{list of modifiers} |
|
60 |
\end{quote} |
|
10795 | 61 |
where the list of \emph{modifiers} fine tunes the behaviour and may |
11309 | 62 |
be empty. Specific modifiers are discussed below. Most if not all of the |
63 |
proofs seen so far could have been performed |
|
9932 | 64 |
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks |
10971 | 65 |
only the first subgoal and may thus need to be repeated --- use |
11428 | 66 |
\methdx{simp_all} to simplify all subgoals. |
11458 | 67 |
If nothing changes, @{text simp} fails. |
9932 | 68 |
*} |
69 |
||
11214 | 70 |
subsection{*Adding and Deleting Simplification Rules*} |
9932 | 71 |
|
72 |
text{* |
|
11458 | 73 |
\index{simplification rules!adding and deleting}% |
9932 | 74 |
If a certain theorem is merely needed in a few proofs by simplification, |
75 |
we do not need to make it a global simplification rule. Instead we can modify |
|
76 |
the set of simplification rules used in a simplification step by adding rules |
|
77 |
to it and/or deleting rules from it. The two modifiers for this are |
|
78 |
\begin{quote} |
|
11458 | 79 |
@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\ |
80 |
@{text"del:"} \textit{list of theorem names}\index{*del (modifier)} |
|
9932 | 81 |
\end{quote} |
11458 | 82 |
Or you can use a specific list of theorems and omit all others: |
9932 | 83 |
\begin{quote} |
11458 | 84 |
@{text"only:"} \textit{list of theorem names}\index{*only (modifier)} |
9932 | 85 |
\end{quote} |
11309 | 86 |
In this example, we invoke the simplifier, adding two distributive |
87 |
laws: |
|
88 |
\begin{quote} |
|
89 |
\isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"} |
|
90 |
\end{quote} |
|
9932 | 91 |
*} |
92 |
||
11214 | 93 |
subsection{*Assumptions*} |
9932 | 94 |
|
95 |
text{*\index{simplification!with/of assumptions} |
|
96 |
By default, assumptions are part of the simplification process: they are used |
|
97 |
as simplification rules and are simplified themselves. For example: |
|
98 |
*} |
|
99 |
||
10171 | 100 |
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"; |
101 |
apply simp; |
|
102 |
done |
|
9932 | 103 |
|
104 |
text{*\noindent |
|
105 |
The second assumption simplifies to @{term"xs = []"}, which in turn |
|
106 |
simplifies the first assumption to @{term"zs = ys"}, thus reducing the |
|
107 |
conclusion to @{term"ys = ys"} and hence to @{term"True"}. |
|
108 |
||
11458 | 109 |
In some cases, using the assumptions can lead to nontermination: |
9932 | 110 |
*} |
111 |
||
10171 | 112 |
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"; |
9932 | 113 |
|
114 |
txt{*\noindent |
|
11458 | 115 |
An unmodified application of @{text"simp"} loops. The culprit is the |
116 |
simplification rule @{term"f x = g (f (g x))"}, which is extracted from |
|
117 |
the assumption. (Isabelle notices certain simple forms of |
|
118 |
nontermination but not this one.) The problem can be circumvented by |
|
119 |
telling the simplifier to ignore the assumptions: |
|
9932 | 120 |
*} |
121 |
||
10171 | 122 |
apply(simp (no_asm)); |
123 |
done |
|
9932 | 124 |
|
125 |
text{*\noindent |
|
11458 | 126 |
Three modifiers influence the treatment of assumptions: |
9932 | 127 |
\begin{description} |
11458 | 128 |
\item[@{text"(no_asm)"}]\index{*no_asm (modifier)} |
9932 | 129 |
means that assumptions are completely ignored. |
11458 | 130 |
\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)} |
9932 | 131 |
means that the assumptions are not simplified but |
132 |
are used in the simplification of the conclusion. |
|
11458 | 133 |
\item[@{text"(no_asm_use)"}]\index{*no_asm_use (modifier)} |
9932 | 134 |
means that the assumptions are simplified but are not |
135 |
used in the simplification of each other or the conclusion. |
|
136 |
\end{description} |
|
10795 | 137 |
Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on |
138 |
the problematic subgoal above. |
|
11458 | 139 |
Only one of the modifiers is allowed, and it must precede all |
11309 | 140 |
other modifiers. |
11206 | 141 |
|
142 |
\begin{warn} |
|
143 |
Assumptions are simplified in a left-to-right fashion. If an |
|
144 |
assumption can help in simplifying one to the left of it, this may get |
|
145 |
overlooked. In such cases you have to rotate the assumptions explicitly: |
|
11428 | 146 |
\isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"} |
11206 | 147 |
causes a cyclic shift by $n$ positions from right to left, if $n$ is |
148 |
positive, and from left to right, if $n$ is negative. |
|
149 |
Beware that such rotations make proofs quite brittle. |
|
150 |
\end{warn} |
|
9932 | 151 |
*} |
152 |
||
11214 | 153 |
subsection{*Rewriting with Definitions*} |
9932 | 154 |
|
11215 | 155 |
text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions} |
11458 | 156 |
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as |
157 |
simplification rules, but by default they are not: the simplifier does not |
|
158 |
expand them automatically. Definitions are intended for introducing abstract |
|
12582
b85acd66f715
removed Misc/Translations (text covered by Documents.thy);
wenzelm
parents:
12533
diff
changeset
|
159 |
concepts and not merely as abbreviations. Of course, we need to expand |
11458 | 160 |
the definition initially, but once we have proved enough abstract properties |
161 |
of the new constant, we can forget its original definition. This style makes |
|
162 |
proofs more robust: if the definition has to be changed, |
|
163 |
only the proofs of the abstract properties will be affected. |
|
164 |
||
165 |
For example, given *} |
|
9932 | 166 |
|
10788 | 167 |
constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
168 |
"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"; |
|
9932 | 169 |
|
170 |
text{*\noindent |
|
171 |
we may want to prove |
|
172 |
*} |
|
173 |
||
10788 | 174 |
lemma "xor A (\<not>A)"; |
9932 | 175 |
|
176 |
txt{*\noindent |
|
11428 | 177 |
Typically, we begin by unfolding some definitions: |
178 |
\indexbold{definitions!unfolding} |
|
9932 | 179 |
*} |
180 |
||
10788 | 181 |
apply(simp only:xor_def); |
9932 | 182 |
|
183 |
txt{*\noindent |
|
184 |
In this particular case, the resulting goal |
|
10362 | 185 |
@{subgoals[display,indent=0]} |
10171 | 186 |
can be proved by simplification. Thus we could have proved the lemma outright by |
10788 | 187 |
*}(*<*)oops;lemma "xor A (\<not>A)";(*>*) |
188 |
apply(simp add: xor_def) |
|
10171 | 189 |
(*<*)done(*>*) |
9932 | 190 |
text{*\noindent |
191 |
Of course we can also unfold definitions in the middle of a proof. |
|
192 |
||
193 |
\begin{warn} |
|
10971 | 194 |
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold |
195 |
occurrences of $f$ with at least two arguments. This may be helpful for unfolding |
|
196 |
$f$ selectively, but it may also get in the way. Defining |
|
197 |
$f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$. |
|
9932 | 198 |
\end{warn} |
12473 | 199 |
|
200 |
There is also the special method \isa{unfold}\index{*unfold (method)|bold} |
|
201 |
which merely unfolds |
|
202 |
one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}. |
|
203 |
This is can be useful in situations where \isa{simp} does too much. |
|
12533 | 204 |
Warning: \isa{unfold} acts on all subgoals! |
9932 | 205 |
*} |
206 |
||
11214 | 207 |
subsection{*Simplifying {\tt\slshape let}-Expressions*} |
9932 | 208 |
|
11458 | 209 |
text{*\index{simplification!of \isa{let}-expressions}\index{*let expressions}% |
210 |
Proving a goal containing \isa{let}-expressions almost invariably requires the |
|
211 |
@{text"let"}-con\-structs to be expanded at some point. Since |
|
212 |
@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for |
|
213 |
the predefined constant @{term"Let"}, expanding @{text"let"}-constructs |
|
214 |
means rewriting with \tdx{Let_def}: *} |
|
9932 | 215 |
|
216 |
lemma "(let xs = [] in xs@ys@xs) = ys"; |
|
10171 | 217 |
apply(simp add: Let_def); |
218 |
done |
|
9932 | 219 |
|
220 |
text{* |
|
221 |
If, in a particular context, there is no danger of a combinatorial explosion |
|
11458 | 222 |
of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by |
9932 | 223 |
default: |
224 |
*} |
|
225 |
declare Let_def [simp] |
|
226 |
||
11458 | 227 |
subsection{*Conditional Simplification Rules*} |
9932 | 228 |
|
229 |
text{* |
|
11458 | 230 |
\index{conditional simplification rules}% |
9932 | 231 |
So far all examples of rewrite rules were equations. The simplifier also |
232 |
accepts \emph{conditional} equations, for example |
|
233 |
*} |
|
234 |
||
10171 | 235 |
lemma hd_Cons_tl[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"; |
236 |
apply(case_tac xs, simp, simp); |
|
237 |
done |
|
9932 | 238 |
|
239 |
text{*\noindent |
|
240 |
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a |
|
241 |
sequence of methods. Assuming that the simplification rule |
|
242 |
@{term"(rev xs = []) = (xs = [])"} |
|
243 |
is present as well, |
|
10795 | 244 |
the lemma below is proved by plain simplification: |
9932 | 245 |
*} |
246 |
||
10171 | 247 |
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"; |
9932 | 248 |
(*<*) |
249 |
by(simp); |
|
250 |
(*>*) |
|
251 |
text{*\noindent |
|
10795 | 252 |
The conditional equation @{thm[source]hd_Cons_tl} above |
9932 | 253 |
can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"} |
254 |
because the corresponding precondition @{term"rev xs ~= []"} |
|
255 |
simplifies to @{term"xs ~= []"}, which is exactly the local |
|
256 |
assumption of the subgoal. |
|
257 |
*} |
|
258 |
||
259 |
||
11214 | 260 |
subsection{*Automatic Case Splits*} |
9932 | 261 |
|
11458 | 262 |
text{*\label{sec:AutoCaseSplits}\indexbold{case splits}% |
263 |
Goals containing @{text"if"}-expressions\index{*if expressions!splitting of} |
|
264 |
are usually proved by case |
|
265 |
distinction on the boolean condition. Here is an example: |
|
9932 | 266 |
*} |
267 |
||
10171 | 268 |
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []"; |
9932 | 269 |
|
270 |
txt{*\noindent |
|
11458 | 271 |
The goal can be split by a special method, \methdx{split}: |
9932 | 272 |
*} |
273 |
||
10654 | 274 |
apply(split split_if) |
9932 | 275 |
|
10362 | 276 |
txt{*\noindent |
277 |
@{subgoals[display,indent=0]} |
|
11428 | 278 |
where \tdx{split_if} is a theorem that expresses splitting of |
10654 | 279 |
@{text"if"}s. Because |
11458 | 280 |
splitting the @{text"if"}s is usually the right proof strategy, the |
281 |
simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"} |
|
9932 | 282 |
on the initial goal above. |
283 |
||
11428 | 284 |
This splitting idea generalizes from @{text"if"} to \sdx{case}. |
11458 | 285 |
Let us simplify a case analysis over lists:\index{*list.split (theorem)} |
10654 | 286 |
*}(*<*)by simp(*>*) |
10171 | 287 |
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"; |
10654 | 288 |
apply(split list.split); |
11309 | 289 |
|
10362 | 290 |
txt{* |
291 |
@{subgoals[display,indent=0]} |
|
11458 | 292 |
The simplifier does not split |
293 |
@{text"case"}-expressions, as it does @{text"if"}-expressions, |
|
294 |
because with recursive datatypes it could lead to nontermination. |
|
295 |
Instead, the simplifier has a modifier |
|
11494 | 296 |
@{text split}\index{*split (modifier)} |
11458 | 297 |
for adding splitting rules explicitly. The |
298 |
lemma above can be proved in one step by |
|
9932 | 299 |
*} |
10362 | 300 |
(*<*)oops; |
10171 | 301 |
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"; |
9932 | 302 |
(*>*) |
10171 | 303 |
apply(simp split: list.split); |
304 |
(*<*)done(*>*) |
|
10654 | 305 |
text{*\noindent |
306 |
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed. |
|
9932 | 307 |
|
11458 | 308 |
Every datatype $t$ comes with a theorem |
9932 | 309 |
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either |
11458 | 310 |
locally as above, or by giving it the \attrdx{split} attribute globally: |
9932 | 311 |
*} |
312 |
||
313 |
declare list.split [split] |
|
314 |
||
315 |
text{*\noindent |
|
316 |
The @{text"split"} attribute can be removed with the @{text"del"} modifier, |
|
317 |
either locally |
|
318 |
*} |
|
319 |
(*<*) |
|
320 |
lemma "dummy=dummy"; |
|
321 |
(*>*) |
|
322 |
apply(simp split del: split_if); |
|
323 |
(*<*) |
|
324 |
oops; |
|
325 |
(*>*) |
|
326 |
text{*\noindent |
|
327 |
or globally: |
|
328 |
*} |
|
329 |
declare list.split [split del] |
|
330 |
||
331 |
text{* |
|
11458 | 332 |
Polished proofs typically perform splitting within @{text simp} rather than |
333 |
invoking the @{text split} method. However, if a goal contains |
|
334 |
several @{text if} and @{text case} expressions, |
|
335 |
the @{text split} method can be |
|
10654 | 336 |
helpful in selectively exploring the effects of splitting. |
337 |
||
11458 | 338 |
The split rules shown above are intended to affect only the subgoal's |
339 |
conclusion. If you want to split an @{text"if"} or @{text"case"}-expression |
|
340 |
in the assumptions, you have to apply \tdx{split_if_asm} or |
|
341 |
$t$@{text".split_asm"}: *} |
|
9932 | 342 |
|
10654 | 343 |
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []" |
344 |
apply(split split_if_asm) |
|
9932 | 345 |
|
10362 | 346 |
txt{*\noindent |
11458 | 347 |
Unlike splitting the conclusion, this step creates two |
348 |
separate subgoals, which here can be solved by @{text"simp_all"}: |
|
10362 | 349 |
@{subgoals[display,indent=0]} |
9932 | 350 |
If you need to split both in the assumptions and the conclusion, |
351 |
use $t$@{text".splits"} which subsumes $t$@{text".split"} and |
|
352 |
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}. |
|
353 |
||
354 |
\begin{warn} |
|
11458 | 355 |
The simplifier merely simplifies the condition of an |
356 |
\isa{if}\index{*if expressions!simplification of} but not the |
|
9932 | 357 |
\isa{then} or \isa{else} parts. The latter are simplified only after the |
358 |
condition reduces to \isa{True} or \isa{False}, or after splitting. The |
|
11428 | 359 |
same is true for \sdx{case}-expressions: only the selector is |
9932 | 360 |
simplified at first, until either the expression reduces to one of the |
361 |
cases or it is split. |
|
11458 | 362 |
\end{warn} |
9932 | 363 |
*} |
10362 | 364 |
(*<*) |
365 |
by(simp_all) |
|
366 |
(*>*) |
|
9932 | 367 |
|
11214 | 368 |
subsection{*Tracing*} |
9932 | 369 |
text{*\indexbold{tracing the simplifier} |
370 |
Using the simplifier effectively may take a bit of experimentation. Set the |
|
11428 | 371 |
\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} |
372 |
to get a better idea of what is going |
|
9932 | 373 |
on: |
374 |
*} |
|
375 |
||
376 |
ML "set trace_simp"; |
|
377 |
lemma "rev [a] = []"; |
|
378 |
apply(simp); |
|
379 |
(*<*)oops(*>*) |
|
380 |
||
381 |
text{*\noindent |
|
382 |
produces the trace |
|
383 |
||
384 |
\begin{ttbox}\makeatother |
|
385 |
Applying instance of rewrite rule: |
|
386 |
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1] |
|
387 |
Rewriting: |
|
10971 | 388 |
rev [a] == rev [] @ [a] |
9932 | 389 |
Applying instance of rewrite rule: |
390 |
rev [] == [] |
|
391 |
Rewriting: |
|
392 |
rev [] == [] |
|
393 |
Applying instance of rewrite rule: |
|
394 |
[] @ ?y == ?y |
|
395 |
Rewriting: |
|
10971 | 396 |
[] @ [a] == [a] |
9932 | 397 |
Applying instance of rewrite rule: |
398 |
?x3 \# ?t3 = ?t3 == False |
|
399 |
Rewriting: |
|
10971 | 400 |
[a] = [] == False |
9932 | 401 |
\end{ttbox} |
402 |
||
11309 | 403 |
The trace lists each rule being applied, both in its general form and the |
404 |
instance being used. For conditional rules, the trace lists the rule |
|
405 |
it is trying to rewrite and gives the result of attempting to prove |
|
406 |
each of the rule's conditions. Many other hints about the simplifier's |
|
407 |
actions will appear. |
|
408 |
||
11458 | 409 |
In more complicated cases, the trace can be quite lengthy. Invocations of the |
410 |
simplifier are often nested, for instance when solving conditions of rewrite |
|
411 |
rules. Thus it is advisable to reset it: |
|
9932 | 412 |
*} |
413 |
||
414 |
ML "reset trace_simp"; |
|
415 |
||
416 |
(*<*) |
|
9922 | 417 |
end |
9932 | 418 |
(*>*) |