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