src/HOL/Library/Mapping.thy

--- a/src/HOL/Library/Mapping.thy	Sat Apr 12 17:26:27 2014 +0200
+++ b/src/HOL/Library/Mapping.thy	Sat Apr 12 11:27:36 2014 +0200
@@ -292,6 +292,10 @@
   "\<not> is_empty (map_default k v f m)"
   by (simp add: map_default_def)
 
+lemma keys_dom_lookup:
+  "keys m = dom (Mapping.lookup m)"
+  by transfer rule
+
 lemma keys_empty [simp]:
   "keys empty = {}"
   by transfer simp