%

\begin{isabellebody}%

%

\begin{isamarkuptext}%

By default, assumptions are part of the simplification process: they are used

as simplification rules and are simplified themselves. For example:%

\end{isamarkuptext}%

\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

\isacommand{by}\ simp%

\begin{isamarkuptext}%

\noindent

The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn

simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the

conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.

In some cases this may be too much of a good thing and may lead to

nontermination:%

\end{isamarkuptext}%

\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}%

\begin{isamarkuptxt}%

\noindent

cannot be solved by an unmodified application of \isa{simp} because the

simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption

does not terminate. Isabelle notices certain simple forms of

nontermination but not this one. The problem can be circumvented by

explicitly telling the simplifier to ignore the assumptions:%

\end{isamarkuptxt}%

\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%

\begin{isamarkuptext}%

\noindent

There are three options that influence the treatment of assumptions:

\begin{description}

\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}

 means that assumptions are completely ignored.

\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}

 means that the assumptions are not simplified but

  are used in the simplification of the conclusion.

\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}

 means that the assumptions are simplified but are not

  used in the simplification of each other or the conclusion.

\end{description}

Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify

the above problematic subgoal.

Note that only one of the above options is allowed, and it must precede all

other arguments.%

\end{isamarkuptext}%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: