[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

Sorry! I forgot to commit my last change (and sorry for the many typos 
in my last email). - chris

On 08/30/2012 03:36 PM, Christian Sternagel wrote:
> Dear developers,
>
> since consolidations where encouraged, please find attached my latest
> attempt (the consolidation lies in the fact that Sublist_Order (from the
> Library), Well_Quasi_Orders (from the AFP), and Myhill_Nerode (from the
> AFP) are now all based on Sublist instead of cooking there separate but
> equivalent list relations):
>
> I renamed List_Prefix into Sublist, which no contains definitions and
> facts about prefixes, suffixes, embedding, and sublists (the special
> case of embedding where we may just drop elements).
>
>
> On 04/26/2012 12:45 PM, Christian Sternagel wrote:
>> Library/Sublist_Order contains another copy (less_eq_list) of (a
>> restricted variant of) embedding on lists.
> Thus is no based on the sublist relation "sub" from Sublist.
>
>>> 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.
> This is exactly what I did. The current naming scheme is
>
> prefixeq/prefix
> suffixeq/suffix
> emb
> sub
>
> in contrast to the previous
>
> prefix/strict_prefix
> postfix
>
> However, I have no strong opinion about those names.
>
>>> 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.
> I dropped the syntax. By the way, also the argument order changed, what
> was "xs >>= ys" (or "postfix xs ys") is now "suffixeq ys xs",
> facilitating the reading that "ys is a suffix of xs".
>
>>> 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.
> Sublist only contains the locale interpretation prefix_order for the
> order locale. I also added theory Prefix_Order merely containing an
> order class instance (+ some accompanying lemmas that are apparently
> needed by the tactics of Codatatype).
>
>>> 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.
> Currently no special syntax for prefixeq/prefix and suffixeq/suffix is
> used at all.
>
> I tested the attached hg bundles against the main repo with
>
>    isabelle build -a -o browser_info -o document=pdf -o document_graph
>
> and against the AFP with
>
>    isabelle build -d . -g AFP
>
> I could however not test JinjaThreads, since even with poly 5.5.0, 4
> cores and 8GB RAM my computer flat-lined a few minutes after 'isabelle
> build -d . -b JinjaThreads' with ISABELLE_BUILD_OPTIONS="threads=4
> parallel_proofs=2". It would be much appreciated if somebody with access
> to a more powerful computer could adapt JinjaThreads.
>
> cheers
>
> chris
>
> PS: one FIXME is to be found in Sublist. I added a (in my opinion) very
> convenient definition transp_on (to characterize predicates that are
> transitive on a given set). More such definitions can be found in
> Restricted_Predicates from my AFP entry Well_Quasi_Orders. I would say,
> the correct place to put them is as part of the Isabelle distribution...
> maybe a theory Predicate (alas, such a theory already exists but is
> concerned with completely different things, as far as I could see).
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: sublist.hgbundle
Type: application/octet-stream
Size: 14894 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120830/f5455fb0/attachment-0002.obj>