[isabelle-dev] Order Relations
Tobias Nipkow
nipkow at in.tum.de
Mon Feb 18 15:31:17 CET 2013
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
>
More information about the isabelle-dev
mailing list