Email Gateway (Aug 22 2022 at 10:28): Email Gateway (Aug 22 2022 at 10:28):From: John Wickerson <johnwickerson@cantab.net>
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?
Cheers,
John
Email Gateway (Aug 22 2022 at 10:28):From: Tobias Nipkow <nipkow@in.tum.de>
Hi John,
There is indeed some inconsistency here. The "_on" suffix means different things
in "refl_on" and "total_on", which is the source of your complaint. I'll have to
figure out if the difference is intentional (I suspect it was) and if it can be
abolished. For "strict_linear_order_on" it is probably not hard, because that
one is hardly used, but "total_on" is a diffent matter...
This may take a little while.
Tobias
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC