--- a/src/HOL/Library/Mapping.thy Thu Feb 05 14:50:43 2009 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Feb 06 09:05:19 2009 +0100
@@ -33,6 +33,9 @@
definition size :: "('a, 'b) map \<Rightarrow> nat" where
"size m = (if finite (keys m) then card (keys m) else 0)"
+definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
+ "replace k v m = (if lookup m k = None then m else update k v m)"
+
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
"tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
@@ -65,6 +68,11 @@
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
by (cases m, simp add: expand_fun_eq)+
+lemma replace_update:
+ "lookup m k = None \<Longrightarrow> replace k v m = m"
+ "lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m"
+ by (auto simp add: replace_def)
+
lemma delete_empty [simp]:
"delete k empty = empty"
by (simp add: empty_def)