1.1 --- a/src/HOL/List.thy Sun Aug 27 06:56:29 2017 +0200
1.2 +++ b/src/HOL/List.thy Fri Sep 01 09:45:56 2017 +0200
1.3 @@ -2607,6 +2607,24 @@
1.4 \<and> n < length xs \<and> n < length ys)"
1.5 by (cases p) (auto simp add: set_zip)
1.6
1.7 +lemma in_set_impl_in_set_zip1:
1.8 + assumes "length xs = length ys"
1.9 + assumes "x \<in> set xs"
1.10 + obtains y where "(x, y) \<in> set (zip xs ys)"
1.11 +proof -
1.12 + from assms have "x \<in> set (map fst (zip xs ys))" by simp
1.13 + from this that show ?thesis by fastforce
1.14 +qed
1.15 +
1.16 +lemma in_set_impl_in_set_zip2:
1.17 + assumes "length xs = length ys"
1.18 + assumes "y \<in> set ys"
1.19 + obtains x where "(x, y) \<in> set (zip xs ys)"
1.20 +proof -
1.21 + from assms have "y \<in> set (map snd (zip xs ys))" by simp
1.22 + from this that show ?thesis by fastforce
1.23 +qed
1.24 +
1.25 lemma pair_list_eqI:
1.26 assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
1.27 shows "xs = ys"

2.1 --- a/src/HOL/Map.thy Sun Aug 27 06:56:29 2017 +0200
2.2 +++ b/src/HOL/Map.thy Fri Sep 01 09:45:56 2017 +0200
2.3 @@ -202,6 +202,20 @@
2.4 ultimately show ?case by simp
2.5 qed
2.6
2.7 +lemma map_of_zip_nth:
2.8 + assumes "length xs = length ys"
2.9 + assumes "distinct xs"
2.10 + assumes "i < length ys"
2.11 + shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
2.12 +using assms proof (induct arbitrary: i rule: list_induct2)
2.13 + case Nil
2.14 + then show ?case by simp
2.15 +next
2.16 + case (Cons x xs y ys)
2.17 + then show ?case
2.18 + using less_Suc_eq_0_disj by auto
2.19 +qed
2.20 +
2.21 lemma map_of_zip_map:
2.22 "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
2.23 by (induct xs) (simp_all add: fun_eq_iff)
2.24 @@ -661,6 +675,11 @@
2.25 ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
2.26 qed
2.27
2.28 +lemma ran_map_of_zip:
2.29 + assumes "length xs = length ys" "distinct xs"
2.30 + shows "ran (map_of (zip xs ys)) = set ys"
2.31 +using assms by (simp add: ran_distinct set_map[symmetric])
2.32 +
2.33 lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
2.34 by (auto simp add: ran_def)
2.35