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