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 

    22 value "count_list (1::nat) [1,1,1]"

    23 value "count_list (1::nat) [2,2,2]"

    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 done

    30  

    31 thm count1

    32 thm refl

    33 thm conjI[OF refl[of "a"] refl[of "b"]]

    34 thm conjI[OF conjI]

    35  

    36 

    37 

    38 

    39