text‹
subsection{Case Expressions}
label{sec:case-expressions}\index{*case expressions}%
also features \isa{case}-expressions for analyzing
of a datatype. For example,
{term[display]"case xs of [] => [] | y#ys => y"}
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
same type, it follows that term‹y› is of type 🍋‹'a list› and hence term‹xs› is of type 🍋‹'a list list›.)
general, case expressions are of the form
[
begin{array}{c}
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null ‹|›~pattern@m~‹==>›~e@m
end{array}
]
in functional programming, patterns are expressions consisting of
constructors (e.g. term‹[]› and ‹#›)
variables, including the wildcard ``\verb$_$''.
all cases need to be covered and the order of cases matters.
, one is well-advised not to wallow in complex patterns because
case distinctions tend to induce complex proofs.
begin{warn}
Isabelle only knows about exhaustive case expressions with
-nested patterns: $pattern@i$ must be of the form
C@i~x@ {i1}~\dots~x@ {ik@i}$ and $C@1, \dots, C@m$ must be exactly the
of the type of $e$.
complex case expressions are automatically
into the simpler form upon parsing but are not translated
for printing. This may lead to surprising output.
end{warn}
begin{warn} ‹if›, ‹case›-expressions may need to be enclosed in
to indicate their scope.
end{warn}
subsection{Structural Induction and Case Distinction}
label{sec:struct-ind-case}
index{case distinctions}\index{induction!structural}%
is invoked by \methdx{induct_tac}, as we have seen above;
works for any datatype. In some cases, induction is overkill and a case
over all constructors of the datatype suffices. This is performed \methdx{case_tac}. Here is a trivial example: ›
txt‹\noindent
in the proof state
{subgoals[display,indent=0,margin=65]}
is solved automatically: ›
apply(auto) (*<*)done(*>*) text‹
that we do not need to give a lemma a name if we do not intend to refer
it explicitly in the future.
basic laws about a datatype are applied automatically during
, 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
(‹case_tac›) works for arbitrary terms, which need to be
quoted if they are non-atomic. However, apart from ‹∧›-bound
variables, the terms must not contain variables that are bound outside.
For example, given the goal prop‹∀xs. xs = [] ∨ (∃y ys. xs = y#ys)›, ‹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} ›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
