src/HOL/List.thy
changeset 36198 ead2db2be11a
parent 35828 46cfc4b8112e
child 36199 4d220994f30b
     1.1 --- a/src/HOL/List.thy	Thu Apr 15 12:27:14 2010 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Apr 19 07:38:08 2010 +0200
     1.3 @@ -1931,6 +1931,12 @@
     1.4  
     1.5  declare zip_Cons [simp del]
     1.6  
     1.7 +lemma [code]:
     1.8 +  "zip [] ys = []"
     1.9 +  "zip xs [] = []"
    1.10 +  "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
    1.11 +  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
    1.12 +
    1.13  lemma zip_Cons1:
    1.14   "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
    1.15  by(auto split:list.split)