[isabelle-dev] Order Relations

[Tobias Nipkow]

Am 19/02/2013 03:50, schrieb 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.

It sounds plausible to me, and I would be in favour of such a change assuming
that your application profits from it and the distribution does not suffer.

Tobias

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