changeset 14802 | e05116289ff9 |
parent 14770 | fe9504ba63d5 |
child 14981 | e73f8140af78 |
--- a/src/HOL/List.thy Fri May 21 21:49:45 2004 +0200 +++ b/src/HOL/List.thy Mon May 24 18:35:34 2004 +0200 @@ -889,6 +889,12 @@ apply (case_tac xs, auto) done +lemma drop_take: "!!m n. drop n (take m xs) = take (m-n) (drop n xs)" +apply(induct xs) + apply simp +apply(simp add: take_Cons drop_Cons split:nat.split) +done + lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs" apply (induct n, auto) apply (case_tac xs, auto)