1.1 --- a/doc-src/TutorialI/Misc/cases.thy	Tue Aug 29 15:13:10 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,39 +0,0 @@
     1.4 -(*<*)
     1.5 -theory "cases" = Main:;
     1.6 -(*>*)
     1.7 -
     1.8 -subsection{*Structural induction and case distinction*}
     1.9 -
    1.10 -text{*
    1.11 -\indexbold{structural induction}
    1.12 -\indexbold{induction!structural}
    1.13 -\indexbold{case distinction}
    1.14 -Almost all the basic laws about a datatype are applied automatically during
    1.15 -simplification. Only induction is invoked by hand via \isaindex{induct_tac},
    1.16 -which works for any datatype. In some cases, induction is overkill and a case
    1.17 -distinction over all constructors of the datatype suffices. This is performed
    1.18 -by \isaindexbold{case_tac}. A trivial example:
    1.19 -*}
    1.20 -
    1.21 -lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
    1.22 -apply(case_tac xs);
    1.23 -
    1.24 -txt{*\noindent
    1.25 -results in the proof state
    1.26 -\begin{isabellepar}%
    1.27 -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
    1.28 -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
    1.29 -\end{isabellepar}%
    1.30 -which is solved automatically:
    1.31 -*}
    1.32 -
    1.33 -by(auto)
    1.34 -
    1.35 -text{*
    1.36 -Note that we do not need to give a lemma a name if we do not intend to refer
    1.37 -to it explicitly in the future.
    1.38 -*}
    1.39 -
    1.40 -(*<*)
    1.41 -end
    1.42 -(*>*)