[isabelle-dev] Order Relations
Lawrence Paulson
lp15 at cam.ac.uk
Mon Feb 18 15:10:45 CET 2013
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
More information about the isabelle-dev
mailing list