Re: [isabelle] Relating class operations and corresponding locale.



Dear Bertram,

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.

Andreas

On 28/06/18 13:29, Bertram Felgenhauer via Cl-isabelle-users wrote:
I 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

   http://isabelle.in.tum.de/repos/isabelle/file/f5ca4c2157a5/src/HOL/Library/RBT_Impl.thy#l2055

Is that really necessary?

Cheers,

Bertram






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.