1.1 --- a/src/HOL/List.thy	Tue Apr 08 20:14:36 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Apr 09 05:30:14 2008 +0200
     1.3 @@ -1388,6 +1388,9 @@
     1.4  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
     1.5  by(induct xs)(auto simp:neq_Nil_conv)
     1.6  
     1.7 +lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
     1.8 +by (induct xs, simp, case_tac xs, simp_all)
     1.9 +
    1.10  
    1.11  subsubsection {* @{text take} and @{text drop} *}
    1.12  
    1.13 @@ -1411,9 +1414,18 @@
    1.14  lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
    1.15  by(cases xs, simp_all)
    1.16  
    1.17 +lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
    1.18 +by (induct xs arbitrary: n) simp_all
    1.19 +
    1.20  lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
    1.21  by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
    1.22  
    1.23 +lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
    1.24 +by (cases n, simp, cases xs, auto)
    1.25 +
    1.26 +lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
    1.27 +by (simp only: drop_tl)
    1.28 +
    1.29  lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
    1.30  apply (induct xs arbitrary: n, simp)
    1.31  apply(simp add:drop_Cons nth_Cons split:nat.splits)
    1.32 @@ -1522,6 +1534,19 @@
    1.33  apply (case_tac xs, auto)
    1.34  done
    1.35  
    1.36 +lemma butlast_take:
    1.37 +  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
    1.38 +by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
    1.39 +
    1.40 +lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
    1.41 +by (simp add: butlast_conv_take drop_take)
    1.42 +
    1.43 +lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
    1.44 +by (simp add: butlast_conv_take min_max.inf_absorb1)
    1.45 +
    1.46 +lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
    1.47 +by (simp add: butlast_conv_take drop_take)
    1.48 +
    1.49  lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
    1.50  by(simp add: hd_conv_nth)
    1.51  

     2.1 --- a/src/HOL/Word/BinBoolList.thy	Tue Apr 08 20:14:36 2008 +0200
     2.2 +++ b/src/HOL/Word/BinBoolList.thy	Wed Apr 09 05:30:14 2008 +0200
     2.3 @@ -38,39 +38,6 @@
     2.4    | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     2.5      if y then rbl_add ws x else ws)"
     2.6  
     2.7 -lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
     2.8 -  apply (cases n, clarsimp)
     2.9 -  apply (cases l, auto)
    2.10 -  done
    2.11 -
    2.12 -lemma take_butlast [rule_format] :
    2.13 -  "ALL n. n < length l --> take n (butlast l) = take n l"
    2.14 -  apply (induct l, clarsimp)
    2.15 -  apply clarsimp
    2.16 -  apply (case_tac n)
    2.17 -  apply auto
    2.18 -  done
    2.19 -
    2.20 -lemma butlast_take [rule_format] :
    2.21 -  "ALL n. n <= length l --> butlast (take n l) = take (n - 1) l"
    2.22 -  apply (induct l, clarsimp)
    2.23 -  apply clarsimp
    2.24 -  apply (case_tac "n")
    2.25 -   apply safe
    2.26 -   apply simp_all
    2.27 -  apply (case_tac "nat")
    2.28 -   apply auto
    2.29 -  done
    2.30 -
    2.31 -lemma butlast_drop [rule_format] :
    2.32 -  "ALL n. butlast (drop n l) = drop n (butlast l)"
    2.33 -  apply (induct l)
    2.34 -   apply clarsimp
    2.35 -  apply clarsimp
    2.36 -  apply safe
    2.37 -   apply ((case_tac n, auto)[1])+
    2.38 -  done
    2.39 -
    2.40  lemma butlast_power:
    2.41    "(butlast ^ n) bl = take (length bl - n) bl"
    2.42    by (induct n) (auto simp: butlast_take)