added lemmas Isabelle2020-RC0
authornipkow
Thu Feb 13 19:11:35 2020 +0100 (12 days ago ago)
changeset 7165621c0b3a9d2f8
parent 71655 ff6394cfc05c
child 71657 e596ea18bf3e
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Feb 13 07:43:48 2020 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Feb 13 19:11:35 2020 +0100
     1.3 @@ -5172,6 +5172,20 @@
     1.4    "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
     1.5  by (induction xs) simp_all
     1.6  
     1.7 +lemma
     1.8 +  assumes "sorted_wrt f xs"
     1.9 +  shows sorted_wrt_take: "sorted_wrt f (take n xs)"
    1.10 +  and   sorted_wrt_drop: "sorted_wrt f (drop n xs)"
    1.11 +proof -
    1.12 +  from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp
    1.13 +  thus "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)"
    1.14 +    unfolding sorted_wrt_append by simp_all
    1.15 +qed
    1.16 +
    1.17 +lemma sorted_wrt_filter:
    1.18 +  "sorted_wrt f xs \<Longrightarrow> sorted_wrt f (filter P xs)"
    1.19 +by (induction xs) auto
    1.20 +
    1.21  lemma sorted_wrt_rev:
    1.22    "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
    1.23  by (induction xs) (auto simp add: sorted_wrt_append)