--- 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
--- 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)
--- 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>