| changeset 25 | a2a7f65f538a |
| parent 24 | 789ade899a53 |
| child 27 | 378077bab5d2 |
--- a/thys/CountSnoc.thy Tue Oct 07 16:17:23 2014 +0100 +++ b/thys/CountSnoc.thy Tue Oct 07 18:43:29 2014 +0100 @@ -22,6 +22,11 @@ value "count_list (1::nat) [1,1,1]" value "count_list (1::nat) [2,2,2]" value "count_list (2::nat) [2,2,1]" + +lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys" +apply(induct xs) +apply(auto) +