src/HOL/List.thy

 where
   "map_filter f P [] = []"
   | "map_filter f P (x#xs) =
      (if P x then f x # map_filter f P xs else map_filter f P xs)"
 
+primrec
+  length_unique :: "'a list \<Rightarrow> nat"
+where
+  "length_unique [] = 0"
+  | "length_unique (x#xs) =
+      (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
+
 text {*
   Only use @{text mem} for generating executable code.  Otherwise use
   @{prop "x : set xs"} instead --- it is much easier to reason about.
   The same is true for @{const list_all} and @{const list_ex}: write
   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL

 
 lemma map_filter_conv [simp]:
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
+lemma lenght_remdups_length_unique [code inline]:
+  "length (remdups xs) = length_unique xs"
+  by (induct xs) simp_all
+
+hide (open) const length_unique
+
 
 text {* Code for bounded quantification and summation over nats. *}
 
 lemma atMost_upto [code unfold]:
   "{..n} = set [0..<Suc n]"