1 % |
|
2 \begin{isabellebody}% |
|
3 % |
|
4 \begin{isamarkuptext}% |
|
5 Goals containing \isa{if}-expressions are usually proved by case |
|
6 distinction on the condition of the \isa{if}. For example the goal% |
|
7 \end{isamarkuptext}% |
|
8 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}% |
|
9 \begin{isamarkuptxt}% |
|
10 \noindent |
|
11 can be split into |
|
12 \begin{isabelle} |
|
13 ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[]) |
|
14 \end{isabelle} |
|
15 by a degenerate form of simplification% |
|
16 \end{isamarkuptxt}% |
|
17 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% |
|
18 \begin{isamarkuptext}% |
|
19 \noindent |
|
20 where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the |
|
21 empty list of theorems) but the rule \isaindexbold{split_if} for |
|
22 splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because |
|
23 case-splitting on \isa{if}s is almost always the right proof strategy, the |
|
24 simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} |
|
25 on the initial goal above. |
|
26 |
|
27 This splitting idea generalizes from \isa{if} to \isaindex{case}:% |
|
28 \end{isamarkuptext}% |
|
29 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}% |
|
30 \begin{isamarkuptxt}% |
|
31 \noindent |
|
32 becomes |
|
33 \begin{isabelle} |
|
34 ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline |
|
35 ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs) |
|
36 \end{isabelle} |
|
37 by typing% |
|
38 \end{isamarkuptxt}% |
|
39 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% |
|
40 \begin{isamarkuptext}% |
|
41 \noindent |
|
42 In contrast to \isa{if}-expressions, the simplifier does not split |
|
43 \isa{case}-expressions by default because this can lead to nontermination |
|
44 in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is |
|
45 dropped, the above goal is solved,% |
|
46 \end{isamarkuptext}% |
|
47 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% |
|
48 \begin{isamarkuptext}% |
|
49 \noindent% |
|
50 which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do. |
|
51 |
|
52 In general, every datatype $t$ comes with a theorem |
|
53 $t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either |
|
54 locally as above, or by giving it the \isa{split} attribute globally:% |
|
55 \end{isamarkuptext}% |
|
56 \isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split% |
|
57 \begin{isamarkuptext}% |
|
58 \noindent |
|
59 The \isa{split} attribute can be removed with the \isa{del} modifier, |
|
60 either locally% |
|
61 \end{isamarkuptext}% |
|
62 \isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% |
|
63 \begin{isamarkuptext}% |
|
64 \noindent |
|
65 or globally:% |
|
66 \end{isamarkuptext}% |
|
67 \isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split% |
|
68 \begin{isamarkuptext}% |
|
69 The above split rules intentionally only affect the conclusion of a |
|
70 subgoal. If you want to split an \isa{if} or \isa{case}-expression in |
|
71 the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or |
|
72 $t$\isa{{\isachardot}split{\isacharunderscore}asm}:% |
|
73 \end{isamarkuptext}% |
|
74 \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
|
75 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}% |
|
76 \begin{isamarkuptxt}% |
|
77 \noindent |
|
78 In contrast to splitting the conclusion, this actually creates two |
|
79 separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}): |
|
80 \begin{isabelle} |
|
81 \ \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 |
|
82 \ \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} |
|
83 \end{isabelle} |
|
84 If you need to split both in the assumptions and the conclusion, |
|
85 use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and |
|
86 $t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.% |
|
87 \end{isamarkuptxt}% |
|
88 \end{isabellebody}% |
|
89 %%% Local Variables: |
|
90 %%% mode: latex |
|
91 %%% TeX-master: "root" |
|
92 %%% End: |
|