--- a/src/HOL/Library/RBT.thy Fri Mar 05 17:51:29 2010 +0100
+++ b/src/HOL/Library/RBT.thy Fri Mar 05 17:55:14 2010 +0100
@@ -10,19 +10,6 @@
imports Main
begin
-lemma map_sorted_distinct_set_unique: (*FIXME move*)
- 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
-
subsection {* Datatype of RB trees *}
datatype color = R | B
--- 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)