# HG changeset patch
# User haftmann
# Date 1233907519 -3600
# Node ID 15344c0899e1c430d69b84ef9beca0c1029a24cb
# Parent  df25a6b1a4756bbd86f9981599d07f7a35140ef7
added replace operation

diff -r df25a6b1a475 -r 15344c0899e1 src/HOL/Library/Mapping.thy
--- 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)