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