[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

Library/Sublist_Order contains another copy (less_eq_list) of (a 
restricted variant of) embedding on lists.

On 04/26/2012 12:33 PM, Christian Sternagel wrote:
> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev