modified zip
authornipkow
Mon Mar 08 13:49:14 1999 +0100 (1999-03-08)
changeset 630681e7fbf61db2
parent 6305 4cbdb974220c
child 6307 fdf236c98914
modified zip
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/List.ML	Fri Mar 05 12:11:54 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Mar 08 13:49:14 1999 +0100
     1.3 @@ -837,9 +837,21 @@
     1.4  by Auto_tac;
     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 +(** zip **)
    1.11 +section "zip";
    1.12 +
    1.13 +Goal "zip [] ys = []";
    1.14 +by(induct_tac "ys" 1);
    1.15 +by Auto_tac;
    1.16 +qed "zip_Nil";
    1.17 +Addsimps [zip_Nil];
    1.18 +
    1.19 +Goal "zip (x#xs) (y#ys) = (x,y)#zip xs ys";
    1.20 +by(Simp_tac 1);
    1.21 +qed "zip_Cons_Cons";
    1.22 +Addsimps [zip_Cons_Cons];
    1.23 +
    1.24 +Delsimps(tl (thms"zip.simps"));
    1.25  
    1.26  
    1.27  (** foldl **)
     2.1 --- a/src/HOL/List.thy	Fri Mar 05 12:11:54 1999 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Mar 08 13:49:14 1999 +0100
     2.3 @@ -140,7 +140,7 @@
     2.4    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
     2.5  primrec
     2.6    "zip xs []     = []"
     2.7 -  "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
     2.8 +  "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
     2.9  primrec
    2.10    "[i..0(] = []"
    2.11    "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"