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

[Tobias Nipkow]

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.

Tobias

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>