9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
8749
|
3 |
%
|
|
4 |
\begin{isamarkuptext}%
|
|
5 |
Goals containing \isaindex{if}-expressions are usually proved by case
|
|
6 |
distinction on the condition of the \isa{if}. For example the goal%
|
|
7 |
\end{isamarkuptext}%
|
9673
|
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}%
|
8749
|
9 |
\begin{isamarkuptxt}%
|
|
10 |
\noindent
|
|
11 |
can be split into
|
9723
|
12 |
\begin{isabelle}
|
8749
|
13 |
~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
|
9723
|
14 |
\end{isabelle}
|
8749
|
15 |
by a degenerate form of simplification%
|
|
16 |
\end{isamarkuptxt}%
|
9673
|
17 |
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
|
8749
|
18 |
\begin{isamarkuptext}%
|
|
19 |
\noindent
|
|
20 |
where no simplification rules are included (\isa{only:} 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:}). 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{(simp)}
|
|
25 |
on the initial goal above.
|
|
26 |
|
|
27 |
This splitting idea generalizes from \isa{if} to \isaindex{case}:%
|
|
28 |
\end{isamarkuptext}%
|
9673
|
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}%
|
8749
|
30 |
\begin{isamarkuptxt}%
|
|
31 |
\noindent
|
|
32 |
becomes
|
9723
|
33 |
\begin{isabelle}
|
8749
|
34 |
~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
|
|
35 |
~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
|
9723
|
36 |
\end{isabelle}
|
8749
|
37 |
by typing%
|
|
38 |
\end{isamarkuptxt}%
|
9673
|
39 |
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
|
8749
|
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:} modifier is
|
8771
|
45 |
dropped, the above goal is solved,%
|
8749
|
46 |
\end{isamarkuptext}%
|
9673
|
47 |
\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
|
8749
|
48 |
\begin{isamarkuptext}%
|
8771
|
49 |
\noindent%
|
|
50 |
which \isacommand{apply}\isa{(simp)} alone will not do.
|
|
51 |
|
8749
|
52 |
In general, every datatype $t$ comes with a theorem
|
|
53 |
\isa{$t$.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}%
|
9673
|
56 |
\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
|
8749
|
57 |
\begin{isamarkuptext}%
|
|
58 |
\noindent
|
|
59 |
The \isa{split} attribute can be removed with the \isa{del} modifier,
|
|
60 |
either locally%
|
|
61 |
\end{isamarkuptext}%
|
9673
|
62 |
\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
|
8749
|
63 |
\begin{isamarkuptext}%
|
|
64 |
\noindent
|
|
65 |
or globally:%
|
|
66 |
\end{isamarkuptext}%
|
9721
|
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\_if\_asm} or $t$\isa{.split_asm}:%
|
|
72 |
\end{isamarkuptext}%
|
|
73 |
\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
|
|
74 |
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
|
|
75 |
\begin{isamarkuptxt}%
|
|
76 |
\noindent
|
|
77 |
In contrast to splitting the conclusion, this actually creates two
|
|
78 |
separate subgoals (which are solved by \isa{simp\_all}):
|
|
79 |
\begin{isabelle}
|
|
80 |
\ \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
|
|
81 |
\ \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}
|
|
82 |
\end{isabelle}
|
|
83 |
If you need to split both in the assumptions and the conclusion,
|
|
84 |
use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
|
|
85 |
\end{isamarkuptxt}%
|
9722
|
86 |
\end{isabellebody}%
|
9145
|
87 |
%%% Local Variables:
|
|
88 |
%%% mode: latex
|
|
89 |
%%% TeX-master: "root"
|
|
90 |
%%% End:
|