c-sterna at jaist.ac.jp
Thu Aug 30 09:19:08 CEST 2012
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
> in contrast to the previous
> 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.
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 14894 bytes
Desc: not available
More information about the isabelle-dev