Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant
Isabelle/HOL theories),
already several times I stumbled upon the definition of Relation.refl_on
(and thus also Order_Relation.Refl) and was irritated.
What is the reason for demanding "r <= A <*> A"? And why are other
properties from Order_Relation, which indicate an explicit domain by
their name, defined by means of corresponding properties with implicit
domain?
E.g., in the following definitions
definition "preorder_on A r == refl_on A r ∧ trans r"
definition "partial_order_on A r == preorder_on A r ∧ antisym r"
definition "linear_order_on A r ==
partial_order_on A r ∧ total_on A r"
definition "strict_linear_order_on A r ==
trans r ∧ irrefl r ∧ total_on A r"
definition "well_order_on A r == linear_order_on A r ∧ wf(r - Id)"
I would expect properties like "trans_on", "antisym_on", "irrefl_on",
and "wf_on" with explicit domain (of course that would only make sense
after dropping "r <= A <*> A" from the definition of "refl_on", since
otherwise r will only ever relate elements of A in the above definitions).
Now I saw that Andrei writes
"Refl_on A r" requires in particular that "r <= A <*> A",
and therefore whenever "Refl_on A r", we have that necessarily
"A = Field r". This means that in a theory of orders the domain
A would be redundant -- we decided not to include it explicitly
for most of the tehory.
in his README to the new Cardinal theories. So this (strange?)
definition of reflexivity is here to stay and used by an ever growing
body of theories.
This occasionally causes me some headache when I start to think about
how my definitions from the AFP entry Well_Quasi_Orders would fit in as
standard definitions in Isabelle/HOL. ( do recall that the current
definition of Relation.refl_on would not have worked for my proofs.)
Any comments are appreciated.
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
