[isabelle-dev] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

[Manuel Eberl]

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.

Manuel


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).
> 
> 
> 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.
> 
> kind regards,
> 
> chris
> 
> 
> -------- Forwarded Message --------
> Subject: 	added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
> 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 at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>