equal
deleted
inserted
replaced
1941 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys" |
1941 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys" |
1942 by simp |
1942 by simp |
1943 |
1943 |
1944 declare zip_Cons [simp del] |
1944 declare zip_Cons [simp del] |
1945 |
1945 |
|
1946 lemma [code]: |
|
1947 "zip [] ys = []" |
|
1948 "zip xs [] = []" |
|
1949 "zip (x # xs) (y # ys) = (x, y) # zip xs ys" |
|
1950 by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+ |
|
1951 |
1946 lemma zip_Cons1: |
1952 lemma zip_Cons1: |
1947 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)" |
1953 "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)" |
1948 by(auto split:list.split) |
1954 by(auto split:list.split) |
1949 |
1955 |
1950 lemma length_zip [simp]: |
1956 lemma length_zip [simp]: |