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