--- a/src/HOL/List.thy Sun Aug 27 06:56:29 2017 +0200
+++ b/src/HOL/List.thy Fri Sep 01 09:45:56 2017 +0200
@@ -2607,6 +2607,24 @@
\<and> n < length xs \<and> n < length ys)"
by (cases p) (auto simp add: set_zip)
+lemma in_set_impl_in_set_zip1:
+ assumes "length xs = length ys"
+ assumes "x \<in> set xs"
+ obtains y where "(x, y) \<in> set (zip xs ys)"
+proof -
+ from assms have "x \<in> set (map fst (zip xs ys))" by simp
+ from this that show ?thesis by fastforce
+qed
+
+lemma in_set_impl_in_set_zip2:
+ assumes "length xs = length ys"
+ assumes "y \<in> set ys"
+ obtains x where "(x, y) \<in> set (zip xs ys)"
+proof -
+ from assms have "y \<in> set (map snd (zip xs ys))" by simp
+ from this that show ?thesis by fastforce
+qed
+
lemma pair_list_eqI:
assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
shows "xs = ys"
--- a/src/HOL/Map.thy Sun Aug 27 06:56:29 2017 +0200
+++ b/src/HOL/Map.thy Fri Sep 01 09:45:56 2017 +0200
@@ -202,6 +202,20 @@
ultimately show ?case by simp
qed
+lemma map_of_zip_nth:
+ assumes "length xs = length ys"
+ assumes "distinct xs"
+ assumes "i < length ys"
+ shows "map_of (zip xs ys) (xs ! i) = Some (ys ! i)"
+using assms proof (induct arbitrary: i rule: list_induct2)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons x xs y ys)
+ then show ?case
+ using less_Suc_eq_0_disj by auto
+qed
+
lemma map_of_zip_map:
"map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
by (induct xs) (simp_all add: fun_eq_iff)
@@ -661,6 +675,11 @@
ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
qed
+lemma ran_map_of_zip:
+ assumes "length xs = length ys" "distinct xs"
+ shows "ran (map_of (zip xs ys)) = set ys"
+using assms by (simp add: ran_distinct set_map[symmetric])
+
lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
by (auto simp add: ran_def)