Re: [isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
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
[isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
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 would also suggest that the predicate version should be done using locales rather than the canonical type class. 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
Re: [isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
