# HG changeset patch
# User nipkow
# Date 1609191601 -3600
# Node ID 9283e9d4506002d28e721513960e51e1d1be3d21
# Parent  8644c1efbda2c03c213c24a2db5fd2c5075e5530
added lemmas

diff -r 8644c1efbda2 -r 9283e9d45060 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 28 17:52:26 2020 +0100
+++ b/src/HOL/List.thy	Mon Dec 28 22:40:01 2020 +0100
@@ -5436,6 +5436,20 @@
   "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
 by(auto simp: sorted_wrt_iff_nth_less)
 
+lemma sorted_wrt_iff_nth_Suc_transp: assumes "transp P"
+  shows "sorted_wrt P xs \<longleftrightarrow> (\<forall>i.  Suc i < length xs \<longrightarrow> P (xs!i) (xs!(Suc i)))" (is "?L = ?R")
+proof
+  assume ?L
+  thus ?R
+    by (simp add: sorted_wrt_iff_nth_less) 
+next
+  assume ?R
+  have "i < j \<Longrightarrow> j < length xs \<Longrightarrow> P (xs ! i) (xs ! j)" for i j
+    by(induct i j rule: less_Suc_induct)(simp add: \<open>?R\<close>, meson assms transpE transp_less)
+  thus ?L
+    by (simp add: sorted_wrt_iff_nth_less)
+qed
+
 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
 by(induction n) (auto simp: sorted_wrt_append)
 
@@ -5507,12 +5521,44 @@
   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
 by (auto simp: sorted_iff_nth_mono)
 
+lemma sorted_iff_nth_Suc: 
+  "sorted xs \<longleftrightarrow> (\<forall>i.  Suc i < length xs \<longrightarrow> xs!i \<le> xs!(Suc i))"
+by(simp add: sorted_sorted_wrt sorted_wrt_iff_nth_Suc_transp)
+
 lemma sorted_rev_nth_mono:
   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
 by auto
 
+lemma sorted_rev_iff_nth_mono:
+  "sorted (rev xs) \<longleftrightarrow> (\<forall> i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs!j \<le> xs!i)" (is "?L = ?R")
+proof
+  assume ?L thus ?R
+    by (blast intro: sorted_rev_nth_mono)
+next
+  assume ?R
+  have "rev xs ! k \<le> rev xs ! l" if asms: "k \<le> l" "l < length(rev xs)" for k l
+  proof -
+    have "k < length xs"  "l < length xs"
+      "length xs - Suc l \<le> length xs - Suc k" "length xs - Suc k < length xs"
+      using asms by auto
+    thus "rev xs ! k \<le> rev xs ! l"
+      using \<open>?R\<close> \<open>k \<le> l\<close> unfolding rev_nth[OF \<open>k < length xs\<close>] rev_nth[OF \<open>l < length xs\<close>] by blast
+  qed
+  thus ?L by (simp add: sorted_iff_nth_mono)
+qed
+
+lemma sorted_rev_iff_nth_Suc: 
+  "sorted (rev xs) \<longleftrightarrow> (\<forall>i.  Suc i < length xs \<longrightarrow> xs!(Suc i) \<le> xs!i)"
+proof-
+  interpret dual: linorder "(\<lambda>x y. y \<le> x)" "(\<lambda>x y. y < x)"
+    using dual_linorder .
+  show ?thesis
+    using dual_linorder dual.sorted_iff_nth_Suc dual.sorted_iff_nth_mono 
+    unfolding sorted_rev_iff_nth_mono by simp
+qed
+
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
 by (induct xs) (auto)