I needed linorder on String.literal, hence I came up with the theory as
in the attachment. It explicitly uses lexord, and only later lifts it to
op <, to explicitly show what the order is and not rely on 'magic' from
the (lin)ord(er) class.
Your detour via lexord does not buy you anything, because your theory
depends on List_lexord and therefore imposes the lexicographic order on
lists. Unfortunately, we have two competing order instantiation for
lists in Isabelle (lexicographic order and prefix order). I think that
it is sensible to pick lexicographic orders for String.literal, but this
choice should restrict the choice for list (and string as the type
synonym for char list). In the current version, your theory forces the
lexicographic order on list, too.
It also defines op < and op <= using the target language operators (save
Scala, for I don't know it) for performance reasons.
For Scala and the symbolic evaluation mechanisms (simp, nbe), your
detour via lexord cause non-termination or no code at all. Therefore,
you should definitely have appropriate code equations for these cases.
Would this be useful for inclusion in HOL/Library?
In general yes, but I suggest that the above issues are addressed first.
I also noted, that there is something similiar (minus code-printing) in
AFP/Containers, but I can't tell if this is the same.
Yes, AFP/Containers/Lexicographic_Order is basically the same (if you
ignore the stuff on list fusion). It differs from your theory in the
1. It avoids the dependency on List_lexord and therefore does not
constrain the order for list.
2. It has code equations that work for all target languages and symbolic
3. There are no code_printing translations.
Hence, it might be sensible to combine your code_printing translations
with my definitions and add this to HOL/Library. I don't know whether it
is sensible to have a separate theory, I suggest that all this could go
into Code_Char (just like implode is also already part of Code_Char).