# HG changeset patch
# User nipkow
# Date 1525969063 -7200
# Node ID b105964ae3c4f99f787e34d167ccc8cc4329a42a
# Parent  9339687ca07193deb8b3c8e925dcbb1831a5a1de
more lemmas

diff -r 9339687ca071 -r b105964ae3c4 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 10 01:34:07 2018 +0200
+++ b/src/HOL/List.thy	Thu May 10 18:17:43 2018 +0200
@@ -4947,17 +4947,25 @@
 
 lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
 
+lemma sorted_wrt_true [simp]:
+  "sorted_wrt (\<lambda>_ _. True) xs"
+by (induction xs) simp_all
+
 lemma sorted_wrt_append:
   "sorted_wrt P (xs @ ys) \<longleftrightarrow>
   sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
 by (induction xs) auto
 
+lemma sorted_wrt_map:
+  "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
+by (induction xs) simp_all
+
 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)
 
-lemma sorted_wrt_mono:
-  "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
+lemma sorted_wrt_mono_rel:
+  "(\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; P x y \<rbrakk> \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
 by(induction xs)(auto)
 
 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
@@ -4965,7 +4973,7 @@
 
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
-lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [0..<n]"
+lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
 by(induction n) (auto simp: sorted_wrt_append)
 
 text \<open>Each element is greater or equal to its index:\<close>