# HG changeset patch # User paulson # 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) = ((\y \ set ys. x \ y) \ sorted ys)" -fun strict_sorted :: "'a list \ bool" where -"strict_sorted [] = True" | -"strict_sorted (x # ys) = ((\y \ List.set ys. x < y) \ strict_sorted ys)" +abbreviation strict_sorted :: "'a list \ bool" where + "strict_sorted \ sorted_wrt (<)" lemma sorted_sorted_wrt: "sorted = sorted_wrt (\)" 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 \ 'a) \ 'b \ 'b list \ '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 {..