src/HOL/Map.thy
changeset 35619 b5f6481772f3
parent 35607 896f01fe825b
child 39198 f967a16dfcdd
equal deleted inserted replaced
35618:b7bfd4cbcfc0 35619:b5f6481772f3
   395 by (simp add: restrict_map_def expand_fun_eq)
   395 by (simp add: restrict_map_def expand_fun_eq)
   396 
   396 
   397 lemma map_of_map_restrict:
   397 lemma map_of_map_restrict:
   398   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   398   "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   399   by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
   399   by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
       
   400 
       
   401 lemma restrict_complement_singleton_eq:
       
   402   "f |` (- {x}) = f(x := None)"
       
   403   by (simp add: restrict_map_def expand_fun_eq)
   400 
   404 
   401 
   405 
   402 subsection {* @{term [source] map_upds} *}
   406 subsection {* @{term [source] map_upds} *}
   403 
   407 
   404 lemma map_upds_Nil1 [simp]: "m([] [|->] bs) = m"
   408 lemma map_upds_Nil1 [simp]: "m([] [|->] bs) = m"
   705     qed
   709     qed
   706   qed
   710   qed
   707 qed
   711 qed
   708 
   712 
   709 end
   713 end
   710