author | haftmann |
Mon, 19 Apr 2010 07:38:35 +0200 | |
changeset 36199 | 4d220994f30b |
parent 36197 | 2e92aca73cab (current diff) |
parent 36198 | ead2db2be11a (diff) |
child 36200 | 4949ae210c38 |
child 36202 | 43ea1f28fc7c |
child 36218 | 0e4a01f3e7d3 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/List.thy Sat Apr 17 23:05:52 2010 +0200 +++ b/src/HOL/List.thy Mon Apr 19 07:38:35 2010 +0200 @@ -1943,6 +1943,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)