# HG changeset patch
# User nipkow
# Date 1505403366 -7200
# Node ID 6f82e2ad261a08fffee1ed406b203772c3f8fdc4
# Parent  8f4d252ce2fe45d92819d277e1390c6302c95798
added lemma

diff -r 8f4d252ce2fe -r 6f82e2ad261a src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 13 17:40:54 2017 +0200
+++ b/src/HOL/List.thy	Thu Sep 14 17:36:06 2017 +0200
@@ -2034,6 +2034,9 @@
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
 by(cases xs, simp_all)
 
+lemma hd_take: "j > 0 \<Longrightarrow> hd (take j xs) = hd xs"
+by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
+
 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
 by (induct xs arbitrary: n) simp_all