src/HOL/Library/Mapping.thy

 
 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "map_default k v f m = map_entry k f (default k v m)" 
 
 subsection {* Properties *}
+
+lemma lookup_update: "lookup (update k v m) k = Some v" 
+  by transfer simp
+
+lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'" 
+  by transfer simp
+
+lemma lookup_empty: "lookup empty k = None" 
+  by transfer simp
 
 lemma keys_is_none_rep [code_unfold]:
   "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   by transfer (auto simp add: is_none_def)