--- a/src/HOL/Library/AList.thy Wed Dec 14 15:50:15 2011 +0100
+++ b/src/HOL/Library/AList.thy Wed Dec 14 16:30:09 2011 +0100
@@ -274,7 +274,7 @@
"map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
-lemma upate_restr_conv [simp]:
+lemma update_restr_conv [simp]:
"x \<in> D \<Longrightarrow>
map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
by (simp add: update_conv' restr_conv')
@@ -653,4 +653,44 @@
(map_of xs k = None \<or> (\<exists>k'. map_of xs k = Some k' \<and> map_of ys k' = None)) "
by (simp add: compose_conv map_comp_None_iff)
+subsection {* @{text map_entry} *}
+
+fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+ "map_entry k f [] = []"
+| "map_entry k f (p # ps) = (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
+
+lemma map_of_map_entry:
+ "map_of (map_entry k f xs) = (map_of xs)(k := case map_of xs k of None => None | Some v' => Some (f v'))"
+by (induct xs) auto
+
+lemma dom_map_entry:
+ "fst ` set (map_entry k f xs) = fst ` set xs"
+by (induct xs) auto
+
+lemma distinct_map_entry:
+ assumes "distinct (map fst xs)"
+ shows "distinct (map fst (map_entry k f xs))"
+using assms by (induct xs) (auto simp add: dom_map_entry)
+
+subsection {* @{text map_default} *}
+
+fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+where
+ "map_default k v f [] = [(k, v)]"
+| "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)"
+
+lemma map_of_map_default:
+ "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'))"
+by (induct xs) auto
+
+lemma dom_map_default:
+ "fst ` set (map_default k v f xs) = insert k (fst ` set xs)"
+by (induct xs) auto
+
+lemma distinct_map_default:
+ assumes "distinct (map fst xs)"
+ shows "distinct (map fst (map_default k v f xs))"
+using assms by (induct xs) (auto simp add: dom_map_default)
+
end
--- a/src/HOL/Library/Multiset.thy Wed Dec 14 15:50:15 2011 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Dec 14 16:30:09 2011 +0100
@@ -1103,7 +1103,7 @@
begin
definition
- "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+ [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
instance proof
qed (simp add: equal_multiset_def eq_iff)