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

added state: 'a * 'b -> 'a * ('a * 'b);

\begin{isabelle}%
\isanewline
\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
\isacommand{apply}(case\_tac~xs)%
\begin{isamarkuptxt}%
\noindent
results in the proof state
\begin{isabellepar}%
~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
\end{isabellepar}%
which is solved automatically:%
\end{isamarkuptxt}%
\isacommand{apply}(auto)\isacommand{.}\isanewline
\end{isabelle}%