No. not yet. - chris On 09/03/2012 01:26 AM, Christian Urban wrote:
Hi Christian, Did this already get into the Distribution and AFP? Christian On Thursday, August 30, 2012 at 16:19:08 (+0900), Christian Sternagel wrote: > 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 > > [email protected] > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > > > xuntyped binary data, sublist.hgbund [Press RETURN to save to a file] > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
