[isabelle] bug in strict_linear_order_on

Dear Isabelle,

I think the definition of "strict_linear_order_on" in HOL/Order_Relation.thy may be wrong, or at least, sub-optimal.

Specifically, the definition does not state that the relation r must be contained within A*A. In contrast, the non-strict version, "linear_order_on", *does* make this restriction.

In which case, can I propose that the definition be updated to (something like): 

> definition "NEW_strict_linear_order_on A r â strict_linear_order_on A r â (r â A Ã A)"

On another, slightly-related, matter -- I was hoping to find a lemma capturing the "order-extension principle". Something a bit like:

"if p is a strict partial order on A, then there exists a strict linear order on A that is a superset of p". [I haven't formulated this very precisely, but can do.]

This doesn't immediately appear to be in the HOL library, but seems an obvious candidate for inclusion. Did I miss it somewhere under a different name?


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