equal
deleted
inserted
replaced
7 \begin{isamarkuptext}% |
7 \begin{isamarkuptext}% |
8 \label{sec:case-expressions} |
8 \label{sec:case-expressions} |
9 HOL also features \isaindexbold{case}-expressions for analyzing |
9 HOL also features \isaindexbold{case}-expressions for analyzing |
10 elements of a datatype. For example, |
10 elements of a datatype. For example, |
11 \begin{isabelle}% |
11 \begin{isabelle}% |
12 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y% |
12 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y% |
13 \end{isabelle} |
13 \end{isabelle} |
14 evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
14 evaluates to \isa{{\isadigit{1}}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
15 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of |
15 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of |
16 the same type, it follows that \isa{y} is of type \isa{nat} and hence |
16 the same type, it follows that \isa{y} is of type \isa{nat} and hence |
17 that \isa{xs} is of type \isa{nat\ list}.) |
17 that \isa{xs} is of type \isa{nat\ list}.) |
18 |
18 |
19 In general, if $e$ is a term of the datatype $t$ defined in |
19 In general, if $e$ is a term of the datatype $t$ defined in |
34 \end{warn} |
34 \end{warn} |
35 \noindent |
35 \noindent |
36 Nested patterns can be simulated by nested \isa{case}-expressions: instead |
36 Nested patterns can be simulated by nested \isa{case}-expressions: instead |
37 of |
37 of |
38 \begin{isabelle}% |
38 \begin{isabelle}% |
39 \ \ \ \ \ 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% |
39 \ \ \ \ \ 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 \end{isabelle} |
40 \end{isabelle} |
41 write |
41 write |
42 \begin{isabelle}% |
42 \begin{isabelle}% |
43 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline |
43 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\isanewline |
44 \ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y% |
44 \ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y% |
45 \end{isabelle} |
45 \end{isabelle} |
46 |
46 |
47 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
47 Note that \isa{case}-expressions may need to be enclosed in parentheses to |
48 indicate their scope% |
48 indicate their scope% |