Multicast using Isabelle -

i'm trying send messages agent list. so, wrote function:

fun  multicast :: "[msg, agent, agent list]=> event set"        multicast_nil:      " multicast m [] ={}"    | multicast_cons: " multicast m (x#xs) =  {says x m} un multicast m xs"  fun knows :: "[agent, event list] => msg set"    knows_nil:  "knows [] = initstate a" | knows_cons: "knows (ev # evs) =      (case ev of says a' b x =>         if a'=a insert x (knows evs) else knows evs) 

the problem wasn't able define corresponding code in knows function in order add sent message knowledge of agents in agent list.