# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1620992599 -3600
# Node ID 60a7884676399cdfa78d031f42cf8d1564b7e774
# Parent  78044b2f001cb674ad4d37d9d2f667f2693cad9d
strict_sorted now an abbreviation

diff -r 78044b2f001c -r 60a788467639 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 12 17:05:29 2021 +0000
+++ b/src/HOL/List.thy	Fri May 14 12:43:19 2021 +0100
@@ -374,9 +374,8 @@
 "sorted [] = True" |
 "sorted (x # ys) = ((\<forall>y \<in> set ys. x \<le> y) \<and> sorted ys)"
 
-fun strict_sorted :: "'a list \<Rightarrow> bool" where
-"strict_sorted [] = True" |
-"strict_sorted (x # ys) = ((\<forall>y \<in> List.set ys. x < y) \<and> strict_sorted ys)"
+abbreviation strict_sorted :: "'a list \<Rightarrow> bool" where
+  "strict_sorted \<equiv> sorted_wrt (<)" 
 
 lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
 proof (rule ext)
@@ -384,12 +383,6 @@
     by(induction xs rule: sorted.induct) auto
 qed
 
-lemma strict_sorted_sorted_wrt: "strict_sorted = sorted_wrt (<)"
-proof (rule ext)
-  fix xs show "strict_sorted xs = sorted_wrt (<) xs"
-    by(induction xs rule: strict_sorted.induct) auto
-qed
-
 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   "insort_key f x [] = [x]" |
   "insort_key f x (y#ys) =
@@ -6227,12 +6220,7 @@
 
 lemma sorted_list_of_set_lessThan_Suc [simp]: 
   "sorted_list_of_set {..<Suc k} = sorted_list_of_set {..<k} @ [k]"
-proof -
-  have "sorted_wrt (<) (sorted_list_of_set {..<k} @ [k])"
-    unfolding sorted_wrt_append  by (auto simp flip: strict_sorted_sorted_wrt)
-  then show ?thesis
-    by (simp add: lessThan_atLeast0)
-qed
+  using le0 lessThan_atLeast0 sorted_list_of_set_range upt_Suc_append by presburger
 
 lemma sorted_list_of_set_atMost_Suc [simp]:
   "sorted_list_of_set {..Suc k} = sorted_list_of_set {..k} @ [Suc k]"