1.1 --- a/src/HOL/Library/Mapping.thy	Thu May 20 16:43:00 2010 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Thu May 20 17:29:43 2010 +0200
     1.3 @@ -40,6 +40,16 @@
     1.4  definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
     1.5    "replace k v m = (if lookup m k = None then m else update k v m)"
     1.6  
     1.7 +definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
     1.8 +  "default k v m = (if lookup m k = None then update k v m else m)"
     1.9 +
    1.10 +definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.11 +  "map_entry k f m = (case lookup m k of None \<Rightarrow> m
    1.12 +    | Some v \<Rightarrow> update k (f v) m)" 
    1.13 +
    1.14 +definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.15 +  "map_default k v f m = map_entry k f (default k v m)" 
    1.16 +
    1.17  definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
    1.18    "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
    1.19  
    1.20 @@ -70,6 +80,10 @@
    1.21    "lookup (delete k m) = (lookup m) (k := None)"
    1.22    by (cases m) simp
    1.23  
    1.24 +lemma lookup_map_entry [simp]:
    1.25 +  "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
    1.26 +  by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq)
    1.27 +
    1.28  lemma lookup_tabulate [simp]:
    1.29    "lookup (tabulate ks f) = (Some o f) |` set ks"
    1.30    by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
    1.31 @@ -122,6 +136,14 @@
    1.32    "bulkload xs = tabulate [0..<length xs] (nth xs)"
    1.33    by (rule mapping_eqI) (simp add: expand_fun_eq)
    1.34  
    1.35 +lemma keys_tabulate:
    1.36 +  "keys (tabulate ks f) = set ks"
    1.37 +  by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
    1.38 +
    1.39 +lemma keys_bulkload:
    1.40 +  "keys (bulkload xs) = {0..<length xs}"
    1.41 +  by (simp add: keys_tabulate bulkload_tabulate)
    1.42 +
    1.43  lemma is_empty_empty:
    1.44    "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
    1.45    by (cases m) (simp add: is_empty_def)