# HG changeset patch
# User haftmann
# Date 1226649007 -3600
# Node ID 5a404273ea8f7a37a3769d0507b384b45682ccd5
# Parent  ff9d8a8932e4fe4889da78ad7bccda4507dc19c6
added length_unique operation for code generation

diff -r ff9d8a8932e4 -r 5a404273ea8f src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 13 22:45:12 2008 +0100
+++ b/src/HOL/List.thy	Fri Nov 14 08:50:07 2008 +0100
@@ -3740,6 +3740,13 @@
   | "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.
@@ -3827,6 +3834,12 @@
   "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. *}