1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{case{\isaliteral{5F}{\isacharunderscore}}exprs}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \subsection{Case Expressions} |
|
20 \label{sec:case-expressions}\index{*case expressions}% |
|
21 HOL also features \isa{case}-expressions for analyzing |
|
22 elements of a datatype. For example, |
|
23 \begin{isabelle}% |
|
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} |
|
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\ {\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{{\isaliteral{27}{\isacharprime}}a\ list} and hence |
|
29 that \isa{xs} is of type \isa{{\isaliteral{27}{\isacharprime}}a\ list\ list}.) |
|
30 |
|
31 In general, case expressions are of the form |
|
32 \[ |
|
33 \begin{array}{c} |
|
34 \isa{case}~e~\isa{of}\ pattern@1~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@1\ \isa{{\isaliteral{7C}{\isacharbar}}}\ \dots\ |
|
35 \isa{{\isaliteral{7C}{\isacharbar}}}~pattern@m~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@m |
|
36 \end{array} |
|
37 \] |
|
38 Like in functional programming, patterns are expressions consisting of |
|
39 datatype constructors (e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and \isa{{\isaliteral{23}{\isacharhash}}}) |
|
40 and variables, including the wildcard ``\verb$_$''. |
|
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 |
|
43 complex case distinctions tend to induce complex proofs. |
|
44 |
|
45 \begin{warn} |
|
46 Internally Isabelle only knows about exhaustive case expressions with |
|
47 non-nested patterns: $pattern@i$ must be of the form |
|
48 $C@i~x@ {i1}~\dots~x@ {ik@i}$ and $C@1, \dots, C@m$ must be exactly the |
|
49 constructors of the type of $e$. |
|
50 % |
|
51 More complex case expressions are automatically |
|
52 translated into the simpler form upon parsing but are not translated |
|
53 back for printing. This may lead to surprising output. |
|
54 \end{warn} |
|
55 |
|
56 \begin{warn} |
|
57 Like \isa{if}, \isa{case}-expressions may need to be enclosed in |
|
58 parentheses to indicate their scope. |
|
59 \end{warn} |
|
60 |
|
61 \subsection{Structural Induction and Case Distinction} |
|
62 \label{sec:struct-ind-case} |
|
63 \index{case distinctions}\index{induction!structural}% |
|
64 Induction is invoked by \methdx{induct_tac}, as we have seen above; |
|
65 it works for any datatype. In some cases, induction is overkill and a case |
|
66 distinction over all constructors of the datatype suffices. This is performed |
|
67 by \methdx{case_tac}. Here is a trivial example:% |
|
68 \end{isamarkuptext}% |
|
69 \isamarkuptrue% |
|
70 \isacommand{lemma}\isamarkupfalse% |
|
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 % |
|
73 \isadelimproof |
|
74 % |
|
75 \endisadelimproof |
|
76 % |
|
77 \isatagproof |
|
78 \isacommand{apply}\isamarkupfalse% |
|
79 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}% |
|
80 \begin{isamarkuptxt}% |
|
81 \noindent |
|
82 results in the proof state |
|
83 \begin{isabelle}% |
|
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}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline |
|
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} |
|
88 which is solved automatically:% |
|
89 \end{isamarkuptxt}% |
|
90 \isamarkuptrue% |
|
91 \isacommand{apply}\isamarkupfalse% |
|
92 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
|
93 \endisatagproof |
|
94 {\isafoldproof}% |
|
95 % |
|
96 \isadelimproof |
|
97 % |
|
98 \endisadelimproof |
|
99 % |
|
100 \begin{isamarkuptext}% |
|
101 Note that we do not need to give a lemma a name if we do not intend to refer |
|
102 to it explicitly in the future. |
|
103 Other basic laws about a datatype are applied automatically during |
|
104 simplification, so no special methods are provided for them. |
|
105 |
|
106 \begin{warn} |
|
107 Induction is only allowed on free (or \isasymAnd-bound) variables that |
|
108 should not occur among the assumptions of the subgoal; see |
|
109 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
|
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{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-bound |
|
112 variables, the terms must not contain variables that are bound outside. |
|
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{\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 |
|
116 \isa{xs} in the goal. |
|
117 \end{warn}% |
|
118 \end{isamarkuptext}% |
|
119 \isamarkuptrue% |
|
120 % |
|
121 \isadelimtheory |
|
122 % |
|
123 \endisadelimtheory |
|
124 % |
|
125 \isatagtheory |
|
126 % |
|
127 \endisatagtheory |
|
128 {\isafoldtheory}% |
|
129 % |
|
130 \isadelimtheory |
|
131 % |
|
132 \endisadelimtheory |
|
133 \end{isabellebody}% |
|
134 %%% Local Variables: |
|
135 %%% mode: latex |
|
136 %%% TeX-master: "root" |
|
137 %%% End: |
|