equal
deleted
inserted
replaced
651 lemma map_comp_None_iff: |
651 lemma map_comp_None_iff: |
652 "(map_of (compose xs ys) k = None) = |
652 "(map_of (compose xs ys) k = None) = |
653 (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " |
653 (map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) " |
654 by (simp add: compose_conv map_comp_None_iff) |
654 by (simp add: compose_conv map_comp_None_iff) |
655 |
655 |
|
656 subsection {* @{text map_default} *} |
|
657 |
|
658 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" |
|
659 where |
|
660 "map_default k v f [] = [(k, v)]" |
|
661 | "map_default k v f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)" |
|
662 |
|
663 lemma map_of_map_default: |
|
664 "map_of (map_default k v f xs) = (map_of xs)(k := case map_of xs k of None => Some v | Some v' => Some (f v'))" |
|
665 by (induct xs) auto |
|
666 |
|
667 lemma dom_map_default: |
|
668 "fst ` set (map_default k v f xs) = insert k (fst ` set xs)" |
|
669 by (induct xs) auto |
|
670 |
|
671 lemma distinct_map_default: |
|
672 assumes "distinct (map fst xs)" |
|
673 shows "distinct (map fst (map_default k v f xs))" |
|
674 using assms by (induct xs) (auto simp add: dom_map_default) |
|
675 |
656 end |
676 end |