[isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

Tobias Nipkow nipkow at in.tum.de
Wed Aug 16 16:10:41 CEST 2017

I feel that take/drop_chain are too specialised for List, although of course 
this is subjective.

Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to informal 
usage. But if many people cry out for "by" we could change that.


On 16/08/2017 12:10, Christian Sternagel wrote:
> Dear all,
> speaking of "chain", for me the main motivation of introducing "linked
> P" was in order to work well together with the corresponding
> generalizations of "take_while" and "drop_while", which are called
> "take_chain" and "drop_chain" in the AFP entry Efficient-Mergesort.
> E.g., "take_chain (op >) [3,2,1,2] = [3,2,1]"
> So besides very basic lemmas about "linked" (concerning append) there
> are some concerning its interaction with "take_chain" and "drop_chain"
> in Efficient_Sort.thy
> chris
> PS: another alternative name: "sorted_by" (I think the suffix "_by" is
> far more common -- e.g., in Haskekll -- than "_wrt").
> On 08/16/2017 11:53 AM, Blanchette, J.C. wrote:
>> Hi Christian, Tobias,
>>> I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
>>> "linked" from the AFP (Efficient_Mergesort).
>>> https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html
>>> Maybe we could unify the constants/names somehow?
>>> At the moment I somewhat prefer "linked" (or maybe "linked_by") since
>>> sortedness implies that "P" is some kind of order, which it doesn't have
>>> to be.
>> It also reminds me of my "derivation" predicate, which arose when formalizing Bachmair & Ganzinger's chapter in the Handbook of Automated Reasoning:
>> https://bitbucket.org/isafol/isafol/src/f0f585fb6cbd7097567cc1c493fe1b3c1223a8da/Bachmair_Ganzinger/Proving_Process.thy?at=master&fileviewer=file-view-default
>> It's a bit different because of the use of lazy lists (to allow infinite derivations) and the different handling of the empty list.
>> Underlying all of these appears to be the concept of a "chain". That's what we often call things of the form x1 > x2 > ... > xn (finite) or x1 > x2 > ... (infinite), where > is some binary relation. In the context of Bachmair & Ganzinger, or, indeed, for formalzing Definition 7.2.3 from Baader & Nipkow, it makes sense to use a relation > that is not transitive.
>> So maybe "chain" could be a good name for the finite concept?
>> Incidentally, Georges Gonthier believes that for nonempty paths in a graph (or more generally chains), the first element should be stored separately from the other ones. I guess the main benefit is when concatenating two paths, he can simply append. I'm not sure how relevant it is to us, though.
>> Jasmin
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170816/403ecdf9/attachment.bin>

More information about the isabelle-dev mailing list