# HG changeset patch
# User haftmann
# Date 1233997027 -3600
# Node ID 9acb915a62fa691664ab8c9a796639593ff9bd4f
# Parent  2bc09b164f2beeff43d977407ca359bcbea2f40f
code theorems for nth, list_update

diff -r 2bc09b164f2b -r 9acb915a62fa src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Feb 07 09:57:03 2009 +0100
+++ b/src/HOL/List.thy	Sat Feb 07 09:57:07 2009 +0100
@@ -1852,6 +1852,15 @@
   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
 by(blast dest: set_zip_leftD set_zip_rightD)
 
+lemma zip_map_fst_snd:
+  "zip (map fst zs) (map snd zs) = zs"
+  by (induct zs) simp_all
+
+lemma zip_eq_conv:
+  "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
+  by (auto simp add: zip_map_fst_snd)
+
+
 subsubsection {* @{text list_all2} *}
 
 lemma list_all2_lengthD [intro?]: