# HG changeset patch
# User wenzelm
# Date 1682278260 -7200
# Node ID 430e6c477ba4986e9943625218c8dba52b813af6
# Parent  b83a561086d3d42fbd8ffa3e278eb357573dcdac
more operations for lexicographic ordering;

diff -r b83a561086d3 -r 430e6c477ba4 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Sun Apr 23 20:15:53 2023 +0200
+++ b/src/Pure/General/set.ML	Sun Apr 23 21:31:00 2023 +0200
@@ -24,6 +24,7 @@
   val member: T -> elem -> bool
   val subset: T * T -> bool
   val eq_set: T * T -> bool
+  val ord: T ord
   val insert: elem -> T -> T
   val make: elem list -> T
   val merge: T * T -> T
@@ -278,9 +279,24 @@
 
 fun subset (set1, set2) = forall (member set2) set1;
 
+
+(* equality and order *)
+
 fun eq_set (set1, set2) =
   pointer_eq (set1, set2) orelse size set1 = size set2 andalso subset (set1, set2);
 
+val ord =
+  pointer_eq_ord (fn (set1, set2) =>
+    (case int_ord (size set1, size set2) of
+      EQUAL =>
+        (case get_first (fn a => if member set2 a then NONE else SOME a) set1 of
+          NONE => EQUAL
+        | SOME a =>
+            (case get_first (fn b => if member set1 b then NONE else SOME b) set2 of
+              NONE => EQUAL
+            | SOME b => Key.ord (a, b)))
+    | order => order));
+
 
 (* insert *)
 
diff -r b83a561086d3 -r 430e6c477ba4 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Apr 23 20:15:53 2023 +0200
+++ b/src/Pure/library.ML	Sun Apr 23 21:31:00 2023 +0200
@@ -210,6 +210,8 @@
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val length_ord: 'a list * 'b list -> order
   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
+  val vector_ord: 'a ord -> 'a vector ord
+  val array_ord: 'a ord -> 'a array ord
   val sort: 'a ord -> 'a list -> 'a list
   val sort_distinct: 'a ord -> 'a list -> 'a list
   val sort_strings: string list -> string list
@@ -957,6 +959,12 @@
 fun length_ord (xs, ys) = int_ord (length xs, length ys);
 fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
 
+fun vector_ord ord =
+  pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord);
+
+fun array_ord ord =
+  pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord);
+
 
 (* sorting *)