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.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 >> > > _______________________________________________ > 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