144 

   144 

   145 

   145 

   146 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where

   146 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where

   147   "retrieve (AONE bs) Void = bs"

   147   "retrieve (AONE bs) Void = bs"

   148 | "retrieve (ACHAR bs c) (Char d) = bs"

   148 | "retrieve (ACHAR bs c) (Char d) = bs"

   150 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

   150 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

   151 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

   151 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

   152 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"

   152 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"

   153 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"

   153 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]"

   154 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 

   154 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 

   455   "distinctBy [] f acc = []"

   455   "distinctBy [] f acc = []"

   456 | "distinctBy (x#xs) f acc = 

   456 | "distinctBy (x#xs) f acc = 

   457      (if (f x) \<in> acc then distinctBy xs f acc 

   457      (if (f x) \<in> acc then distinctBy xs f acc 

   458       else x # (distinctBy xs f ({f x} \<union> acc)))"

   458       else x # (distinctBy xs f ({f x} \<union> acc)))"

   459 

   459 

   461 

   461 

   462 fun flts :: "arexp list \<Rightarrow> arexp list"

   462 fun flts :: "arexp list \<Rightarrow> arexp list"

   463   where 

   463   where 

   464   "flts [] = []"

   464   "flts [] = []"

   465 | "flts (AZERO # rs) = flts rs"

   465 | "flts (AZERO # rs) = flts rs"