8749
|
1 |
\begin{isabelle}%
|
|
2 |
%
|
|
3 |
\begin{isamarkuptext}%
|
|
4 |
Goals containing \isaindex{if}-expressions are usually proved by case
|
|
5 |
distinction on the condition of the \isa{if}. For example the goal%
|
|
6 |
\end{isamarkuptext}%
|
|
7 |
\isacommand{lemma}~{"}{\isasymforall}xs.~if~xs~=~[]~then~rev~xs~=~[]~else~rev~xs~{\isasymnoteq}~[]{"}%
|
|
8 |
\begin{isamarkuptxt}%
|
|
9 |
\noindent
|
|
10 |
can be split into
|
|
11 |
\begin{isabellepar}%
|
|
12 |
~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
|
|
13 |
\end{isabellepar}%
|
|
14 |
by a degenerate form of simplification%
|
|
15 |
\end{isamarkuptxt}%
|
|
16 |
\isacommand{apply}(simp~only:~split:~split\_if)%
|
|
17 |
\begin{isamarkuptext}%
|
|
18 |
\noindent
|
|
19 |
where no simplification rules are included (\isa{only:} is followed by the
|
|
20 |
empty list of theorems) but the rule \isaindexbold{split_if} for
|
|
21 |
splitting \isa{if}s is added (via the modifier \isa{split:}). Because
|
|
22 |
case-splitting on \isa{if}s is almost always the right proof strategy, the
|
|
23 |
simplifier performs it automatically. Try \isacommand{apply}\isa{(simp)}
|
|
24 |
on the initial goal above.
|
|
25 |
|
|
26 |
This splitting idea generalizes from \isa{if} to \isaindex{case}:%
|
|
27 |
\end{isamarkuptext}%
|
|
28 |
\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~zs~|~y\#ys~{\isasymRightarrow}~y\#(ys@zs))~=~xs@zs{"}%
|
|
29 |
\begin{isamarkuptxt}%
|
|
30 |
\noindent
|
|
31 |
becomes
|
|
32 |
\begin{isabellepar}%
|
|
33 |
~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
|
|
34 |
~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
|
|
35 |
\end{isabellepar}%
|
|
36 |
by typing%
|
|
37 |
\end{isamarkuptxt}%
|
|
38 |
\isacommand{apply}(simp~only:~split:~list.split)%
|
|
39 |
\begin{isamarkuptext}%
|
|
40 |
\noindent
|
|
41 |
In contrast to \isa{if}-expressions, the simplifier does not split
|
|
42 |
\isa{case}-expressions by default because this can lead to nontermination
|
|
43 |
in case of recursive datatypes. Again, if the \isa{only:} modifier is
|
8771
|
44 |
dropped, the above goal is solved,%
|
8749
|
45 |
\end{isamarkuptext}%
|
|
46 |
\isacommand{apply}(simp~split:~list.split)\isacommand{.}%
|
|
47 |
\begin{isamarkuptext}%
|
8771
|
48 |
\noindent%
|
|
49 |
which \isacommand{apply}\isa{(simp)} alone will not do.
|
|
50 |
|
8749
|
51 |
In general, every datatype $t$ comes with a theorem
|
|
52 |
\isa{$t$.split} which can be declared to be a \bfindex{split rule} either
|
|
53 |
locally as above, or by giving it the \isa{split} attribute globally:%
|
|
54 |
\end{isamarkuptext}%
|
|
55 |
\isacommand{theorems}~[split]~=~list.split%
|
|
56 |
\begin{isamarkuptext}%
|
|
57 |
\noindent
|
|
58 |
The \isa{split} attribute can be removed with the \isa{del} modifier,
|
|
59 |
either locally%
|
|
60 |
\end{isamarkuptext}%
|
|
61 |
\isacommand{apply}(simp~split~del:~split\_if)%
|
|
62 |
\begin{isamarkuptext}%
|
|
63 |
\noindent
|
|
64 |
or globally:%
|
|
65 |
\end{isamarkuptext}%
|
|
66 |
\isacommand{theorems}~[split~del]~=~list.split\isanewline
|
|
67 |
\end{isabelle}%
|
9145
|
68 |
%%% Local Variables:
|
|
69 |
%%% mode: latex
|
|
70 |
%%% TeX-master: "root"
|
|
71 |
%%% End:
|