diff -r 35b437f7ad51 -r 21ffc770ebc0 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/List.thy	Sat May 09 07:25:22 2009 +0200
@@ -1347,8 +1347,7 @@
 by (induct xs, auto)
 
 lemma update_zip:
-  "length xs = length ys ==>
-  (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
+  "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
 
 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
@@ -1829,6 +1828,10 @@
 apply simp_all
 done
 
+text{* Courtesy of Andreas Lochbihler: *}
+lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
+by(induct xs) auto
+
 lemma nth_zip [simp]:
 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
 apply (induct ys arbitrary: i xs, simp)
@@ -1838,11 +1841,11 @@
 
 lemma set_zip:
 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
-by (simp add: set_conv_nth cong: rev_conj_cong)
+by(simp add: set_conv_nth cong: rev_conj_cong)
 
 lemma zip_update:
-"length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
-by (rule sym, simp add: update_zip)
+  "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
+by(rule sym, simp add: update_zip)
 
 lemma zip_replicate [simp]:
   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
@@ -2577,6 +2580,11 @@
 apply (simp add: add_commute)
 done
 
+text{* Courtesy of Andreas Lochbihler: *}
+lemma filter_replicate:
+  "filter P (replicate n x) = (if P x then replicate n x else [])"
+by(induct n) auto
+
 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
 by (induct n) auto