# 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 @@ "\ sorted_wrt P xs; i < j; j < length xs \ \ 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 \ (\i. Suc i < length xs \ 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 \ j < length xs \ P (xs ! i) (xs ! j)" for i j + by(induct i j rule: less_Suc_induct)(simp add: \?R\, meson assms transpE transp_less) + thus ?L + by (simp add: sorted_wrt_iff_nth_less) +qed + lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m.. i \ j \ j < length xs \ xs!i \ xs!j" by (auto simp: sorted_iff_nth_mono) +lemma sorted_iff_nth_Suc: + "sorted xs \ (\i. Suc i < length xs \ xs!i \ xs!(Suc i))" +by(simp add: sorted_sorted_wrt sorted_wrt_iff_nth_Suc_transp) + lemma sorted_rev_nth_mono: "sorted (rev xs) \ i \ j \ j < length xs \ xs!j \ 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) \ (\ i j. i \ j \ j < length xs \ xs!j \ xs!i)" (is "?L = ?R") +proof + assume ?L thus ?R + by (blast intro: sorted_rev_nth_mono) +next + assume ?R + have "rev xs ! k \ rev xs ! l" if asms: "k \ l" "l < length(rev xs)" for k l + proof - + have "k < length xs" "l < length xs" + "length xs - Suc l \ length xs - Suc k" "length xs - Suc k < length xs" + using asms by auto + thus "rev xs ! k \ rev xs ! l" + using \?R\ \k \ l\ unfolding rev_nth[OF \k < length xs\] rev_nth[OF \l < length xs\] by blast + qed + thus ?L by (simp add: sorted_iff_nth_mono) +qed + +lemma sorted_rev_iff_nth_Suc: + "sorted (rev xs) \ (\i. Suc i < length xs \ xs!(Suc i) \ xs!i)" +proof- + interpret dual: linorder "(\x y. y \ x)" "(\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) \ sorted (map f (remove1 x xs))" by (induct xs) (auto)