| changeset 56545 | 8f1e7596deb7 |
| parent 55466 | 786edc984c98 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Map.thy Sat Apr 12 17:26:27 2014 +0200 +++ b/src/HOL/Map.thy Sat Apr 12 11:27:36 2014 +0200 @@ -249,6 +249,10 @@ "dom (\<lambda>k. map_option (f k) (m k)) = dom m" by (simp add: dom_def) +lemma dom_map_option_comp [simp]: + "dom (map_option g \<circ> m) = dom m" + using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def) + subsection {* @{const map_option} related *}