src/HOL/List.thy

   by (simp add: butlast_conv_take min.absorb1)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   by (simp add: butlast_conv_take drop_take ac_simps)
 
+lemma butlast_power: "(butlast ^^ n) xs = take (length xs - n) xs"
+  by (induct n) (auto simp: butlast_take)
+
 lemma hd_drop_conv_nth: "n < length xs \<Longrightarrow> hd(drop n xs) = xs!n"
   by(simp add: hd_conv_nth)
 
 lemma set_take_subset_set_take:
   "m \<le> n \<Longrightarrow> set(take m xs) \<le> set(take n xs)"