merged

--- a/src/HOL/List.thy	Fri Sep 01 11:33:32 2017 +0200
+++ b/src/HOL/List.thy	Fri Sep 01 12:19:40 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	Fri Sep 01 11:33:32 2017 +0200
+++ b/src/HOL/Map.thy	Fri Sep 01 12:19:40 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)
@@ -619,6 +633,33 @@
  apply auto
 done
 
+lemma ran_map_add:
+  assumes "dom m1 \<inter> dom m2 = {}"
+  shows "ran (m1 ++ m2) = ran m1 \<union> ran m2"
+proof
+  show "ran (m1 ++ m2) \<subseteq> ran m1 \<union> ran m2"
+    unfolding ran_def by auto
+next
+  show "ran m1 \<union> ran m2 \<subseteq> ran (m1 ++ m2)"
+  proof -
+    have "(m1 ++ m2) x = Some y" if "m1 x = Some y" for x y
+      using assms map_add_comm that by fastforce
+    moreover have "(m1 ++ m2) x = Some y" if "m2 x = Some y" for x y
+      using assms that by auto
+    ultimately show ?thesis
+      unfolding ran_def by blast
+  qed
+qed
+
+lemma finite_ran:
+  assumes "finite (dom p)"
+  shows "finite (ran p)"
+proof -
+  have "ran p = (\<lambda>x. the (p x)) ` dom p"
+    unfolding ran_def by force
+  from this \<open>finite (dom p)\<close> show ?thesis by auto
+qed
+
 lemma ran_distinct:
   assumes dist: "distinct (map fst al)"
   shows "ran (map_of al) = snd ` set al"
@@ -634,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)
 

--- a/src/HOL/Parity.thy	Fri Sep 01 11:33:32 2017 +0200
+++ b/src/HOL/Parity.thy	Fri Sep 01 12:19:40 2017 +0200
@@ -242,6 +242,9 @@
 lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
   by simp
 
+lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
+  by (cases "even (n + k)") auto
+
 end
 
 context linordered_idom