1 % |
|
2 \begin{isabellebody}% |
|
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}% |
|
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 |
|
9 \isacommand{by}\ simp% |
|
10 \begin{isamarkuptext}% |
|
11 \noindent |
|
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}. |
|
15 |
|
16 In some cases this may be too much of a good thing and may lead to |
|
17 nontermination:% |
|
18 \end{isamarkuptext}% |
|
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}% |
|
20 \begin{isamarkuptxt}% |
|
21 \noindent |
|
22 cannot be solved by an unmodified application of \isa{simp} because the |
|
23 simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption |
|
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}% |
|
28 \isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}% |
|
29 \begin{isamarkuptext}% |
|
30 \noindent |
|
31 There are three options that influence the treatment of assumptions: |
|
32 \begin{description} |
|
33 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm} |
|
34 means that assumptions are completely ignored. |
|
35 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp} |
|
36 means that the assumptions are not simplified but |
|
37 are used in the simplification of the conclusion. |
|
38 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use} |
|
39 means that the assumptions are simplified but are not |
|
40 used in the simplification of each other or the conclusion. |
|
41 \end{description} |
|
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. |
|
44 |
|
45 Note that only one of the above options is allowed, and it must precede all |
|
46 other arguments.% |
|
47 \end{isamarkuptext}% |
|
48 \end{isabellebody}% |
|
49 %%% Local Variables: |
|
50 %%% mode: latex |
|
51 %%% TeX-master: "root" |
|
52 %%% End: |
|