lemma drop_Suc_conv_tl added.
authormehta
Fri Apr 16 15:46:50 2004 +0200 (2004-04-16)
changeset 145917be4d5dadf15
parent 14590 276ef51cedbf
child 14592 dd1a2905ea73
lemma drop_Suc_conv_tl added.
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Apr 16 13:52:43 2004 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Apr 16 15:46:50 2004 +0200
     1.3 @@ -847,6 +847,12 @@
     1.4  apply (case_tac i, auto)
     1.5  done
     1.6  
     1.7 +lemma drop_Suc_conv_tl:
     1.8 +  "!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
     1.9 +apply (induct xs, simp)
    1.10 +apply (case_tac i, auto)
    1.11 +done
    1.12 +
    1.13  lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
    1.14  by (induct n) (auto, case_tac xs, auto)
    1.15