# 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 \<Longrightarrow> 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 \<le> 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 \<le> y` show ?thesis by (cases m) simp_all
+  qed
+qed
+
+lemma sorted_drop:
+  "sorted xs \<Longrightarrow> 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..<j]"