equal
deleted
inserted
replaced
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Parametricity transfer rules\<close> |
11 subsection \<open>Parametricity transfer rules\<close> |
12 |
12 |
13 lemma map_of_foldr: -- \<open>FIXME move\<close> |
13 lemma map_of_foldr: \<comment> \<open>FIXME move\<close> |
14 "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty" |
14 "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty" |
15 using map_add_map_of_foldr [of Map.empty] by auto |
15 using map_add_map_of_foldr [of Map.empty] by auto |
16 |
16 |
17 context |
17 context |
18 begin |
18 begin |
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]] |
109 declare [[code drop: Mapping.lookup]] |
110 setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> -- \<open>FIXME lifting\<close> |
110 setup \<open>Code.add_default_eqn @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close> |
111 |
111 |
112 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" |
113 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 . |
114 |
114 |
115 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" |