--- a/src/HOL/List.ML Tue Nov 04 20:46:56 1997 +0100
+++ b/src/HOL/List.ML Tue Nov 04 20:47:38 1997 +0100
@@ -713,6 +713,9 @@
by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
qed_spec_mp"set_take_whileD";
+qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);
+qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys"
+ (K [Simp_tac 1]);
(** replicate **)
section "replicate";
--- a/src/HOL/List.thy Tue Nov 04 20:46:56 1997 +0100
+++ b/src/HOL/List.thy Tue Nov 04 20:47:38 1997 +0100
@@ -26,6 +26,8 @@
dropWhile :: ('a => bool) => 'a list => 'a list
tl, butlast :: 'a list => 'a list
rev :: 'a list => 'a list
+ zip :: "'a list => 'b list => ('a * 'b) list"
+ nodup :: "'a list => bool"
replicate :: nat => 'a => 'a list
syntax
@@ -112,6 +114,12 @@
primrec dropWhile list
"dropWhile P [] = []"
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
+primrec zip list
+ "zip xs [] = []"
+ "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
+primrec nodup list
+ "nodup [] = True"
+ "nodup (x#xs) = (x ~: set xs & nodup xs)"
primrec replicate nat
replicate_0 "replicate 0 x = []"
replicate_Suc "replicate (Suc n) x = x # replicate n x"