[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

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
>   > > 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
>   > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>