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.


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


Attachment: 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

Reply via email to