more facts on Map.map_of and List.zip
authorbulwahn
Fri Sep 01 09:45:56 2017 +0200 (20 months ago)
changeset 66584acb02fa48ef3
parent 66583 ac183ddc9fef
child 66585 75c090d0e699
more facts on Map.map_of and List.zip
src/HOL/List.thy
src/HOL/Map.thy
     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