Re: [isabelle] Code_String: linorder in String.literal
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.
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.
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.
It also defines op < and op <= using the target language operators (save
Scala, for I don't know it) for performance reasons.
Would this be useful for inclusion in HOL/Library?
In general yes, but I suggest that the above issues are addressed first.
Yes, AFP/Containers/Lexicographic_Order is basically the same (if you ignore the stuff on
list fusion). It differs from your theory in the following:
I also noted, that there is something similiar (minus code-printing) in
AFP/Containers, but I can't tell if this is the same.
1. It avoids the dependency on List_lexord and therefore does not constrain the order for
2. It has code equations that work for all target languages and symbolic evaluation.
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and