330 lemma inj_on_map_add_dom [iff]: |
330 lemma inj_on_map_add_dom [iff]: |
331 "inj_on (m ++ m') (dom m') = inj_on m' (dom m')" |
331 "inj_on (m ++ m') (dom m') = inj_on m' (dom m')" |
332 by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits) |
332 by (fastsimp simp: map_add_def dom_def inj_on_def split: option.splits) |
333 |
333 |
334 lemma map_upds_fold_map_upd: |
334 lemma map_upds_fold_map_upd: |
335 "f(ks[\<mapsto>]vs) = foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs)" |
335 "m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)" |
336 unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length) |
336 unfolding map_upds_def proof (rule sym, rule zip_obtain_same_length) |
337 fix ks :: "'a list" and vs :: "'b list" |
337 fix ks :: "'a list" and vs :: "'b list" |
338 assume "length ks = length vs" |
338 assume "length ks = length vs" |
339 then show "foldl (\<lambda>f (k, v). f(k\<mapsto>v)) f (zip ks vs) = f ++ map_of (rev (zip ks vs))" |
339 then show "foldl (\<lambda>m (k, v). m(k\<mapsto>v)) m (zip ks vs) = m ++ map_of (rev (zip ks vs))" |
340 by (induct arbitrary: f rule: list_induct2) simp_all |
340 by(induct arbitrary: m rule: list_induct2) simp_all |
341 qed |
341 qed |
342 |
342 |
343 lemma map_add_map_of_foldr: |
343 lemma map_add_map_of_foldr: |
344 "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m" |
344 "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m" |
345 by (induct ps) (auto simp add: expand_fun_eq map_add_def) |
345 by (induct ps) (auto simp add: expand_fun_eq map_add_def) |