equal
deleted
inserted
replaced
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 |
|