equal
deleted
inserted
replaced
39 |
39 |
40 definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
40 definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
41 "delete k m = Mapping ((lookup m)(k := None))" |
41 "delete k m = Mapping ((lookup m)(k := None))" |
42 |
42 |
43 |
43 |
|
44 subsection {* Functorial structure *} |
|
45 |
|
46 definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where |
|
47 "map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)" |
|
48 |
|
49 lemma lookup_map [simp]: |
|
50 "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" |
|
51 by (simp add: map_def) |
|
52 |
|
53 type_mapper map |
|
54 by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity) |
|
55 |
|
56 |
44 subsection {* Derived operations *} |
57 subsection {* Derived operations *} |
45 |
58 |
46 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |
59 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |
47 "keys m = dom (lookup m)" |
60 "keys m = dom (lookup m)" |
48 |
61 |
67 |
80 |
68 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
81 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where |
69 "map_default k v f m = map_entry k f (default k v m)" |
82 "map_default k v f m = map_entry k f (default k v m)" |
70 |
83 |
71 definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where |
84 definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where |
72 "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))" |
85 "tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))" |
73 |
86 |
74 definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where |
87 definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where |
75 "bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)" |
88 "bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)" |
76 |
89 |
77 |
90 |
292 |
305 |
293 end |
306 end |
294 |
307 |
295 |
308 |
296 hide_const (open) empty is_empty lookup update delete ordered_keys keys size |
309 hide_const (open) empty is_empty lookup update delete ordered_keys keys size |
297 replace default map_entry map_default tabulate bulkload |
310 replace default map_entry map_default tabulate bulkload map |
298 |
311 |
299 end |
312 end |