merged
authornipkow
Tue May 15 06:23:12 2018 +0200 (12 months ago)
changeset 6818748262e3a2bde
parent 68185 c80b0a35eb54
parent 68186 56fcf7e980e3
child 68188 2af1f142f855
merged
     1.1 --- a/src/HOL/List.thy	Mon May 14 22:23:25 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Tue May 15 06:23:12 2018 +0200
     1.3 @@ -4932,7 +4932,7 @@
     1.4  
     1.5  subsubsection \<open>@{const sorted_wrt}\<close>
     1.6  
     1.7 -text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is to aggressive
     1.8 +text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is too aggressive
     1.9  because it relates each list element to \emph{all} its successors. Then this equation
    1.10  should be removed and \<open>sorted_wrt2_simps\<close> should be added instead.\<close>
    1.11  
    1.12 @@ -5013,7 +5013,7 @@
    1.13  context linorder
    1.14  begin
    1.15  
    1.16 -text \<open>Sometimes the second equation in the definition of @{const sorted} is to aggressive
    1.17 +text \<open>Sometimes the second equation in the definition of @{const sorted} is too aggressive
    1.18  because it relates each list element to \emph{all} its successors. Then this equation
    1.19  should be removed and \<open>sorted2_simps\<close> should be added instead.
    1.20  Executable code is one such use case.\<close>
    1.21 @@ -5043,13 +5043,17 @@
    1.22    "sorted xs \<Longrightarrow> sorted (tl xs)"
    1.23  by (cases xs) (simp_all)
    1.24  
    1.25 -lemma sorted_iff_nth_mono:
    1.26 +lemma sorted_iff_nth_mono_less:
    1.27    "sorted xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
    1.28  by (simp add: sorted_sorted_wrt sorted_wrt_iff_nth_less)
    1.29  
    1.30 +lemma sorted_iff_nth_mono:
    1.31 +  "sorted xs = (\<forall>i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
    1.32 +by (auto simp: sorted_iff_nth_mono_less nat_less_le)
    1.33 +
    1.34  lemma sorted_nth_mono:
    1.35    "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
    1.36 -by (auto simp: sorted_iff_nth_mono nat_less_le)
    1.37 +by (auto simp: sorted_iff_nth_mono)
    1.38  
    1.39  lemma sorted_rev_nth_mono:
    1.40    "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"