equal
deleted
inserted
replaced
266 lemma dom_map_option_comp [simp]: |
266 lemma dom_map_option_comp [simp]: |
267 "dom (map_option g \<circ> m) = dom m" |
267 "dom (map_option g \<circ> m) = dom m" |
268 using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def) |
268 using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def) |
269 |
269 |
270 |
270 |
271 subsection \<open>@{const map_option} related\<close> |
271 subsection \<open>\<^const>\<open>map_option\<close> related\<close> |
272 |
272 |
273 lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty" |
273 lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty" |
274 by (rule ext) simp |
274 by (rule ext) simp |
275 |
275 |
276 lemma map_option_o_map_upd [simp]: |
276 lemma map_option_o_map_upd [simp]: |