equal
deleted
inserted
replaced
2 theory case_exprs = Main: |
2 theory case_exprs = Main: |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 subsection{*Case Expressions*} |
5 subsection{*Case Expressions*} |
6 |
6 |
7 text{*\label{sec:case-expressions} |
7 text{*\label{sec:case-expressions}\index{*case expressions}% |
8 HOL also features \sdx{case}-expressions for analyzing |
8 HOL also features \isa{case}-expressions for analyzing |
9 elements of a datatype. For example, |
9 elements of a datatype. For example, |
10 @{term[display]"case xs of [] => 1 | y#ys => y"} |
10 @{term[display]"case xs of [] => 1 | y#ys => y"} |
11 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if |
11 evaluates to @{term"1"} 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 |
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"nat"} and hence |
13 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence |
41 *} |
41 *} |
42 |
42 |
43 subsection{*Structural Induction and Case Distinction*} |
43 subsection{*Structural Induction and Case Distinction*} |
44 |
44 |
45 text{*\label{sec:struct-ind-case} |
45 text{*\label{sec:struct-ind-case} |
46 \indexbold{structural induction} |
46 \index{case distinctions}\index{induction!structural}% |
47 \indexbold{induction!structural} |
47 Induction is invoked by \methdx{induct_tac}, as we have seen above; |
48 \indexbold{case distinction} |
48 it works for any datatype. In some cases, induction is overkill and a case |
49 Almost all the basic laws about a datatype are applied automatically during |
49 distinction over all constructors of the datatype suffices. This is performed |
50 simplification. Only induction is invoked by hand via \methdx{induct_tac}, |
50 by \methdx{case_tac}. Here is a trivial example: |
51 which works for any datatype. In some cases, induction is overkill and a case |
|
52 distinction over all constructors of the datatype suffices. This is performed |
|
53 by \methdx{case_tac}. A trivial example: |
|
54 *} |
51 *} |
55 |
52 |
56 lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"; |
53 lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"; |
57 apply(case_tac xs); |
54 apply(case_tac xs); |
58 |
55 |
65 apply(auto) |
62 apply(auto) |
66 (*<*)done(*>*) |
63 (*<*)done(*>*) |
67 text{* |
64 text{* |
68 Note that we do not need to give a lemma a name if we do not intend to refer |
65 Note that we do not need to give a lemma a name if we do not intend to refer |
69 to it explicitly in the future. |
66 to it explicitly in the future. |
|
67 Other basic laws about a datatype are applied automatically during |
|
68 simplification, so no special methods are provided for them. |
70 |
69 |
71 \begin{warn} |
70 \begin{warn} |
|
71 |
72 Induction is only allowed on free (or \isasymAnd-bound) variables that |
72 Induction is only allowed on free (or \isasymAnd-bound) variables that |
73 should not occur among the assumptions of the subgoal; see |
73 should not occur among the assumptions of the subgoal; see |
74 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
74 \S\ref{sec:ind-var-in-prems} for details. Case distinction |
75 (@{text"case_tac"}) works for arbitrary terms, which need to be |
75 (@{text"case_tac"}) works for arbitrary terms, which need to be |
76 quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound |
76 quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound |