# HG changeset patch
# User haftmann
# Date 1267808114 -3600
# Node ID c0db094d0d803f63869e620221bcb27724b6aace
# Parent  e814157560e8c4ffbeb2129fa561998d6e02b723
moved lemma map_sorted_distinct_set_unique

diff -r e814157560e8 -r c0db094d0d80 src/HOL/Library/RBT.thy
--- 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
diff -r e814157560e8 -r c0db094d0d80 src/HOL/List.thy
--- 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)