# HG changeset patch # User haftmann # Date 1232954621 -3600 # Node ID 6f8aada233c124a7f5ddf8d4c4ed4568d6ab487a # Parent a04710c3e09648b6676a62b4c92a7e44c2d76e1e sorted_take, sorted_drop diff -r a04710c3e096 -r 6f8aada233c1 src/HOL/List.thy --- a/src/HOL/List.thy Fri Jan 23 19:52:02 2009 +0100 +++ b/src/HOL/List.thy Mon Jan 26 08:23:41 2009 +0100 @@ -2887,6 +2887,35 @@ apply (auto simp: sorted_distinct_set_unique) done +lemma sorted_take: + "sorted xs \ sorted (take n xs)" +proof (induct xs arbitrary: n rule: sorted.induct) + case 1 show ?case by simp +next + case 2 show ?case by (cases n) simp_all +next + case (3 x y xs) + then have "x \ y" by simp + show ?case proof (cases n) + case 0 then show ?thesis by simp + next + case (Suc m) + with 3 have "sorted (take m (y # xs))" by simp + with Suc `x \ y` show ?thesis by (cases m) simp_all + qed +qed + +lemma sorted_drop: + "sorted xs \ sorted (drop n xs)" +proof (induct xs arbitrary: n rule: sorted.induct) + case 1 show ?case by simp +next + case 2 show ?case by (cases n) simp_all +next + case 3 then show ?case by (cases n) simp_all +qed + + end lemma sorted_upt[simp]: "sorted[i..