christian.urban at kcl.ac.uk
Sun Sep 2 18:26:59 CEST 2012
Did this already get into the Distribution and AFP?
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
> > isabelle-dev at in.tum.de
> > 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
> isabelle-dev at in.tum.de
More information about the isabelle-dev