21 The simplification attribute of theorems can be turned on and off as follows: |
21 The simplification attribute of theorems can be turned on and off as follows: |
22 \begin{quote} |
22 \begin{quote} |
23 \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\ |
23 \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\ |
24 \isacommand{declare} \textit{theorem-name}@{text"[simp del]"} |
24 \isacommand{declare} \textit{theorem-name}@{text"[simp del]"} |
25 \end{quote} |
25 \end{quote} |
26 As a rule of thumb, equations that really simplify (like @{prop"rev(rev xs) = |
26 Only equations that really simplify, like \isa{rev\ |
27 xs"} and @{prop"xs @ [] = xs"}) should be made simplification |
27 {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and |
28 rules. Those of a more specific nature (e.g.\ distributivity laws, which |
28 \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ |
29 alter the structure of terms considerably) should only be used selectively, |
29 {\isacharequal}\ xs}, should be declared as default simplification rules. |
30 i.e.\ they should not be default simplification rules. Conversely, it may |
30 More specific ones should only be used selectively and should |
31 also happen that a simplification rule needs to be disabled in certain |
31 not be made default. Distributivity laws, for example, alter |
32 proofs. Frequent changes in the simplification status of a theorem may |
32 the structure of terms and can produce an exponential blow-up instead of |
33 indicate a badly designed theory. |
33 simplification. A default simplification rule may |
|
34 need to be disabled in certain proofs. Frequent changes in the simplification |
|
35 status of a theorem may indicate an unwise use of defaults. |
34 \begin{warn} |
36 \begin{warn} |
35 Simplification may run forever, for example if both $f(x) = g(x)$ and |
37 Simplification may run forever, for example if both $f(x) = g(x)$ and |
36 $g(x) = f(x)$ are simplification rules. It is the user's responsibility not |
38 $g(x) = f(x)$ are simplification rules. It is the user's responsibility not |
37 to include simplification rules that can lead to nontermination, either on |
39 to include simplification rules that can lead to nontermination, either on |
38 their own or in combination with other simplification rules. |
40 their own or in combination with other simplification rules. |
45 The general format of the simplification method is |
47 The general format of the simplification method is |
46 \begin{quote} |
48 \begin{quote} |
47 @{text simp} \textit{list of modifiers} |
49 @{text simp} \textit{list of modifiers} |
48 \end{quote} |
50 \end{quote} |
49 where the list of \emph{modifiers} fine tunes the behaviour and may |
51 where the list of \emph{modifiers} fine tunes the behaviour and may |
50 be empty. Most if not all of the proofs seen so far could have been performed |
52 be empty. Specific modifiers are discussed below. Most if not all of the |
|
53 proofs seen so far could have been performed |
51 with @{text simp} instead of \isa{auto}, except that @{text simp} attacks |
54 with @{text simp} instead of \isa{auto}, except that @{text simp} attacks |
52 only the first subgoal and may thus need to be repeated --- use |
55 only the first subgoal and may thus need to be repeated --- use |
53 \isaindex{simp_all} to simplify all subgoals. |
56 \isaindex{simp_all} to simplify all subgoals. |
54 Note that @{text simp} fails if nothing changes. |
57 Note that @{text simp} fails if nothing changes. |
55 *} |
58 *} |
68 In case you want to use only a specific list of theorems and ignore all |
71 In case you want to use only a specific list of theorems and ignore all |
69 others: |
72 others: |
70 \begin{quote} |
73 \begin{quote} |
71 @{text"only:"} \textit{list of theorem names} |
74 @{text"only:"} \textit{list of theorem names} |
72 \end{quote} |
75 \end{quote} |
|
76 In this example, we invoke the simplifier, adding two distributive |
|
77 laws: |
|
78 \begin{quote} |
|
79 \isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"} |
|
80 \end{quote} |
73 *} |
81 *} |
74 |
82 |
75 subsection{*Assumptions*} |
83 subsection{*Assumptions*} |
76 |
84 |
77 text{*\index{simplification!with/of assumptions} |
85 text{*\index{simplification!with/of assumptions} |
118 used in the simplification of each other or the conclusion. |
126 used in the simplification of each other or the conclusion. |
119 \end{description} |
127 \end{description} |
120 Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on |
128 Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on |
121 the problematic subgoal above. |
129 the problematic subgoal above. |
122 Note that only one of the modifiers is allowed, and it must precede all |
130 Note that only one of the modifiers is allowed, and it must precede all |
123 other arguments. |
131 other modifiers. |
124 |
132 |
125 \begin{warn} |
133 \begin{warn} |
126 Assumptions are simplified in a left-to-right fashion. If an |
134 Assumptions are simplified in a left-to-right fashion. If an |
127 assumption can help in simplifying one to the left of it, this may get |
135 assumption can help in simplifying one to the left of it, this may get |
128 overlooked. In such cases you have to rotate the assumptions explicitly: |
136 overlooked. In such cases you have to rotate the assumptions explicitly: |
256 @{text"if"}s. Because |
264 @{text"if"}s. Because |
257 case-splitting on @{text"if"}s is almost always the right proof strategy, the |
265 case-splitting on @{text"if"}s is almost always the right proof strategy, the |
258 simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"} |
266 simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"} |
259 on the initial goal above. |
267 on the initial goal above. |
260 |
268 |
261 This splitting idea generalizes from @{text"if"} to \isaindex{case}: |
269 This splitting idea generalizes from @{text"if"} to \isaindex{case}. |
|
270 Let us simplify a case analysis over lists: |
262 *}(*<*)by simp(*>*) |
271 *}(*<*)by simp(*>*) |
263 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"; |
272 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"; |
264 apply(split list.split); |
273 apply(split list.split); |
265 |
274 |
266 txt{* |
275 txt{* |
267 @{subgoals[display,indent=0]} |
276 @{subgoals[display,indent=0]} |
268 In contrast to @{text"if"}-expressions, the simplifier does not split |
277 In contrast to @{text"if"}-expressions, the simplifier does not split |
269 @{text"case"}-expressions by default because this can lead to nontermination |
278 @{text"case"}-expressions by default because this can lead to nontermination |
270 in case of recursive datatypes. Therefore the simplifier has a modifier |
279 in case of recursive datatypes. Therefore the simplifier has a modifier |
394 ?x3 \# ?t3 = ?t3 == False |
403 ?x3 \# ?t3 = ?t3 == False |
395 Rewriting: |
404 Rewriting: |
396 [a] = [] == False |
405 [a] = [] == False |
397 \end{ttbox} |
406 \end{ttbox} |
398 |
407 |
399 In more complicated cases, the trace can be quite lenghty, especially since |
408 The trace lists each rule being applied, both in its general form and the |
|
409 instance being used. For conditional rules, the trace lists the rule |
|
410 it is trying to rewrite and gives the result of attempting to prove |
|
411 each of the rule's conditions. Many other hints about the simplifier's |
|
412 actions will appear. |
|
413 |
|
414 In more complicated cases, the trace can be quite lengthy, especially since |
400 invocations of the simplifier are often nested (e.g.\ when solving conditions |
415 invocations of the simplifier are often nested (e.g.\ when solving conditions |
401 of rewrite rules). Thus it is advisable to reset it: |
416 of rewrite rules). Thus it is advisable to reset it: |
402 *} |
417 *} |
403 |
418 |
404 ML "reset trace_simp"; |
419 ML "reset trace_simp"; |