equal
deleted
inserted
replaced
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 |
25 |
26 lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys" |
26 lemma count1: "count_list n (xs @ ys) = count_list n xs + count_list n ys" |
27 apply(induct xs) |
27 apply(induct xs) |
28 apply(auto) |
28 apply(auto) |
29 done |
29 done |
30 |
30 |
|
31 thm count1 |
|
32 thm refl |
|
33 thm conjI[OF refl[of "a"] refl[of "b"]] |
|
34 thm conjI[OF conjI] |
31 |
35 |
32 |
36 |
33 |
37 |
34 |
38 |
35 |
39 |