[isabelle-dev] Library/List_Prefix

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120428/9a9866c1/attachment.sig>