1.1 --- a/src/HOL/List.thy	Wed Jun 15 09:01:48 2005 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Jun 15 11:54:13 2005 +0200
     1.3 @@ -1650,6 +1650,13 @@
     1.4  lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
     1.5  by (induct n) auto
     1.6  
     1.7 +text{* Courtesy of Matthias Daum: *}
     1.8 +lemma append_replicate_commute:
     1.9 +  "replicate n x @ replicate k x = replicate k x @ replicate n x"
    1.10 +apply (simp add: replicate_add [THEN sym])
    1.11 +apply (simp add: add_commute)
    1.12 +done
    1.13 +
    1.14  lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
    1.15  by (induct n) auto
    1.16  
    1.17 @@ -1664,6 +1671,27 @@
    1.18  apply (simp add: nth_Cons split: nat.split)
    1.19  done
    1.20  
    1.21 +text{* Courtesy of Matthias Daum (2 lemmas): *}
    1.22 +lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
    1.23 +apply (case_tac "k \<le> i")
    1.24 + apply  (simp add: min_def)
    1.25 +apply (drule not_leE)
    1.26 +apply (simp add: min_def)
    1.27 +apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
    1.28 + apply  simp
    1.29 +apply (simp add: replicate_add [symmetric])
    1.30 +done
    1.31 +
    1.32 +lemma drop_replicate[simp]: "!!i. drop i (replicate k x) = replicate (k-i) x"
    1.33 +apply (induct k)
    1.34 + apply simp
    1.35 +apply clarsimp
    1.36 +apply (case_tac i)
    1.37 + apply simp
    1.38 +apply clarsimp
    1.39 +done
    1.40 +
    1.41 +
    1.42  lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
    1.43  by (induct n) auto
    1.44