\begin{isabelle}%

%

\begin{isamarkuptext}%

Goals containing \isaindex{if}-expressions are usually proved by case

distinction on the condition of the \isa{if}. For example the goal%

\end{isamarkuptext}%

\isacommand{lemma}~{"}{\isasymforall}xs.~if~xs~=~[]~then~rev~xs~=~[]~else~rev~xs~{\isasymnoteq}~[]{"}%

\begin{isamarkuptxt}%

\noindent

can be split into

\begin{isabellepar}%

~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%

\end{isabellepar}%

by a degenerate form of simplification%

\end{isamarkuptxt}%

\isacommand{apply}(simp~only:~split:~split\_if)%

\begin{isamarkuptext}%

\noindent

where no simplification rules are included (\isa{only:} is followed by the

empty list of theorems) but the rule \isaindexbold{split_if} for

splitting \isa{if}s is added (via the modifier \isa{split:}). Because

case-splitting on \isa{if}s is almost always the right proof strategy, the

simplifier performs it automatically. Try \isacommand{apply}\isa{(simp)}

on the initial goal above.

This splitting idea generalizes from \isa{if} to \isaindex{case}:%

\end{isamarkuptext}%

\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~zs~|~y\#ys~{\isasymRightarrow}~y\#(ys@zs))~=~xs@zs{"}%

\begin{isamarkuptxt}%

\noindent

becomes

\begin{isabellepar}%

~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline

~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%

\end{isabellepar}%

by typing%

\end{isamarkuptxt}%

\isacommand{apply}(simp~only:~split:~list.split)%

\begin{isamarkuptext}%

\noindent

In contrast to \isa{if}-expressions, the simplifier does not split

\isa{case}-expressions by default because this can lead to nontermination

in case of recursive datatypes. Again, if the \isa{only:} modifier is

dropped, the above goal is solved,%

\end{isamarkuptext}%

\isacommand{apply}(simp~split:~list.split)\isacommand{.}%

\begin{isamarkuptext}%

\noindent%

which \isacommand{apply}\isa{(simp)} alone will not do.

In general, every datatype $t$ comes with a theorem

\isa{$t$.split} which can be declared to be a \bfindex{split rule} either

locally as above, or by giving it the \isa{split} attribute globally:%

\end{isamarkuptext}%

\isacommand{theorems}~[split]~=~list.split%

\begin{isamarkuptext}%

\noindent

The \isa{split} attribute can be removed with the \isa{del} modifier,

either locally%

\end{isamarkuptext}%

\isacommand{apply}(simp~split~del:~split\_if)%

\begin{isamarkuptext}%

\noindent

or globally:%

\end{isamarkuptext}%

\isacommand{theorems}~[split~del]~=~list.split\isanewline

\end{isabelle}%