22
|
1 |
theory CountSnoc
|
|
2 |
imports Main
|
|
3 |
begin
|
|
4 |
|
|
5 |
|
|
6 |
datatype 'a myList = Nil | Cons 'a "'a myList"
|
|
7 |
|
|
8 |
fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
|
|
9 |
"app_list Nil ys = ys" |
|
|
10 |
"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
|
|
11 |
|
|
12 |
fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
|
|
13 |
"rev_list Nil = Nil" |
|
|
14 |
"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
|
|
15 |
|
|
16 |
fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
|
|
17 |
"count_list x [] = 0" |
|
|
18 |
"count_list x (y#xs) = (
|
|
19 |
if x = y then Suc(count_list x xs)
|
|
20 |
else count_list x xs)"
|
|
21 |
|
24
789ade899a53
added type information to produce the expected result with value
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
value "count_list (1::nat) [1,1,1]"
|
789ade899a53
added type information to produce the expected result with value
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
value "count_list (1::nat) [2,2,2]"
|
789ade899a53
added type information to produce the expected result with value
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
value "count_list (2::nat) [2,2,1]"
|
25
|
25 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
lemma count1: "count_list n (xs @ ys) = count_list n xs + count_list n ys"
|
25
|
27 |
apply(induct xs)
|
|
28 |
apply(auto)
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
done
|
25
|
30 |
|
34
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
thm count1
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
thm refl
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
thm conjI[OF refl[of "a"] refl[of "b"]]
|
33065bde3bbd
added a file for calculating all answers...still incomplete
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
thm conjI[OF conjI]
|
22
|
35 |
|
|
36 |
|
|
37 |
|
|
38 |
|
|
39 |
|