[isabelle-dev] lex_prod changes

[Lawrence Paulson]

As somebody who’s wasted a week trying to do this, I can’t say that I like it myself.

Larry

> On 20 Aug 2020, at 21:27, Bertram Felgenhauer <bertram.felgenhauer at googlemail.com> wrote:
> 
> Hi,
> 
> I've gotten some emails from Jenkins lately and finally taken a moment
> to investigate.
> 
> Apparently, R1 <*lex*> R2 was changed to artificially impose
> irreflexivity on R1 (checking  a ~= a'  in addition to  a R1 a').
> 
> What are the benefits of doing this? There is a (heavy, to me)
> downside: It destroys the property that the lexicographic product is
> transitive if both input relations are. More fundamentally, while in
> the previous formulation, the lexicographic product was a meaningful
> and useful operation for quasi-orders, now that use case is closed
> off.
> 
> Was this change discussed in advance? I may have missed it... in any
> case I strongly dislike it.
> 
> Cheers,
> 
> Bertram
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev