1.1 --- a/src/HOL/Library/Mapping.thy	Thu Feb 05 14:50:43 2009 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Fri Feb 06 09:05:19 2009 +0100
     1.3 @@ -33,6 +33,9 @@
     1.4  definition size :: "('a, 'b) map \<Rightarrow> nat" where
     1.5    "size m = (if finite (keys m) then card (keys m) else 0)"
     1.6  
     1.7 +definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) map \<Rightarrow> ('a, 'b) map" where
     1.8 +  "replace k v m = (if lookup m k = None then m else update k v m)"
     1.9 +
    1.10  definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) map" where
    1.11    "tabulate ks f = Map (map_of (map (\<lambda>k. (k, f k)) ks))"
    1.12  
    1.13 @@ -65,6 +68,11 @@
    1.14    "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
    1.15    by (cases m, simp add: expand_fun_eq)+
    1.16  
    1.17 +lemma replace_update:
    1.18 +  "lookup m k = None \<Longrightarrow> replace k v m = m"
    1.19 +  "lookup m k \<noteq> None \<Longrightarrow> replace k v m = update k v m"
    1.20 +  by (auto simp add: replace_def)
    1.21 +
    1.22  lemma delete_empty [simp]:
    1.23    "delete k empty = empty"
    1.24    by (simp add: empty_def)