equal
deleted
inserted
replaced
1 (*<*) |
|
2 theory trace_simp = Main:; |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
6 Using the simplifier effectively may take a bit of experimentation. Set the |
|
7 \isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going |
|
8 on: |
|
9 *} |
|
10 ML "set trace_simp"; |
|
11 lemma "rev [a] = []"; |
|
12 apply(simp); |
|
13 |
|
14 txt{*\noindent |
|
15 produces the trace |
|
16 |
|
17 \begin{ttbox} |
|
18 Applying instance of rewrite rule: |
|
19 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1] |
|
20 Rewriting: |
|
21 rev [x] == rev [] @ [x] |
|
22 Applying instance of rewrite rule: |
|
23 rev [] == [] |
|
24 Rewriting: |
|
25 rev [] == [] |
|
26 Applying instance of rewrite rule: |
|
27 [] @ ?y == ?y |
|
28 Rewriting: |
|
29 [] @ [x] == [x] |
|
30 Applying instance of rewrite rule: |
|
31 ?x3 \# ?t3 = ?t3 == False |
|
32 Rewriting: |
|
33 [x] = [] == False |
|
34 \end{ttbox} |
|
35 |
|
36 In more complicated cases, the trace can be quite lenghty, especially since |
|
37 invocations of the simplifier are often nested (e.g.\ when solving conditions |
|
38 of rewrite rules). Thus it is advisable to reset it: |
|
39 *} |
|
40 |
|
41 ML "reset trace_simp"; |
|
42 |
|
43 (*<*) |
|
44 oops; |
|
45 end |
|
46 (*>*) |
|