equal
deleted
inserted
replaced
46 |
46 |
47 text{*\noindent |
47 text{*\noindent |
48 In contrast to \isa{if}-expressions, the simplifier does not split |
48 In contrast to \isa{if}-expressions, the simplifier does not split |
49 \isa{case}-expressions by default because this can lead to nontermination |
49 \isa{case}-expressions by default because this can lead to nontermination |
50 in case of recursive datatypes. Again, if the \isa{only:} modifier is |
50 in case of recursive datatypes. Again, if the \isa{only:} modifier is |
51 dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)} |
51 dropped, the above goal is solved, |
52 alone will not do: |
|
53 *} |
52 *} |
54 (*<*) |
53 (*<*) |
55 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
54 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
56 (*>*) |
55 (*>*) |
57 apply(simp split: list.split).; |
56 apply(simp split: list.split).; |
58 |
57 |
59 text{* |
58 text{*\noindent% |
|
59 which \isacommand{apply}\isa{(simp)} alone will not do. |
|
60 |
60 In general, every datatype $t$ comes with a theorem |
61 In general, every datatype $t$ comes with a theorem |
61 \isa{$t$.split} which can be declared to be a \bfindex{split rule} either |
62 \isa{$t$.split} which can be declared to be a \bfindex{split rule} either |
62 locally as above, or by giving it the \isa{split} attribute globally: |
63 locally as above, or by giving it the \isa{split} attribute globally: |
63 *} |
64 *} |
64 |
65 |