equal
deleted
inserted
replaced
473 (simp_all add: clearjunk_delete delete_map assms) |
473 (simp_all add: clearjunk_delete delete_map assms) |
474 |
474 |
475 |
475 |
476 subsection \<open>\<open>map_ran\<close>\<close> |
476 subsection \<open>\<open>map_ran\<close>\<close> |
477 |
477 |
478 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" |
478 definition map_ran :: "('key \<Rightarrow> 'val1 \<Rightarrow> 'val2) \<Rightarrow> ('key \<times> 'val1) list \<Rightarrow> ('key \<times> 'val2) list" |
479 where "map_ran f = map (\<lambda>(k, v). (k, f k v))" |
479 where "map_ran f = map (\<lambda>(k, v). (k, f k v))" |
480 |
480 |
481 lemma map_ran_simps [simp]: |
481 lemma map_ran_simps [simp]: |
482 "map_ran f [] = []" |
482 "map_ran f [] = []" |
483 "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps" |
483 "map_ran f ((k, v) # ps) = (k, f k v) # map_ran f ps" |