# HG changeset patch
# User oheimb
# Date 878672858 -3600
# Node ID daff3c9987cce0e645f2192bc3d4978ed65dee22
# Parent  916641b592197586c085931e87ac3d5d46d0e59e
added zip and nodup

diff -r 916641b59219 -r daff3c9987cc src/HOL/List.ML
--- 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";
 
diff -r 916641b59219 -r daff3c9987cc src/HOL/List.thy
--- 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"