summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Map.thy

changeset 66584 | acb02fa48ef3 |

parent 66583 | ac183ddc9fef |

child 67051 | e7e54a0b9197 |

1.1 --- a/src/HOL/Map.thy Sun Aug 27 06:56:29 2017 +0200 1.2 +++ b/src/HOL/Map.thy Fri Sep 01 09:45:56 2017 +0200 1.3 @@ -202,6 +202,20 @@ 1.4 ultimately show ?case by simp 1.5 qed 1.6 1.7 +lemma map_of_zip_nth: 1.8 + assumes "length xs = length ys" 1.9 + assumes "distinct xs" 1.10 + assumes "i < length ys" 1.11 + shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)" 1.12 +using assms proof (induct arbitrary: i rule: list_induct2) 1.13 + case Nil 1.14 + then show ?case by simp 1.15 +next 1.16 + case (Cons x xs y ys) 1.17 + then show ?case 1.18 + using less_Suc_eq_0_disj by auto 1.19 +qed 1.20 + 1.21 lemma map_of_zip_map: 1.22 "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)" 1.23 by (induct xs) (simp_all add: fun_eq_iff) 1.24 @@ -661,6 +675,11 @@ 1.25 ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp 1.26 qed 1.27 1.28 +lemma ran_map_of_zip: 1.29 + assumes "length xs = length ys" "distinct xs" 1.30 + shows "ran (map_of (zip xs ys)) = set ys" 1.31 +using assms by (simp add: ran_distinct set_map[symmetric]) 1.32 + 1.33 lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m" 1.34 by (auto simp add: ran_def) 1.35