added lemma
authornipkow
Thu Sep 14 17:36:06 2017 +0200 (21 months ago)
changeset 666576f82e2ad261a
parent 66656 8f4d252ce2fe
child 66658 59acf5e73176
added lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Sep 13 17:40:54 2017 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 14 17:36:06 2017 +0200
     1.3 @@ -2034,6 +2034,9 @@
     1.4  lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
     1.5  by(cases xs, simp_all)
     1.6  
     1.7 +lemma hd_take: "j > 0 \<Longrightarrow> hd (take j xs) = hd xs"
     1.8 +by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
     1.9 +
    1.10  lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
    1.11  by (induct xs arbitrary: n) simp_all
    1.12