[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

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).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sublist.hgbundle
Type: application/octet-stream
Size: 14631 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120830/c67704d8/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sublist-afp.hgbundle
Type: application/octet-stream
Size: 10371 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120830/c67704d8/attachment-0003.obj>