# HG changeset patch
# User haftmann
# Date 1290096076 -3600
# Node ID 0bc28f978bcfcdb43c6c2b4e3f23e6d1c65eb919
# Parent  c0770657c8dec6d08c1be6a0f0717b5c0d45ad5b
mapper for mapping type

diff -r c0770657c8de -r 0bc28f978bcf src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu Nov 18 17:01:15 2010 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Nov 18 17:01:16 2010 +0100
@@ -41,6 +41,19 @@
   "delete k m = Mapping ((lookup m)(k := None))"
 
 
+subsection {* Functorial structure *}
+
+definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where
+  "map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)"
+
+lemma lookup_map [simp]:
+  "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
+  by (simp add: map_def)
+
+type_mapper map
+  by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
+
+
 subsection {* Derived operations *}
 
 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
@@ -69,7 +82,7 @@
   "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))"
+  "tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))"
 
 definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where
   "bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
@@ -294,6 +307,6 @@
 
 
 hide_const (open) empty is_empty lookup update delete ordered_keys keys size
-  replace default map_entry map_default tabulate bulkload
+  replace default map_entry map_default tabulate bulkload map
 
 end
\ No newline at end of file