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