5 By default, assumptions are part of the simplification process: they are used
6 as simplification rules and are simplified themselves. For example:%
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
10 \begin{isamarkuptext}%
12 The second assumption simplifies to \isa{\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
13 simplifies the first assumption to \isa{\mbox{zs}\ {\isacharequal}\ \mbox{ys}}, thus reducing the
14 conclusion to \isa{\mbox{ys}\ {\isacharequal}\ \mbox{ys}} and hence to \isa{True}.
16 In some cases this may be too much of a good thing and may lead to
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}%
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
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:%
28 \isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
29 \begin{isamarkuptext}%
31 There are three options that influence the treatment of assumptions:
33 \item[\isa{(no_asm)}]\indexbold{*no_asm}
34 means that assumptions are completely ignored.
35 \item[\isa{(no_asm_simp)}]\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{(no_asm_use)}]\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.
42 Neither \isa{(no_asm_simp)} nor \isa{(no_asm_use)} allow to simplify the above
45 Note that only one of the above options is allowed, and it must precede all
51 %%% TeX-master: "root"