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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
