# HG changeset patch
# User nipkow
# Date 1189444863 -7200
# Node ID 2bfa0215904c7966522e3d53ef8c4536d726d2ec
# Parent  08578e380a41e238d8aba83722bfa158821b7854
added lemma

diff -r 08578e380a41 -r 2bfa0215904c src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 10 16:09:01 2007 +0200
+++ b/src/HOL/List.thy	Mon Sep 10 19:21:03 2007 +0200
@@ -2030,6 +2030,15 @@
 lemma distinct_remdups [iff]: "distinct (remdups xs)"
 by (induct xs) auto
 
+lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
+proof -
+  assume "finite A"
+  then obtain xs where "set xs = A" by(auto dest!:finite_list)
+  hence "set(remdups xs) = A & distinct(remdups xs)" by simp
+  thus ?thesis ..
+qed
+(* by (metis distinct_remdups finite_list set_remdups) *)
+
 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
 by (induct x, auto)