src/HOL/List.thy

     case 2 thus ?case by (simp add:sorted_Cons)
        (metis Diff_insert_absorb antisym insertE insert_iff)
   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)
 apply clarify
 apply(rule_tac a="sort xs" in ex1I)