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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev