--- a/src/HOL/List.thy Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/List.thy Sat Aug 08 14:00:56 1998 +0200
@@ -145,6 +145,22 @@
replicate_0 "replicate 0 x = []"
replicate_Suc "replicate (Suc n) x = x # replicate n x"
+(** Lexcicographic orderings on lists **)
+
+consts
+ lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
+primrec
+"lexn r 0 = {}"
+"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
+ {(xs,ys). length xs = Suc n & length ys = Suc n}"
+
+constdefs
+ lex :: "('a * 'a)set => ('a list * 'a list)set"
+"lex r == UN n. lexn r n"
+
+ lexico :: "('a * 'a)set => ('a list * 'a list)set"
+"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
+
end
ML