[isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
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
> 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).
>>> 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:
>> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev