1 (*<*) |
|
2 theory case_exprs imports Main begin |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
6 \subsection{Case Expressions} |
|
7 \label{sec:case-expressions}\index{*case expressions}% |
|
8 HOL also features \isa{case}-expressions for analyzing |
|
9 elements of a datatype. For example, |
|
10 @{term[display]"case xs of [] => [] | y#ys => y"} |
|
11 evaluates to @{term"[]"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if |
|
12 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of |
|
13 the same type, it follows that @{term y} is of type @{typ"'a list"} and hence |
|
14 that @{term xs} is of type @{typ"'a list list"}.) |
|
15 |
|
16 In general, case expressions are of the form |
|
17 \[ |
|
18 \begin{array}{c} |
|
19 @{text"case"}~e~@{text"of"}\ pattern@1~@{text"\<Rightarrow>"}~e@1\ @{text"|"}\ \dots\ |
|
20 @{text"|"}~pattern@m~@{text"\<Rightarrow>"}~e@m |
|
21 \end{array} |
|
22 \] |
|
23 Like in functional programming, patterns are expressions consisting of |
|
24 datatype constructors (e.g. @{term"[]"} and @{text"#"}) |
|
25 and variables, including the wildcard ``\verb$_$''. |
|
26 Not all cases need to be covered and the order of cases matters. |
|
27 However, one is well-advised not to wallow in complex patterns because |
|
28 complex case distinctions tend to induce complex proofs. |
|
29 |
|
30 \begin{warn} |
|
31 Internally Isabelle only knows about exhaustive case expressions with |
|
32 non-nested patterns: $pattern@i$ must be of the form |
|
33 $C@i~x@ {i1}~\dots~x@ {ik@i}$ and $C@1, \dots, C@m$ must be exactly the |
|
34 constructors of the type of $e$. |
|
35 % |
|
36 More complex case expressions are automatically |
|
37 translated into the simpler form upon parsing but are not translated |
|
38 back for printing. This may lead to surprising output. |
|
39 \end{warn} |
|
40 |
|
41 \begin{warn} |
|
42 Like @{text"if"}, @{text"case"}-expressions may need to be enclosed in |
|
43 parentheses to indicate their scope. |
|
44 \end{warn} |
|
45 |
|
46 \subsection{Structural Induction and Case Distinction} |
|
47 \label{sec:struct-ind-case} |
|
48 \index{case distinctions}\index{induction!structural}% |
|
49 Induction is invoked by \methdx{induct_tac}, as we have seen above; |
|
50 it works for any datatype. In some cases, induction is overkill and a case |
|
51 distinction over all constructors of the datatype suffices. This is performed |
|
52 by \methdx{case_tac}. Here is a trivial example: |
|
53 *} |
|
54 |
|
55 lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"; |
|
56 apply(case_tac xs); |
|
57 |
|
58 txt{*\noindent |
|
59 results in the proof state |
|
60 @{subgoals[display,indent=0,margin=65]} |
|
61 which is solved automatically: |
|
62 *} |
|
63 |
|
64 apply(auto) |
|
65 (*<*)done(*>*) |
|
66 text{* |
|
67 Note that we do not need to give a lemma a name if we do not intend to refer |
|
68 to it explicitly in the future. |
|
69 Other basic laws about a datatype are applied automatically during |
|
70 simplification, so no special methods are provided for them. |
|
71 |
|
72 \begin{warn} |
|
73 Induction is only allowed on free (or \isasymAnd-bound) variables that |
|
74 should not occur among the assumptions of the subgoal; see |
|
75 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
|
76 (@{text"case_tac"}) works for arbitrary terms, which need to be |
|
77 quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound |
|
78 variables, the terms must not contain variables that are bound outside. |
|
79 For example, given the goal @{prop"\<forall>xs. xs = [] \<or> (\<exists>y ys. xs = y#ys)"}, |
|
80 @{text"case_tac xs"} will not work as expected because Isabelle interprets |
|
81 the @{term xs} as a new free variable distinct from the bound |
|
82 @{term xs} in the goal. |
|
83 \end{warn} |
|
84 *} |
|
85 |
|
86 (*<*) |
|
87 end |
|
88 (*>*) |
|