# HG changeset patch
# User nipkow
# Date 1118829253 -7200
# Node ID c047008f88d4545d24766445cd16f19a4383949c
# Parent  d9d2a0cadd5eb4c8c1867c705b0ef156c2f31f3f
added lemmas

diff -r d9d2a0cadd5e -r c047008f88d4 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 15 09:01:48 2005 +0200
+++ b/src/HOL/List.thy	Wed Jun 15 11:54:13 2005 +0200
@@ -1650,6 +1650,13 @@
 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
 by (induct n) auto
 
+text{* Courtesy of Matthias Daum: *}
+lemma append_replicate_commute:
+  "replicate n x @ replicate k x = replicate k x @ replicate n x"
+apply (simp add: replicate_add [THEN sym])
+apply (simp add: add_commute)
+done
+
 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
 by (induct n) auto
 
@@ -1664,6 +1671,27 @@
 apply (simp add: nth_Cons split: nat.split)
 done
 
+text{* Courtesy of Matthias Daum (2 lemmas): *}
+lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
+apply (case_tac "k \<le> i")
+ apply  (simp add: min_def)
+apply (drule not_leE)
+apply (simp add: min_def)
+apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
+ apply  simp
+apply (simp add: replicate_add [symmetric])
+done
+
+lemma drop_replicate[simp]: "!!i. drop i (replicate k x) = replicate (k-i) x"
+apply (induct k)
+ apply simp
+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