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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
