Re: [isabelle] Relating class operations and corresponding locale.
- To: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Relating class operations and corresponding locale.
- From: Andreas Lochbihler <mail at andreas-lochbihler.de>
- Date: Thu, 28 Jun 2018 20:23:27 +0200
- In-reply-to: <20180628112949.GC15468@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>
- References: <20180628105948.GB15468@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <20180628112949.GC15468@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0
The change in the sort constraint goes back to a small renovation I did a few years ago.
Originally, all the rbt_* functions were defined in the locales for the classes order and
linorder. I then moved them to the syntactic class ord such that the code generator can
generate code for the locale-based version without further ado. For backwards
compatibility, I re-installed the former sort constraints.
The problem of relaxing the sort constraints is that the rbt_* operations do not really
make sense with more general types, because they use if conditions of the form
if x < y then X else if y < x then Y else Z
If they were changed to
if x <= y then if y <= x then Z else X else Y
then they would also make sense, e.g., if the order is not antisymmetric. Changing this
would mean to change the proofs, too. Moreover, since red-black trees are mainly used for
code generation, it would be nice to change them to use a comparator, which is independent
of the logical order. René Thiemann has done some work in that direction in the AFP, but
this has not yet been propagated into the Isabelle standard library.
So, in short: No, it does not have to be this way. It is a historic relic and nobody was
sufficiently annoyed by it to put up the effort and change it.
On 28/06/18 13:29, Bertram Felgenhauer via Cl-isabelle-users wrote:
"ord.rbt_sorted (op <) = rbt_sorted"
On a related note, I was confused that rbt_sorted has a linorder
constraint while being defined in an ord context. This is a
consequence of the setup around
Is that really necessary?
This archive was generated by a fusion of
Pipermail (Mailman edition) and