equal
deleted
inserted
replaced
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) |