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.
Tobias 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 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
