# HG changeset patch
# User nipkow
# Date 1604692267 -3600
# Node ID 653ac845b4662735bb900509bb69bfc7b74b4c2d
# Parent  81518b38b3165d95a4eef2b30dfee01036e3fc77
added lemma

diff -r 81518b38b316 -r 653ac845b466 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Nov 06 14:32:42 2020 +0100
+++ b/src/HOL/List.thy	Fri Nov 06 20:51:07 2020 +0100
@@ -2255,6 +2255,9 @@
 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)