added lemmas Isabelle2020-RC0
authornipkow
Thu, 13 Feb 2020 19:11:35 +0100
changeset 71656 21c0b3a9d2f8
parent 71655 ff6394cfc05c
child 71657 e596ea18bf3e
added lemmas
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)