5 \isamarkupsubsection{Case Expressions% |
5 \isamarkupsubsection{Case Expressions% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:case-expressions} |
9 \label{sec:case-expressions} |
10 HOL also features \isaindexbold{case}-expressions for analyzing |
10 HOL also features \sdx{case}-expressions for analyzing |
11 elements of a datatype. For example, |
11 elements of a datatype. For example, |
12 \begin{isabelle}% |
12 \begin{isabelle}% |
13 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y% |
13 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y% |
14 \end{isabelle} |
14 \end{isabelle} |
15 evaluates to \isa{{\isadigit{1}}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
15 evaluates to \isa{{\isadigit{1}}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
56 \label{sec:struct-ind-case} |
56 \label{sec:struct-ind-case} |
57 \indexbold{structural induction} |
57 \indexbold{structural induction} |
58 \indexbold{induction!structural} |
58 \indexbold{induction!structural} |
59 \indexbold{case distinction} |
59 \indexbold{case distinction} |
60 Almost all the basic laws about a datatype are applied automatically during |
60 Almost all the basic laws about a datatype are applied automatically during |
61 simplification. Only induction is invoked by hand via \isaindex{induct_tac}, |
61 simplification. Only induction is invoked by hand via \methdx{induct_tac}, |
62 which works for any datatype. In some cases, induction is overkill and a case |
62 which works for any datatype. In some cases, induction is overkill and a case |
63 distinction over all constructors of the datatype suffices. This is performed |
63 distinction over all constructors of the datatype suffices. This is performed |
64 by \isaindexbold{case_tac}. A trivial example:% |
64 by \methdx{case_tac}. A trivial example:% |
65 \end{isamarkuptext}% |
65 \end{isamarkuptext}% |
66 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
66 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline |
67 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% |
67 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% |
68 \begin{isamarkuptxt}% |
68 \begin{isamarkuptxt}% |
69 \noindent |
69 \noindent |