[isabelle-dev] lex_prod changes

[Jasmin Blanchette]

Dear Stepan,

> I am completely unfamiliar with the process by which changes are decided and implemented, and I am sorry if I caused a confusion.

Don't worry: You did nothing wrong. You made a bona fide suggestion to the mailing list. You should not let this discourage you.

As I wrote, I wanted to answer back. But there are plenty of people on the list who understand orders better than I do, including the original author of "lex_prod" and all the IsaFoR people (including Bertram), so I thought I'd wait before answering and let the experts talk first. Then I forgot about the matter.

> I already understand that it is desirable that lex_product  of general relations keeps transitivity. However, it still trikes me as highly unusual that lex_product of partial orders is not (in general) a partial order (the same for lexord).

I don't even know the answer to your question. What I know that I and other people have been using it successfully, with orders and with quasi-orders (which are also important). I also know that all order and term-rewriting definitions are extremely subtle. And when I see a "not equal", I immediately think: This will break with quasi-orders.

My impression (which could be wrong, but the experts have been curiously silent so far) is that lex_prod and company are designed to be used with strict orders and strict quasi-orders. You're trying to use it with nonstrict orders (or at least reflexive relations). You can't have one single definition that makes strict and nonstrict, quasi- and non-quasi-orders happy all at once. Since strict and nonstrict are just two ways of presenting the same information, w.l.o.g. we can focus on the strict case.

Cheers,

Jasmin