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 pr
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) be
The name "sorted_wrt" came from Manuel and I would like to keep it. For
transtive predicates it is the same as sorted (I will add that lemma to List).
I looked into your theory but did not find any further generic lemmas about
"linked". Let me know if I missed any that should go into List.
To
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?
>
>
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 (
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:
On 16/08/17 16:10, Tobias Nipkow wrote:
>
> 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.
In Isabelle/ML we used to have "sort_wrt" for some decades, but I have
changed that recently into into "sort_b
However, sort_by takes a function mapping the elements into a linear order, which is less general than allowing arbitrary (preorder?) relations.Peter Original Message Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thyFrom: Makar
Indeed, and that is consistent with informal language, eg "sorted by size". It
looks like "wrt" is really better for relations.
Tobias
On 16/08/2017 17:04, Peter Lammich wrote:
However, sort_by takes a function mapping the elements into a linear order,
which is less general than allowing arbit
