96 |
96 |
97 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" |
97 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" |
98 morphisms rep Mapping |
98 morphisms rep Mapping |
99 .. |
99 .. |
100 |
100 |
101 setup_lifting (no_code) type_definition_mapping |
101 setup_lifting type_definition_mapping |
102 |
102 |
103 lift_definition empty :: "('a, 'b) mapping" |
103 lift_definition empty :: "('a, 'b) mapping" |
104 is Map.empty parametric empty_parametric . |
104 is Map.empty parametric empty_parametric . |
105 |
105 |
106 lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option" |
106 lift_definition lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<Rightarrow> 'b option" |
107 is "\<lambda>m k. m k" parametric lookup_parametric . |
107 is "\<lambda>m k. m k" parametric lookup_parametric . |
108 |
108 |
|
109 declare [[code drop: Mapping.lookup]] |
|
110 setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close> |
|
111 |
109 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
112 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
110 is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric . |
113 is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric . |
111 |
114 |
112 lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
115 lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
113 is "\<lambda>k m. m(k := None)" parametric delete_parametric . |
116 is "\<lambda>k m. m(k := None)" parametric delete_parametric . |
121 lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" |
124 lift_definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" |
122 is "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_parametric . |
125 is "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_parametric . |
123 |
126 |
124 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" |
127 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" |
125 is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric . |
128 is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric . |
|
129 |
|
130 declare [[code drop: map]] |
126 |
131 |
127 |
132 |
128 subsection {* Functorial structure *} |
133 subsection {* Functorial structure *} |
129 |
134 |
130 functor map: map |
135 functor map: map |