--- a/src/HOL/Library/RBT.thy Thu Oct 18 15:47:01 2012 +0200
+++ b/src/HOL/Library/RBT.thy Thu Oct 18 15:52:31 2012 +0200
@@ -97,6 +97,13 @@
"RBT_Impl.keys (impl_of t) = keys t"
by transfer (rule refl)
+(* FIXME *)
+lemma [transfer_rule]: "(fun_rel (fun_rel op = op =) op =) dom dom" unfolding fun_rel_def by auto
+
+lemma lookup_keys:
+ "dom (lookup t) = set (keys t)"
+ by transfer (simp add: rbt_lookup_keys)
+
lemma lookup_empty [simp]:
"lookup empty = Map.empty"
by (simp add: empty_def lookup_RBT fun_eq_iff)