theory CountSnoc
imports Main
begin


datatype 'a myList = Nil | Cons 'a "'a myList"

fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
"app_list Nil ys = ys" |
"app_list (Cons x xs) ys = Cons x (app_list xs ys)"

fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
"rev_list Nil = Nil" |
"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"

fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
"count_list x [] = 0" |
"count_list x (y#xs) = (
  if x = y then Suc(count_list x xs) 
  else count_list x xs)"

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)
done
 
thm count1
thm refl
thm conjI[OF refl[of "a"] refl[of "b"]]
thm conjI[OF conjI]