# HG changeset patch
# User haftmann
# Date 1274369383 -7200
# Node ID 7e8979a155ae40cc0a16b62631a454081530a183
# Parent  8a5718d54e71ba0ccb82e9cb64cd05383dc5e71c
operations default, map_entry, map_default; more lemmas

diff -r 8a5718d54e71 -r 7e8979a155ae src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu May 20 16:43:00 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Thu May 20 17:29:43 2010 +0200
@@ -40,6 +40,16 @@
 definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "replace k v m = (if lookup m k = None then m else update k v m)"
 
+definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+  "default k v m = (if lookup m k = None then update k v m else m)"
+
+definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+  "map_entry k f m = (case lookup m k of None \<Rightarrow> m
+    | Some v \<Rightarrow> update k (f v) m)" 
+
+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)" 
+
 definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
   "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
 
@@ -70,6 +80,10 @@
   "lookup (delete k m) = (lookup m) (k := None)"
   by (cases m) simp
 
+lemma lookup_map_entry [simp]:
+  "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
+  by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq)
+
 lemma lookup_tabulate [simp]:
   "lookup (tabulate ks f) = (Some o f) |` set ks"
   by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
@@ -122,6 +136,14 @@
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
   by (rule mapping_eqI) (simp add: expand_fun_eq)
 
+lemma keys_tabulate:
+  "keys (tabulate ks f) = set ks"
+  by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
+
+lemma keys_bulkload:
+  "keys (bulkload xs) = {0..<length xs}"
+  by (simp add: keys_tabulate bulkload_tabulate)
+
 lemma is_empty_empty:
   "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
   by (cases m) (simp add: is_empty_def)