changeset 36198 | ead2db2be11a |
parent 35828 | 46cfc4b8112e |
child 36199 | 4d220994f30b |
--- 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)