1 (*<*) |
|
2 theory case_splits = Main:; |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
6 Goals containing @{text"if"}-expressions are usually proved by case |
|
7 distinction on the condition of the @{text"if"}. For example the goal |
|
8 *} |
|
9 |
|
10 lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []"; |
|
11 |
|
12 txt{*\noindent |
|
13 can be split into |
|
14 \begin{isabelle} |
|
15 ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[]) |
|
16 \end{isabelle} |
|
17 by a degenerate form of simplification |
|
18 *} |
|
19 |
|
20 apply(simp only: split: split_if); |
|
21 (*<*)oops;(*>*) |
|
22 |
|
23 text{*\noindent |
|
24 where no simplification rules are included (@{text"only:"} is followed by the |
|
25 empty list of theorems) but the rule \isaindexbold{split_if} for |
|
26 splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because |
|
27 case-splitting on @{text"if"}s is almost always the right proof strategy, the |
|
28 simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"} |
|
29 on the initial goal above. |
|
30 |
|
31 This splitting idea generalizes from @{text"if"} to \isaindex{case}: |
|
32 *} |
|
33 |
|
34 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
|
35 txt{*\noindent |
|
36 becomes |
|
37 \begin{isabelle} |
|
38 ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline |
|
39 ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs) |
|
40 \end{isabelle} |
|
41 by typing |
|
42 *} |
|
43 |
|
44 apply(simp only: split: list.split); |
|
45 (*<*)oops;(*>*) |
|
46 |
|
47 text{*\noindent |
|
48 In contrast to @{text"if"}-expressions, the simplifier does not split |
|
49 @{text"case"}-expressions by default because this can lead to nontermination |
|
50 in case of recursive datatypes. Again, if the @{text"only:"} modifier is |
|
51 dropped, the above goal is solved, |
|
52 *} |
|
53 (*<*) |
|
54 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
|
55 (*>*) |
|
56 by(simp split: list.split); |
|
57 |
|
58 text{*\noindent% |
|
59 which \isacommand{apply}@{text"(simp)"} alone will not do. |
|
60 |
|
61 In general, every datatype $t$ comes with a theorem |
|
62 $t$@{text".split"} which can be declared to be a \bfindex{split rule} either |
|
63 locally as above, or by giving it the @{text"split"} attribute globally: |
|
64 *} |
|
65 |
|
66 lemmas [split] = list.split; |
|
67 |
|
68 text{*\noindent |
|
69 The @{text"split"} attribute can be removed with the @{text"del"} modifier, |
|
70 either locally |
|
71 *} |
|
72 (*<*) |
|
73 lemma "dummy=dummy"; |
|
74 (*>*) |
|
75 apply(simp split del: split_if); |
|
76 (*<*) |
|
77 oops; |
|
78 (*>*) |
|
79 text{*\noindent |
|
80 or globally: |
|
81 *} |
|
82 lemmas [split del] = list.split; |
|
83 |
|
84 text{* |
|
85 The above split rules intentionally only affect the conclusion of a |
|
86 subgoal. If you want to split an @{text"if"} or @{text"case"}-expression in |
|
87 the assumptions, you have to apply @{thm[source]split_if_asm} or |
|
88 $t$@{text".split_asm"}: |
|
89 *} |
|
90 |
|
91 lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []" |
|
92 apply(simp only: split: split_if_asm); |
|
93 |
|
94 txt{*\noindent |
|
95 In contrast to splitting the conclusion, this actually creates two |
|
96 separate subgoals (which are solved by @{text"simp_all"}): |
|
97 \begin{isabelle} |
|
98 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline |
|
99 \ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright} |
|
100 \end{isabelle} |
|
101 If you need to split both in the assumptions and the conclusion, |
|
102 use $t$@{text".splits"} which subsumes $t$@{text".split"} and |
|
103 $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}. |
|
104 *} |
|
105 |
|
106 (*<*) |
|
107 by(simp_all) |
|
108 end |
|
109 (*>*) |
|