# HG changeset patch
# User kuncar
# Date 1350568351 -7200
# Node ID cde0a46b4224e4b08fa3e1598a846f394187e8dd
# Parent  a9f5a74962581df9416594d21e0ddfce82f71f18
new theorem

diff -r a9f5a7496258 -r cde0a46b4224 src/HOL/Library/RBT.thy
--- 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)