1.1 --- a/src/HOL/List.thy	Sat Feb 07 09:57:03 2009 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Feb 07 09:57:07 2009 +0100
     1.3 @@ -1852,6 +1852,15 @@
     1.4    "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
     1.5  by(blast dest: set_zip_leftD set_zip_rightD)
     1.6  
     1.7 +lemma zip_map_fst_snd:
     1.8 +  "zip (map fst zs) (map snd zs) = zs"
     1.9 +  by (induct zs) simp_all
    1.10 +
    1.11 +lemma zip_eq_conv:
    1.12 +  "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
    1.13 +  by (auto simp add: zip_map_fst_snd)
    1.14 +
    1.15 +
    1.16  subsubsection {* @{text list_all2} *}
    1.17  
    1.18  lemma list_all2_lengthD [intro?]: