src/HOL/List.thy

--- a/src/HOL/List.thy	Tue Apr 08 20:14:36 2008 +0200
+++ b/src/HOL/List.thy	Wed Apr 09 05:30:14 2008 +0200
@@ -1388,6 +1388,9 @@
 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
 by(induct xs)(auto simp:neq_Nil_conv)
 
+lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
+by (induct xs, simp, case_tac xs, simp_all)
+
 
 subsubsection {* @{text take} and @{text drop} *}
 
@@ -1411,9 +1414,18 @@
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
 by(cases xs, simp_all)
 
+lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
+by (induct xs arbitrary: n) simp_all
+
 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
 
+lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
+by (cases n, simp, cases xs, auto)
+
+lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
+by (simp only: drop_tl)
+
 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
 apply (induct xs arbitrary: n, simp)
 apply(simp add:drop_Cons nth_Cons split:nat.splits)
@@ -1522,6 +1534,19 @@
 apply (case_tac xs, auto)
 done
 
+lemma butlast_take:
+  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
+by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
+
+lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
+by (simp add: butlast_conv_take drop_take)
+
+lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
+by (simp add: butlast_conv_take min_max.inf_absorb1)
+
+lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
+by (simp add: butlast_conv_take drop_take)
+
 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
 by(simp add: hd_conv_nth)