19 \subsection{Case Expressions} |
19 \subsection{Case Expressions} |
20 \label{sec:case-expressions}\index{*case expressions}% |
20 \label{sec:case-expressions}\index{*case expressions}% |
21 HOL also features \isa{case}-expressions for analyzing |
21 HOL also features \isa{case}-expressions for analyzing |
22 elements of a datatype. For example, |
22 elements of a datatype. For example, |
23 \begin{isabelle}% |
23 \begin{isabelle}% |
24 \ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y% |
24 \ \ \ \ \ case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ y% |
25 \end{isabelle} |
25 \end{isabelle} |
26 evaluates to \isa{{\isacharbrackleft}{\isacharbrackright}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if |
26 evaluates to \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} if \isa{xs} is \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and to \isa{y} if |
27 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of |
27 \isa{xs} is \isa{y\ {\isaliteral{23}{\isacharhash}}\ ys}. (Since the result in both branches must be of |
28 the same type, it follows that \isa{y} is of type \isa{{\isacharprime}a\ list} and hence |
28 the same type, it follows that \isa{y} is of type \isa{{\isaliteral{27}{\isacharprime}}a\ list} and hence |
29 that \isa{xs} is of type \isa{{\isacharprime}a\ list\ list}.) |
29 that \isa{xs} is of type \isa{{\isaliteral{27}{\isacharprime}}a\ list\ list}.) |
30 |
30 |
31 In general, case expressions are of the form |
31 In general, case expressions are of the form |
32 \[ |
32 \[ |
33 \begin{array}{c} |
33 \begin{array}{c} |
34 \isa{case}~e~\isa{of}\ pattern@1~\isa{{\isasymRightarrow}}~e@1\ \isa{{\isacharbar}}\ \dots\ |
34 \isa{case}~e~\isa{of}\ pattern@1~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@1\ \isa{{\isaliteral{7C}{\isacharbar}}}\ \dots\ |
35 \isa{{\isacharbar}}~pattern@m~\isa{{\isasymRightarrow}}~e@m |
35 \isa{{\isaliteral{7C}{\isacharbar}}}~pattern@m~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@m |
36 \end{array} |
36 \end{array} |
37 \] |
37 \] |
38 Like in functional programming, patterns are expressions consisting of |
38 Like in functional programming, patterns are expressions consisting of |
39 datatype constructors (e.g. \isa{{\isacharbrackleft}{\isacharbrackright}} and \isa{{\isacharhash}}) |
39 datatype constructors (e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and \isa{{\isaliteral{23}{\isacharhash}}}) |
40 and variables, including the wildcard ``\verb$_$''. |
40 and variables, including the wildcard ``\verb$_$''. |
41 Not all cases need to be covered and the order of cases matters. |
41 Not all cases need to be covered and the order of cases matters. |
42 However, one is well-advised not to wallow in complex patterns because |
42 However, one is well-advised not to wallow in complex patterns because |
43 complex case distinctions tend to induce complex proofs. |
43 complex case distinctions tend to induce complex proofs. |
44 |
44 |
66 distinction over all constructors of the datatype suffices. This is performed |
66 distinction over all constructors of the datatype suffices. This is performed |
67 by \methdx{case_tac}. Here is a trivial example:% |
67 by \methdx{case_tac}. Here is a trivial example:% |
68 \end{isamarkuptext}% |
68 \end{isamarkuptext}% |
69 \isamarkuptrue% |
69 \isamarkuptrue% |
70 \isacommand{lemma}\isamarkupfalse% |
70 \isacommand{lemma}\isamarkupfalse% |
71 \ {\isachardoublequoteopen}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline |
71 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y{\isaliteral{23}{\isacharhash}}ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
72 % |
72 % |
73 \isadelimproof |
73 \isadelimproof |
74 % |
74 % |
75 \endisadelimproof |
75 \endisadelimproof |
76 % |
76 % |
77 \isatagproof |
77 \isatagproof |
78 \isacommand{apply}\isamarkupfalse% |
78 \isacommand{apply}\isamarkupfalse% |
79 {\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% |
79 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}% |
80 \begin{isamarkuptxt}% |
80 \begin{isamarkuptxt}% |
81 \noindent |
81 \noindent |
82 results in the proof state |
82 results in the proof state |
83 \begin{isabelle}% |
83 \begin{isabelle}% |
84 \ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline |
84 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\isanewline |
85 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline |
85 \ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline |
86 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs% |
86 \isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }xs\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs% |
87 \end{isabelle} |
87 \end{isabelle} |
88 which is solved automatically:% |
88 which is solved automatically:% |
89 \end{isamarkuptxt}% |
89 \end{isamarkuptxt}% |
90 \isamarkuptrue% |
90 \isamarkuptrue% |
91 \isacommand{apply}\isamarkupfalse% |
91 \isacommand{apply}\isamarkupfalse% |
92 {\isacharparenleft}auto{\isacharparenright}% |
92 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
93 \endisatagproof |
93 \endisatagproof |
94 {\isafoldproof}% |
94 {\isafoldproof}% |
95 % |
95 % |
96 \isadelimproof |
96 \isadelimproof |
97 % |
97 % |
105 |
105 |
106 \begin{warn} |
106 \begin{warn} |
107 Induction is only allowed on free (or \isasymAnd-bound) variables that |
107 Induction is only allowed on free (or \isasymAnd-bound) variables that |
108 should not occur among the assumptions of the subgoal; see |
108 should not occur among the assumptions of the subgoal; see |
109 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
109 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
110 (\isa{case{\isacharunderscore}tac}) works for arbitrary terms, which need to be |
110 (\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}) works for arbitrary terms, which need to be |
111 quoted if they are non-atomic. However, apart from \isa{{\isasymAnd}}-bound |
111 quoted if they are non-atomic. However, apart from \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-bound |
112 variables, the terms must not contain variables that are bound outside. |
112 variables, the terms must not contain variables that are bound outside. |
113 For example, given the goal \isa{{\isasymforall}xs{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}y\ ys{\isachardot}\ xs\ {\isacharequal}\ y\ {\isacharhash}\ ys{\isacharparenright}}, |
113 For example, given the goal \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y\ ys{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}}, |
114 \isa{case{\isacharunderscore}tac\ xs} will not work as expected because Isabelle interprets |
114 \isa{case{\isaliteral{5F}{\isacharunderscore}}tac\ xs} will not work as expected because Isabelle interprets |
115 the \isa{xs} as a new free variable distinct from the bound |
115 the \isa{xs} as a new free variable distinct from the bound |
116 \isa{xs} in the goal. |
116 \isa{xs} in the goal. |
117 \end{warn}% |
117 \end{warn}% |
118 \end{isamarkuptext}% |
118 \end{isamarkuptext}% |
119 \isamarkuptrue% |
119 \isamarkuptrue% |