[isabelle-dev] Order Relations

[Christian Sternagel]

On 02/18/2013 11:31 PM, Tobias Nipkow wrote:
> 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.
My main problem with the current definition is that it is not (just) 
reflexivity, but rather reflexivity plus an additional property (that 
ensures that a relation is only defined on a domain). Why not split 
these in two separate predicates and use the second one only where 
really necessary?

I'm not sure how much work it would be to use this new definition of 
reflexivity. But if people think that what I say makes sense (or is more 
natural as reflexivity), I would give it a try and report afterwards.

cheers

chris

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