# HG changeset patch
# User haftmann
# Date 1271655488 -7200
# Node ID ead2db2be11a809f809f77f4f5ddf305857d0c9f
# Parent  b43b22f636659a86518bffe3416fd21a3316f8d6
more convenient equations for zip

diff -r b43b22f63665 -r ead2db2be11a src/HOL/List.thy
--- 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)