src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
@@ -2308,6 +2308,14 @@
   ==> dropWhile P l = dropWhile Q k"
 by (induct k arbitrary: l, simp_all)
 
+lemma takeWhile_idem [simp]:
+  "takeWhile P (takeWhile P xs) = takeWhile P xs"
+  by (induct xs) auto
+
+lemma dropWhile_idem [simp]:
+  "dropWhile P (dropWhile P xs) = dropWhile P xs"
+  by (induct xs) auto
+
 
 subsubsection {* @{const zip} *}
 
@@ -2947,6 +2955,10 @@
 apply (auto simp add: less_diff_conv)
 done
 
+lemma map_decr_upt:
+  "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
+  by (induct n) simp_all
+
 lemma nth_take_lemma:
   "k <= length xs ==> k <= length ys ==>
      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3703,7 +3715,6 @@
 apply clarsimp
 done
 
-
 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
 by (induct n) auto
 
@@ -3819,6 +3830,22 @@
   then show ?thesis by blast
 qed
 
+lemma Cons_replicate_eq:
+  "x # xs = replicate n y \<longleftrightarrow> x = y \<and> n > 0 \<and> xs = replicate (n - 1) x"
+  by (induct n) auto
+
+lemma replicate_length_same:
+  "(\<forall>y\<in>set xs. y = x) \<Longrightarrow> replicate (length xs) x = xs"
+  by (induct xs) simp_all
+
+lemma foldr_replicate [simp]:
+  "foldr f (replicate n x) = f x ^^ n"
+  by (induct n) (simp_all)
+
+lemma fold_replicate [simp]:
+  "fold f (replicate n x) = f x ^^ n"
+  by (subst foldr_fold [symmetric]) simp_all
+
 
 subsubsection {* @{const enumerate} *}