Hi Christian, > 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.
Consoldiations to the library are always welcome!
Best,
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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
