[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

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!