Quelle case_exprs.thy

Sprache: Isabelle

(*<*)
theory case_exprs imports Main begin
(*>*)

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:
›

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

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}
›

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.