Dear all,
recently I reinvented (a tiny) wheel. In my well-quasi-order AFP entry I
use suffixes of lists (mainly to do induction over suffixes, but
anyway). Afterwards (by chance) I found Library/List_Prefix which
defines the same thing under the name "postfix".
Moreover I used another relation on lists: embedding.
How about replacing List_Prefix by a theory Sublist and populating it
with facts about prefixes, suffixes (or postfixes, whichever is
preferred) .oO(I just noticed that my spell-checker knows "suffix" but
it doesn't know "postfix" ;)) and sublists (i.e., embedded lists). The
latter are used in at least two different AFP entries.
Two other issues with List_Prefix:
1) It defines the syntax >>= for suffixes (which I would prefer for
monadic bind). Moreover, prefixes do not use <<= and hence it is not
symmetric anyway.
2) It gives the prefix relation as an instance of "order". But there are
many different orders on lists (e.g., prefix, suffix, embedding, length,
...). Could this be changed to merely have a locale interpretation.
Concerning syntax: could this be localized to List_Prefix (aehh... I
mean Sublist ;)) by introducing \<le> and \<ge> in a context block? Then
we have the convenient syntax inside the whole theory. But afterwards
\<le> and \<ge> is still available for users and they can define
whatever syntax they like for the relations on lists.
cheers
chris
PS: of course this can wait until after the release!
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
