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