added zip and nodup
authoroheimb
Tue Nov 04 20:47:38 1997 +0100 (1997-11-04)
changeset 4132daff3c9987cc
parent 4131 916641b59219
child 4133 0a08c2b9b1ed
added zip and nodup
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/List.ML	Tue Nov 04 20:46:56 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Nov 04 20:47:38 1997 +0100
     1.3 @@ -713,6 +713,9 @@
     1.4  by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
     1.5  qed_spec_mp"set_take_whileD";
     1.6  
     1.7 +qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
     1.8 +qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
     1.9 +						      (K [Simp_tac 1]);
    1.10  (** replicate **)
    1.11  section "replicate";
    1.12  
     2.1 --- a/src/HOL/List.thy	Tue Nov 04 20:46:56 1997 +0100
     2.2 +++ b/src/HOL/List.thy	Tue Nov 04 20:47:38 1997 +0100
     2.3 @@ -26,6 +26,8 @@
     2.4    dropWhile   :: ('a => bool) => 'a list => 'a list
     2.5    tl, butlast :: 'a list => 'a list
     2.6    rev         :: 'a list => 'a list
     2.7 +  zip	      :: "'a list => 'b list => ('a * 'b) list"
     2.8 +  nodup	      :: "'a list => bool"
     2.9    replicate   :: nat => 'a => 'a list
    2.10  
    2.11  syntax
    2.12 @@ -112,6 +114,12 @@
    2.13  primrec dropWhile list
    2.14    "dropWhile P [] = []"
    2.15    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
    2.16 +primrec zip list
    2.17 +  "zip xs []     = []"
    2.18 +  "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
    2.19 +primrec nodup list
    2.20 +  "nodup []     = True"
    2.21 +  "nodup (x#xs) = (x ~: set xs & nodup xs)"
    2.22  primrec replicate nat
    2.23  replicate_0   "replicate 0 x       = []"
    2.24  replicate_Suc "replicate (Suc n) x = x # replicate n x"