src/HOL/List.thy

 lemma dropWhile_cong [fundef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |] 
   ==> 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} *}
 
 lemma zip_Nil [simp]: "zip [] ys = []"
 by (induct ys) auto

 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
 apply (induct n m  arbitrary: i rule: diff_induct)
 prefer 3 apply (subst map_Suc_upt[symmetric])
 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"
 apply (atomize, induct k arbitrary: xs ys)

 apply clarsimp
 apply (case_tac i)
  apply simp
 apply clarsimp
 done
-
 
 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
 by (induct n) auto
 
 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"

   then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys"
     using `xs \<noteq> []` and `ys \<noteq> []`
     by (auto simp: replicate_add)
   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} *}
 
 lemma enumerate_simps [simp, code]: