src/HOL/Map.thy
changeset 35607 896f01fe825b
parent 35565 56b070cd7ab3
child 35619 b5f6481772f3
equal deleted inserted replaced
35606:7c5b40c7e8c4 35607:896f01fe825b
   241 
   241 
   242 lemma map_of_filter_in:
   242 lemma map_of_filter_in:
   243   "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
   243   "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
   244 by (induct xs) auto
   244 by (induct xs) auto
   245 
   245 
   246 lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
   246 lemma map_of_map:
   247 by (induct xs) auto
   247   "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
       
   248   by (induct xs) (auto simp add: expand_fun_eq)
       
   249 
       
   250 lemma dom_option_map:
       
   251   "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
       
   252   by (simp add: dom_def)
   248 
   253 
   249 
   254 
   250 subsection {* @{const Option.map} related *}
   255 subsection {* @{const Option.map} related *}
   251 
   256 
   252 lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
   257 lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
   552   unfolding dom_def by simp
   557   unfolding dom_def by simp
   553 
   558 
   554 lemma insert_dom:
   559 lemma insert_dom:
   555   "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
   560   "f x = Some y \<Longrightarrow> insert x (dom f) = dom f"
   556   unfolding dom_def by auto
   561   unfolding dom_def by auto
       
   562 
       
   563 lemma map_of_map_keys:
       
   564   "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
       
   565   by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
   557 
   566 
   558 
   567 
   559 subsection {* @{term [source] ran} *}
   568 subsection {* @{term [source] ran} *}
   560 
   569 
   561 lemma ranI: "m a = Some b ==> b : ran m"
   570 lemma ranI: "m a = Some b ==> b : ran m"