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

[Blanchette, J.C.]

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