7 \end{isamarkuptext}% |
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 |
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% |
9 \isacommand{by}\ simp% |
10 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
11 \noindent |
11 \noindent |
12 The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn |
12 The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn |
13 simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the |
13 simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the |
14 conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}. |
14 conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}. |
15 |
15 |
16 In some cases this may be too much of a good thing and may lead to |
16 In some cases this may be too much of a good thing and may lead to |
17 nontermination:% |
17 nontermination:% |
18 \end{isamarkuptext}% |
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}% |
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}% |
20 \begin{isamarkuptxt}% |
21 \noindent |
21 \noindent |
22 cannot be solved by an unmodified application of \isa{simp} because the |
22 cannot be solved by an unmodified application of \isa{simp} because the |
23 simplification rule \isa{\mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ {\isacharparenleft}\mbox{f}\ {\isacharparenleft}\mbox{g}\ \mbox{x}{\isacharparenright}{\isacharparenright}} extracted from the assumption |
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 |
24 does not terminate. Isabelle notices certain simple forms of |
25 nontermination but not this one. The problem can be circumvented by |
25 nontermination but not this one. The problem can be circumvented by |
26 explicitly telling the simplifier to ignore the assumptions:% |
26 explicitly telling the simplifier to ignore the assumptions:% |
27 \end{isamarkuptxt}% |
27 \end{isamarkuptxt}% |
28 \isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}% |
28 \isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}% |
29 \begin{isamarkuptext}% |
29 \begin{isamarkuptext}% |
30 \noindent |
30 \noindent |
31 There are three options that influence the treatment of assumptions: |
31 There are three options that influence the treatment of assumptions: |
32 \begin{description} |
32 \begin{description} |
33 \item[\isa{(no_asm)}]\indexbold{*no_asm} |
33 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm} |
34 means that assumptions are completely ignored. |
34 means that assumptions are completely ignored. |
35 \item[\isa{(no_asm_simp)}]\indexbold{*no_asm_simp} |
35 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp} |
36 means that the assumptions are not simplified but |
36 means that the assumptions are not simplified but |
37 are used in the simplification of the conclusion. |
37 are used in the simplification of the conclusion. |
38 \item[\isa{(no_asm_use)}]\indexbold{*no_asm_use} |
38 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use} |
39 means that the assumptions are simplified but are not |
39 means that the assumptions are simplified but are not |
40 used in the simplification of each other or the conclusion. |
40 used in the simplification of each other or the conclusion. |
41 \end{description} |
41 \end{description} |
42 Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above |
42 Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify |
43 problematic subgoal. |
43 the above problematic subgoal. |
44 |
44 |
45 Note that only one of the above options is allowed, and it must precede all |
45 Note that only one of the above options is allowed, and it must precede all |
46 other arguments.% |
46 other arguments.% |
47 \end{isamarkuptext}% |
47 \end{isamarkuptext}% |
48 \end{isabellebody}% |
48 \end{isabellebody}% |