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

[Florian Haftmann]

> 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>