[isabelle-dev] lex_prod changes

[Bertram Felgenhauer]

Bertram Felgenhauer wrote:
> Apparently, R1 <*lex*> R2 was changed to artificially impose
> irreflexivity on R1 (checking  a ~= a'  in addition to  a R1 a').

Is there a chance to revert this?

Instead, one could define a relation version of `mk_less`, say[*]

  definition less_rel where
    "less_rel R = {(x,y) |x y. (x,y) ∈ R ∧ (y,x) ∉ R}"

and use

  less_rel R1 <*lex*> R2

instead of the new definition of <*lex*>. That looks like a tolerable
overhead to me.

Note that `less_rel` is defined slightly differently from the new
<*lex*> check, but we can prove equivalence for antisymmetric
relations:

  lemma less_rel_antisym:
    "antisym R ⟹ ((x,y) ∈ less_rel R ⟷ x ≠ y ∧ (x,y) ∈ R)"
    by (auto simp: less_rel_def antisym_def)

But a lot hinges on why the change was made in the first place.

Cheers,

Bertram

[*] This should probably be an inductive set. And there may be better
names, like `strict_part`.