[isabelle-dev] Library/List_Prefix

[Christian Urban]

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

--