src/HOL/List.thy
 changeset 71656 21c0b3a9d2f8 parent 71647 d8fb621fea02 child 71781 4b1021677f15
equal 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:`