Re: [isabelle] system of representatives of an equivalence relation

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.



On 04/11/2014 01:41 PM, Lawrence Paulson wrote:
Are specific representatives actually needed? It might be better to use the equivalence classes themselves. That is the point of this construction.


On 11 Apr 2014, at 09:16, Christian Sternagel <c.sternagel at> wrote:

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?



btw: I could not find the constant "proj" in Equiv_Relations.

On 04/11/2014 10:07 AM, Dmitriy Traytel wrote:
Hi Chris,

Am 11.04.2014 09:49, schrieb Christian Sternagel:
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?

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.