# HG changeset patch
# User nipkow
# Date 1526140392 -7200
# Node ID 7da3af31ca4db708185e0fa2800d535c945c08dc
# Parent  8b50f29a1992566b9503b2740f40e3d6a05edb9c
added lemmas

diff -r 8b50f29a1992 -r 7da3af31ca4d src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 12 11:24:11 2018 +0200
+++ b/src/HOL/List.thy	Sat May 12 17:53:12 2018 +0200
@@ -4971,6 +4971,17 @@
 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
 by(auto simp: le_Suc_eq length_Suc_conv)
 
+lemma sorted_wrt_iff_nth_Suc:
+  "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
+apply(induction xs)
+ apply simp
+apply(force simp: in_set_conv_nth nth_Cons split: nat.split)
+done
+
+lemma sorted_wrt_nth_less:
+  "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
+by(auto simp: sorted_wrt_iff_nth_Suc)
+
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"