# 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 \ bool" where "sorted \ sorted_wrt (<)" +lemmas sorted_wrt_Cons = sorted_wrt.simps(2) + text \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.\ -lemma sorted_wrt1 [simp]: "sorted_wrt P [x]" -by simp - -lemma sorted2 [simp]: "sorted (x # y # zs) = (x < y \ 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) \ 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 \Sorting\ - subsubsection \@{const sorted_wrt}\ -lemma sorted_wrt_ConsI: - "\ \y. y \ set xs \ P x y; sorted_wrt P xs \ \ sorted_wrt P (x # xs)" -by (induction xs) simp_all +text \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 \sorted_wrt2_simps\ should be added instead.\ + +lemma sorted_wrt1: "sorted_wrt P [x] = True" +by(simp) + +lemma sorted_wrt2: "transp P \ sorted_wrt P (x # y # zs) = (P x y \ 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) \