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

[Christian Sternagel]

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
>