src/HOL/List.thy
changeset 71656 21c0b3a9d2f8
parent 71647 d8fb621fea02
child 71781 4b1021677f15
equal deleted inserted replaced
71655:ff6394cfc05c 71656:21c0b3a9d2f8
  5170 
  5170 
  5171 lemma sorted_wrt_map:
  5171 lemma sorted_wrt_map:
  5172   "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
  5172   "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
  5173 by (induction xs) simp_all
  5173 by (induction xs) simp_all
  5174 
  5174 
       
  5175 lemma
       
  5176   assumes "sorted_wrt f xs"
       
  5177   shows sorted_wrt_take: "sorted_wrt f (take n xs)"
       
  5178   and   sorted_wrt_drop: "sorted_wrt f (drop n xs)"
       
  5179 proof -
       
  5180   from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp
       
  5181   thus "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)"
       
  5182     unfolding sorted_wrt_append by simp_all
       
  5183 qed
       
  5184 
       
  5185 lemma sorted_wrt_filter:
       
  5186   "sorted_wrt f xs \<Longrightarrow> sorted_wrt f (filter P xs)"
       
  5187 by (induction xs) auto
       
  5188 
  5175 lemma sorted_wrt_rev:
  5189 lemma sorted_wrt_rev:
  5176   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
  5190   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
  5177 by (induction xs) (auto simp add: sorted_wrt_append)
  5191 by (induction xs) (auto simp add: sorted_wrt_append)
  5178 
  5192 
  5179 lemma sorted_wrt_mono_rel:
  5193 lemma sorted_wrt_mono_rel: