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-...@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
