equal
deleted
inserted
replaced
119 is "\<lambda>m k. m k" parametric lookup_parametric . |
119 is "\<lambda>m k. m k" parametric lookup_parametric . |
120 |
120 |
121 definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)" |
121 definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)" |
122 |
122 |
123 declare [[code drop: Mapping.lookup]] |
123 declare [[code drop: Mapping.lookup]] |
124 setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close> |
124 setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close> |
125 |
125 |
126 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
126 lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
127 is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric . |
127 is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric . |
128 |
128 |
129 lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |
129 lift_definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" |