I agree that this predicate probably has more general uses than
sortedness. Other possible names could be "successively" or "consecutively".
One might, however, still consider keeping "sorted_wrt" around (perhaps
as an (input) abbreviation, perhaps with a more restrictive type class
constraint) because I think it communicates the intent better when we
really do mean sortedness.
On 2017-08-16 10:44, Christian Sternagel wrote:
> Dear 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.
> kind regards,
> -------- Forwarded Message --------
> Subject: added sorted_wrt to List; added
> Date: Tue, 15 Aug 2017 19:47:08 +0200
> From: nipkow <>
> added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy added
> sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
> isabelle-dev mailing list
isabelle-dev mailing list