mapper for mapping type
authorhaftmann
Thu Nov 18 17:01:16 2010 +0100 (2010-11-18)
changeset 406050bc28f978bcf
parent 40604 c0770657c8de
child 40606 af1a0b0c6202
mapper for mapping type
src/HOL/Library/Mapping.thy
     1.1 --- a/src/HOL/Library/Mapping.thy	Thu Nov 18 17:01:15 2010 +0100
     1.2 +++ b/src/HOL/Library/Mapping.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -41,6 +41,19 @@
     1.4    "delete k m = Mapping ((lookup m)(k := None))"
     1.5  
     1.6  
     1.7 +subsection {* Functorial structure *}
     1.8 +
     1.9 +definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where
    1.10 +  "map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)"
    1.11 +
    1.12 +lemma lookup_map [simp]:
    1.13 +  "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f"
    1.14 +  by (simp add: map_def)
    1.15 +
    1.16 +type_mapper map
    1.17 +  by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)
    1.18 +
    1.19 +
    1.20  subsection {* Derived operations *}
    1.21  
    1.22  definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where
    1.23 @@ -69,7 +82,7 @@
    1.24    "map_default k v f m = map_entry k f (default k v m)" 
    1.25  
    1.26  definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
    1.27 -  "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
    1.28 +  "tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))"
    1.29  
    1.30  definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where
    1.31    "bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
    1.32 @@ -294,6 +307,6 @@
    1.33  
    1.34  
    1.35  hide_const (open) empty is_empty lookup update delete ordered_keys keys size
    1.36 -  replace default map_entry map_default tabulate bulkload
    1.37 +  replace default map_entry map_default tabulate bulkload map
    1.38  
    1.39  end
    1.40 \ No newline at end of file