| changeset 25 | a2a7f65f538a |
| parent 24 | 789ade899a53 |
| child 27 | 378077bab5d2 |
| 24:789ade899a53 | 25:a2a7f65f538a |
|---|---|
20 else count_list x xs)" |
20 else count_list x xs)" |
21 |
21 |
22 value "count_list (1::nat) [1,1,1]" |
22 value "count_list (1::nat) [1,1,1]" |
23 value "count_list (1::nat) [2,2,2]" |
23 value "count_list (1::nat) [2,2,2]" |
24 value "count_list (2::nat) [2,2,1]" |
24 value "count_list (2::nat) [2,2,1]" |
25 |
|
26 lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys" |
|
27 apply(induct xs) |
|
28 apply(auto) |
|
29 |
|
25 |
30 |
26 |
31 |
27 |
32 |
28 |
33 |
29 |
34 |