more convenient equations for zip

--- a/src/HOL/List.thy	Thu Apr 15 12:27:14 2010 +0200
+++ b/src/HOL/List.thy	Mon Apr 19 07:38:08 2010 +0200
@@ -1931,6 +1931,12 @@
 
 declare zip_Cons [simp del]
 
+lemma [code]:
+  "zip [] ys = []"
+  "zip xs [] = []"
+  "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
+  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
+
 lemma zip_Cons1:
  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
 by(auto split:list.split)