author nipkow Tue, 15 May 2018 06:23:12 +0200 changeset 68187 48262e3a2bde parent 68185 c80b0a35eb54 (current diff) parent 68186 56fcf7e980e3 (diff) child 68188 2af1f142f855
merged
--- a/src/HOL/List.thy	Mon May 14 22:23:25 2018 +0200
+++ b/src/HOL/List.thy	Tue May 15 06:23:12 2018 +0200
@@ -4932,7 +4932,7 @@

subsubsection \<open>@{const sorted_wrt}\<close>

-text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is to aggressive
+text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is too aggressive
because it relates each list element to \emph{all} its successors. Then this equation

@@ -5013,7 +5013,7 @@
context linorder
begin

-text \<open>Sometimes the second equation in the definition of @{const sorted} is to aggressive
+text \<open>Sometimes the second equation in the definition of @{const sorted} is too aggressive
because it relates each list element to \emph{all} its successors. Then this equation
Executable code is one such use case.\<close>
@@ -5043,13 +5043,17 @@
"sorted xs \<Longrightarrow> sorted (tl xs)"
by (cases xs) (simp_all)

-lemma sorted_iff_nth_mono:
+lemma sorted_iff_nth_mono_less:
"sorted xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"

+lemma sorted_iff_nth_mono:
+  "sorted xs = (\<forall>i j. i \<le> j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
+by (auto simp: sorted_iff_nth_mono_less nat_less_le)
+
lemma sorted_nth_mono:
"sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
-by (auto simp: sorted_iff_nth_mono nat_less_le)
+by (auto simp: sorted_iff_nth_mono)

lemma sorted_rev_nth_mono:
"sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"