added dom_option_map, map_of_map_keys
authorhaftmann
Sat Mar 06 09:58:30 2010 +0100 (2010-03-06)
changeset 35607896f01fe825b
parent 35606 7c5b40c7e8c4
child 35608 db4045d1406e
added dom_option_map, map_of_map_keys
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Sat Mar 06 09:58:28 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Sat Mar 06 09:58:30 2010 +0100
     1.3 @@ -243,8 +243,13 @@
     1.4    "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
     1.5  by (induct xs) auto
     1.6  
     1.7 -lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
     1.8 -by (induct xs) auto
     1.9 +lemma map_of_map:
    1.10 +  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
    1.11 +  by (induct xs) (auto simp add: expand_fun_eq)
    1.12 +
    1.13 +lemma dom_option_map:
    1.14 +  "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
    1.15 +  by (simp add: dom_def)
    1.16  
    1.17  
    1.18  subsection {* @{const Option.map} related *}
    1.19 @@ -555,6 +560,10 @@
    1.20    "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
    1.21    unfolding dom_def by auto
    1.22  
    1.23 +lemma map_of_map_keys:
    1.24 +  "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
    1.25 +  by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
    1.26 +
    1.27  
    1.28  subsection {* @{term [source] ran} *}
    1.29