doc-src/TutorialI/Misc/case_exprs.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

(*<*)
theory case_exprs = Main:
(*>*)

subsection{*Case Expressions*}

text{*\label{sec:case-expressions}\index{*case expressions}%
HOL also features \isa{case}-expressions for analyzing
elements of a datatype. For example,
@{term[display]"case xs of [] => [] | y#ys => y"}
evaluates to @{term"[]"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
@{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of
the same type, it follows that @{term y} is of type @{typ"'a list"} and hence
that @{term xs} is of type @{typ"'a list list"}.)

In general, if $e$ is a term of the datatype $t$ defined in
\S\ref{sec:general-datatype} above, the corresponding
@{text"case"}-expression analyzing $e$ is
\[
\begin{array}{rrcl}
@{text"case"}~e~@{text"of"} & C@1~x@ {11}~\dots~x@ {1k@1} & \To & e@1 \\
                           \vdots \\
                           \mid & C@m~x@ {m1}~\dots~x@ {mk@m} & \To & e@m
\end{array}
\]

\begin{warn}
\emph{All} constructors must be present, their order is fixed, and nested
patterns are not supported.  Violating these restrictions results in strange
error messages.
\end{warn}
\noindent
Nested patterns can be simulated by nested @{text"case"}-expressions: instead
of
@{text[display]"case xs of [] => [] | [x] => x | x # (y # zs) => y"}
write
@{term[display,eta_contract=false,margin=50]"case xs of [] => [] | x#ys => (case ys of [] => x | y#zs => y)"}

Note that @{text"case"}-expressions may need to be enclosed in parentheses to
indicate their scope
*}

subsection{*Structural Induction and Case Distinction*}

text{*\label{sec:struct-ind-case}
\index{case distinctions}\index{induction!structural}%
Induction is invoked by \methdx{induct_tac}, as we have seen above; 
it works for any datatype.  In some cases, induction is overkill and a case
distinction over all constructors of the datatype suffices.  This is performed
by \methdx{case_tac}.  Here is a trivial example:
*}

lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
apply(case_tac xs);

txt{*\noindent
results in the proof state
@{subgoals[display,indent=0,margin=65]}
which is solved automatically:
*}

apply(auto)
(*<*)done(*>*)
text{*
Note that we do not need to give a lemma a name if we do not intend to refer
to it explicitly in the future.
Other basic laws about a datatype are applied automatically during
simplification, so no special methods are provided for them.

\begin{warn}
  Induction is only allowed on free (or \isasymAnd-bound) variables that
  should not occur among the assumptions of the subgoal; see
  \S\ref{sec:ind-var-in-prems} for details. Case distinction
  (@{text"case_tac"}) works for arbitrary terms, which need to be
  quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound
  variables, the terms must not contain variables that are bound outside.
  For example, given the goal @{prop"\<forall>xs. xs = [] \<or> (\<exists>y ys. xs = y#ys)"},
  @{text"case_tac xs"} will not work as expected because Isabelle interprets
  the @{term xs} as a new free variable distinct from the bound
  @{term xs} in the goal.
\end{warn}
*}

(*<*)
end
(*>*)