[isabelle-dev] Order Relations

[Christian Sternagel]

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