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.
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".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.
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).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.
Currently no special syntax for prefixeq/prefix and suffixeq/suffix is used at all.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.
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 AFPI 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 chrisPS: 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).
sublist.hgbundle
Description: Binary data
sublist-afp.hgbundle
Description: Binary data
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
