lib+proof: rename set_zip_helper to in_set_zipD and move to Lib

Signed-off-by: Michael McInerney <[email protected]>

lib/Lib.thy

@@ -2268,6 +2268,10 @@ lemma in_set_zip2:
   "(x, y) \<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
   by (erule in_set_zipE)
 
+lemma in_set_zipD:
+  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
+  by (clarsimp simp add: set_zip)
+
 lemma map_zip_snd_take:
   "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)"
   apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp)

proof/access-control/Syscall_AC.thy

@@ -976,7 +976,7 @@ crunch_ignore (add: cap_swap_ext cap_move_ext cap_insert_ext create_cap_ext set_
 
 lemma zet_zip_contrapos:
   "fst t \<notin> set xs  \<Longrightarrow> t \<notin> set (zip xs ys)"
-  by (auto simp: set_zip_helper)
+  by (auto simp: in_set_zipD)
 
 lemma ct_active_update[simp]:
   "ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s"

proof/crefine/ARM_HYP/Arch_C.thy

@@ -2102,7 +2102,7 @@ lemma performPageInvocationMapPDE_ccorres:
           apply (simp add: typ_at_to_obj_at_arches[symmetric])
           apply ((wp mapM_x_storePDE_pde_mappings' mapM_x_wp' valid_pde_slots_lift2 | simp add: split_def)+)[2]
          apply (clarsimp simp: valid_pde_mapping'_def valid_pde_slots'2_def)
-         apply (drule set_zip_helper, clarsimp)
+         apply (drule in_set_zipD, clarsimp)
         apply clarsimp
         apply (simp add: typ_at_to_obj_at_arches)
         apply (frule bspec, erule hd_in_zip_set)

proof/invariant-abstract/Untyped_AI.thy

@@ -1380,12 +1380,6 @@ lemma retype_ret_valid_caps:
  done
 end
 
-(* FIXME: move to Lib *)
-lemma set_zip_helper:
-  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys"
-  by (clarsimp simp add: set_zip)
-
-
 lemma ex_cte_cap_protects:
   "\<lbrakk> ex_cte_cap_wp_to P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s;
      descendants_range_in S p' s; untyped_children_in_mdb s; S\<subseteq> untyped_range (UntypedCap dev ptr bits idx);
@@ -3277,7 +3271,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs:
   apply (rule hoare_gen_asm)
   apply (subgoal_tac "set (zip crefs orefs) \<subseteq> set crefs \<times> set (retype_addrs ptr tp (length slots) us)")
    prefer 2
-   apply (auto dest!: set_zip_helper)[1]
+   apply (auto dest!: in_set_zipD)[1]
   apply (induct ("zip crefs orefs"))
    apply (simp add: mapM_x_def sequence_x_def)
    apply wpsimp
@@ -3567,7 +3561,7 @@ lemma retype_region_post_retype_invs_folded:
 
 lemma tup_in_fst_image_set_zipD:
   "x \<in> fst ` set (zip xs ys) \<Longrightarrow> x \<in> set xs"
-  by (auto dest!: set_zip_helper)
+  by (auto dest!: in_set_zipD)
 
 lemma distinct_map_fst_zip:
   "distinct xs \<Longrightarrow> distinct (map fst (zip xs ys))"