1 (*<*) |
|
2 theory asm_simp = Main:; |
|
3 |
|
4 (*>*)text{* |
|
5 By default, assumptions are part of the simplification process: they are used |
|
6 as simplification rules and are simplified themselves. For example: |
|
7 *} |
|
8 |
|
9 lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs"; |
|
10 by simp; |
|
11 |
|
12 text{*\noindent |
|
13 The second assumption simplifies to @{term"xs = []"}, which in turn |
|
14 simplifies the first assumption to @{term"zs = ys"}, thus reducing the |
|
15 conclusion to @{term"ys = ys"} and hence to @{term"True"}. |
|
16 |
|
17 In some cases this may be too much of a good thing and may lead to |
|
18 nontermination: |
|
19 *} |
|
20 |
|
21 lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []"; |
|
22 |
|
23 txt{*\noindent |
|
24 cannot be solved by an unmodified application of @{text"simp"} because the |
|
25 simplification rule @{term"f x = g (f (g x))"} extracted from the assumption |
|
26 does not terminate. Isabelle notices certain simple forms of |
|
27 nontermination but not this one. The problem can be circumvented by |
|
28 explicitly telling the simplifier to ignore the assumptions: |
|
29 *} |
|
30 |
|
31 by(simp (no_asm)); |
|
32 |
|
33 text{*\noindent |
|
34 There are three options that influence the treatment of assumptions: |
|
35 \begin{description} |
|
36 \item[@{text"(no_asm)"}]\indexbold{*no_asm} |
|
37 means that assumptions are completely ignored. |
|
38 \item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp} |
|
39 means that the assumptions are not simplified but |
|
40 are used in the simplification of the conclusion. |
|
41 \item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use} |
|
42 means that the assumptions are simplified but are not |
|
43 used in the simplification of each other or the conclusion. |
|
44 \end{description} |
|
45 Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify |
|
46 the above problematic subgoal. |
|
47 |
|
48 Note that only one of the above options is allowed, and it must precede all |
|
49 other arguments. |
|
50 *} |
|
51 (*<*)end(*>*) |
|