equal
deleted
inserted
replaced
639 moreover from Cons.prems have "map_of al (fst kv) = None" |
639 moreover from Cons.prems have "map_of al (fst kv) = None" |
640 by (simp add: map_of_eq_None_iff) |
640 by (simp add: map_of_eq_None_iff) |
641 ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp |
641 ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp |
642 qed |
642 qed |
643 |
643 |
|
644 lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m" |
|
645 by(auto simp add: ran_def) |
644 |
646 |
645 subsection {* @{text "map_le"} *} |
647 subsection {* @{text "map_le"} *} |
646 |
648 |
647 lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g" |
649 lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g" |
648 by (simp add: map_le_def) |
650 by (simp add: map_le_def) |