# HG changeset patch
# User huffman
# Date 1207711814 -7200
# Node ID 46f3b89b2445ae3aead388a2346b867228d9536e
# Parent  9f81ab1b7b64f447937af5d2b09d8692717d0981
move lemmas from Word/BinBoolList.thy to List.thy

diff -r 9f81ab1b7b64 -r 46f3b89b2445 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)
 
diff -r 9f81ab1b7b64 -r 46f3b89b2445 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Tue Apr 08 20:14:36 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Wed Apr 09 05:30:14 2008 +0200
@@ -38,39 +38,6 @@
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     if y then rbl_add ws x else ws)"
 
-lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
-  apply (cases n, clarsimp)
-  apply (cases l, auto)
-  done
-
-lemma take_butlast [rule_format] :
-  "ALL n. n < length l --> take n (butlast l) = take n l"
-  apply (induct l, clarsimp)
-  apply clarsimp
-  apply (case_tac n)
-  apply auto
-  done
-
-lemma butlast_take [rule_format] :
-  "ALL n. n <= length l --> butlast (take n l) = take (n - 1) l"
-  apply (induct l, clarsimp)
-  apply clarsimp
-  apply (case_tac "n")
-   apply safe
-   apply simp_all
-  apply (case_tac "nat")
-   apply auto
-  done
-
-lemma butlast_drop [rule_format] :
-  "ALL n. butlast (drop n l) = drop n (butlast l)"
-  apply (induct l)
-   apply clarsimp
-  apply clarsimp
-  apply safe
-   apply ((case_tac n, auto)[1])+
-  done
-
 lemma butlast_power:
   "(butlast ^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)