> 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