[isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]

[Andreas Lochbihler]

Hi Florian,

 > Just a remark on
 > http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
 > lexicographic orderings in List.thy is now numerous enough but still
 > self-contained to justify a separate theory Lexorder.thy.

I agree that a separate theory would be nice. But before doing so, we should also try to 
consolidate what's there already. The current state in List.thy is as follows (8c0a27b9c1bd):

1. lexord :: ('a * 'a) set => ('a list * 'a list) set
    a set version of the irreflexive lexicographic order, the parameter corresponds to <
    equality of elements is determined by "op =".

2. lexordp ::('a => 'a => bool) => 'a list => 'a list => bool
    the predicate version of lexord, apparently used only for code generation

3. ord_class.lexordp :: 'a list => 'a list => bool
    a predicate version of the irreflexive lexicographic order
    equality of elements x and y is determined by "~ (x < y) & ~ (y < x)"

4. ord_class.lexordp_eq :: 'a list => 'a list => bool
    a predicate version of the reflexive lexicographic order,
    equality of elements x and y is determined by "~ (x < y) & ~ (y < x)"

5. lexn defines the length-lexicographic order where only lists of the same
    length are comparable (listed here only for completeness).

3 and 4 also yield parametrized versions ord.lexordp and ord.lexordp_eq where the 
parameter corresponds to op <.

While definitions 1 to 4 yield the same when the order on the elements is linear, they 
differ in the details when they are not. I think that none of 1 to 4 is optimal, because:

(i) 1 and 2 explicitly use HOL equality which need not be related to the ordering that is 
passed in (e.g. in a quasi-order) -- they also make the functions dependent on the 
equality type class for code generation, which is a problem for AFP/Containers.

(ii) For non-linear quasi-orders, 3 and 4 do not work well, because they consider all 
unrelated elements as equal, even if they belong to different equivalence classes of the 
quasi-order.

If I could start from scratch, I would define a predicate version like 4, but with 
equality of x and y determined by "x <= y & y <= x". Then, however, the order parameter 
would change from irreflexive to reflexive. I do not know how much breaks if we attempt 
such a change.

> I would also
> suggest that the predicate version should be done using locales rather
> than the canonical type class.

Using the canoncial type class has the advantage that I can write

   lexordp_eq [1,2] [1,3]

and obtain the order on the elements implicitly. With a locale, it is more complicated to 
achieve the same effect.

Andreas