added lemmas
authornipkow
Sat May 12 17:53:12 2018 +0200 (12 months ago)
changeset 681567da3af31ca4d
parent 68155 8b50f29a1992
child 68157 057d5b4ce47e
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sat May 12 11:24:11 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Sat May 12 17:53:12 2018 +0200
     1.3 @@ -4971,6 +4971,17 @@
     1.4  lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
     1.5  by(auto simp: le_Suc_eq length_Suc_conv)
     1.6  
     1.7 +lemma sorted_wrt_iff_nth_Suc:
     1.8 +  "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
     1.9 +apply(induction xs)
    1.10 + apply simp
    1.11 +apply(force simp: in_set_conv_nth nth_Cons split: nat.split)
    1.12 +done
    1.13 +
    1.14 +lemma sorted_wrt_nth_less:
    1.15 +  "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
    1.16 +by(auto simp: sorted_wrt_iff_nth_Suc)
    1.17 +
    1.18  text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
    1.19  
    1.20  lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"