# HG changeset patch
# User nipkow
# Date 1525844934 -7200
# Node ID 2e5b737810a60a9f504f9c7f4168b3433d71a9c4
# Parent  14e0c89040616ad0f2a209b6ea882f8852f86496
announce sorted changes

diff -r 14e0c8904061 -r 2e5b737810a6 NEWS
--- a/NEWS	Tue May 08 21:03:06 2018 +0100
+++ b/NEWS	Wed May 09 07:48:54 2018 +0200
@@ -296,7 +296,6 @@
   - span_eq ~> span_eq_iff
 INCOMPATIBILITY.
 
-
 * HOL-Algebra: renamed (^) to [^]
 
 * Session HOL-Analysis: Moebius functions, the Riemann mapping
@@ -306,6 +305,9 @@
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
 
+* Theory List: functions "sorted_wrt" and "sorted" now compare every
+  element in a list to all following elements, not just the next one.
+
 * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
 
 * Predicate coprime is now a real definition, not a mere
diff -r 14e0c8904061 -r 2e5b737810a6 src/HOL/Data_Structures/Sorted_Less.thy
--- a/src/HOL/Data_Structures/Sorted_Less.thy	Tue May 08 21:03:06 2018 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Wed May 09 07:48:54 2018 +0200
@@ -13,18 +13,14 @@
 abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
 "sorted \<equiv> sorted_wrt (<)"
 
+lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
+
 text \<open>The definition of @{const sorted_wrt} relates each element to all the elements after it.
 This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close>
 
-lemma sorted_wrt1 [simp]: "sorted_wrt P [x]"
-by simp
-
-lemma sorted2 [simp]: "sorted (x # y # zs) = (x < y \<and> sorted (y # zs))"
-by(induction zs) auto
-
-lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
-
-declare sorted_wrt.simps(2)[simp del]
+declare
+  sorted_wrt.simps(2)[simp del]
+  sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
 
 lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
 by(simp add: sorted_wrt_Cons)
diff -r 14e0c8904061 -r 2e5b737810a6 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 08 21:03:06 2018 +0100
+++ b/src/HOL/List.thy	Wed May 09 07:48:54 2018 +0200
@@ -4930,12 +4930,22 @@
 
 subsection \<open>Sorting\<close>
 
-
 subsubsection \<open>@{const sorted_wrt}\<close>
 
-lemma sorted_wrt_ConsI:
-  "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
-by (induction xs) simp_all
+text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is to aggressive
+because it relates each list element to \emph{all} its successors. Then this equation
+should be removed and \<open>sorted_wrt2_simps\<close> should be added instead.\<close>
+
+lemma sorted_wrt1: "sorted_wrt P [x] = True"
+by(simp)
+
+lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
+apply(induction zs arbitrary: x y)
+apply(auto dest: transpD)
+apply (meson transpD)
+done
+
+lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
 
 lemma sorted_wrt_append:
   "sorted_wrt P (xs @ ys) \<longleftrightarrow>