equal
deleted
inserted
replaced
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:case-expressions}\index{*case expressions}% |
9 \label{sec:case-expressions}\index{*case expressions}% |
10 HOL also features \isa{case}-expressions for analyzing |
10 HOL also features \isa{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}}{\isasymColon}{\isacharprime}a\ {\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}}{\isasymColon}{\isacharprime}a} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
16 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of |
16 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of |
17 the same type, it follows that \isa{y} is of type \isa{nat} and hence |
17 the same type, it follows that \isa{y} is of type \isa{nat} and hence |
18 that \isa{xs} is of type \isa{nat\ list}.) |
18 that \isa{xs} is of type \isa{nat\ list}.) |
19 |
19 |
20 In general, if $e$ is a term of the datatype $t$ defined in |
20 In general, if $e$ is a term of the datatype $t$ defined in |
39 \begin{isabelle}% |
39 \begin{isabelle}% |
40 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ {\isadigit{1}}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y% |
40 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ {\isadigit{1}}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y% |
41 \end{isabelle} |
41 \end{isabelle} |
42 write |
42 write |
43 \begin{isabelle}% |
43 \begin{isabelle}% |
44 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\isanewline |
44 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}{\isasymColon}{\isacharprime}a\isanewline |
45 \isaindent{\ \ \ \ \ }{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y% |
45 \isaindent{\ \ \ \ \ }{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y% |
46 \end{isabelle} |
46 \end{isabelle} |
47 |
47 |
48 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
48 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
49 indicate their scope% |
49 indicate their scope% |