--- a/src/HOL/Map.thy Sat Mar 06 09:58:28 2010 +0100
+++ b/src/HOL/Map.thy Sat Mar 06 09:58:30 2010 +0100
@@ -243,8 +243,13 @@
"map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
by (induct xs) auto
-lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
-by (induct xs) auto
+lemma map_of_map:
+ "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
+ by (induct xs) (auto simp add: expand_fun_eq)
+
+lemma dom_option_map:
+ "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
+ by (simp add: dom_def)
subsection {* @{const Option.map} related *}
@@ -555,6 +560,10 @@
"f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
unfolding dom_def by auto
+lemma map_of_map_keys:
+ "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
+ by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
+
subsection {* @{term [source] ran} *}