announce sorted changes
authornipkow
Wed May 09 07:48:54 2018 +0200 (20 months ago ago)
changeset 681252e5b737810a6
parent 68124 14e0c8904061
child 68126 137d5d0112bb
child 68127 5da8b97d9183
child 68139 cba8eaa2174f
announce sorted changes
NEWS
src/HOL/Data_Structures/Sorted_Less.thy
src/HOL/List.thy
     1.1 --- a/NEWS	Tue May 08 21:03:06 2018 +0100
     1.2 +++ b/NEWS	Wed May 09 07:48:54 2018 +0200
     1.3 @@ -296,7 +296,6 @@
     1.4    - span_eq ~> span_eq_iff
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -
     1.8  * HOL-Algebra: renamed (^) to [^]
     1.9  
    1.10  * Session HOL-Analysis: Moebius functions, the Riemann mapping
    1.11 @@ -306,6 +305,9 @@
    1.12  * Class linordered_semiring_1 covers zero_less_one also, ruling out
    1.13  pathologic instances. Minor INCOMPATIBILITY.
    1.14  
    1.15 +* Theory List: functions "sorted_wrt" and "sorted" now compare every
    1.16 +  element in a list to all following elements, not just the next one.
    1.17 +
    1.18  * Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
    1.19  
    1.20  * Predicate coprime is now a real definition, not a mere
     2.1 --- a/src/HOL/Data_Structures/Sorted_Less.thy	Tue May 08 21:03:06 2018 +0100
     2.2 +++ b/src/HOL/Data_Structures/Sorted_Less.thy	Wed May 09 07:48:54 2018 +0200
     2.3 @@ -13,18 +13,14 @@
     2.4  abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
     2.5  "sorted \<equiv> sorted_wrt (<)"
     2.6  
     2.7 +lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
     2.8 +
     2.9  text \<open>The definition of @{const sorted_wrt} relates each element to all the elements after it.
    2.10  This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close>
    2.11  
    2.12 -lemma sorted_wrt1 [simp]: "sorted_wrt P [x]"
    2.13 -by simp
    2.14 -
    2.15 -lemma sorted2 [simp]: "sorted (x # y # zs) = (x < y \<and> sorted (y # zs))"
    2.16 -by(induction zs) auto
    2.17 -
    2.18 -lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
    2.19 -
    2.20 -declare sorted_wrt.simps(2)[simp del]
    2.21 +declare
    2.22 +  sorted_wrt.simps(2)[simp del]
    2.23 +  sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
    2.24  
    2.25  lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
    2.26  by(simp add: sorted_wrt_Cons)
     3.1 --- a/src/HOL/List.thy	Tue May 08 21:03:06 2018 +0100
     3.2 +++ b/src/HOL/List.thy	Wed May 09 07:48:54 2018 +0200
     3.3 @@ -4930,12 +4930,22 @@
     3.4  
     3.5  subsection \<open>Sorting\<close>
     3.6  
     3.7 -
     3.8  subsubsection \<open>@{const sorted_wrt}\<close>
     3.9  
    3.10 -lemma sorted_wrt_ConsI:
    3.11 -  "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
    3.12 -by (induction xs) simp_all
    3.13 +text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is to aggressive
    3.14 +because it relates each list element to \emph{all} its successors. Then this equation
    3.15 +should be removed and \<open>sorted_wrt2_simps\<close> should be added instead.\<close>
    3.16 +
    3.17 +lemma sorted_wrt1: "sorted_wrt P [x] = True"
    3.18 +by(simp)
    3.19 +
    3.20 +lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
    3.21 +apply(induction zs arbitrary: x y)
    3.22 +apply(auto dest: transpD)
    3.23 +apply (meson transpD)
    3.24 +done
    3.25 +
    3.26 +lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
    3.27  
    3.28  lemma sorted_wrt_append:
    3.29    "sorted_wrt P (xs @ ys) \<longleftrightarrow>