[isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Tue Dec 3 21:50:26 CET 2013
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131203/1762c9f9/attachment.asc>
More information about the isabelle-dev
mailing list