doc-src/TutorialI/Misc/document/cond_rewr.tex

*** empty log message ***

\begin{isabelle}%
%
\begin{isamarkuptext}%
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example%
\end{isamarkuptext}%
\isacommand{lemma}~hd\_Cons\_tl[simp]:~{"}xs~{\isasymnoteq}~[]~~{\isasymLongrightarrow}~~hd~xs~\#~tl~xs~=~xs{"}\isanewline
\isacommand{apply}(case\_tac~xs,~simp,~simp)\isacommand{.}%
\begin{isamarkuptext}%
\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
sequence of methods. Assuming that the simplification rule%
\end{isamarkuptext}%
~{"}(rev~xs~=~[])~=~(xs~=~[]){"}%
\begin{isamarkuptext}%
\noindent
is present as well,%
\end{isamarkuptext}%
\isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}%
\begin{isamarkuptext}%
\noindent
is proved by plain simplification:
the conditional equation \isa{hd_Cons_tl} above
can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
assumption of the subgoal.%
\end{isamarkuptext}%
\end{isabelle}%