Email Gateway (Aug 19 2022 at 14:16): Email Gateway (Aug 19 2022 at 14:16):From: Christian Sternagel <c.sternagel@gmail.com>
Dear fellow Isabellers,
I am wondering whether there is already a way in the Isabelle/HOL
library (or the AFP, for that matter) to obtain a system of
representatives (I'm not sure whether this is the correct term, in
German it is called "Repräsentantensystem") for a given equivalence
relation, i.e., a set containing one representative of each equivalence
class?
thanks in advance and cheers
chris
Email Gateway (Aug 19 2022 at 14:16):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Chris,
Something like this: "(λX. SOME x. x ∈ X) Equiv_Relations.proj r
Field r"
The function Equiv_Relations.proj gives you the (non-empty) equivalence
class of an element.
Dmitriy
Email Gateway (Aug 19 2022 at 14:16):From: Christian Sternagel <c.sternagel@gmail.com>
Thanks Dimitriy,
That looks similar to the construction I'm currently using ;), i.e.,
"repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
I was hoping that some properties are already proved about it. E.g.,
that two non-equal elements of "repsys A R" are not in relation w.r.t.
"R", "repsys A R" is a subset of "A", ...
But it should be easy to do anyway. Would this be interesting for
anybody else?
cheers
chris
btw: I could not find the constant "proj" in Equiv_Relations.
Email Gateway (Aug 19 2022 at 14:16):From: Dmitriy Traytel <traytel@in.tum.de>
Am 11.04.2014 10:16, schrieb Christian Sternagel:
Thanks Dimitriy,
That looks similar to the construction I'm currently using ;), i.e.,
"repsys A R = {(SOME x. x ∈ X) | X. X ∈ A // R}"
I was hoping that some properties are already proved about it. E.g.,
that two non-equal elements of "repsys A R" are not in relation w.r.t.
"R", "repsys A R" is a subset of "A", ...But it should be easy to do anyway.
Indeed.
btw: I could not find the constant "proj" in Equiv_Relations.
Oops, accidentally my answer referred to a development version (e.g.
aff193f53a64), sorry for that. In Isabelle2013-2 this constant is in
src/HOL/BNF/Equiv_Relations_More.
Dmitriy
Email Gateway (Aug 19 2022 at 14:17):From: Lawrence Paulson <lp15@cam.ac.uk>
Are specific representatives actually needed? It might be better to use the equivalence classes themselves. That is the point of this construction.
--lcp
Email Gateway (Aug 19 2022 at 14:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Larry,
at least I'm under the impression that the representatives are needed ;).
Let me elaborate: I am formalizing a proof as part of IsaFoR (mainly
first-order term rewriting). In the remainder of IsaFoR (which is
already quite huge) term rewrite systems (TRS) are just represented as
sets of pairs of terms. This is a well-supported type and easy to use.
But in the new proof a crucial property is that at a certain point a TRS
does not contain variants (i.e., variable renamed versions of rules).
Since I want to reuse all the existing lemmas about TRSs but for the
current proof I need a TRS without variants, I defined the operation of
removing variants from TRSs (via first building the equivalence classes
w.r.t. variable renaming and then projecting, using SOME, to a system of
representatives).
Please let me know what you think about this setup or if you have any
suggestions for improvements.
cheers
chris
Email Gateway (Aug 19 2022 at 14:17):From: Lawrence Paulson <lp15@cam.ac.uk>
A general suggestion that might work in this type of situation is to prove your theorems in a context that assumes that you have an element of an equivalence class. In your case, perhaps you need the additional assumption that this element contains no variants. Then it may be enough to show that every equivalence class contains at least one such element.
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC