# HG changeset patch
# User nipkow
# Date 1581617495 -3600
# Node ID 21c0b3a9d2f8f27800f7ea9c8f0fe92139e9e2c3
# Parent  ff6394cfc05c609605b68ef7c761d2b538c2e81b
added lemmas

diff -r ff6394cfc05c -r 21c0b3a9d2f8 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 13 07:43:48 2020 +0100
+++ b/src/HOL/List.thy	Thu Feb 13 19:11:35 2020 +0100
@@ -5172,6 +5172,20 @@
   "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
 by (induction xs) simp_all
 
+lemma
+  assumes "sorted_wrt f xs"
+  shows sorted_wrt_take: "sorted_wrt f (take n xs)"
+  and   sorted_wrt_drop: "sorted_wrt f (drop n xs)"
+proof -
+  from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp
+  thus "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)"
+    unfolding sorted_wrt_append by simp_all
+qed
+
+lemma sorted_wrt_filter:
+  "sorted_wrt f xs \<Longrightarrow> sorted_wrt f (filter P xs)"
+by (induction xs) auto
+
 lemma sorted_wrt_rev:
   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
 by (induction xs) (auto simp add: sorted_wrt_append)