8745
|
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";
|
9458
|
10 |
by simp;
|
8745
|
11 |
|
|
12 |
text{*\noindent
|
9541
|
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 \isa{True}.
|
8745
|
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 \isa{simp} because the
|
9541
|
25 |
simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
|
8745
|
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 |
|
9458
|
31 |
by(simp (no_asm));
|
8745
|
32 |
|
|
33 |
text{*\noindent
|
8823
|
34 |
There are three options that influence the treatment of assumptions:
|
8745
|
35 |
\begin{description}
|
9494
|
36 |
\item[\isa{(no_asm)}]\indexbold{*no_asm}
|
|
37 |
means that assumptions are completely ignored.
|
|
38 |
\item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp}
|
|
39 |
means that the assumptions are not simplified but
|
8745
|
40 |
are used in the simplification of the conclusion.
|
9494
|
41 |
\item[\isa{(no_asm_use)}]\indexbold{*no_asm_use}
|
|
42 |
means that the assumptions are simplified but are not
|
8745
|
43 |
used in the simplification of each other or the conclusion.
|
|
44 |
\end{description}
|
8823
|
45 |
Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
|
8745
|
46 |
problematic subgoal.
|
|
47 |
|
8823
|
48 |
Note that only one of the above options is allowed, and it must precede all
|
|
49 |
other arguments.
|
8745
|
50 |
*}
|
|
51 |
(*<*)end(*>*)
|