> 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).
[…]
> 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.
Thanks for the observations. This needs to be considered, but seems
worth the effort. x <= y & y <= x is indeed the best characterization
for equality since it does not rule out quasi-orders.
>> 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.
My statement was misleading: in a type class you always have the locale
version for free. I was just thinking whether that development should
take place in the canonical type class or in a separate extension. This
is maybe too much detail to be considered at the moment.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
