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}%
|
|
7 |
\isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline
|
|
8 |
\isacommand{apply}~simp\isacommand{.}%
|
|
9 |
\begin{isamarkuptext}%
|
|
10 |
\noindent
|
|
11 |
The second assumption simplifies to \isa{xs = []}, which in turn
|
|
12 |
simplifies the first assumption to \isa{zs = ys}, thus reducing the
|
|
13 |
conclusion to \isa{ys = ys} and hence to \isa{True}.
|
|
14 |
|
|
15 |
In some cases this may be too much of a good thing and may lead to
|
|
16 |
nontermination:%
|
|
17 |
\end{isamarkuptext}%
|
|
18 |
\isacommand{lemma}~{"}{\isasymforall}x.~f~x~=~g~(f~(g~x))~{\isasymLongrightarrow}~f~[]~=~f~[]~@~[]{"}%
|
|
19 |
\begin{isamarkuptxt}%
|
|
20 |
\noindent
|
|
21 |
cannot be solved by an unmodified application of \isa{simp} because the
|
|
22 |
simplification rule \isa{f x = g(f(g x))} extracted from the assumption
|
|
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}%
|
8823
|
27 |
\isacommand{apply}(simp~(no\_asm))\isacommand{.}%
|
8749
|
28 |
\begin{isamarkuptext}%
|
|
29 |
\noindent
|
8823
|
30 |
There are three options that influence the treatment of assumptions:
|
8749
|
31 |
\begin{description}
|
8823
|
32 |
\item[\isaindexbold{(no_asm)}] means that assumptions are completely ignored.
|
|
33 |
\item[\isaindexbold{(no_asm_simp)}] means that the assumptions are not simplified but
|
8749
|
34 |
are used in the simplification of the conclusion.
|
8823
|
35 |
\item[\isaindexbold{(no_asm_use)}] means that the assumptions are simplified
|
8749
|
36 |
but are not
|
|
37 |
used in the simplification of each other or the conclusion.
|
|
38 |
\end{description}
|
8823
|
39 |
Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
|
8749
|
40 |
problematic subgoal.
|
|
41 |
|
8823
|
42 |
Note that only one of the above options is allowed, and it must precede all
|
|
43 |
other arguments.%
|
8749
|
44 |
\end{isamarkuptext}%
|
|
45 |
\end{isabelle}%
|