# 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 \ 1 \ sorted_wrt P xs" by(auto simp: le_Suc_eq length_Suc_conv) +lemma sorted_wrt_iff_nth_Suc: + "sorted_wrt P xs = (\i j. i < j \ j < length xs \ 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: + "\ sorted_wrt P xs; i < j; j < length xs \ \ P (xs ! i) (xs ! j)" +by(auto simp: sorted_wrt_iff_nth_Suc) + text \Strictly Ascending Sequences of Natural Numbers\ lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..