src/HOL/List.thy
changeset 14591 7be4d5dadf15
parent 14589 feae7b5fd425
child 14770 fe9504ba63d5
equal deleted inserted replaced
14590:276ef51cedbf 14591:7be4d5dadf15
   845  "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   845  "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
   846 apply (induct xs, simp)
   846 apply (induct xs, simp)
   847 apply (case_tac i, auto)
   847 apply (case_tac i, auto)
   848 done
   848 done
   849 
   849 
       
   850 lemma drop_Suc_conv_tl:
       
   851   "!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
       
   852 apply (induct xs, simp)
       
   853 apply (case_tac i, auto)
       
   854 done
       
   855 
   850 lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
   856 lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
   851 by (induct n) (auto, case_tac xs, auto)
   857 by (induct n) (auto, case_tac xs, auto)
   852 
   858 
   853 lemma length_drop [simp]: "!!xs. length (drop n xs) = (length xs - n)"
   859 lemma length_drop [simp]: "!!xs. length (drop n xs) = (length xs - n)"
   854 by (induct n) (auto, case_tac xs, auto)
   860 by (induct n) (auto, case_tac xs, auto)