39 \begin{isamarkuptext}% |
39 \begin{isamarkuptext}% |
40 \noindent |
40 \noindent |
41 In contrast to \isa{if}-expressions, the simplifier does not split |
41 In contrast to \isa{if}-expressions, the simplifier does not split |
42 \isa{case}-expressions by default because this can lead to nontermination |
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 |
43 in case of recursive datatypes. Again, if the \isa{only:} modifier is |
44 dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)} |
44 dropped, the above goal is solved,% |
45 alone will not do:% |
|
46 \end{isamarkuptext}% |
45 \end{isamarkuptext}% |
47 \isacommand{apply}(simp~split:~list.split)\isacommand{.}% |
46 \isacommand{apply}(simp~split:~list.split)\isacommand{.}% |
48 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
|
48 \noindent% |
|
49 which \isacommand{apply}\isa{(simp)} alone will not do. |
|
50 |
49 In general, every datatype $t$ comes with a theorem |
51 In general, every datatype $t$ comes with a theorem |
50 \isa{$t$.split} which can be declared to be a \bfindex{split rule} either |
52 \isa{$t$.split} which can be declared to be a \bfindex{split rule} either |
51 locally as above, or by giving it the \isa{split} attribute globally:% |
53 locally as above, or by giving it the \isa{split} attribute globally:% |
52 \end{isamarkuptext}% |
54 \end{isamarkuptext}% |
53 \isacommand{theorems}~[split]~=~list.split% |
55 \isacommand{theorems}~[split]~=~list.split% |