[isabelle-dev] Order Relations

[Tobias Nipkow]

Am 18/02/2013 15:10, schrieb 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.

I believe it was me who ported those definitions. I vaguley recall that I tried
various alternatives but this one seemed to work best for the theory at hand,
Zorn. I am completely open to a nicer definition but would not want to redo all
the proofs that depend on it myself.

Tobias

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