[isabelle-dev] Order Relations

[Lawrence Paulson]

These definitions originate in Isabelle/ZF, where it is quite essential to have a condition such as "r <= A <*> A", because otherwise no reflexive r could exist. They aren't is obviously necessary in Isabelle/HOL, but nevertheless the idea that the domain type can be identified with the actual domain of a relation is inflexible in many applications, where it's essential to have a separate carrier set, a subset of the full type.

And of course, even if they aren't ideal, I'm afraid that we are stuck with them; at least, I suspect that changing them now would be more trouble than it is worth.

Larry

On 18 Feb 2013, at 05:45, Christian Sternagel <c.sternagel at gmail.com> wrote:

> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev