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