--- a/src/HOL/List.thy Fri Mar 05 17:51:29 2010 +0100
+++ b/src/HOL/List.thy Fri Mar 05 17:55:14 2010 +0100
@@ -3609,6 +3609,19 @@
qed
qed
+lemma map_sorted_distinct_set_unique:
+ assumes "inj_on f (set xs \<union> set ys)"
+ assumes "sorted (map f xs)" "distinct (map f xs)"
+ "sorted (map f ys)" "distinct (map f ys)"
+ assumes "set xs = set ys"
+ shows "xs = ys"
+proof -
+ from assms have "map f xs = map f ys"
+ by (simp add: sorted_distinct_set_unique)
+ moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
+ by (blast intro: map_inj_on)
+qed
+
lemma finite_sorted_distinct_unique:
shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
apply(drule finite_distinct_list)